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 = ( 𝑥𝐵 , 𝑦𝐵 ↦ ( 𝑥 + 𝑦 ) )