Nuprl Lemma : iabgrp_properties
∀[g:IAbGrp{i}]. Comm(|g|;*)
Proof
Definitions occuring in Statement :
iabgrp: IAbGrp{i}
,
grp_op: *
,
grp_car: |g|
,
comm: Comm(T;op)
,
uall: ∀[x:A]. B[x]
Definitions unfolded in proof :
uall: ∀[x:A]. B[x]
,
member: t ∈ T
,
iabgrp: IAbGrp{i}
,
igrp: IGroup
,
imon: IMonoid
,
sq_stable: SqStable(P)
,
implies: P
⇒ Q
,
squash: ↓T
,
comm: Comm(T;op)
Lemmas referenced :
iabgrp_wf,
grp_op_wf,
grp_car_wf,
sq_stable__comm
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation,
introduction,
cut,
sqequalHypSubstitution,
setElimination,
thin,
rename,
lemma_by_obid,
isectElimination,
hypothesisEquality,
hypothesis,
independent_functionElimination,
sqequalRule,
imageMemberEquality,
baseClosed,
imageElimination,
isect_memberEquality,
axiomEquality
Latex:
\mforall{}[g:IAbGrp\{i\}]. Comm(|g|;*)
Date html generated:
2016_05_15-PM-00_09_15
Last ObjectModification:
2016_01_15-PM-11_06_15
Theory : groups_1
Home
Index