Metamath Proof Explorer

Theorem hvaddcan2

Description: Cancellation law for vector addition. (Contributed by NM, 18-May-2005) (New usage is discouraged.)

Ref Expression
Assertion hvaddcan2 ⊢A∈ℋ∧B∈ℋ∧C∈ℋ→A+ℎC=B+ℎC↔A=B

Proof

Step Hyp Ref Expression
1 ax-hvcom ⊢C∈ℋ∧A∈ℋ→C+ℎA=A+ℎC
2 1 3adant3 ⊢C∈ℋ∧A∈ℋ∧B∈ℋ→C+ℎA=A+ℎC
3 ax-hvcom ⊢C∈ℋ∧B∈ℋ→C+ℎB=B+ℎC
4 3 3adant2 ⊢C∈ℋ∧A∈ℋ∧B∈ℋ→C+ℎB=B+ℎC
5 2 4 eqeq12d ⊢C∈ℋ∧A∈ℋ∧B∈ℋ→C+ℎA=C+ℎB↔A+ℎC=B+ℎC
6 hvaddcan ⊢C∈ℋ∧A∈ℋ∧B∈ℋ→C+ℎA=C+ℎB↔A=B
7 5 6 bitr3d ⊢C∈ℋ∧A∈ℋ∧B∈ℋ→A+ℎC=B+ℎC↔A=B
8 7 3coml ⊢A∈ℋ∧B∈ℋ∧C∈ℋ→A+ℎC=B+ℎC↔A=B