# 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 ) ) )`