Metamath Proof Explorer

Theorem grpoidinv2

Description: A group's properties using the explicit identity element. (Contributed by NM, 5-Feb-2010) (Revised by Mario Carneiro, 15-Dec-2013) (New usage is discouraged.)

Ref Expression
Hypotheses grpoidval.1 
|- X = ran G
grpoidval.2 
|- U = ( GId ` G )
Assertion grpoidinv2 
|- ( ( G e. GrpOp /\ A e. X ) -> ( ( ( U G A ) = A /\ ( A G U ) = A ) /\ E. y e. X ( ( y G A ) = U /\ ( A G y ) = U ) ) )

Proof

Step Hyp Ref Expression
1 grpoidval.1 
 |-  X = ran G
2 grpoidval.2 
 |-  U = ( GId ` G )
3 1 2 grpoidval 
 |-  ( G e. GrpOp -> U = ( iota_ u e. X A. x e. X ( u G x ) = x ) )
4 1 grpoideu 
 |-  ( G e. GrpOp -> E! u e. X A. x e. X ( u G x ) = x )
5 riotacl2 
 |-  ( E! u e. X A. x e. X ( u G x ) = x -> ( iota_ u e. X A. x e. X ( u G x ) = x ) e. { u e. X | A. x e. X ( u G x ) = x } )
6 4 5 syl 
 |-  ( G e. GrpOp -> ( iota_ u e. X A. x e. X ( u G x ) = x ) e. { u e. X | A. x e. X ( u G x ) = x } )
7 3 6 eqeltrd 
 |-  ( G e. GrpOp -> U e. { u e. X | A. x e. X ( u G x ) = x } )
8 simpll 
 |-  ( ( ( ( u G x ) = x /\ ( x G u ) = x ) /\ E. y e. X ( ( y G x ) = u /\ ( x G y ) = u ) ) -> ( u G x ) = x )
9 8 ralimi 
 |-  ( A. x e. X ( ( ( u G x ) = x /\ ( x G u ) = x ) /\ E. y e. X ( ( y G x ) = u /\ ( x G y ) = u ) ) -> A. x e. X ( u G x ) = x )
10 9 rgenw 
 |-  A. 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 ) ) -> A. x e. X ( u G x ) = x )
11 10 a1i 
 |-  ( G e. GrpOp -> A. 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 ) ) -> A. x e. X ( u G x ) = x ) )
12 1 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 ) ) )
13 11 12 4 3jca 
 |-  ( G e. GrpOp -> ( A. 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 ) ) -> A. x e. X ( u G x ) = x ) /\ 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 ) ) /\ E! u e. X A. x e. X ( u G x ) = x ) )
14 reupick2 
 |-  ( ( ( A. 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 ) ) -> A. x e. X ( u G x ) = x ) /\ 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 ) ) /\ E! u e. X A. x e. X ( u G x ) = x ) /\ u e. X ) -> ( A. x e. X ( u G x ) = 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 ) ) ) )
15 13 14 sylan 
 |-  ( ( G e. GrpOp /\ u e. X ) -> ( A. x e. X ( u G x ) = 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 ) ) ) )
16 15 rabbidva 
 |-  ( G e. GrpOp -> { u e. X | A. x e. X ( u G x ) = x } = { 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 ) ) } )
17 7 16 eleqtrd 
 |-  ( G e. GrpOp -> U 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 ) ) } )
18 oveq1 
 |-  ( u = U -> ( u G x ) = ( U G x ) )
19 18 eqeq1d 
 |-  ( u = U -> ( ( u G x ) = x <-> ( U G x ) = x ) )
20 oveq2 
 |-  ( u = U -> ( x G u ) = ( x G U ) )
21 20 eqeq1d 
 |-  ( u = U -> ( ( x G u ) = x <-> ( x G U ) = x ) )
22 19 21 anbi12d 
 |-  ( u = U -> ( ( ( u G x ) = x /\ ( x G u ) = x ) <-> ( ( U G x ) = x /\ ( x G U ) = x ) ) )
23 eqeq2 
 |-  ( u = U -> ( ( y G x ) = u <-> ( y G x ) = U ) )
24 eqeq2 
 |-  ( u = U -> ( ( x G y ) = u <-> ( x G y ) = U ) )
25 23 24 anbi12d 
 |-  ( u = U -> ( ( ( y G x ) = u /\ ( x G y ) = u ) <-> ( ( y G x ) = U /\ ( x G y ) = U ) ) )
26 25 rexbidv 
 |-  ( u = U -> ( E. y e. X ( ( y G x ) = u /\ ( x G y ) = u ) <-> E. y e. X ( ( y G x ) = U /\ ( x G y ) = U ) ) )
27 22 26 anbi12d 
 |-  ( u = U -> ( ( ( ( u G x ) = x /\ ( x G u ) = x ) /\ E. y e. X ( ( y G x ) = u /\ ( x G y ) = u ) ) <-> ( ( ( U G x ) = x /\ ( x G U ) = x ) /\ E. y e. X ( ( y G x ) = U /\ ( x G y ) = U ) ) ) )
28 27 ralbidv 
 |-  ( u = 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 ) ) <-> A. x e. X ( ( ( U G x ) = x /\ ( x G U ) = x ) /\ E. y e. X ( ( y G x ) = U /\ ( x G y ) = U ) ) ) )
29 28 elrab 
 |-  ( U 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 ) ) } <-> ( 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 ) ) ) )
30 17 29 sylib 
 |-  ( G e. GrpOp -> ( 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 ) ) ) )
31 30 simprd 
 |-  ( G e. GrpOp -> 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 oveq2 
 |-  ( x = A -> ( U G x ) = ( U G A ) )
33 id 
 |-  ( x = A -> x = A )
34 32 33 eqeq12d 
 |-  ( x = A -> ( ( U G x ) = x <-> ( U G A ) = A ) )
35 oveq1 
 |-  ( x = A -> ( x G U ) = ( A G U ) )
36 35 33 eqeq12d 
 |-  ( x = A -> ( ( x G U ) = x <-> ( A G U ) = A ) )
37 34 36 anbi12d 
 |-  ( x = A -> ( ( ( U G x ) = x /\ ( x G U ) = x ) <-> ( ( U G A ) = A /\ ( A G U ) = A ) ) )
38 oveq2 
 |-  ( x = A -> ( y G x ) = ( y G A ) )
39 38 eqeq1d 
 |-  ( x = A -> ( ( y G x ) = U <-> ( y G A ) = U ) )
40 oveq1 
 |-  ( x = A -> ( x G y ) = ( A G y ) )
41 40 eqeq1d 
 |-  ( x = A -> ( ( x G y ) = U <-> ( A G y ) = U ) )
42 39 41 anbi12d 
 |-  ( x = A -> ( ( ( y G x ) = U /\ ( x G y ) = U ) <-> ( ( y G A ) = U /\ ( A G y ) = U ) ) )
43 42 rexbidv 
 |-  ( x = A -> ( E. y e. X ( ( y G x ) = U /\ ( x G y ) = U ) <-> E. y e. X ( ( y G A ) = U /\ ( A G y ) = U ) ) )
44 37 43 anbi12d 
 |-  ( x = A -> ( ( ( ( U G x ) = x /\ ( x G U ) = x ) /\ E. y e. X ( ( y G x ) = U /\ ( x G y ) = U ) ) <-> ( ( ( U G A ) = A /\ ( A G U ) = A ) /\ E. y e. X ( ( y G A ) = U /\ ( A G y ) = U ) ) ) )
45 44 rspccva 
 |-  ( ( A. x e. X ( ( ( U G x ) = x /\ ( x G U ) = x ) /\ E. y e. X ( ( y G x ) = U /\ ( x G y ) = U ) ) /\ A e. X ) -> ( ( ( U G A ) = A /\ ( A G U ) = A ) /\ E. y e. X ( ( y G A ) = U /\ ( A G y ) = U ) ) )
46 31 45 sylan 
 |-  ( ( G e. GrpOp /\ A e. X ) -> ( ( ( U G A ) = A /\ ( A G U ) = A ) /\ E. y e. X ( ( y G A ) = U /\ ( A G y ) = U ) ) )