Metamath Proof Explorer


Theorem grpsubfval

Description: Group subtraction (division) operation. For a shorter proof using ax-rep , see grpsubfvalALT . (Contributed by NM, 31-Mar-2014) (Revised by Stefan O'Rear, 27-Mar-2015) Remove dependency on ax-rep . (Revised by Rohan Ridenour, 17-Aug-2023) (Proof shortened by AV, 19-Feb-2024)

Ref Expression
Hypotheses grpsubval.b 𝐵 = ( Base ‘ 𝐺 )
grpsubval.p + = ( +g𝐺 )
grpsubval.i 𝐼 = ( invg𝐺 )
grpsubval.m = ( -g𝐺 )
Assertion grpsubfval = ( 𝑥𝐵 , 𝑦𝐵 ↦ ( 𝑥 + ( 𝐼𝑦 ) ) )

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 2 fvexi + ∈ V
18 17 rnex ran + ∈ V
19 p0ex { ∅ } ∈ V
20 18 19 unex ( ran + ∪ { ∅ } ) ∈ V
21 df-ov ( 𝑥 + ( 𝐼𝑦 ) ) = ( + ‘ ⟨ 𝑥 , ( 𝐼𝑦 ) ⟩ )
22 fvrn0 ( + ‘ ⟨ 𝑥 , ( 𝐼𝑦 ) ⟩ ) ∈ ( ran + ∪ { ∅ } )
23 21 22 eqeltri ( 𝑥 + ( 𝐼𝑦 ) ) ∈ ( ran + ∪ { ∅ } )
24 23 rgen2w 𝑥𝐵𝑦𝐵 ( 𝑥 + ( 𝐼𝑦 ) ) ∈ ( ran + ∪ { ∅ } )
25 16 16 20 24 mpoexw ( 𝑥𝐵 , 𝑦𝐵 ↦ ( 𝑥 + ( 𝐼𝑦 ) ) ) ∈ V
26 14 15 25 fvmpt ( 𝐺 ∈ V → ( -g𝐺 ) = ( 𝑥𝐵 , 𝑦𝐵 ↦ ( 𝑥 + ( 𝐼𝑦 ) ) ) )
27 4 26 eqtrid ( 𝐺 ∈ V → = ( 𝑥𝐵 , 𝑦𝐵 ↦ ( 𝑥 + ( 𝐼𝑦 ) ) ) )
28 fvprc ( ¬ 𝐺 ∈ V → ( -g𝐺 ) = ∅ )
29 4 28 eqtrid ( ¬ 𝐺 ∈ V → = ∅ )
30 fvprc ( ¬ 𝐺 ∈ V → ( Base ‘ 𝐺 ) = ∅ )
31 1 30 eqtrid ( ¬ 𝐺 ∈ V → 𝐵 = ∅ )
32 31 olcd ( ¬ 𝐺 ∈ V → ( 𝐵 = ∅ ∨ 𝐵 = ∅ ) )
33 0mpo0 ( ( 𝐵 = ∅ ∨ 𝐵 = ∅ ) → ( 𝑥𝐵 , 𝑦𝐵 ↦ ( 𝑥 + ( 𝐼𝑦 ) ) ) = ∅ )
34 32 33 syl ( ¬ 𝐺 ∈ V → ( 𝑥𝐵 , 𝑦𝐵 ↦ ( 𝑥 + ( 𝐼𝑦 ) ) ) = ∅ )
35 29 34 eqtr4d ( ¬ 𝐺 ∈ V → = ( 𝑥𝐵 , 𝑦𝐵 ↦ ( 𝑥 + ( 𝐼𝑦 ) ) ) )
36 27 35 pm2.61i = ( 𝑥𝐵 , 𝑦𝐵 ↦ ( 𝑥 + ( 𝐼𝑦 ) ) )