Metamath Proof Explorer

Theorem hvmulcan

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

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

Proof

Step Hyp Ref Expression
1 df-ne ⊢ A ≠ 0 ↔ ¬ A = 0
2 biorf ⊢ ¬ A = 0 → B - ℎ C = 0 ℎ ↔ A = 0 ∨ B - ℎ C = 0 ℎ
3 1 2 sylbi ⊢ A ≠ 0 → B - ℎ C = 0 ℎ ↔ A = 0 ∨ B - ℎ C = 0 ℎ
4 3 ad2antlr ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ B ∈ ℋ → B - ℎ C = 0 ℎ ↔ A = 0 ∨ B - ℎ C = 0 ℎ
5 4 3adant3 ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ B ∈ ℋ ∧ C ∈ ℋ → B - ℎ C = 0 ℎ ↔ A = 0 ∨ B - ℎ C = 0 ℎ
6 hvsubeq0 ⊢ B ∈ ℋ ∧ C ∈ ℋ → B - ℎ C = 0 ℎ ↔ B = C
7 6 3adant1 ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ B ∈ ℋ ∧ C ∈ ℋ → B - ℎ C = 0 ℎ ↔ B = C
8 hvsubdistr1 ⊢ A ∈ ℂ ∧ B ∈ ℋ ∧ C ∈ ℋ → A ⋅ ℎ B - ℎ C = A ⋅ ℎ B - ℎ A ⋅ ℎ C
9 8 eqeq1d ⊢ A ∈ ℂ ∧ B ∈ ℋ ∧ C ∈ ℋ → A ⋅ ℎ B - ℎ C = 0 ℎ ↔ A ⋅ ℎ B - ℎ A ⋅ ℎ C = 0 ℎ
10 hvsubcl ⊢ B ∈ ℋ ∧ C ∈ ℋ → B - ℎ C ∈ ℋ
11 hvmul0or ⊢ A ∈ ℂ ∧ B - ℎ C ∈ ℋ → A ⋅ ℎ B - ℎ C = 0 ℎ ↔ A = 0 ∨ B - ℎ C = 0 ℎ
12 10 11 sylan2 ⊢ A ∈ ℂ ∧ B ∈ ℋ ∧ C ∈ ℋ → A ⋅ ℎ B - ℎ C = 0 ℎ ↔ A = 0 ∨ B - ℎ C = 0 ℎ
13 12 3impb ⊢ A ∈ ℂ ∧ B ∈ ℋ ∧ C ∈ ℋ → A ⋅ ℎ B - ℎ C = 0 ℎ ↔ A = 0 ∨ B - ℎ C = 0 ℎ
14 hvmulcl ⊢ A ∈ ℂ ∧ B ∈ ℋ → A ⋅ ℎ B ∈ ℋ
15 14 3adant3 ⊢ A ∈ ℂ ∧ B ∈ ℋ ∧ C ∈ ℋ → A ⋅ ℎ B ∈ ℋ
16 hvmulcl ⊢ A ∈ ℂ ∧ C ∈ ℋ → A ⋅ ℎ C ∈ ℋ
17 16 3adant2 ⊢ A ∈ ℂ ∧ B ∈ ℋ ∧ C ∈ ℋ → A ⋅ ℎ C ∈ ℋ
18 hvsubeq0 ⊢ A ⋅ ℎ B ∈ ℋ ∧ A ⋅ ℎ C ∈ ℋ → A ⋅ ℎ B - ℎ A ⋅ ℎ C = 0 ℎ ↔ A ⋅ ℎ B = A ⋅ ℎ C
19 15 17 18 syl2anc ⊢ A ∈ ℂ ∧ B ∈ ℋ ∧ C ∈ ℋ → A ⋅ ℎ B - ℎ A ⋅ ℎ C = 0 ℎ ↔ A ⋅ ℎ B = A ⋅ ℎ C
20 9 13 19 3bitr3d ⊢ A ∈ ℂ ∧ B ∈ ℋ ∧ C ∈ ℋ → A = 0 ∨ B - ℎ C = 0 ℎ ↔ A ⋅ ℎ B = A ⋅ ℎ C
21 20 3adant1r ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ B ∈ ℋ ∧ C ∈ ℋ → A = 0 ∨ B - ℎ C = 0 ℎ ↔ A ⋅ ℎ B = A ⋅ ℎ C
22 5 7 21 3bitr3rd ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ B ∈ ℋ ∧ C ∈ ℋ → A ⋅ ℎ B = A ⋅ ℎ C ↔ B = C