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 syl5eq ⊢ ( 𝐺 ∈ V → − = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 + ( 𝐼 ‘ 𝑦 ) ) ) )
28 fvprc ⊢ ( ¬ 𝐺 ∈ V → ( -g ‘ 𝐺 ) = ∅ )
29 4 28 syl5eq ⊢ ( ¬ 𝐺 ∈ V → − = ∅ )
30 fvprc ⊢ ( ¬ 𝐺 ∈ V → ( Base ‘ 𝐺 ) = ∅ )
31 1 30 syl5eq ⊢ ( ¬ 𝐺 ∈ V → 𝐵 = ∅ )
32 31 olcd ⊢ ( ¬ 𝐺 ∈ V → ( 𝐵 = ∅ ∨ 𝐵 = ∅ ) )
33 0mpo0 ⊢ ( ( 𝐵 = ∅ ∨ 𝐵 = ∅ ) → ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 + ( 𝐼 ‘ 𝑦 ) ) ) = ∅ )
34 32 33 syl ⊢ ( ¬ 𝐺 ∈ V → ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 + ( 𝐼 ‘ 𝑦 ) ) ) = ∅ )
35 29 34 eqtr4d ⊢ ( ¬ 𝐺 ∈ V → − = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 + ( 𝐼 ‘ 𝑦 ) ) ) )
36 27 35 pm2.61i ⊢ − = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 + ( 𝐼 ‘ 𝑦 ) ) )