Theorem addrfn

Description: Vector addition produces a function. (Contributed by Andrew Salmon, 27-Jan-2012)

	Ref	Expression
Assertion	addrfn	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → ( 𝐴 +𝑟 𝐵 ) Fn ℝ )

Proof

Step	Hyp	Ref	Expression
1		ovex	⊢ ( ( 𝐴 ‘ 𝑥 ) + ( 𝐵 ‘ 𝑥 ) ) ∈ V
2		eqid	⊢ ( 𝑥 ∈ ℝ ↦ ( ( 𝐴 ‘ 𝑥 ) + ( 𝐵 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ℝ ↦ ( ( 𝐴 ‘ 𝑥 ) + ( 𝐵 ‘ 𝑥 ) ) )
3	1 2	fnmpti	⊢ ( 𝑥 ∈ ℝ ↦ ( ( 𝐴 ‘ 𝑥 ) + ( 𝐵 ‘ 𝑥 ) ) ) Fn ℝ
4		addrval	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → ( 𝐴 +𝑟 𝐵 ) = ( 𝑥 ∈ ℝ ↦ ( ( 𝐴 ‘ 𝑥 ) + ( 𝐵 ‘ 𝑥 ) ) ) )
5	4	fneq1d	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → ( ( 𝐴 +𝑟 𝐵 ) Fn ℝ ↔ ( 𝑥 ∈ ℝ ↦ ( ( 𝐴 ‘ 𝑥 ) + ( 𝐵 ‘ 𝑥 ) ) ) Fn ℝ ) )
6	3 5	mpbiri	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → ( 𝐴 +𝑟 𝐵 ) Fn ℝ )