Metamath Proof Explorer

Theorem hvmulcan2

Description: Cancellation law for scalar multiplication. (Contributed by NM, 19-May-2005) (New usage is discouraged.)

Ref Expression
Assertion hvmulcan2 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℋ ∧ C ≠ 0 ℎ → A ⋅ ℎ C = B ⋅ ℎ C ↔ A = B

Proof

Step Hyp Ref Expression
1 hvmulcl ⊢ A ∈ ℂ ∧ C ∈ ℋ → A ⋅ ℎ C ∈ ℋ
2 1 3adant2 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℋ → A ⋅ ℎ C ∈ ℋ
3 hvmulcl ⊢ B ∈ ℂ ∧ C ∈ ℋ → B ⋅ ℎ C ∈ ℋ
4 3 3adant1 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℋ → B ⋅ ℎ C ∈ ℋ
5 hvsubeq0 ⊢ A ⋅ ℎ C ∈ ℋ ∧ B ⋅ ℎ C ∈ ℋ → A ⋅ ℎ C - ℎ B ⋅ ℎ C = 0 ℎ ↔ A ⋅ ℎ C = B ⋅ ℎ C
6 2 4 5 syl2anc ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℋ → A ⋅ ℎ C - ℎ B ⋅ ℎ C = 0 ℎ ↔ A ⋅ ℎ C = B ⋅ ℎ C
7 6 3adant3r ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℋ ∧ C ≠ 0 ℎ → A ⋅ ℎ C - ℎ B ⋅ ℎ C = 0 ℎ ↔ A ⋅ ℎ C = B ⋅ ℎ C
8 hvsubdistr2 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℋ → A − B ⋅ ℎ C = A ⋅ ℎ C - ℎ B ⋅ ℎ C
9 8 eqeq1d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℋ → A − B ⋅ ℎ C = 0 ℎ ↔ A ⋅ ℎ C - ℎ B ⋅ ℎ C = 0 ℎ
10 subcl ⊢ A ∈ ℂ ∧ B ∈ ℂ → A − B ∈ ℂ
11 hvmul0or ⊢ A − B ∈ ℂ ∧ C ∈ ℋ → A − B ⋅ ℎ C = 0 ℎ ↔ A − B = 0 ∨ C = 0 ℎ
12 10 11 stoic3 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℋ → A − B ⋅ ℎ C = 0 ℎ ↔ A − B = 0 ∨ C = 0 ℎ
13 9 12 bitr3d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℋ → A ⋅ ℎ C - ℎ B ⋅ ℎ C = 0 ℎ ↔ A − B = 0 ∨ C = 0 ℎ
14 13 3adant3r ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℋ ∧ C ≠ 0 ℎ → A ⋅ ℎ C - ℎ B ⋅ ℎ C = 0 ℎ ↔ A − B = 0 ∨ C = 0 ℎ
15 df-ne ⊢ C ≠ 0 ℎ ↔ ¬ C = 0 ℎ
16 biorf ⊢ ¬ C = 0 ℎ → A − B = 0 ↔ C = 0 ℎ ∨ A − B = 0
17 orcom ⊢ C = 0 ℎ ∨ A − B = 0 ↔ A − B = 0 ∨ C = 0 ℎ
18 16 17 bitrdi ⊢ ¬ C = 0 ℎ → A − B = 0 ↔ A − B = 0 ∨ C = 0 ℎ
19 15 18 sylbi ⊢ C ≠ 0 ℎ → A − B = 0 ↔ A − B = 0 ∨ C = 0 ℎ
20 19 ad2antll ⊢ B ∈ ℂ ∧ C ∈ ℋ ∧ C ≠ 0 ℎ → A − B = 0 ↔ A − B = 0 ∨ C = 0 ℎ
21 20 3adant1 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℋ ∧ C ≠ 0 ℎ → A − B = 0 ↔ A − B = 0 ∨ C = 0 ℎ
22 subeq0 ⊢ A ∈ ℂ ∧ B ∈ ℂ → A − B = 0 ↔ A = B
23 22 3adant3 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℋ ∧ C ≠ 0 ℎ → A − B = 0 ↔ A = B
24 14 21 23 3bitr2d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℋ ∧ C ≠ 0 ℎ → A ⋅ ℎ C - ℎ B ⋅ ℎ C = 0 ℎ ↔ A = B
25 7 24 bitr3d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℋ ∧ C ≠ 0 ℎ → A ⋅ ℎ C = B ⋅ ℎ C ↔ A = B