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