Nuprl Lemma : massoc_imp_unit_diff

g:IAbMonoid. (Cancel(|g|;|g|;*)  (∀a,b:|g|.  ((a b)  (∃u:|g|. ((g-unit(u)) c∧ (a (u b) ∈ |g|))))))


Proof




Definitions occuring in Statement :  massoc: b munit: g-unit(u) cand: c∧ B infix_ap: y all: x:A. B[x] exists: x:A. B[x] implies:  Q equal: t ∈ T iabmonoid: IAbMonoid grp_op: * grp_car: |g| cancel: Cancel(T;S;op)
Definitions unfolded in proof :  all: x:A. B[x] implies:  Q member: t ∈ T prop: iabmonoid: IAbMonoid imon: IMonoid uall: [x:A]. B[x] cancel: Cancel(T;S;op) massoc: b symmetrize: Symmetrize(x,y.R[x; y];a;b) and: P ∧ Q mdivides: a exists: x:A. B[x] infix_ap: y squash: T true: True subtype_rel: A ⊆B uimplies: supposing a guard: {T} iff: ⇐⇒ Q rev_implies:  Q cand: c∧ B munit: g-unit(u)
Lemmas referenced :  massoc_wf grp_car_wf cancel_wf grp_op_wf iabmonoid_wf equal_wf squash_wf true_wf mon_assoc iff_weakening_equal mon_ident grp_id_wf munit_wf abmonoid_comm
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut introduction extract_by_obid sqequalHypSubstitution dependent_functionElimination thin setElimination rename hypothesisEquality hypothesis isectElimination because_Cache productElimination equalitySymmetry hyp_replacement applyLambdaEquality applyEquality lambdaEquality imageElimination equalityTransitivity universeEquality equalityUniverse levelHypothesis natural_numberEquality sqequalRule imageMemberEquality baseClosed independent_isectElimination independent_functionElimination dependent_pairFormation independent_pairFormation productEquality

Latex:
\mforall{}g:IAbMonoid
    (Cancel(|g|;|g|;*)  {}\mRightarrow{}  (\mforall{}a,b:|g|.    ((a  \msim{}  b)  {}\mRightarrow{}  (\mexists{}u:|g|.  ((g-unit(u))  c\mwedge{}  (a  =  (u  *  b)))))))



Date html generated: 2017_10_01-AM-09_58_03
Last ObjectModification: 2017_03_03-PM-00_59_33

Theory : factor_1


Home Index