Nuprl Lemma : zhgrp_op_mon_hom_1
∀[g:IMonoid]. ∀[a:|g|]. IsMonHom{<ℤ+>↓hgrp,g}(λn.(nat(n) ⋅ a))
Proof
Definitions occuring in Statement :
int_hgrp_to_nat: nat(n),
int_add_grp: <ℤ+>,
mon_nat_op: n ⋅ e,
hgrp_of_ocgrp: g↓hgrp,
monoid_hom_p: IsMonHom{M1,M2}(f),
imon: IMonoid,
grp_car: |g|,
uall: ∀[x:A]. B[x],
lambda: λx.A[x]
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
monoid_hom_p: IsMonHom{M1,M2}(f),
and: P ∧ Q,
fun_thru_2op: FunThru2op(A;B;opa;opb;f),
imon: IMonoid,
subtype_rel: A ⊆r B,
nat_add_mon: <ℕ,+>,
grp_car: |g|,
pi1: fst(t),
uimplies: b supposing a,
compose: f o g
Lemmas referenced :
grp_car_wf,
hgrp_of_ocgrp_wf,
int_add_grp_wf2,
imon_wf,
nat_op_mon_hom_1,
zhgrp_to_nat_is_hom,
mon_hom_p_comp,
nat_add_mon_wf,
int_hgrp_to_nat_wf,
nat_wf,
mon_nat_op_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation,
introduction,
cut,
sqequalRule,
sqequalHypSubstitution,
productElimination,
thin,
independent_pairEquality,
isect_memberEquality,
isectElimination,
hypothesisEquality,
axiomEquality,
hypothesis,
lemma_by_obid,
setElimination,
rename,
because_Cache,
lambdaEquality,
applyEquality,
independent_isectElimination
Latex:
\mforall{}[g:IMonoid]. \mforall{}[a:|g|]. IsMonHom\{<\mBbbZ{}+>\mdownarrow{}hgrp,g\}(\mlambda{}n.(nat(n) \mcdot{} a))
Date html generated:
2016_05_15-PM-00_19_45
Last ObjectModification:
2015_12_26-PM-11_37_33
Theory : groups_1
Home
Index