Nuprl Lemma : bag-summation-linear1-right

[T,R:Type]. ∀[add,mul:R ⟶ R ⟶ R]. ∀[zero:R]. ∀[b:bag(T)]. ∀[f:T ⟶ R].
∀a:R. (x∈b). f[x] mul (x∈b). f[x] mul a) ∈ R)

Proof

Definitions occuring in Statement :  bag-summation: Σ(x∈b). f[x] bag: bag(T) comm: Comm(T;op) uimplies: supposing a uall: [x:A]. B[x] infix_ap: y so_apply: x[s] all: x:A. B[x] exists: x:A. B[x] and: P ∧ Q function: x:A ⟶ B[x] universe: Type equal: t ∈ T group_p: IsGroup(T;op;id;inv) bilinear: BiLinear(T;pl;tm)
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a all: x:A. B[x] and: P ∧ Q so_lambda: λ2x.t[x] so_apply: x[s] cand: c∧ B prop: squash: T exists: x:A. B[x] infix_ap: y true: True group_p: IsGroup(T;op;id;inv) monoid_p: IsMonoid(T;op;id) guard: {T} ident: Ident(T;op;id) subtype_rel: A ⊆B iff: ⇐⇒ Q rev_implies:  Q implies:  Q assoc: Assoc(T;op)
Lemmas referenced :  bag-summation-linear-right equal_wf squash_wf true_wf bag-summation_wf exists_wf group_p_wf comm_wf bilinear_wf bag_wf bag-summation-zero iff_weakening_equal
Rules used in proof :  cut introduction extract_by_obid sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation hypothesis sqequalHypSubstitution isectElimination thin hypothesisEquality lambdaFormation productElimination sqequalRule lambdaEquality cumulativity independent_isectElimination independent_pairFormation dependent_functionElimination hyp_replacement equalitySymmetry applyEquality imageElimination equalityTransitivity universeEquality because_Cache imageMemberEquality baseClosed natural_numberEquality axiomEquality productEquality functionEquality functionExtensionality independent_functionElimination

Latex:
\mforall{}[T,R:Type].  \mforall{}[add,mul:R  {}\mrightarrow{}  R  {}\mrightarrow{}  R].  \mforall{}[zero:R].  \mforall{}[b:bag(T)].  \mforall{}[f:T  {}\mrightarrow{}  R].
\mforall{}a:R.  (\mSigma{}(x\mmember{}b).  f[x]  mul  a  =  (\mSigma{}(x\mmember{}b).  f[x]  mul  a))