### Nuprl Lemma : dist_hom_over_mset_for

`∀s:DSet. ∀m,n:IAbMonoid. ∀f:MonHom(m,n). ∀a:MSet{s}. ∀g:|s| ⟶ |m|.`
`  ((f (msFor{m} x ∈ a. g[x])) = (msFor{n} x ∈ a. (f g[x])) ∈ |n|)`

Proof

Definitions occuring in Statement :  mset_for: mset_for mset: `MSet{s}` so_apply: `x[s]` all: `∀x:A. B[x]` apply: `f a` function: `x:A ⟶ B[x]` equal: `s = t ∈ T` monoid_hom: `MonHom(M1,M2)` iabmonoid: `IAbMonoid` grp_car: `|g|` dset: `DSet` set_car: `|p|`
Definitions unfolded in proof :  all: `∀x:A. B[x]` member: `t ∈ T` uall: `∀[x:A]. B[x]` iabmonoid: `IAbMonoid` imon: `IMonoid` so_lambda: `λ2x.t[x]` top: `Top` so_apply: `x[s]` dset: `DSet` monoid_hom: `MonHom(M1,M2)` implies: `P `` Q` iff: `P `⇐⇒` Q` and: `P ∧ Q` rev_implies: `P `` Q` prop: `ℙ`
Lemmas referenced :  monoid_hom_wf iabmonoid_wf dset_wf mset_for_elim_lemma all_mset_elim all_wf set_car_wf grp_car_wf equal_wf mset_for_wf mset_wf sq_stable__all sq_stable__equal list_wf mon_for_wf dist_hom_over_mon_for
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut lemma_by_obid sqequalHypSubstitution isectElimination thin setElimination rename hypothesisEquality hypothesis addLevel sqequalRule dependent_functionElimination isect_memberEquality voidElimination voidEquality lambdaEquality functionEquality applyEquality because_Cache independent_functionElimination productElimination levelHypothesis

Latex:
\mforall{}s:DSet.  \mforall{}m,n:IAbMonoid.  \mforall{}f:MonHom(m,n).  \mforall{}a:MSet\{s\}.  \mforall{}g:|s|  {}\mrightarrow{}  |m|.
((f  (msFor\{m\}  x  \mmember{}  a.  g[x]))  =  (msFor\{n\}  x  \mmember{}  a.  (f  g[x])))

Date html generated: 2016_05_16-AM-07_47_55
Last ObjectModification: 2015_12_28-PM-06_03_21

Theory : mset

Home Index