Metamath Proof Explorer

Theorem addrcom

Description: Vector addition is commutative. (Contributed by Andrew Salmon, 28-Jan-2012)

Ref Expression
Assertion addrcom ⊢ A ∈ C ∧ B ∈ D → A + r B = B + r A

Proof

Step Hyp Ref Expression
1 addrfn ⊢ A ∈ C ∧ B ∈ D → A + r B Fn ℝ
2 addrfn ⊢ B ∈ D ∧ A ∈ C → B + r A Fn ℝ
3 2 ancoms ⊢ A ∈ C ∧ B ∈ D → B + r A Fn ℝ
4 addcomgi ⊢ A ⁡ x + B ⁡ x = B ⁡ x + A ⁡ x
5 addrfv ⊢ A ∈ C ∧ B ∈ D ∧ x ∈ ℝ → A + r B ⁡ x = A ⁡ x + B ⁡ x
6 addrfv ⊢ B ∈ D ∧ A ∈ C ∧ x ∈ ℝ → B + r A ⁡ x = B ⁡ x + A ⁡ x
7 6 3com12 ⊢ A ∈ C ∧ B ∈ D ∧ x ∈ ℝ → B + r A ⁡ x = B ⁡ x + A ⁡ x
8 4 5 7 3eqtr4a ⊢ A ∈ C ∧ B ∈ D ∧ x ∈ ℝ → A + r B ⁡ x = B + r A ⁡ x
9 8 3expia ⊢ A ∈ C ∧ B ∈ D → x ∈ ℝ → A + r B ⁡ x = B + r A ⁡ x
10 9 ralrimiv ⊢ A ∈ C ∧ B ∈ D → ∀ x ∈ ℝ A + r B ⁡ x = B + r A ⁡ x
11 eqfnfv ⊢ A + r B Fn ℝ ∧ B + r A Fn ℝ → A + r B = B + r A ↔ ∀ x ∈ ℝ A + r B ⁡ x = B + r A ⁡ x
12 10 11 syl5ibrcom ⊢ A ∈ C ∧ B ∈ D → A + r B Fn ℝ ∧ B + r A Fn ℝ → A + r B = B + r A
13 1 3 12 mp2and ⊢ A ∈ C ∧ B ∈ D → A + r B = B + r A