Metamath Proof Explorer

Theorem nvmul0or

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

Ref Expression
Hypotheses nvmul0or.1 
|- X = ( BaseSet ` U )
nvmul0or.4 
|- S = ( .sOLD ` U )
nvmul0or.6 
|- Z = ( 0vec ` U )
Assertion nvmul0or 
|- ( ( U e. NrmCVec /\ A e. CC /\ B e. X ) -> ( ( A S B ) = Z <-> ( A = 0 \/ B = Z ) ) )

Proof

Step Hyp Ref Expression
1 nvmul0or.1 
 |-  X = ( BaseSet ` U )
2 nvmul0or.4 
 |-  S = ( .sOLD ` U )
3 nvmul0or.6 
 |-  Z = ( 0vec ` U )
4 df-ne 
 |-  ( A =/= 0 <-> -. A = 0 )
5 oveq2 
 |-  ( ( A S B ) = Z -> ( ( 1 / A ) S ( A S B ) ) = ( ( 1 / A ) S Z ) )
6 5 ad2antlr 
 |-  ( ( ( ( U e. NrmCVec /\ A e. CC /\ B e. X ) /\ ( A S B ) = Z ) /\ A =/= 0 ) -> ( ( 1 / A ) S ( A S B ) ) = ( ( 1 / A ) S Z ) )
7 recid2 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( ( 1 / A ) x. A ) = 1 )
8 7 oveq1d 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( ( ( 1 / A ) x. A ) S B ) = ( 1 S B ) )
9 8 3ad2antl2 
 |-  ( ( ( U e. NrmCVec /\ A e. CC /\ B e. X ) /\ A =/= 0 ) -> ( ( ( 1 / A ) x. A ) S B ) = ( 1 S B ) )
10 simpl1 
 |-  ( ( ( U e. NrmCVec /\ A e. CC /\ B e. X ) /\ A =/= 0 ) -> U e. NrmCVec )
11 reccl 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( 1 / A ) e. CC )
12 11 3ad2antl2 
 |-  ( ( ( U e. NrmCVec /\ A e. CC /\ B e. X ) /\ A =/= 0 ) -> ( 1 / A ) e. CC )
13 simpl2 
 |-  ( ( ( U e. NrmCVec /\ A e. CC /\ B e. X ) /\ A =/= 0 ) -> A e. CC )
14 simpl3 
 |-  ( ( ( U e. NrmCVec /\ A e. CC /\ B e. X ) /\ A =/= 0 ) -> B e. X )
15 1 2 nvsass 
 |-  ( ( U e. NrmCVec /\ ( ( 1 / A ) e. CC /\ A e. CC /\ B e. X ) ) -> ( ( ( 1 / A ) x. A ) S B ) = ( ( 1 / A ) S ( A S B ) ) )
16 10 12 13 14 15 syl13anc 
 |-  ( ( ( U e. NrmCVec /\ A e. CC /\ B e. X ) /\ A =/= 0 ) -> ( ( ( 1 / A ) x. A ) S B ) = ( ( 1 / A ) S ( A S B ) ) )
17 1 2 nvsid 
 |-  ( ( U e. NrmCVec /\ B e. X ) -> ( 1 S B ) = B )
18 17 3adant2 
 |-  ( ( U e. NrmCVec /\ A e. CC /\ B e. X ) -> ( 1 S B ) = B )
19 18 adantr 
 |-  ( ( ( U e. NrmCVec /\ A e. CC /\ B e. X ) /\ A =/= 0 ) -> ( 1 S B ) = B )
20 9 16 19 3eqtr3d 
 |-  ( ( ( U e. NrmCVec /\ A e. CC /\ B e. X ) /\ A =/= 0 ) -> ( ( 1 / A ) S ( A S B ) ) = B )
21 20 adantlr 
 |-  ( ( ( ( U e. NrmCVec /\ A e. CC /\ B e. X ) /\ ( A S B ) = Z ) /\ A =/= 0 ) -> ( ( 1 / A ) S ( A S B ) ) = B )
22 2 3 nvsz 
 |-  ( ( U e. NrmCVec /\ ( 1 / A ) e. CC ) -> ( ( 1 / A ) S Z ) = Z )
23 11 22 sylan2 
 |-  ( ( U e. NrmCVec /\ ( A e. CC /\ A =/= 0 ) ) -> ( ( 1 / A ) S Z ) = Z )
24 23 anassrs 
 |-  ( ( ( U e. NrmCVec /\ A e. CC ) /\ A =/= 0 ) -> ( ( 1 / A ) S Z ) = Z )
25 24 3adantl3 
 |-  ( ( ( U e. NrmCVec /\ A e. CC /\ B e. X ) /\ A =/= 0 ) -> ( ( 1 / A ) S Z ) = Z )
26 25 adantlr 
 |-  ( ( ( ( U e. NrmCVec /\ A e. CC /\ B e. X ) /\ ( A S B ) = Z ) /\ A =/= 0 ) -> ( ( 1 / A ) S Z ) = Z )
27 6 21 26 3eqtr3d 
 |-  ( ( ( ( U e. NrmCVec /\ A e. CC /\ B e. X ) /\ ( A S B ) = Z ) /\ A =/= 0 ) -> B = Z )
28 27 ex 
 |-  ( ( ( U e. NrmCVec /\ A e. CC /\ B e. X ) /\ ( A S B ) = Z ) -> ( A =/= 0 -> B = Z ) )
29 4 28 syl5bir 
 |-  ( ( ( U e. NrmCVec /\ A e. CC /\ B e. X ) /\ ( A S B ) = Z ) -> ( -. A = 0 -> B = Z ) )
30 29 orrd 
 |-  ( ( ( U e. NrmCVec /\ A e. CC /\ B e. X ) /\ ( A S B ) = Z ) -> ( A = 0 \/ B = Z ) )
31 30 ex 
 |-  ( ( U e. NrmCVec /\ A e. CC /\ B e. X ) -> ( ( A S B ) = Z -> ( A = 0 \/ B = Z ) ) )
32 1 2 3 nv0 
 |-  ( ( U e. NrmCVec /\ B e. X ) -> ( 0 S B ) = Z )
33 oveq1 
 |-  ( A = 0 -> ( A S B ) = ( 0 S B ) )
34 33 eqeq1d 
 |-  ( A = 0 -> ( ( A S B ) = Z <-> ( 0 S B ) = Z ) )
35 32 34 syl5ibrcom 
 |-  ( ( U e. NrmCVec /\ B e. X ) -> ( A = 0 -> ( A S B ) = Z ) )
36 35 3adant2 
 |-  ( ( U e. NrmCVec /\ A e. CC /\ B e. X ) -> ( A = 0 -> ( A S B ) = Z ) )
37 2 3 nvsz 
 |-  ( ( U e. NrmCVec /\ A e. CC ) -> ( A S Z ) = Z )
38 oveq2 
 |-  ( B = Z -> ( A S B ) = ( A S Z ) )
39 38 eqeq1d 
 |-  ( B = Z -> ( ( A S B ) = Z <-> ( A S Z ) = Z ) )
40 37 39 syl5ibrcom 
 |-  ( ( U e. NrmCVec /\ A e. CC ) -> ( B = Z -> ( A S B ) = Z ) )
41 40 3adant3 
 |-  ( ( U e. NrmCVec /\ A e. CC /\ B e. X ) -> ( B = Z -> ( A S B ) = Z ) )
42 36 41 jaod 
 |-  ( ( U e. NrmCVec /\ A e. CC /\ B e. X ) -> ( ( A = 0 \/ B = Z ) -> ( A S B ) = Z ) )
43 31 42 impbid 
 |-  ( ( U e. NrmCVec /\ A e. CC /\ B e. X ) -> ( ( A S B ) = Z <-> ( A = 0 \/ B = Z ) ) )