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

Proof

Step Hyp Ref Expression
1 df-ne 
 |-  ( A =/= 0 <-> -. A = 0 )
2 biorf 
 |-  ( -. A = 0 -> ( ( B -h C ) = 0h <-> ( A = 0 \/ ( B -h C ) = 0h ) ) )
3 1 2 sylbi 
 |-  ( A =/= 0 -> ( ( B -h C ) = 0h <-> ( A = 0 \/ ( B -h C ) = 0h ) ) )
4 3 ad2antlr 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ B e. ~H ) -> ( ( B -h C ) = 0h <-> ( A = 0 \/ ( B -h C ) = 0h ) ) )
5 4 3adant3 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ B e. ~H /\ C e. ~H ) -> ( ( B -h C ) = 0h <-> ( A = 0 \/ ( B -h C ) = 0h ) ) )
6 hvsubeq0 
 |-  ( ( B e. ~H /\ C e. ~H ) -> ( ( B -h C ) = 0h <-> B = C ) )
7 6 3adant1 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ B e. ~H /\ C e. ~H ) -> ( ( B -h C ) = 0h <-> B = C ) )
8 hvsubdistr1 
 |-  ( ( A e. CC /\ B e. ~H /\ C e. ~H ) -> ( A .h ( B -h C ) ) = ( ( A .h B ) -h ( A .h C ) ) )
9 8 eqeq1d 
 |-  ( ( A e. CC /\ B e. ~H /\ C e. ~H ) -> ( ( A .h ( B -h C ) ) = 0h <-> ( ( A .h B ) -h ( A .h C ) ) = 0h ) )
10 hvsubcl 
 |-  ( ( B e. ~H /\ C e. ~H ) -> ( B -h C ) e. ~H )
11 hvmul0or 
 |-  ( ( A e. CC /\ ( B -h C ) e. ~H ) -> ( ( A .h ( B -h C ) ) = 0h <-> ( A = 0 \/ ( B -h C ) = 0h ) ) )
12 10 11 sylan2 
 |-  ( ( A e. CC /\ ( B e. ~H /\ C e. ~H ) ) -> ( ( A .h ( B -h C ) ) = 0h <-> ( A = 0 \/ ( B -h C ) = 0h ) ) )
13 12 3impb 
 |-  ( ( A e. CC /\ B e. ~H /\ C e. ~H ) -> ( ( A .h ( B -h C ) ) = 0h <-> ( A = 0 \/ ( B -h C ) = 0h ) ) )
14 hvmulcl 
 |-  ( ( A e. CC /\ B e. ~H ) -> ( A .h B ) e. ~H )
15 14 3adant3 
 |-  ( ( A e. CC /\ B e. ~H /\ C e. ~H ) -> ( A .h B ) e. ~H )
16 hvmulcl 
 |-  ( ( A e. CC /\ C e. ~H ) -> ( A .h C ) e. ~H )
17 16 3adant2 
 |-  ( ( A e. CC /\ B e. ~H /\ C e. ~H ) -> ( A .h C ) e. ~H )
18 hvsubeq0 
 |-  ( ( ( A .h B ) e. ~H /\ ( A .h C ) e. ~H ) -> ( ( ( A .h B ) -h ( A .h C ) ) = 0h <-> ( A .h B ) = ( A .h C ) ) )
19 15 17 18 syl2anc 
 |-  ( ( A e. CC /\ B e. ~H /\ C e. ~H ) -> ( ( ( A .h B ) -h ( A .h C ) ) = 0h <-> ( A .h B ) = ( A .h C ) ) )
20 9 13 19 3bitr3d 
 |-  ( ( A e. CC /\ B e. ~H /\ C e. ~H ) -> ( ( A = 0 \/ ( B -h C ) = 0h ) <-> ( A .h B ) = ( A .h C ) ) )
21 20 3adant1r 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ B e. ~H /\ C e. ~H ) -> ( ( A = 0 \/ ( B -h C ) = 0h ) <-> ( A .h B ) = ( A .h C ) ) )
22 5 7 21 3bitr3rd 
 |-  ( ( ( A e. CC /\ A =/= 0 ) /\ B e. ~H /\ C e. ~H ) -> ( ( A .h B ) = ( A .h C ) <-> B = C ) )