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