Metamath Proof Explorer

Theorem hvaddsub12

Description: Commutative/associative law. (Contributed by NM, 19-Oct-1999) (New usage is discouraged.)

Ref Expression
Assertion hvaddsub12 ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ → A + ℎ B - ℎ C = B + ℎ A - ℎ C

Proof

Step Hyp Ref Expression
1 neg1cn ⊢ − 1 ∈ ℂ
2 hvmulcl ⊢ − 1 ∈ ℂ ∧ C ∈ ℋ → -1 ⋅ ℎ C ∈ ℋ
3 1 2 mpan ⊢ C ∈ ℋ → -1 ⋅ ℎ C ∈ ℋ
4 hvadd12 ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ -1 ⋅ ℎ C ∈ ℋ → A + ℎ B + ℎ -1 ⋅ ℎ C = B + ℎ A + ℎ -1 ⋅ ℎ C
5 3 4 syl3an3 ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ → A + ℎ B + ℎ -1 ⋅ ℎ C = B + ℎ A + ℎ -1 ⋅ ℎ C
6 hvsubval ⊢ B ∈ ℋ ∧ C ∈ ℋ → B - ℎ C = B + ℎ -1 ⋅ ℎ C
7 6 oveq2d ⊢ B ∈ ℋ ∧ C ∈ ℋ → A + ℎ B - ℎ C = A + ℎ B + ℎ -1 ⋅ ℎ C
8 7 3adant1 ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ → A + ℎ B - ℎ C = A + ℎ B + ℎ -1 ⋅ ℎ C
9 hvsubval ⊢ A ∈ ℋ ∧ C ∈ ℋ → A - ℎ C = A + ℎ -1 ⋅ ℎ C
10 9 oveq2d ⊢ A ∈ ℋ ∧ C ∈ ℋ → B + ℎ A - ℎ C = B + ℎ A + ℎ -1 ⋅ ℎ C
11 10 3adant2 ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ → B + ℎ A - ℎ C = B + ℎ A + ℎ -1 ⋅ ℎ C
12 5 8 11 3eqtr4d ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ → A + ℎ B - ℎ C = B + ℎ A - ℎ C