Nuprl Lemma : oal_grp_wf
∀s:LOSet. ∀g:AbDGrp. (oal_grp(s;g) ∈ AbDGrp)
Proof
Definitions occuring in Statement :
oal_grp: oal_grp(s;g),
all: ∀x:A. B[x],
member: t ∈ T,
abdgrp: AbDGrp,
loset: LOSet
Definitions unfolded in proof :
member: t ∈ T,
all: ∀x:A. B[x],
oal_grp: oal_grp(s;g),
grp_eq: =b,
grp_inv: ~,
prop: ℙ,
uall: ∀[x:A]. B[x],
grp_id: e,
pi2: snd(t),
grp_op: *,
pi1: fst(t),
grp_car: |g|,
mon: Mon,
grp: Group{i},
abgrp: AbGrp,
abdgrp: AbDGrp,
squash: ↓T,
sq_stable: SqStable(P),
implies: P ⇒ Q,
uimplies: b supposing a,
so_apply: x[s],
so_lambda: λ2x.t[x],
dmon: DMon,
abdmonoid: AbDMon,
subtype_rel: A ⊆r B,
grp_sig: GrpSig,
ident: Ident(T;op;id),
infix_ap: x f y,
assoc: Assoc(T;op),
and: P ∧ Q,
monoid_p: IsMonoid(T;op;id),
inverse: Inverse(T;op;id;inv),
comm: Comm(T;op)
Lemmas referenced :
dset_properties,
oal_merge_comm,
oal_neg_right_inv,
oal_neg_left_inv,
oal_merge_assoc,
oal_nil_ident_r,
oal_nil_ident_l,
set_car_wf,
oalist_wf,
subtype_rel_sets,
mon_wf,
set_wf,
sq_stable__comm,
set_eq_wf,
oal_ble_wf,
oal_merge_wf2,
oal_nil_wf,
oal_neg_wf2,
bool_wf,
monoid_p_wf,
grp_car_wf,
grp_op_wf,
grp_id_wf,
inverse_wf,
grp_inv_wf,
comm_wf,
eqfun_p_wf,
grp_eq_wf,
abdgrp_wf,
loset_wf
Rules used in proof :
lemma_by_obid,
hypothesis,
sqequalHypSubstitution,
cut,
lambdaFormation,
computationStep,
sqequalTransitivity,
sqequalReflexivity,
sqequalRule,
sqequalSubstitution,
rename,
setElimination,
hypothesisEquality,
thin,
isectElimination,
dependent_set_memberEquality,
productEquality,
functionEquality,
imageElimination,
baseClosed,
imageMemberEquality,
introduction,
independent_functionElimination,
independent_isectElimination,
universeEquality,
because_Cache,
lambdaEquality,
cumulativity,
setEquality,
instantiate,
applyEquality,
dependent_functionElimination,
dependent_pairEquality,
independent_pairEquality,
productElimination,
axiomEquality,
isect_memberEquality,
isect_memberFormation,
independent_pairFormation,
equalitySymmetry,
equalityTransitivity
Latex:
\mforall{}s:LOSet. \mforall{}g:AbDGrp. (oal\_grp(s;g) \mmember{} AbDGrp)
Date html generated:
2016_05_16-AM-08_20_46
Last ObjectModification:
2016_01_16-PM-11_57_47
Theory : polynom_2
Home
Index