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