Metamath Proof Explorer

Theorem hvsubcan2

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

Ref Expression
Assertion hvsubcan2 ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ → A - ℎ C = B - ℎ C ↔ A = B

Proof

Step Hyp Ref Expression
1 hvsubcl ⊢ C ∈ ℋ ∧ A ∈ ℋ → C - ℎ A ∈ ℋ
2 1 3adant3 ⊢ C ∈ ℋ ∧ A ∈ ℋ ∧ B ∈ ℋ → C - ℎ A ∈ ℋ
3 hvsubcl ⊢ C ∈ ℋ ∧ B ∈ ℋ → C - ℎ B ∈ ℋ
4 3 3adant2 ⊢ C ∈ ℋ ∧ A ∈ ℋ ∧ B ∈ ℋ → C - ℎ B ∈ ℋ
5 neg1cn ⊢ − 1 ∈ ℂ
6 neg1ne0 ⊢ − 1 ≠ 0
7 5 6 pm3.2i ⊢ − 1 ∈ ℂ ∧ − 1 ≠ 0
8 hvmulcan ⊢ − 1 ∈ ℂ ∧ − 1 ≠ 0 ∧ C - ℎ A ∈ ℋ ∧ C - ℎ B ∈ ℋ → -1 ⋅ ℎ C - ℎ A = -1 ⋅ ℎ C - ℎ B ↔ C - ℎ A = C - ℎ B
9 7 8 mp3an1 ⊢ C - ℎ A ∈ ℋ ∧ C - ℎ B ∈ ℋ → -1 ⋅ ℎ C - ℎ A = -1 ⋅ ℎ C - ℎ B ↔ C - ℎ A = C - ℎ B
10 2 4 9 syl2anc ⊢ C ∈ ℋ ∧ A ∈ ℋ ∧ B ∈ ℋ → -1 ⋅ ℎ C - ℎ A = -1 ⋅ ℎ C - ℎ B ↔ C - ℎ A = C - ℎ B
11 hvnegdi ⊢ C ∈ ℋ ∧ A ∈ ℋ → -1 ⋅ ℎ C - ℎ A = A - ℎ C
12 11 3adant3 ⊢ C ∈ ℋ ∧ A ∈ ℋ ∧ B ∈ ℋ → -1 ⋅ ℎ C - ℎ A = A - ℎ C
13 hvnegdi ⊢ C ∈ ℋ ∧ B ∈ ℋ → -1 ⋅ ℎ C - ℎ B = B - ℎ C
14 13 3adant2 ⊢ C ∈ ℋ ∧ A ∈ ℋ ∧ B ∈ ℋ → -1 ⋅ ℎ C - ℎ B = B - ℎ C
15 12 14 eqeq12d ⊢ C ∈ ℋ ∧ A ∈ ℋ ∧ B ∈ ℋ → -1 ⋅ ℎ C - ℎ A = -1 ⋅ ℎ C - ℎ B ↔ A - ℎ C = B - ℎ C
16 hvsubcan ⊢ C ∈ ℋ ∧ A ∈ ℋ ∧ B ∈ ℋ → C - ℎ A = C - ℎ B ↔ A = B
17 10 15 16 3bitr3d ⊢ C ∈ ℋ ∧ A ∈ ℋ ∧ B ∈ ℋ → A - ℎ C = B - ℎ C ↔ A = B
18 17 3coml ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ → A - ℎ C = B - ℎ C ↔ A = B