mulvfn

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

		Ref	Expression
	Assertion	mulvfn	$⊢ (A \in C \land B \in D) \to (A \cdot_{v} B) Fn ℝ$

Step	Hyp	Ref	Expression
1		ovex	$⊢ A B (x) \in V$
2		eqid	$⊢ (x \in ℝ ⟼ A B (x)) = (x \in ℝ ⟼ A B (x))$
3	1 2	fnmpti	$⊢ (x \in ℝ ⟼ A B (x)) Fn ℝ$
4		mulvval	$⊢ (A \in C \land B \in D) \to A \cdot_{v} B = (x \in ℝ ⟼ A B (x))$
5	4	fneq1d	$⊢ (A \in C \land B \in D) \to ((A \cdot_{v} B) Fn ℝ \leftrightarrow (x \in ℝ ⟼ A B (x)) Fn ℝ)$
6	3 5	mpbiri	$⊢ (A \in C \land B \in D) \to (A \cdot_{v} B) Fn ℝ$

Metamath Proof Explorer