Theorem plusffn

Description: The group addition operation is a function. (Contributed by Mario Carneiro, 20-Sep-2015)

	Ref	Expression
Hypotheses	plusffn.1	⊢ 𝐵 = ( Base ‘ 𝐺 )
	plusffn.2	⊢ ⨣ = ( +𝑓 ‘ 𝐺 )
Assertion	plusffn	⊢ ⨣ Fn ( 𝐵 × 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		plusffn.1	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		plusffn.2	⊢ ⨣ = ( +𝑓 ‘ 𝐺 )
3		eqid	⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
4	1 3 2	plusffval	⊢ ⨣ = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) )
5		ovex	⊢ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ V
6	4 5	fnmpoi	⊢ ⨣ Fn ( 𝐵 × 𝐵 )