mulvfv

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

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

Step	Hyp	Ref	Expression
1		mulvval	$⊢ (A \in E \land B \in D) \to A \cdot_{v} B = (x \in ℝ ⟼ A B (x))$
2	1	fveq1d	$⊢ (A \in E \land B \in D) \to (A \cdot_{v} B) (C) = (x \in ℝ ⟼ A B (x)) (C)$
3		fveq2	$⊢ x = C \to B (x) = B (C)$
4	3	oveq2d	$⊢ x = C \to A B (x) = A B (C)$
5		eqid	$⊢ (x \in ℝ ⟼ A B (x)) = (x \in ℝ ⟼ A B (x))$
6		ovex	$⊢ A B (C) \in V$
7	4 5 6	fvmpt	$⊢ C \in ℝ \to (x \in ℝ ⟼ A B (x)) (C) = A B (C)$
8	2 7	sylan9eq	$⊢ ((A \in E \land B \in D) \land C \in ℝ) \to (A \cdot_{v} B) (C) = A B (C)$
9	8	3impa	$⊢ (A \in E \land B \in D \land C \in ℝ) \to (A \cdot_{v} B) (C) = A B (C)$

Metamath Proof Explorer