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 e. CC /\ B e. CC /\ ( C e. ~H /\ C =/= 0h ) ) -> ( ( A .h C ) = ( B .h C ) <-> A = B ) )

Proof

Step Hyp Ref Expression
1 hvmulcl
 |-  ( ( A e. CC /\ C e. ~H ) -> ( A .h C ) e. ~H )
2 1 3adant2
 |-  ( ( A e. CC /\ B e. CC /\ C e. ~H ) -> ( A .h C ) e. ~H )
3 hvmulcl
 |-  ( ( B e. CC /\ C e. ~H ) -> ( B .h C ) e. ~H )
4 3 3adant1
 |-  ( ( A e. CC /\ B e. CC /\ C e. ~H ) -> ( B .h C ) e. ~H )
5 hvsubeq0
 |-  ( ( ( A .h C ) e. ~H /\ ( B .h C ) e. ~H ) -> ( ( ( A .h C ) -h ( B .h C ) ) = 0h <-> ( A .h C ) = ( B .h C ) ) )
6 2 4 5 syl2anc
 |-  ( ( A e. CC /\ B e. CC /\ C e. ~H ) -> ( ( ( A .h C ) -h ( B .h C ) ) = 0h <-> ( A .h C ) = ( B .h C ) ) )
7 6 3adant3r
 |-  ( ( A e. CC /\ B e. CC /\ ( C e. ~H /\ C =/= 0h ) ) -> ( ( ( A .h C ) -h ( B .h C ) ) = 0h <-> ( A .h C ) = ( B .h C ) ) )
8 hvsubdistr2
 |-  ( ( A e. CC /\ B e. CC /\ C e. ~H ) -> ( ( A - B ) .h C ) = ( ( A .h C ) -h ( B .h C ) ) )
9 8 eqeq1d
 |-  ( ( A e. CC /\ B e. CC /\ C e. ~H ) -> ( ( ( A - B ) .h C ) = 0h <-> ( ( A .h C ) -h ( B .h C ) ) = 0h ) )
10 subcl
 |-  ( ( A e. CC /\ B e. CC ) -> ( A - B ) e. CC )
11 hvmul0or
 |-  ( ( ( A - B ) e. CC /\ C e. ~H ) -> ( ( ( A - B ) .h C ) = 0h <-> ( ( A - B ) = 0 \/ C = 0h ) ) )
12 10 11 stoic3
 |-  ( ( A e. CC /\ B e. CC /\ C e. ~H ) -> ( ( ( A - B ) .h C ) = 0h <-> ( ( A - B ) = 0 \/ C = 0h ) ) )
13 9 12 bitr3d
 |-  ( ( A e. CC /\ B e. CC /\ C e. ~H ) -> ( ( ( A .h C ) -h ( B .h C ) ) = 0h <-> ( ( A - B ) = 0 \/ C = 0h ) ) )
14 13 3adant3r
 |-  ( ( A e. CC /\ B e. CC /\ ( C e. ~H /\ C =/= 0h ) ) -> ( ( ( A .h C ) -h ( B .h C ) ) = 0h <-> ( ( A - B ) = 0 \/ C = 0h ) ) )
15 df-ne
 |-  ( C =/= 0h <-> -. C = 0h )
16 biorf
 |-  ( -. C = 0h -> ( ( A - B ) = 0 <-> ( C = 0h \/ ( A - B ) = 0 ) ) )
17 orcom
 |-  ( ( C = 0h \/ ( A - B ) = 0 ) <-> ( ( A - B ) = 0 \/ C = 0h ) )
18 16 17 bitrdi
 |-  ( -. C = 0h -> ( ( A - B ) = 0 <-> ( ( A - B ) = 0 \/ C = 0h ) ) )
19 15 18 sylbi
 |-  ( C =/= 0h -> ( ( A - B ) = 0 <-> ( ( A - B ) = 0 \/ C = 0h ) ) )
20 19 ad2antll
 |-  ( ( B e. CC /\ ( C e. ~H /\ C =/= 0h ) ) -> ( ( A - B ) = 0 <-> ( ( A - B ) = 0 \/ C = 0h ) ) )
21 20 3adant1
 |-  ( ( A e. CC /\ B e. CC /\ ( C e. ~H /\ C =/= 0h ) ) -> ( ( A - B ) = 0 <-> ( ( A - B ) = 0 \/ C = 0h ) ) )
22 subeq0
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( A - B ) = 0 <-> A = B ) )
23 22 3adant3
 |-  ( ( A e. CC /\ B e. CC /\ ( C e. ~H /\ C =/= 0h ) ) -> ( ( A - B ) = 0 <-> A = B ) )
24 14 21 23 3bitr2d
 |-  ( ( A e. CC /\ B e. CC /\ ( C e. ~H /\ C =/= 0h ) ) -> ( ( ( A .h C ) -h ( B .h C ) ) = 0h <-> A = B ) )
25 7 24 bitr3d
 |-  ( ( A e. CC /\ B e. CC /\ ( C e. ~H /\ C =/= 0h ) ) -> ( ( A .h C ) = ( B .h C ) <-> A = B ) )