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	syl5eq	⊢ ( ¬ 𝐺 ∈ 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	⊢ ⨣ = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 + 𝑦 ) )