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 𝐵 = ( Base ‘ 𝐺 )
grpsubval.p + = ( +g𝐺 )
grpsubval.i 𝐼 = ( invg𝐺 )
grpsubval.m = ( -g𝐺 )
Assertion grpsubfvalALT = ( 𝑥𝐵 , 𝑦𝐵 ↦ ( 𝑥 + ( 𝐼𝑦 ) ) )

Proof

Step Hyp Ref Expression
1 grpsubval.b 𝐵 = ( Base ‘ 𝐺 )
2 grpsubval.p + = ( +g𝐺 )
3 grpsubval.i 𝐼 = ( invg𝐺 )
4 grpsubval.m = ( -g𝐺 )
5 fveq2 ( 𝑔 = 𝐺 → ( Base ‘ 𝑔 ) = ( Base ‘ 𝐺 ) )
6 5 1 eqtr4di ( 𝑔 = 𝐺 → ( Base ‘ 𝑔 ) = 𝐵 )
7 fveq2 ( 𝑔 = 𝐺 → ( +g𝑔 ) = ( +g𝐺 ) )
8 7 2 eqtr4di ( 𝑔 = 𝐺 → ( +g𝑔 ) = + )
9 eqidd ( 𝑔 = 𝐺𝑥 = 𝑥 )
10 fveq2 ( 𝑔 = 𝐺 → ( invg𝑔 ) = ( invg𝐺 ) )
11 10 3 eqtr4di ( 𝑔 = 𝐺 → ( invg𝑔 ) = 𝐼 )
12 11 fveq1d ( 𝑔 = 𝐺 → ( ( invg𝑔 ) ‘ 𝑦 ) = ( 𝐼𝑦 ) )
13 8 9 12 oveq123d ( 𝑔 = 𝐺 → ( 𝑥 ( +g𝑔 ) ( ( invg𝑔 ) ‘ 𝑦 ) ) = ( 𝑥 + ( 𝐼𝑦 ) ) )
14 6 6 13 mpoeq123dv ( 𝑔 = 𝐺 → ( 𝑥 ∈ ( Base ‘ 𝑔 ) , 𝑦 ∈ ( Base ‘ 𝑔 ) ↦ ( 𝑥 ( +g𝑔 ) ( ( invg𝑔 ) ‘ 𝑦 ) ) ) = ( 𝑥𝐵 , 𝑦𝐵 ↦ ( 𝑥 + ( 𝐼𝑦 ) ) ) )
15 df-sbg -g = ( 𝑔 ∈ V ↦ ( 𝑥 ∈ ( Base ‘ 𝑔 ) , 𝑦 ∈ ( Base ‘ 𝑔 ) ↦ ( 𝑥 ( +g𝑔 ) ( ( invg𝑔 ) ‘ 𝑦 ) ) ) )
16 1 fvexi 𝐵 ∈ V
17 16 16 mpoex ( 𝑥𝐵 , 𝑦𝐵 ↦ ( 𝑥 + ( 𝐼𝑦 ) ) ) ∈ V
18 14 15 17 fvmpt ( 𝐺 ∈ V → ( -g𝐺 ) = ( 𝑥𝐵 , 𝑦𝐵 ↦ ( 𝑥 + ( 𝐼𝑦 ) ) ) )
19 4 18 eqtrid ( 𝐺 ∈ V → = ( 𝑥𝐵 , 𝑦𝐵 ↦ ( 𝑥 + ( 𝐼𝑦 ) ) ) )
20 fvprc ( ¬ 𝐺 ∈ V → ( -g𝐺 ) = ∅ )
21 4 20 eqtrid ( ¬ 𝐺 ∈ V → = ∅ )
22 fvprc ( ¬ 𝐺 ∈ V → ( Base ‘ 𝐺 ) = ∅ )
23 1 22 eqtrid ( ¬ 𝐺 ∈ V → 𝐵 = ∅ )
24 23 olcd ( ¬ 𝐺 ∈ V → ( 𝐵 = ∅ ∨ 𝐵 = ∅ ) )
25 0mpo0 ( ( 𝐵 = ∅ ∨ 𝐵 = ∅ ) → ( 𝑥𝐵 , 𝑦𝐵 ↦ ( 𝑥 + ( 𝐼𝑦 ) ) ) = ∅ )
26 24 25 syl ( ¬ 𝐺 ∈ V → ( 𝑥𝐵 , 𝑦𝐵 ↦ ( 𝑥 + ( 𝐼𝑦 ) ) ) = ∅ )
27 21 26 eqtr4d ( ¬ 𝐺 ∈ V → = ( 𝑥𝐵 , 𝑦𝐵 ↦ ( 𝑥 + ( 𝐼𝑦 ) ) ) )
28 19 27 pm2.61i = ( 𝑥𝐵 , 𝑦𝐵 ↦ ( 𝑥 + ( 𝐼𝑦 ) ) )