mulvval

Description: Value of the operation of scalar multiplication. (Contributed by Andrew Salmon, 27-Jan-2012)

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

Step	Hyp	Ref	Expression
1		elex	$⊢ A \in C \to A \in V$
2		elex	$⊢ B \in D \to B \in V$
3		fveq1	$⊢ y = B \to y (v) = B (v)$
4		oveq12	$⊢ (x = A \land y (v) = B (v)) \to x y (v) = A B (v)$
5	3 4	sylan2	$⊢ (x = A \land y = B) \to x y (v) = A B (v)$
6	5	mpteq2dv	$⊢ (x = A \land y = B) \to (v \in ℝ ⟼ x y (v)) = (v \in ℝ ⟼ A B (v))$
7		df-mulv	$⊢ \cdot_{v} = (x \in V, y \in V ⟼ (v \in ℝ ⟼ x y (v)))$
8		reex	$⊢ ℝ \in V$
9	8	mptex	$⊢ (v \in ℝ ⟼ A B (v)) \in V$
10	6 7 9	ovmpoa	$⊢ (A \in V \land B \in V) \to A \cdot_{v} B = (v \in ℝ ⟼ A B (v))$
11	1 2 10	syl2an	$⊢ (A \in C \land B \in D) \to A \cdot_{v} B = (v \in ℝ ⟼ A B (v))$

Metamath Proof Explorer