Metamath Proof Explorer

Theorem grpoidinv

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

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

Proof

Step Hyp Ref Expression
1 grpfo.1 
 |-  X = ran G
2 simpl 
 |-  ( ( ( u G z ) = z /\ E. w e. X ( w G z ) = u ) -> ( u G z ) = z )
3 2 ralimi 
 |-  ( A. z e. X ( ( u G z ) = z /\ E. w e. X ( w G z ) = u ) -> A. z e. X ( u G z ) = z )
4 oveq2 
 |-  ( z = x -> ( u G z ) = ( u G x ) )
5 id 
 |-  ( z = x -> z = x )
6 4 5 eqeq12d 
 |-  ( z = x -> ( ( u G z ) = z <-> ( u G x ) = x ) )
7 6 rspccva 
 |-  ( ( A. z e. X ( u G z ) = z /\ x e. X ) -> ( u G x ) = x )
8 3 7 sylan 
 |-  ( ( A. z e. X ( ( u G z ) = z /\ E. w e. X ( w G z ) = u ) /\ x e. X ) -> ( u G x ) = x )
9 8 adantll 
 |-  ( ( ( u e. X /\ A. z e. X ( ( u G z ) = z /\ E. w e. X ( w G z ) = u ) ) /\ x e. X ) -> ( u G x ) = x )
10 9 adantll 
 |-  ( ( ( G e. GrpOp /\ ( u e. X /\ A. z e. X ( ( u G z ) = z /\ E. w e. X ( w G z ) = u ) ) ) /\ x e. X ) -> ( u G x ) = x )
11 simpl 
 |-  ( ( G e. GrpOp /\ ( u e. X /\ A. z e. X ( ( u G z ) = z /\ E. w e. X ( w G z ) = u ) ) ) -> G e. GrpOp )
12 11 anim1i 
 |-  ( ( ( G e. GrpOp /\ ( u e. X /\ A. z e. X ( ( u G z ) = z /\ E. w e. X ( w G z ) = u ) ) ) /\ x e. X ) -> ( G e. GrpOp /\ x e. X ) )
13 id 
 |-  ( ( G e. GrpOp /\ u e. X ) -> ( G e. GrpOp /\ u e. X ) )
14 13 adantrr 
 |-  ( ( G e. GrpOp /\ ( u e. X /\ A. z e. X ( ( u G z ) = z /\ E. w e. X ( w G z ) = u ) ) ) -> ( G e. GrpOp /\ u e. X ) )
15 14 adantr 
 |-  ( ( ( G e. GrpOp /\ ( u e. X /\ A. z e. X ( ( u G z ) = z /\ E. w e. X ( w G z ) = u ) ) ) /\ x e. X ) -> ( G e. GrpOp /\ u e. X ) )
16 3 adantl 
 |-  ( ( u e. X /\ A. z e. X ( ( u G z ) = z /\ E. w e. X ( w G z ) = u ) ) -> A. z e. X ( u G z ) = z )
17 16 ad2antlr 
 |-  ( ( ( G e. GrpOp /\ ( u e. X /\ A. z e. X ( ( u G z ) = z /\ E. w e. X ( w G z ) = u ) ) ) /\ x e. X ) -> A. z e. X ( u G z ) = z )
18 simpr 
 |-  ( ( ( u G z ) = z /\ E. w e. X ( w G z ) = u ) -> E. w e. X ( w G z ) = u )
19 18 ralimi 
 |-  ( A. z e. X ( ( u G z ) = z /\ E. w e. X ( w G z ) = u ) -> A. z e. X E. w e. X ( w G z ) = u )
20 19 adantl 
 |-  ( ( u e. X /\ A. z e. X ( ( u G z ) = z /\ E. w e. X ( w G z ) = u ) ) -> A. z e. X E. w e. X ( w G z ) = u )
21 20 ad2antlr 
 |-  ( ( ( G e. GrpOp /\ ( u e. X /\ A. z e. X ( ( u G z ) = z /\ E. w e. X ( w G z ) = u ) ) ) /\ x e. X ) -> A. z e. X E. w e. X ( w G z ) = u )
22 15 17 21 jca32 
 |-  ( ( ( G e. GrpOp /\ ( u e. X /\ A. z e. X ( ( u G z ) = z /\ E. w e. X ( w G z ) = u ) ) ) /\ x e. X ) -> ( ( G e. GrpOp /\ u e. X ) /\ ( A. z e. X ( u G z ) = z /\ A. z e. X E. w e. X ( w G z ) = u ) ) )
23 biid 
 |-  ( A. z e. X ( u G z ) = z <-> A. z e. X ( u G z ) = z )
24 biid 
 |-  ( A. z e. X E. w e. X ( w G z ) = u <-> A. z e. X E. w e. X ( w G z ) = u )
25 1 23 24 grpoidinvlem3 
 |-  ( ( ( ( G e. GrpOp /\ u e. X ) /\ ( A. z e. X ( u G z ) = z /\ A. z e. X E. w e. X ( w G z ) = u ) ) /\ x e. X ) -> E. y e. X ( ( y G x ) = u /\ ( x G y ) = u ) )
26 22 25 sylancom 
 |-  ( ( ( G e. GrpOp /\ ( u e. X /\ A. z e. X ( ( u G z ) = z /\ E. w e. X ( w G z ) = u ) ) ) /\ x e. X ) -> E. y e. X ( ( y G x ) = u /\ ( x G y ) = u ) )
27 1 grpoidinvlem4 
 |-  ( ( ( G e. GrpOp /\ x e. X ) /\ E. y e. X ( ( y G x ) = u /\ ( x G y ) = u ) ) -> ( x G u ) = ( u G x ) )
28 12 26 27 syl2anc 
 |-  ( ( ( G e. GrpOp /\ ( u e. X /\ A. z e. X ( ( u G z ) = z /\ E. w e. X ( w G z ) = u ) ) ) /\ x e. X ) -> ( x G u ) = ( u G x ) )
29 28 10 eqtrd 
 |-  ( ( ( G e. GrpOp /\ ( u e. X /\ A. z e. X ( ( u G z ) = z /\ E. w e. X ( w G z ) = u ) ) ) /\ x e. X ) -> ( x G u ) = x )
30 10 29 26 jca31 
 |-  ( ( ( G e. GrpOp /\ ( u e. X /\ A. z e. X ( ( u G z ) = z /\ E. w e. X ( w G z ) = u ) ) ) /\ x e. X ) -> ( ( ( u G x ) = x /\ ( x G u ) = x ) /\ E. y e. X ( ( y G x ) = u /\ ( x G y ) = u ) ) )
31 30 ralrimiva 
 |-  ( ( G e. GrpOp /\ ( u e. X /\ A. z e. X ( ( u G z ) = z /\ E. w e. X ( w G z ) = u ) ) ) -> A. x e. X ( ( ( u G x ) = x /\ ( x G u ) = x ) /\ E. y e. X ( ( y G x ) = u /\ ( x G y ) = u ) ) )
32 1 grpolidinv 
 |-  ( G e. GrpOp -> E. u e. X A. z e. X ( ( u G z ) = z /\ E. w e. X ( w G z ) = u ) )
33 31 32 reximddv 
 |-  ( G e. GrpOp -> E. u e. X A. x e. X ( ( ( u G x ) = x /\ ( x G u ) = x ) /\ E. y e. X ( ( y G x ) = u /\ ( x G y ) = u ) ) )