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. ) )