Metamath Proof Explorer

Theorem subrfv

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

Ref Expression
Assertion subrfv ⊢ A ∈ E ∧ B ∈ D ∧ C ∈ ℝ → A - r B ⁡ C = A ⁡ C − B ⁡ C

Proof

Step Hyp Ref Expression
1 subrval ⊢ A ∈ E ∧ B ∈ D → A - r B = x ∈ ℝ ⟼ A ⁡ x − B ⁡ x
2 1 fveq1d ⊢ A ∈ E ∧ B ∈ D → A - r B ⁡ C = x ∈ ℝ ⟼ A ⁡ x − B ⁡ x ⁡ C
3 fveq2 ⊢ x = C → A ⁡ x = A ⁡ C
4 fveq2 ⊢ x = C → B ⁡ x = B ⁡ C
5 3 4 oveq12d ⊢ x = C → A ⁡ x − B ⁡ x = A ⁡ C − B ⁡ C
6 eqid ⊢ x ∈ ℝ ⟼ A ⁡ x − B ⁡ x = x ∈ ℝ ⟼ A ⁡ x − B ⁡ x
7 ovex ⊢ A ⁡ C − B ⁡ C ∈ V
8 5 6 7 fvmpt ⊢ C ∈ ℝ → x ∈ ℝ ⟼ A ⁡ x − B ⁡ x ⁡ C = A ⁡ C − B ⁡ C
9 2 8 sylan9eq ⊢ A ∈ E ∧ B ∈ D ∧ C ∈ ℝ → A - r B ⁡ C = A ⁡ C − B ⁡ C
10 9 3impa ⊢ A ∈ E ∧ B ∈ D ∧ C ∈ ℝ → A - r B ⁡ C = A ⁡ C − B ⁡ C