Metamath Proof Explorer

Theorem addrfv

Description: Vector addition at a value. The operation takes each vector A and B and forms a new vector whose values are the sum of each of the values of A and B . (Contributed by Andrew Salmon, 27-Jan-2012)

Ref Expression
Assertion addrfv ⊢ A ∈ E ∧ B ∈ D ∧ C ∈ ℝ → A + r B ⁡ C = A ⁡ C + B ⁡ C

Proof

Step Hyp Ref Expression
1 addrval ⊢ 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