This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem plusffval

Description: The group addition operation as a function. (Contributed by Mario Carneiro, 14-Aug-2015) (Proof shortened by AV, 2-Mar-2024)

Ref Expression
Hypotheses plusffval.1 ⊢ 𝐵 = ( Base ‘ 𝐺 )
plusffval.2 ⊢ + = ( +g ‘ 𝐺 )
plusffval.3 ⊢ ⨣ = ( +𝑓 ‘ 𝐺 )
Assertion plusffval ⨣ = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 + 𝑦 ) )

Proof

Step Hyp Ref Expression
1 plusffval.1 ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 plusffval.2 ⊢ + = ( +g ‘ 𝐺 )
3 plusffval.3 ⊢ ⨣ = ( +𝑓 ‘ 𝐺 )
4 fveq2 ⊢ ( 𝑔 = 𝐺 → ( Base ‘ 𝑔 ) = ( Base ‘ 𝐺 ) )
5 4 1 eqtr4di ⊢ ( 𝑔 = 𝐺 → ( Base ‘ 𝑔 ) = 𝐵 )
6 fveq2 ⊢ ( 𝑔 = 𝐺 → ( +g ‘ 𝑔 ) = ( +g ‘ 𝐺 ) )
7 6 2 eqtr4di ⊢ ( 𝑔 = 𝐺 → ( +g ‘ 𝑔 ) = + )
8 7 oveqd ⊢ ( 𝑔 = 𝐺 → ( 𝑥 ( +g ‘ 𝑔 ) 𝑦 ) = ( 𝑥 + 𝑦 ) )
9 5 5 8 mpoeq123dv ⊢ ( 𝑔 = 𝐺 → ( 𝑥 ∈ ( Base ‘ 𝑔 ) , 𝑦 ∈ ( Base ‘ 𝑔 ) ↦ ( 𝑥 ( +g ‘ 𝑔 ) 𝑦 ) ) = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 + 𝑦 ) ) )
10 df-plusf ⊢ +𝑓 = ( 𝑔 ∈ V ↦ ( 𝑥 ∈ ( Base ‘ 𝑔 ) , 𝑦 ∈ ( Base ‘ 𝑔 ) ↦ ( 𝑥 ( +g ‘ 𝑔 ) 𝑦 ) ) )
11 1 fvexi ⊢ 𝐵 ∈ V
12 2 fvexi ⊢ + ∈ V
13 12 rnex ⊢ ran + ∈ V
14 p0ex ⊢ { ∅ } ∈ V
15 13 14 unex ⊢ ( ran + ∪ { ∅ } ) ∈ V
16 df-ov ⊢ ( 𝑥 + 𝑦 ) = ( + ‘ ⟨ 𝑥 , 𝑦 ⟩ )
17 fvrn0 ⊢ ( + ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ∈ ( ran + ∪ { ∅ } )
18 16 17 eqeltri ⊢ ( 𝑥 + 𝑦 ) ∈ ( ran + ∪ { ∅ } )
19 18 rgen2w ⊢ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 + 𝑦 ) ∈ ( ran + ∪ { ∅ } )
20 11 11 15 19 mpoexw ⊢ ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 + 𝑦 ) ) ∈ V
21 9 10 20 fvmpt ⊢ ( 𝐺 ∈ V → ( +𝑓 ‘ 𝐺 ) = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 + 𝑦 ) ) )
22 fvprc ⊢ ( ¬ 𝐺 ∈ V → ( +𝑓 ‘ 𝐺 ) = ∅ )
23 fvprc ⊢ ( ¬ 𝐺 ∈ V → ( Base ‘ 𝐺 ) = ∅ )
24 1 23 eqtrid ⊢ ( ¬ 𝐺 ∈ V → 𝐵 = ∅ )
25 24 olcd ⊢ ( ¬ 𝐺 ∈ V → ( 𝐵 = ∅ ∨ 𝐵 = ∅ ) )
26 0mpo0 ⊢ ( ( 𝐵 = ∅ ∨ 𝐵 = ∅ ) → ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 + 𝑦 ) ) = ∅ )
27 25 26 syl ⊢ ( ¬ 𝐺 ∈ V → ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 + 𝑦 ) ) = ∅ )
28 22 27 eqtr4d ⊢ ( ¬ 𝐺 ∈ V → ( +𝑓 ‘ 𝐺 ) = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 + 𝑦 ) ) )
29 21 28 pm2.61i ⊢ ( +𝑓 ‘ 𝐺 ) = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 + 𝑦 ) )
30 3 29 eqtri ⊢ ⨣ = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 + 𝑦 ) )