Nuprl Lemma : grp_op_cancel_l

[g:IGroup]. ∀[a,b,c:|g|].  c ∈ |g| supposing (a b) (a c) ∈ |g|


Proof




Definitions occuring in Statement :  igrp: IGroup grp_op: * grp_car: |g| uimplies: supposing a uall: [x:A]. B[x] infix_ap: y equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a prop: igrp: IGroup imon: IMonoid infix_ap: y squash: T true: True subtype_rel: A ⊆B and: P ∧ Q guard: {T} iff: ⇐⇒ Q implies:  Q
Lemmas referenced :  equal_wf grp_car_wf grp_op_wf igrp_wf grp_op_l grp_inv_wf squash_wf true_wf mon_assoc grp_inverse mon_ident iff_weakening_equal
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut hypothesis extract_by_obid sqequalHypSubstitution isectElimination thin setElimination rename hypothesisEquality applyEquality because_Cache sqequalRule isect_memberEquality axiomEquality equalityTransitivity equalitySymmetry independent_isectElimination lambdaEquality imageElimination universeEquality natural_numberEquality imageMemberEquality baseClosed productElimination independent_functionElimination

Latex:
\mforall{}[g:IGroup].  \mforall{}[a,b,c:|g|].    b  =  c  supposing  (a  *  b)  =  (a  *  c)



Date html generated: 2017_10_01-AM-08_13_30
Last ObjectModification: 2017_02_28-PM-01_57_47

Theory : groups_1


Home Index