Theorem grpolidinv

Description: A group has a left identity element, and every member has a left inverse. (Contributed by NM, 2-Nov-2006) (New usage is discouraged.)

	Ref	Expression
Hypothesis	grpfo.1	|- X = ran G
Assertion	grpolidinv	|- ( G e. GrpOp -> E. u e. X A. x e. X ( ( u G x ) = x /\ E. y e. X ( y G x ) = u ) )

Proof

Step	Hyp	Ref	Expression
1		grpfo.1	|- X = ran G
2	1	isgrpo	|- ( G e. GrpOp -> ( G e. GrpOp <-> ( G : ( X X. X ) --> X /\ A. x e. X A. y e. X A. z e. X ( ( x G y ) G z ) = ( x G ( y G z ) ) /\ E. u e. X A. x e. X ( ( u G x ) = x /\ E. y e. X ( y G x ) = u ) ) ) )
3	2	ibi	|- ( G e. GrpOp -> ( G : ( X X. X ) --> X /\ A. x e. X A. y e. X A. z e. X ( ( x G y ) G z ) = ( x G ( y G z ) ) /\ E. u e. X A. x e. X ( ( u G x ) = x /\ E. y e. X ( y G x ) = u ) ) )
4	3	simp3d	|- ( G e. GrpOp -> E. u e. X A. x e. X ( ( u G x ) = x /\ E. y e. X ( y G x ) = u ) )