### Nuprl Lemma : bag-summation-equal2

`∀[T:Type]. ∀[r:Rng]. ∀[f,g:T ⟶ |r|]. ∀[b,c:bag(T)].`
`  Σ(x∈b). f[x] = Σ(x∈c). g[x] ∈ |r| supposing (∀x:T. (x ↓∈ b `` (f[x] = g[x] ∈ |r|))) ∧ (b = c ∈ bag(T))`

Proof

Definitions occuring in Statement :  bag-member: `x ↓∈ bs` bag-summation: `Σ(x∈b). f[x]` bag: `bag(T)` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` so_apply: `x[s]` all: `∀x:A. B[x]` implies: `P `` Q` and: `P ∧ Q` function: `x:A ⟶ B[x]` universe: `Type` equal: `s = t ∈ T` rng: `Rng` rng_zero: `0` rng_plus: `+r` rng_car: `|r|`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` and: `P ∧ Q` comm: `Comm(T;op)` cand: `A c∧ B` rng: `Rng` rng_sig: `RngSig` so_lambda: `λ2x.t[x]` so_apply: `x[s]` prop: `ℙ` implies: `P `` Q` all: `∀x:A. B[x]` ring_p: `IsRing(T;plus;zero;neg;times;one)` group_p: `IsGroup(T;op;id;inv)`
Lemmas referenced :  rng_plus_comm rng_all_properties rng_properties bag-summation-equal rng_car_wf rng_plus_wf rng_zero_wf equal_wf bag-summation_wf all_wf bag-member_wf bag_wf rng_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalHypSubstitution productElimination thin extract_by_obid isectElimination hypothesisEquality hypothesis independent_pairFormation setElimination rename equalitySymmetry because_Cache sqequalRule lambdaEquality applyEquality functionExtensionality cumulativity independent_isectElimination hyp_replacement applyLambdaEquality equalityTransitivity productEquality functionEquality isect_memberEquality axiomEquality

Latex:
\mforall{}[T:Type].  \mforall{}[r:Rng].  \mforall{}[f,g:T  {}\mrightarrow{}  |r|].  \mforall{}[b,c:bag(T)].
\mSigma{}(x\mmember{}b).  f[x]  =  \mSigma{}(x\mmember{}c).  g[x]  supposing  (\mforall{}x:T.  (x  \mdownarrow{}\mmember{}  b  {}\mRightarrow{}  (f[x]  =  g[x])))  \mwedge{}  (b  =  c)

Date html generated: 2017_10_01-AM-09_01_37
Last ObjectModification: 2017_07_26-PM-04_42_59

Theory : bags

Home Index