Metamath Proof Explorer

Theorem grpomndo

Description: A group is a monoid. (Contributed by FL, 2-Nov-2009) (Revised by Mario Carneiro, 22-Dec-2013) (New usage is discouraged.)

Ref Expression
Assertion grpomndo 
|- ( G e. GrpOp -> G e. MndOp )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ran G = ran G
2 1 isgrpo 
 |-  ( G e. GrpOp -> ( G e. GrpOp <-> ( G : ( ran G X. ran G ) --> ran G /\ A. x e. ran G A. y e. ran G A. z e. ran G ( ( x G y ) G z ) = ( x G ( y G z ) ) /\ E. w e. ran G A. x e. ran G ( ( w G x ) = x /\ E. y e. ran G ( y G x ) = w ) ) ) )
3 2 biimpd 
 |-  ( G e. GrpOp -> ( G e. GrpOp -> ( G : ( ran G X. ran G ) --> ran G /\ A. x e. ran G A. y e. ran G A. z e. ran G ( ( x G y ) G z ) = ( x G ( y G z ) ) /\ E. w e. ran G A. x e. ran G ( ( w G x ) = x /\ E. y e. ran G ( y G x ) = w ) ) ) )
4 1 grpoidinv 
 |-  ( G e. GrpOp -> E. x e. ran G A. y e. ran G ( ( ( x G y ) = y /\ ( y G x ) = y ) /\ E. w e. ran G ( ( w G y ) = x /\ ( y G w ) = x ) ) )
5 simpl 
 |-  ( ( ( ( x G y ) = y /\ ( y G x ) = y ) /\ E. w e. ran G ( ( w G y ) = x /\ ( y G w ) = x ) ) -> ( ( x G y ) = y /\ ( y G x ) = y ) )
6 5 ralimi 
 |-  ( A. y e. ran G ( ( ( x G y ) = y /\ ( y G x ) = y ) /\ E. w e. ran G ( ( w G y ) = x /\ ( y G w ) = x ) ) -> A. y e. ran G ( ( x G y ) = y /\ ( y G x ) = y ) )
7 6 reximi 
 |-  ( E. x e. ran G A. y e. ran G ( ( ( x G y ) = y /\ ( y G x ) = y ) /\ E. w e. ran G ( ( w G y ) = x /\ ( y G w ) = x ) ) -> E. x e. ran G A. y e. ran G ( ( x G y ) = y /\ ( y G x ) = y ) )
8 1 ismndo2 
 |-  ( G e. GrpOp -> ( G e. MndOp <-> ( G : ( ran G X. ran G ) --> ran G /\ A. x e. ran G A. y e. ran G A. z e. ran G ( ( x G y ) G z ) = ( x G ( y G z ) ) /\ E. x e. ran G A. y e. ran G ( ( x G y ) = y /\ ( y G x ) = y ) ) ) )
9 8 biimprcd 
 |-  ( ( G : ( ran G X. ran G ) --> ran G /\ A. x e. ran G A. y e. ran G A. z e. ran G ( ( x G y ) G z ) = ( x G ( y G z ) ) /\ E. x e. ran G A. y e. ran G ( ( x G y ) = y /\ ( y G x ) = y ) ) -> ( G e. GrpOp -> G e. MndOp ) )
10 9 3exp 
 |-  ( G : ( ran G X. ran G ) --> ran G -> ( A. x e. ran G A. y e. ran G A. z e. ran G ( ( x G y ) G z ) = ( x G ( y G z ) ) -> ( E. x e. ran G A. y e. ran G ( ( x G y ) = y /\ ( y G x ) = y ) -> ( G e. GrpOp -> G e. MndOp ) ) ) )
11 10 impcom 
 |-  ( ( A. x e. ran G A. y e. ran G A. z e. ran G ( ( x G y ) G z ) = ( x G ( y G z ) ) /\ G : ( ran G X. ran G ) --> ran G ) -> ( E. x e. ran G A. y e. ran G ( ( x G y ) = y /\ ( y G x ) = y ) -> ( G e. GrpOp -> G e. MndOp ) ) )
12 11 com3l 
 |-  ( E. x e. ran G A. y e. ran G ( ( x G y ) = y /\ ( y G x ) = y ) -> ( G e. GrpOp -> ( ( A. x e. ran G A. y e. ran G A. z e. ran G ( ( x G y ) G z ) = ( x G ( y G z ) ) /\ G : ( ran G X. ran G ) --> ran G ) -> G e. MndOp ) ) )
13 7 12 syl 
 |-  ( E. x e. ran G A. y e. ran G ( ( ( x G y ) = y /\ ( y G x ) = y ) /\ E. w e. ran G ( ( w G y ) = x /\ ( y G w ) = x ) ) -> ( G e. GrpOp -> ( ( A. x e. ran G A. y e. ran G A. z e. ran G ( ( x G y ) G z ) = ( x G ( y G z ) ) /\ G : ( ran G X. ran G ) --> ran G ) -> G e. MndOp ) ) )
14 4 13 mpcom 
 |-  ( G e. GrpOp -> ( ( A. x e. ran G A. y e. ran G A. z e. ran G ( ( x G y ) G z ) = ( x G ( y G z ) ) /\ G : ( ran G X. ran G ) --> ran G ) -> G e. MndOp ) )
15 14 expdcom 
 |-  ( A. x e. ran G A. y e. ran G A. z e. ran G ( ( x G y ) G z ) = ( x G ( y G z ) ) -> ( G : ( ran G X. ran G ) --> ran G -> ( G e. GrpOp -> G e. MndOp ) ) )
16 15 a1i 
 |-  ( E. w e. ran G A. x e. ran G ( ( w G x ) = x /\ E. y e. ran G ( y G x ) = w ) -> ( A. x e. ran G A. y e. ran G A. z e. ran G ( ( x G y ) G z ) = ( x G ( y G z ) ) -> ( G : ( ran G X. ran G ) --> ran G -> ( G e. GrpOp -> G e. MndOp ) ) ) )
17 16 com13 
 |-  ( G : ( ran G X. ran G ) --> ran G -> ( A. x e. ran G A. y e. ran G A. z e. ran G ( ( x G y ) G z ) = ( x G ( y G z ) ) -> ( E. w e. ran G A. x e. ran G ( ( w G x ) = x /\ E. y e. ran G ( y G x ) = w ) -> ( G e. GrpOp -> G e. MndOp ) ) ) )
18 17 3imp 
 |-  ( ( G : ( ran G X. ran G ) --> ran G /\ A. x e. ran G A. y e. ran G A. z e. ran G ( ( x G y ) G z ) = ( x G ( y G z ) ) /\ E. w e. ran G A. x e. ran G ( ( w G x ) = x /\ E. y e. ran G ( y G x ) = w ) ) -> ( G e. GrpOp -> G e. MndOp ) )
19 3 18 syli 
 |-  ( G e. GrpOp -> ( G e. GrpOp -> G e. MndOp ) )
20 19 pm2.43i 
 |-  ( G e. GrpOp -> G e. MndOp )