This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ) )