Metamath Proof Explorer

Theorem addrval

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

Ref Expression
Assertion addrval ⊢ A ∈ C ∧ B ∈ D → A + r B = v ∈ ℝ ⟼ A ⁡ v + B ⁡ v

Proof

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