Nuprl Lemma : bag-summation-minus

`∀[T:Type]. ∀[r:Rng]. ∀[b:bag(T)]. ∀[f:T ⟶ |r|].  (Σ(x∈b). -r f[x] = (-r Σ(x∈b). f[x]) ∈ |r|)`

Proof

Definitions occuring in Statement :  bag-summation: `Σ(x∈b). f[x]` bag: `bag(T)` uall: `∀[x:A]. B[x]` so_apply: `x[s]` apply: `f a` function: `x:A ⟶ B[x]` universe: `Type` equal: `s = t ∈ T` rng: `Rng` rng_minus: `-r` rng_zero: `0` rng_plus: `+r` rng_car: `|r|`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` rng: `Rng` comm: `Comm(T;op)` uimplies: `b supposing a` and: `P ∧ Q` cand: `A c∧ B` exists: `∃x:A. B[x]` rng_sig: `RngSig` prop: `ℙ` ring_p: `IsRing(T;plus;zero;neg;times;one)` all: `∀x:A. B[x]` squash: `↓T` true: `True` so_lambda: `λ2x.t[x]` so_apply: `x[s]` subtype_rel: `A ⊆r B` guard: `{T}` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` implies: `P `` Q`
Lemmas referenced :  rng_car_wf bag_wf rng_wf rng_plus_comm bag-summation-linear1 rng_plus_wf rng_times_wf rng_zero_wf rng_minus_wf rng_properties group_p_wf rng_all_properties rng_one_wf equal_wf squash_wf true_wf bag-summation_wf assoc_wf comm_wf rng_times_over_minus rng_times_one iff_weakening_equal
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut hypothesis functionEquality cumulativity hypothesisEquality extract_by_obid sqequalHypSubstitution isectElimination thin setElimination rename sqequalRule isect_memberEquality axiomEquality because_Cache universeEquality independent_isectElimination dependent_pairFormation productElimination functionExtensionality applyEquality independent_pairFormation dependent_functionElimination hyp_replacement equalitySymmetry lambdaEquality imageElimination equalityTransitivity natural_numberEquality imageMemberEquality baseClosed productEquality independent_functionElimination

Latex:
\mforall{}[T:Type].  \mforall{}[r:Rng].  \mforall{}[b:bag(T)].  \mforall{}[f:T  {}\mrightarrow{}  |r|].    (\mSigma{}(x\mmember{}b).  -r  f[x]  =  (-r  \mSigma{}(x\mmember{}b).  f[x]))

Date html generated: 2017_10_01-AM-08_51_01
Last ObjectModification: 2017_07_26-PM-04_33_04

Theory : bags

Home Index