### Nuprl Lemma : bag-summation-hom

`∀[r,s:Rng]. ∀[f:|r| ⟶ |s|].`
`  ∀[A:Type]. ∀[g:A ⟶ |r|]. ∀[b:bag(A)].  (Σ(x∈b). f[g[x]] = f[Σ(x∈b). g[x]] ∈ |s|) supposing rng_hom_p(r;s;f)`

Proof

Definitions occuring in Statement :  bag-summation: `Σ(x∈b). f[x]` bag: `bag(T)` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` so_apply: `x[s]` function: `x:A ⟶ B[x]` universe: `Type` equal: `s = t ∈ T` rng_hom_p: `rng_hom_p(r;s;f)` 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` monoid_p: `IsMonoid(T;op;id)` squash: `↓T` exists: `∃x:A. B[x]` so_lambda: `λ2x.t[x]` rng: `Rng` so_apply: `x[s]` subtype_rel: `A ⊆r B` cand: `A c∧ B` implies: `P `` Q` empty-bag: `{}` top: `Top` all: `∀x:A. B[x]` cons-bag: `x.b` prop: `ℙ` true: `True` guard: `{T}` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` rng_hom_p: `rng_hom_p(r;s;f)` fun_thru_2op: `FunThru2op(A;B;opa;opb;f)` infix_ap: `x f y`
Lemmas referenced :  rng_all_properties bag_to_squash_list list_induction equal_wf rng_car_wf bag-summation_wf rng_plus_wf rng_zero_wf list-subtype-bag rng_plus_comm2 list_wf bag-summation-empty bag_wf rng_hom_p_wf rng_wf squash_wf true_wf bag-summation-cons iff_weakening_equal rng_hom_zero infix_ap_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut independent_pairFormation extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality productElimination hypothesis because_Cache promote_hyp imageElimination rename sqequalRule lambdaEquality setElimination cumulativity applyEquality functionExtensionality independent_isectElimination independent_functionElimination isect_memberEquality voidElimination voidEquality lambdaFormation dependent_functionElimination hyp_replacement equalitySymmetry applyLambdaEquality axiomEquality functionEquality universeEquality equalityTransitivity equalityUniverse levelHypothesis natural_numberEquality imageMemberEquality baseClosed

Latex:
\mforall{}[r,s:Rng].  \mforall{}[f:|r|  {}\mrightarrow{}  |s|].
\mforall{}[A:Type].  \mforall{}[g:A  {}\mrightarrow{}  |r|].  \mforall{}[b:bag(A)].    (\mSigma{}(x\mmember{}b).  f[g[x]]  =  f[\mSigma{}(x\mmember{}b).  g[x]])
supposing  rng\_hom\_p(r;s;f)

Date html generated: 2017_10_01-AM-08_51_28
Last ObjectModification: 2017_07_26-PM-04_33_19

Theory : bags

Home Index