Metamath Proof Explorer

Theorem grpinvfval

Description: The inverse function of a group. For a shorter proof using ax-rep , see grpinvfvalALT . (Contributed by NM, 24-Aug-2011) (Revised by Mario Carneiro, 7-Aug-2013) Remove dependency on ax-rep . (Revised by Rohan Ridenour, 13-Aug-2023)

Ref Expression
Hypotheses grpinvval.b 
|- B = ( Base ` G )
grpinvval.p 
|- .+ = ( +g ` G )
grpinvval.o 
|- .0. = ( 0g ` G )
grpinvval.n 
|- N = ( invg ` G )
Assertion grpinvfval 
|- N = ( x e. B |-> ( iota_ y e. B ( y .+ x ) = .0. ) )

Proof

Step Hyp Ref Expression
1 grpinvval.b 
 |-  B = ( Base ` G )
2 grpinvval.p 
 |-  .+ = ( +g ` G )
3 grpinvval.o 
 |-  .0. = ( 0g ` G )
4 grpinvval.n 
 |-  N = ( invg ` G )
5 fveq2 
 |-  ( g = G -> ( Base ` g ) = ( Base ` G ) )
6 5 1 eqtr4di 
 |-  ( g = G -> ( Base ` g ) = B )
7 fveq2 
 |-  ( g = G -> ( +g ` g ) = ( +g ` G ) )
8 7 2 eqtr4di 
 |-  ( g = G -> ( +g ` g ) = .+ )
9 8 oveqd 
 |-  ( g = G -> ( y ( +g ` g ) x ) = ( y .+ x ) )
10 fveq2 
 |-  ( g = G -> ( 0g ` g ) = ( 0g ` G ) )
11 10 3 eqtr4di 
 |-  ( g = G -> ( 0g ` g ) = .0. )
12 9 11 eqeq12d 
 |-  ( g = G -> ( ( y ( +g ` g ) x ) = ( 0g ` g ) <-> ( y .+ x ) = .0. ) )
13 6 12 riotaeqbidv 
 |-  ( g = G -> ( iota_ y e. ( Base ` g ) ( y ( +g ` g ) x ) = ( 0g ` g ) ) = ( iota_ y e. B ( y .+ x ) = .0. ) )
14 6 13 mpteq12dv 
 |-  ( g = G -> ( x e. ( Base ` g ) |-> ( iota_ y e. ( Base ` g ) ( y ( +g ` g ) x ) = ( 0g ` g ) ) ) = ( x e. B |-> ( iota_ y e. B ( y .+ x ) = .0. ) ) )
15 df-minusg 
 |-  invg = ( g e. _V |-> ( x e. ( Base ` g ) |-> ( iota_ y e. ( Base ` g ) ( y ( +g ` g ) x ) = ( 0g ` g ) ) ) )
16 1 fvexi 
 |-  B e. _V
17 p0ex 
 |-  { (/) } e. _V
18 17 16 unex 
 |-  ( { (/) } u. B ) e. _V
19 ssun2 
 |-  B C_ ( { (/) } u. B )
20 riotacl 
 |-  ( E! y e. B ( y .+ x ) = .0. -> ( iota_ y e. B ( y .+ x ) = .0. ) e. B )
21 19 20 sselid 
 |-  ( E! y e. B ( y .+ x ) = .0. -> ( iota_ y e. B ( y .+ x ) = .0. ) e. ( { (/) } u. B ) )
22 ssun1 
 |-  { (/) } C_ ( { (/) } u. B )
23 riotaund 
 |-  ( -. E! y e. B ( y .+ x ) = .0. -> ( iota_ y e. B ( y .+ x ) = .0. ) = (/) )
24 riotaex 
 |-  ( iota_ y e. B ( y .+ x ) = .0. ) e. _V
25 24 elsn 
 |-  ( ( iota_ y e. B ( y .+ x ) = .0. ) e. { (/) } <-> ( iota_ y e. B ( y .+ x ) = .0. ) = (/) )
26 23 25 sylibr 
 |-  ( -. E! y e. B ( y .+ x ) = .0. -> ( iota_ y e. B ( y .+ x ) = .0. ) e. { (/) } )
27 22 26 sselid 
 |-  ( -. E! y e. B ( y .+ x ) = .0. -> ( iota_ y e. B ( y .+ x ) = .0. ) e. ( { (/) } u. B ) )
28 21 27 pm2.61i 
 |-  ( iota_ y e. B ( y .+ x ) = .0. ) e. ( { (/) } u. B )
29 28 rgenw 
 |-  A. x e. B ( iota_ y e. B ( y .+ x ) = .0. ) e. ( { (/) } u. B )
30 16 18 29 mptexw 
 |-  ( x e. B |-> ( iota_ y e. B ( y .+ x ) = .0. ) ) e. _V
31 14 15 30 fvmpt 
 |-  ( G e. _V -> ( invg ` G ) = ( x e. B |-> ( iota_ y e. B ( y .+ x ) = .0. ) ) )
32 fvprc 
 |-  ( -. G e. _V -> ( invg ` G ) = (/) )
33 mpt0 
 |-  ( x e. (/) |-> ( iota_ y e. B ( y .+ x ) = .0. ) ) = (/)
34 32 33 eqtr4di 
 |-  ( -. G e. _V -> ( invg ` G ) = ( x e. (/) |-> ( iota_ y e. B ( y .+ x ) = .0. ) ) )
35 fvprc 
 |-  ( -. G e. _V -> ( Base ` G ) = (/) )
36 1 35 eqtrid 
 |-  ( -. G e. _V -> B = (/) )
37 36 mpteq1d 
 |-  ( -. G e. _V -> ( x e. B |-> ( iota_ y e. B ( y .+ x ) = .0. ) ) = ( x e. (/) |-> ( iota_ y e. B ( y .+ x ) = .0. ) ) )
38 34 37 eqtr4d 
 |-  ( -. G e. _V -> ( invg ` G ) = ( x e. B |-> ( iota_ y e. B ( y .+ x ) = .0. ) ) )
39 31 38 pm2.61i 
 |-  ( invg ` G ) = ( x e. B |-> ( iota_ y e. B ( y .+ x ) = .0. ) )
40 4 39 eqtri 
 |-  N = ( x e. B |-> ( iota_ y e. B ( y .+ x ) = .0. ) )