Metamath Proof Explorer

Theorem subrval

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

Ref Expression
Assertion subrval ⊢ 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-subr ⊢ - 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