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
grpinvval.o 0 ˙ = 0 G
grpinvval.n N = inv g G
Assertion grpinvfvalALT N = x B ι y B | y + ˙ x = 0 ˙

Proof

Step Hyp Ref Expression
1 grpinvval.b B = Base G
2 grpinvval.p + ˙ = + G
3 grpinvval.o 0 ˙ = 0 G
4 grpinvval.n N = inv g G
5 fveq2 g = G Base g = Base G
6 5 1 eqtr4di g = G Base g = B
7 fveq2 g = G + g = + G
8 7 2 eqtr4di g = G + g = + ˙
9 8 oveqd g = G y + g x = y + ˙ x
10 fveq2 g = G 0 g = 0 G
11 10 3 eqtr4di g = G 0 g = 0 ˙
12 9 11 eqeq12d g = G y + g x = 0 g y + ˙ x = 0 ˙
13 6 12 riotaeqbidv g = G ι y Base g | y + g x = 0 g = ι y B | y + ˙ x = 0 ˙
14 6 13 mpteq12dv g = G x Base g ι y Base g | y + g x = 0 g = x B ι y B | y + ˙ x = 0 ˙
15 df-minusg inv g = g V x Base g ι y Base g | y + g x = 0 g
16 14 15 1 mptfvmpt G V inv g G = x B ι y B | y + ˙ x = 0 ˙
17 fvprc ¬ G V inv g G =
18 mpt0 x ι y B | y + ˙ x = 0 ˙ =
19 17 18 eqtr4di ¬ G V inv g G = x ι y B | y + ˙ x = 0 ˙
20 fvprc ¬ G V Base G =
21 1 20 eqtrid ¬ G V B =
22 21 mpteq1d ¬ G V x B ι y B | y + ˙ x = 0 ˙ = x ι y B | y + ˙ x = 0 ˙
23 19 22 eqtr4d ¬ G V inv g G = x B ι y B | y + ˙ x = 0 ˙
24 16 23 pm2.61i inv g G = x B ι y B | y + ˙ x = 0 ˙
25 4 24 eqtri N = x B ι y B | y + ˙ x = 0 ˙