Nuprl Lemma : quot_grp_inv_wf

g:IGroup. ∀h:NormSubGrp{i}(g).  (~ ∈ |g//h| ⟶ |g//h|)


Proof




Definitions occuring in Statement :  quot_grp_car: |g//h| norm_subgrp: NormSubGrp{i}(g) igrp: IGroup grp_inv: ~ all: x:A. B[x] member: t ∈ T function: x:A ⟶ B[x]
Definitions unfolded in proof :  all: x:A. B[x] member: t ∈ T norm_subgrp: NormSubGrp{i}(g) uall: [x:A]. B[x] igrp: IGroup imon: IMonoid and: P ∧ Q cand: c∧ B prop: quot_grp_car: |g//h| quotient: x,y:A//B[x; y] implies:  Q so_lambda: λ2y.t[x; y] so_apply: x[s1;s2] uimplies: supposing a guard: {T} subgrp_p: SubGrp of g eqv_mod_subset: a ≡ (mod in g) norm_subset_p: norm_subset_p(g;s) infix_ap: y true: True squash: T subtype_rel: A ⊆B iff: ⇐⇒ Q rev_implies:  Q
Lemmas referenced :  norm_subgrp_wf igrp_wf grp_inv_wf quot_grp_car_wf subgrp_p_wf grp_car_wf norm_subset_p_wf eqv_mod_subset_wf equal_wf equal-wf-base quotient-member-eq eqv_mod_subset_is_eqv grp_op_wf infix_ap_wf squash_wf true_wf grp_inv_thru_op grp_inv_inv mon_assoc grp_inv_assoc iff_weakening_equal
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut sqequalHypSubstitution setElimination thin rename hypothesis introduction extract_by_obid isectElimination hypothesisEquality functionExtensionality productElimination dependent_functionElimination independent_pairFormation dependent_set_memberEquality productEquality applyEquality because_Cache pointwiseFunctionalityForEquality sqequalRule pertypeElimination equalityTransitivity equalitySymmetry independent_functionElimination lambdaEquality independent_isectElimination hyp_replacement natural_numberEquality imageElimination universeEquality imageMemberEquality baseClosed

Latex:
\mforall{}g:IGroup.  \mforall{}h:NormSubGrp\{i\}(g).    (\msim{}  \mmember{}  |g//h|  {}\mrightarrow{}  |g//h|)



Date html generated: 2017_10_01-AM-08_13_55
Last ObjectModification: 2017_02_28-PM-01_58_29

Theory : groups_1


Home Index