Metamath Proof Explorer

Theorem hvsubcan

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

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

Proof

Step Hyp Ref Expression
1 hvsubval ⊢ A ∈ ℋ ∧ B ∈ ℋ → A - ℎ B = A + ℎ -1 ⋅ ℎ B
2 1 3adant3 ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ → A - ℎ B = A + ℎ -1 ⋅ ℎ B
3 hvsubval ⊢ A ∈ ℋ ∧ C ∈ ℋ → A - ℎ C = A + ℎ -1 ⋅ ℎ C
4 3 3adant2 ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ → A - ℎ C = A + ℎ -1 ⋅ ℎ C
5 2 4 eqeq12d ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ → A - ℎ B = A - ℎ C ↔ A + ℎ -1 ⋅ ℎ B = A + ℎ -1 ⋅ ℎ C
6 neg1cn ⊢ − 1 ∈ ℂ
7 hvmulcl ⊢ − 1 ∈ ℂ ∧ B ∈ ℋ → -1 ⋅ ℎ B ∈ ℋ
8 6 7 mpan ⊢ B ∈ ℋ → -1 ⋅ ℎ B ∈ ℋ
9 hvmulcl ⊢ − 1 ∈ ℂ ∧ C ∈ ℋ → -1 ⋅ ℎ C ∈ ℋ
10 6 9 mpan ⊢ C ∈ ℋ → -1 ⋅ ℎ C ∈ ℋ
11 hvaddcan ⊢ A ∈ ℋ ∧ -1 ⋅ ℎ B ∈ ℋ ∧ -1 ⋅ ℎ C ∈ ℋ → A + ℎ -1 ⋅ ℎ B = A + ℎ -1 ⋅ ℎ C ↔ -1 ⋅ ℎ B = -1 ⋅ ℎ C
12 10 11 syl3an3 ⊢ A ∈ ℋ ∧ -1 ⋅ ℎ B ∈ ℋ ∧ C ∈ ℋ → A + ℎ -1 ⋅ ℎ B = A + ℎ -1 ⋅ ℎ C ↔ -1 ⋅ ℎ B = -1 ⋅ ℎ C
13 8 12 syl3an2 ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ → A + ℎ -1 ⋅ ℎ B = A + ℎ -1 ⋅ ℎ C ↔ -1 ⋅ ℎ B = -1 ⋅ ℎ C
14 neg1ne0 ⊢ − 1 ≠ 0
15 6 14 pm3.2i ⊢ − 1 ∈ ℂ ∧ − 1 ≠ 0
16 hvmulcan ⊢ − 1 ∈ ℂ ∧ − 1 ≠ 0 ∧ B ∈ ℋ ∧ C ∈ ℋ → -1 ⋅ ℎ B = -1 ⋅ ℎ C ↔ B = C
17 15 16 mp3an1 ⊢ B ∈ ℋ ∧ C ∈ ℋ → -1 ⋅ ℎ B = -1 ⋅ ℎ C ↔ B = C
18 17 3adant1 ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ → -1 ⋅ ℎ B = -1 ⋅ ℎ C ↔ B = C
19 5 13 18 3bitrd ⊢ A ∈ ℋ ∧ B ∈ ℋ ∧ C ∈ ℋ → A - ℎ B = A - ℎ C ↔ B = C