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