Metamath Proof Explorer


Theorem grpsubfvalALT

Description: Shorter proof of grpsubfval using ax-rep . (Contributed by NM, 31-Mar-2014) (Revised by Stefan O'Rear, 27-Mar-2015) (Proof shortened by AV, 19-Feb-2024) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses grpsubval.b B = Base G
grpsubval.p + ˙ = + G
grpsubval.i I = inv g G
grpsubval.m - ˙ = - G
Assertion grpsubfvalALT - ˙ = x B , y B x + ˙ I y

Proof

Step Hyp Ref Expression
1 grpsubval.b B = Base G
2 grpsubval.p + ˙ = + G
3 grpsubval.i I = inv g G
4 grpsubval.m - ˙ = - 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 eqidd g = G x = x
10 fveq2 g = G inv g g = inv g G
11 10 3 eqtr4di g = G inv g g = I
12 11 fveq1d g = G inv g g y = I y
13 8 9 12 oveq123d g = G x + g inv g g y = x + ˙ I y
14 6 6 13 mpoeq123dv g = G x Base g , y Base g x + g inv g g y = x B , y B x + ˙ I y
15 df-sbg - 𝑔 = g V x Base g , y Base g x + g inv g g y
16 1 fvexi B V
17 16 16 mpoex x B , y B x + ˙ I y V
18 14 15 17 fvmpt G V - G = x B , y B x + ˙ I y
19 4 18 eqtrid G V - ˙ = x B , y B x + ˙ I y
20 fvprc ¬ G V - G =
21 4 20 eqtrid ¬ G V - ˙ =
22 fvprc ¬ G V Base G =
23 1 22 eqtrid ¬ G V B =
24 23 olcd ¬ G V B = B =
25 0mpo0 B = B = x B , y B x + ˙ I y =
26 24 25 syl ¬ G V x B , y B x + ˙ I y =
27 21 26 eqtr4d ¬ G V - ˙ = x B , y B x + ˙ I y
28 19 27 pm2.61i - ˙ = x B , y B x + ˙ I y