Nuprl Lemma : bag-summation-append

`∀[R:Type]. ∀[add:R ⟶ R ⟶ R]. ∀[zero:R].`
`  ∀[T:Type]. ∀[f:T ⟶ R]. ∀[b,c:bag(T)].  (Σ(x∈b + c). f[x] = (Σ(x∈b). f[x] add Σ(x∈c). f[x]) ∈ R) `
`  supposing IsMonoid(R;add;zero) ∧ Comm(R;add)`

Proof

Definitions occuring in Statement :  bag-summation: `Σ(x∈b). f[x]` bag-append: `as + bs` bag: `bag(T)` comm: `Comm(T;op)` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` infix_ap: `x f y` so_apply: `x[s]` and: `P ∧ Q` function: `x:A ⟶ B[x]` universe: `Type` equal: `s = t ∈ T` monoid_p: `IsMonoid(T;op;id)`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` and: `P ∧ Q` bag: `bag(T)` quotient: `x,y:A//B[x; y]` all: `∀x:A. B[x]` implies: `P `` Q` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]` prop: `ℙ` so_lambda: `λ2x.t[x]` so_apply: `x[s]` cand: `A c∧ B` subtype_rel: `A ⊆r B` monoid_p: `IsMonoid(T;op;id)` nat: `ℕ` false: `False` ge: `i ≥ j ` satisfiable_int_formula: `satisfiable_int_formula(fmla)` exists: `∃x:A. B[x]` not: `¬A` top: `Top` guard: `{T}` int_seg: `{i..j-}` lelt: `i ≤ j < k` decidable: `Dec(P)` or: `P ∨ Q` le: `A ≤ B` less_than': `less_than'(a;b)` less_than: `a < b` squash: `↓T` empty-bag: `{}` cons: `[a / b]` assert: `↑b` ifthenelse: `if b then t else f fi ` bfalse: `ff` iff: `P `⇐⇒` Q` uiff: `uiff(P;Q)` rev_implies: `P `` Q` int_iseg: `{i...j}` single-bag: `{x}` bag-append: `as + bs` true: `True` ident: `Ident(T;op;id)` infix_ap: `x f y` assoc: `Assoc(T;op)` bag-summation: `Σ(x∈b). f[x]` bag-accum: `bag-accum(v,x.f[v; x];init;bs)` comm: `Comm(T;op)`
Lemmas referenced :  list_wf quotient-member-eq permutation_wf permutation-equiv equal_wf bag-summation_wf bag-append_wf infix_ap_wf list-subtype-bag equal-wf-base bag_wf monoid_p_wf comm_wf nat_properties satisfiable-full-omega-tt intformand_wf intformle_wf itermConstant_wf itermVar_wf intformless_wf int_formula_prop_and_lemma int_formula_prop_le_lemma int_term_value_constant_lemma int_term_value_var_lemma int_formula_prop_less_lemma int_formula_prop_wf ge_wf less_than_wf le_wf length_wf int_seg_wf int_seg_properties decidable__le subtract_wf intformnot_wf itermSubtract_wf int_formula_prop_not_lemma int_term_value_subtract_lemma decidable__equal_int int_seg_subtype false_wf intformeq_wf int_formula_prop_eq_lemma non_neg_length decidable__lt lelt_wf decidable__assert null_wf list-cases bag-summation-empty empty_bag_append_lemma product_subtype_list null_cons_lemma last-lemma-sq pos_length iff_transitivity not_wf equal-wf-T-base assert_wf bnot_wf assert_of_null iff_weakening_uiff assert_of_bnot firstn_wf length_firstn itermAdd_wf int_term_value_add_lemma nat_wf length_wf_nat single-bag_wf last_wf squash_wf true_wf bag-append-assoc iff_weakening_equal list_accum_append bag-subtype-list list_accum_cons_lemma list_accum_nil_lemma subtype_rel_list top_wf list_accum_wf bag-accum_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalHypSubstitution productElimination thin pointwiseFunctionalityForEquality because_Cache sqequalRule pertypeElimination equalityTransitivity hypothesis equalitySymmetry extract_by_obid isectElimination cumulativity hypothesisEquality lambdaFormation rename lambdaEquality independent_isectElimination dependent_functionElimination independent_functionElimination hyp_replacement applyLambdaEquality functionExtensionality applyEquality independent_pairFormation productEquality isect_memberEquality axiomEquality functionEquality universeEquality setElimination intWeakElimination natural_numberEquality dependent_pairFormation int_eqEquality intEquality voidElimination voidEquality computeAll unionElimination hypothesis_subsumption dependent_set_memberEquality imageElimination promote_hyp baseClosed impliesFunctionality addEquality imageMemberEquality

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