Metamath Proof Explorer

Theorem mulvval

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

Ref Expression
Assertion mulvval ⊢ A ∈ C ∧ B ∈ D → A ⋅ v B = v ∈ ℝ ⟼ A ⁢ B ⁡ v

Proof

Step Hyp Ref Expression
1 elex ⊢ A ∈ C → A ∈ V
2 elex ⊢ B ∈ D → B ∈ V
3 fveq1 ⊢ y = B → y ⁡ v = B ⁡ v
4 oveq12 ⊢ x = A ∧ y ⁡ v = B ⁡ v → x ⁢ y ⁡ v = A ⁢ B ⁡ v
5 3 4 sylan2 ⊢ x = A ∧ y = B → x ⁢ y ⁡ v = A ⁢ B ⁡ v
6 5 mpteq2dv ⊢ x = A ∧ y = B → v ∈ ℝ ⟼ x ⁢ y ⁡ v = v ∈ ℝ ⟼ A ⁢ B ⁡ v
7 df-mulv ⊢ ⋅ v = x ∈ V , y ∈ V ⟼ v ∈ ℝ ⟼ x ⁢ y ⁡ v
8 reex ⊢ ℝ ∈ V
9 8 mptex ⊢ v ∈ ℝ ⟼ A ⁢ B ⁡ v ∈ V
10 6 7 9 ovmpoa ⊢ A ∈ V ∧ B ∈ V → A ⋅ v B = v ∈ ℝ ⟼ A ⁢ B ⁡ v
11 1 2 10 syl2an ⊢ A ∈ C ∧ B ∈ D → A ⋅ v B = v ∈ ℝ ⟼ A ⁢ B ⁡ v