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