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 syl5eq ⊢ ( 𝐺 ∈ V → − = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 + ( 𝐼 ‘ 𝑦 ) ) ) )
20 fvprc ⊢ ( ¬ 𝐺 ∈ V → ( -g ‘ 𝐺 ) = ∅ )
21 4 20 syl5eq ⊢ ( ¬ 𝐺 ∈ V → − = ∅ )
22 fvprc ⊢ ( ¬ 𝐺 ∈ V → ( Base ‘ 𝐺 ) = ∅ )
23 1 22 syl5eq ⊢ ( ¬ 𝐺 ∈ V → 𝐵 = ∅ )
24 23 olcd ⊢ ( ¬ 𝐺 ∈ V → ( 𝐵 = ∅ ∨ 𝐵 = ∅ ) )
25 0mpo0 ⊢ ( ( 𝐵 = ∅ ∨ 𝐵 = ∅ ) → ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 + ( 𝐼 ‘ 𝑦 ) ) ) = ∅ )
26 24 25 syl ⊢ ( ¬ 𝐺 ∈ V → ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 + ( 𝐼 ‘ 𝑦 ) ) ) = ∅ )
27 21 26 eqtr4d ⊢ ( ¬ 𝐺 ∈ V → − = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 + ( 𝐼 ‘ 𝑦 ) ) ) )
28 19 27 pm2.61i ⊢ − = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 + ( 𝐼 ‘ 𝑦 ) ) )