Theorem plusfval

Description: The group addition operation as a function. (Contributed by Mario Carneiro, 14-Aug-2015)

	Ref	Expression
Hypotheses	plusffval.1	⊢ 𝐵 = ( Base ‘ 𝐺 )
	plusffval.2	⊢ + = ( +g ‘ 𝐺 )
	plusffval.3	⊢ ⨣ = ( +𝑓 ‘ 𝐺 )
Assertion	plusfval	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ⨣ 𝑌 ) = ( 𝑋 + 𝑌 ) )

Proof

Step	Hyp	Ref	Expression
1		plusffval.1	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		plusffval.2	⊢ + = ( +g ‘ 𝐺 )
3		plusffval.3	⊢ ⨣ = ( +𝑓 ‘ 𝐺 )
4		oveq12	⊢ ( ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) → ( 𝑥 + 𝑦 ) = ( 𝑋 + 𝑌 ) )
5	1 2 3	plusffval	⊢ ⨣ = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 + 𝑦 ) )
6		ovex	⊢ ( 𝑋 + 𝑌 ) ∈ V
7	4 5 6	ovmpoa	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ⨣ 𝑌 ) = ( 𝑋 + 𝑌 ) )