Metamath Proof Explorer

Theorem grpinvfvalALT

Description: Shorter proof of grpinvfval using ax-rep . (Contributed by NM, 24-Aug-2011) (Revised by Mario Carneiro, 7-Aug-2013) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses grpinvval.b 
|- B = ( Base ` G )
grpinvval.p 
|- .+ = ( +g ` G )
grpinvval.o 
|- .0. = ( 0g ` G )
grpinvval.n 
|- N = ( invg ` G )
Assertion grpinvfvalALT 
|- 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 14 15 1 mptfvmpt 
 |-  ( G e. _V -> ( invg ` G ) = ( x e. B |-> ( iota_ y e. B ( y .+ x ) = .0. ) ) )
17 fvprc 
 |-  ( -. G e. _V -> ( invg ` G ) = (/) )
18 mpt0 
 |-  ( x e. (/) |-> ( iota_ y e. B ( y .+ x ) = .0. ) ) = (/)
19 17 18 eqtr4di 
 |-  ( -. G e. _V -> ( invg ` G ) = ( x e. (/) |-> ( iota_ y e. B ( y .+ x ) = .0. ) ) )
20 fvprc 
 |-  ( -. G e. _V -> ( Base ` G ) = (/) )
21 1 20 eqtrid 
 |-  ( -. G e. _V -> B = (/) )
22 21 mpteq1d 
 |-  ( -. G e. _V -> ( x e. B |-> ( iota_ y e. B ( y .+ x ) = .0. ) ) = ( x e. (/) |-> ( iota_ y e. B ( y .+ x ) = .0. ) ) )
23 19 22 eqtr4d 
 |-  ( -. G e. _V -> ( invg ` G ) = ( x e. B |-> ( iota_ y e. B ( y .+ x ) = .0. ) ) )
24 16 23 pm2.61i 
 |-  ( invg ` G ) = ( x e. B |-> ( iota_ y e. B ( y .+ x ) = .0. ) )
25 4 24 eqtri 
 |-  N = ( x e. B |-> ( iota_ y e. B ( y .+ x ) = .0. ) )