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

Metamath Proof Explorer

Theorem hvmul0or

Description: If a scalar product is zero, one of its factors must be zero. (Contributed by NM, 19-May-2005) (New usage is discouraged.)

Ref Expression
Assertion hvmul0or 
|- ( ( A e. CC /\ B e. ~H ) -> ( ( A .h B ) = 0h <-> ( A = 0 \/ B = 0h ) ) )

Proof

Step Hyp Ref Expression
1 df-ne 
 |-  ( A =/= 0 <-> -. A = 0 )
2 oveq2 
 |-  ( ( A .h B ) = 0h -> ( ( 1 / A ) .h ( A .h B ) ) = ( ( 1 / A ) .h 0h ) )
3 2 ad2antlr 
 |-  ( ( ( ( A e. CC /\ B e. ~H ) /\ ( A .h B ) = 0h ) /\ A =/= 0 ) -> ( ( 1 / A ) .h ( A .h B ) ) = ( ( 1 / A ) .h 0h ) )
4 recid2 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( ( 1 / A ) x. A ) = 1 )
5 4 oveq1d 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( ( ( 1 / A ) x. A ) .h B ) = ( 1 .h B ) )
6 5 adantlr 
 |-  ( ( ( A e. CC /\ B e. ~H ) /\ A =/= 0 ) -> ( ( ( 1 / A ) x. A ) .h B ) = ( 1 .h B ) )
7 reccl 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( 1 / A ) e. CC )
8 7 adantlr 
 |-  ( ( ( A e. CC /\ B e. ~H ) /\ A =/= 0 ) -> ( 1 / A ) e. CC )
9 simpll 
 |-  ( ( ( A e. CC /\ B e. ~H ) /\ A =/= 0 ) -> A e. CC )
10 simplr 
 |-  ( ( ( A e. CC /\ B e. ~H ) /\ A =/= 0 ) -> B e. ~H )
11 ax-hvmulass 
 |-  ( ( ( 1 / A ) e. CC /\ A e. CC /\ B e. ~H ) -> ( ( ( 1 / A ) x. A ) .h B ) = ( ( 1 / A ) .h ( A .h B ) ) )
12 8 9 10 11 syl3anc 
 |-  ( ( ( A e. CC /\ B e. ~H ) /\ A =/= 0 ) -> ( ( ( 1 / A ) x. A ) .h B ) = ( ( 1 / A ) .h ( A .h B ) ) )
13 ax-hvmulid 
 |-  ( B e. ~H -> ( 1 .h B ) = B )
14 13 ad2antlr 
 |-  ( ( ( A e. CC /\ B e. ~H ) /\ A =/= 0 ) -> ( 1 .h B ) = B )
15 6 12 14 3eqtr3d 
 |-  ( ( ( A e. CC /\ B e. ~H ) /\ A =/= 0 ) -> ( ( 1 / A ) .h ( A .h B ) ) = B )
16 15 adantlr 
 |-  ( ( ( ( A e. CC /\ B e. ~H ) /\ ( A .h B ) = 0h ) /\ A =/= 0 ) -> ( ( 1 / A ) .h ( A .h B ) ) = B )
17 hvmul0 
 |-  ( ( 1 / A ) e. CC -> ( ( 1 / A ) .h 0h ) = 0h )
18 7 17 syl 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( ( 1 / A ) .h 0h ) = 0h )
19 18 adantlr 
 |-  ( ( ( A e. CC /\ B e. ~H ) /\ A =/= 0 ) -> ( ( 1 / A ) .h 0h ) = 0h )
20 19 adantlr 
 |-  ( ( ( ( A e. CC /\ B e. ~H ) /\ ( A .h B ) = 0h ) /\ A =/= 0 ) -> ( ( 1 / A ) .h 0h ) = 0h )
21 3 16 20 3eqtr3d 
 |-  ( ( ( ( A e. CC /\ B e. ~H ) /\ ( A .h B ) = 0h ) /\ A =/= 0 ) -> B = 0h )
22 21 ex 
 |-  ( ( ( A e. CC /\ B e. ~H ) /\ ( A .h B ) = 0h ) -> ( A =/= 0 -> B = 0h ) )
23 1 22 biimtrrid 
 |-  ( ( ( A e. CC /\ B e. ~H ) /\ ( A .h B ) = 0h ) -> ( -. A = 0 -> B = 0h ) )
24 23 orrd 
 |-  ( ( ( A e. CC /\ B e. ~H ) /\ ( A .h B ) = 0h ) -> ( A = 0 \/ B = 0h ) )
25 24 ex 
 |-  ( ( A e. CC /\ B e. ~H ) -> ( ( A .h B ) = 0h -> ( A = 0 \/ B = 0h ) ) )
26 ax-hvmul0 
 |-  ( B e. ~H -> ( 0 .h B ) = 0h )
27 oveq1 
 |-  ( A = 0 -> ( A .h B ) = ( 0 .h B ) )
28 27 eqeq1d 
 |-  ( A = 0 -> ( ( A .h B ) = 0h <-> ( 0 .h B ) = 0h ) )
29 26 28 syl5ibrcom 
 |-  ( B e. ~H -> ( A = 0 -> ( A .h B ) = 0h ) )
30 29 adantl 
 |-  ( ( A e. CC /\ B e. ~H ) -> ( A = 0 -> ( A .h B ) = 0h ) )
31 hvmul0 
 |-  ( A e. CC -> ( A .h 0h ) = 0h )
32 oveq2 
 |-  ( B = 0h -> ( A .h B ) = ( A .h 0h ) )
33 32 eqeq1d 
 |-  ( B = 0h -> ( ( A .h B ) = 0h <-> ( A .h 0h ) = 0h ) )
34 31 33 syl5ibrcom 
 |-  ( A e. CC -> ( B = 0h -> ( A .h B ) = 0h ) )
35 34 adantr 
 |-  ( ( A e. CC /\ B e. ~H ) -> ( B = 0h -> ( A .h B ) = 0h ) )
36 30 35 jaod 
 |-  ( ( A e. CC /\ B e. ~H ) -> ( ( A = 0 \/ B = 0h ) -> ( A .h B ) = 0h ) )
37 25 36 impbid 
 |-  ( ( A e. CC /\ B e. ~H ) -> ( ( A .h B ) = 0h <-> ( A = 0 \/ B = 0h ) ) )