Theorem mulvfn

Description: Scalar multiplication producees a function. (Contributed by Andrew Salmon, 27-Jan-2012)

	Ref	Expression
Assertion	mulvfn	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → ( 𝐴 .𝑣 𝐵 ) Fn ℝ )

Proof

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