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