Nuprl Lemma : bag-summation-product

`∀[r:Rng]. ∀[A,B:Type]. ∀[f:A ⟶ |r|]. ∀[c:bag(B)]. ∀[g:B ⟶ |r|]. ∀[b:bag(A)].`
`  ((Σ(x∈b). f[x] * Σ(y∈c). g[y]) = Σ(p∈b × c). f[fst(p)] * g[snd(p)] ∈ |r|)`

Proof

Definitions occuring in Statement :  bag-summation: `Σ(x∈b). f[x]` bag-product: `bs × cs` bag: `bag(T)` uall: `∀[x:A]. B[x]` infix_ap: `x f y` so_apply: `x[s]` pi1: `fst(t)` pi2: `snd(t)` function: `x:A ⟶ B[x]` universe: `Type` equal: `s = t ∈ T` rng: `Rng` rng_times: `*` rng_zero: `0` rng_plus: `+r` rng_car: `|r|`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` comm: `Comm(T;op)` rng: `Rng` rng_sig: `RngSig` prop: `ℙ` and: `P ∧ Q` squash: `↓T` exists: `∃x:A. B[x]` so_lambda: `λ2x.t[x]` so_apply: `x[s]` subtype_rel: `A ⊆r B` uimplies: `b supposing a` cand: `A c∧ B` pi1: `fst(t)` pi2: `snd(t)` implies: `P `` Q` all: `∀x:A. B[x]` empty-bag: `{}` top: `Top` single-bag: `{x}` bag-append: `as + bs` append: `as @ bs` so_lambda: `so_lambda(x,y,z.t[x; y; z])` so_apply: `x[s1;s2;s3]` ring_p: `IsRing(T;plus;zero;neg;times;one)` group_p: `IsGroup(T;op;id;inv)` infix_ap: `x f y` true: `True` guard: `{T}` iff: `P `⇐⇒` Q` rev_implies: `P `` Q`
Lemmas referenced :  rng_plus_comm rng_properties rng_all_properties bool_wf unit_wf2 ring_p_wf rng_car_wf rng_plus_wf rng_zero_wf rng_minus_wf rng_times_wf rng_one_wf bag_to_squash_list list_induction equal_wf infix_ap_wf bag-summation_wf list-subtype-bag bag-product_wf list_wf bag_wf rng_wf bag-product-empty rng_times_zero bag-summation-empty list_ind_cons_lemma list_ind_nil_lemma single-bag_wf bag-subtype-list subtype_rel_list top_wf bag-map_wf bag-product-append bag-product-single pi1_wf pi2_wf bag-summation-single iff_weakening_equal squash_wf true_wf bag-summation-append bag-summation-map bag-summation-linear1 rng_times_over_plus group_p_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis setElimination rename productElimination dependent_set_memberEquality sqequalRule dependent_pairEquality productEquality functionEquality cumulativity unionEquality promote_hyp because_Cache imageElimination lambdaEquality applyEquality functionExtensionality independent_isectElimination independent_pairFormation independent_functionElimination lambdaFormation dependent_functionElimination hyp_replacement equalitySymmetry applyLambdaEquality isect_memberEquality axiomEquality universeEquality voidElimination voidEquality independent_pairEquality equalityTransitivity equalityUniverse levelHypothesis natural_numberEquality imageMemberEquality baseClosed dependent_pairFormation

Latex:
\mforall{}[r:Rng].  \mforall{}[A,B:Type].  \mforall{}[f:A  {}\mrightarrow{}  |r|].  \mforall{}[c:bag(B)].  \mforall{}[g:B  {}\mrightarrow{}  |r|].  \mforall{}[b:bag(A)].
((\mSigma{}(x\mmember{}b).  f[x]  *  \mSigma{}(y\mmember{}c).  g[y])  =  \mSigma{}(p\mmember{}b  \mtimes{}  c).  f[fst(p)]  *  g[snd(p)])

Date html generated: 2017_10_01-AM-08_51_24
Last ObjectModification: 2017_07_26-PM-04_33_17

Theory : bags

Home Index