Metamath Proof Explorer

Theorem nlmmul0or

Description: If a scalar product is zero, one of its factors must be zero. (Contributed by NM, 6-Dec-2007) (Revised by Mario Carneiro, 4-Oct-2015)

Ref Expression
Hypotheses nlmmul0or.v 
|- V = ( Base ` W )
nlmmul0or.s 
|- .x. = ( .s ` W )
nlmmul0or.z 
|- .0. = ( 0g ` W )
nlmmul0or.f 
|- F = ( Scalar ` W )
nlmmul0or.k 
|- K = ( Base ` F )
nlmmul0or.o 
|- O = ( 0g ` F )
Assertion nlmmul0or 
|- ( ( W e. NrmMod /\ A e. K /\ B e. V ) -> ( ( A .x. B ) = .0. <-> ( A = O \/ B = .0. ) ) )

Proof

Step Hyp Ref Expression
1 nlmmul0or.v 
 |-  V = ( Base ` W )
2 nlmmul0or.s 
 |-  .x. = ( .s ` W )
3 nlmmul0or.z 
 |-  .0. = ( 0g ` W )
4 nlmmul0or.f 
 |-  F = ( Scalar ` W )
5 nlmmul0or.k 
 |-  K = ( Base ` F )
6 nlmmul0or.o 
 |-  O = ( 0g ` F )
7 4 nlmngp2 
 |-  ( W e. NrmMod -> F e. NrmGrp )
8 7 3ad2ant1 
 |-  ( ( W e. NrmMod /\ A e. K /\ B e. V ) -> F e. NrmGrp )
9 simp2 
 |-  ( ( W e. NrmMod /\ A e. K /\ B e. V ) -> A e. K )
10 eqid 
 |-  ( norm ` F ) = ( norm ` F )
11 5 10 nmcl 
 |-  ( ( F e. NrmGrp /\ A e. K ) -> ( ( norm ` F ) ` A ) e. RR )
12 8 9 11 syl2anc 
 |-  ( ( W e. NrmMod /\ A e. K /\ B e. V ) -> ( ( norm ` F ) ` A ) e. RR )
13 12 recnd 
 |-  ( ( W e. NrmMod /\ A e. K /\ B e. V ) -> ( ( norm ` F ) ` A ) e. CC )
14 nlmngp 
 |-  ( W e. NrmMod -> W e. NrmGrp )
15 14 3ad2ant1 
 |-  ( ( W e. NrmMod /\ A e. K /\ B e. V ) -> W e. NrmGrp )
16 simp3 
 |-  ( ( W e. NrmMod /\ A e. K /\ B e. V ) -> B e. V )
17 eqid 
 |-  ( norm ` W ) = ( norm ` W )
18 1 17 nmcl 
 |-  ( ( W e. NrmGrp /\ B e. V ) -> ( ( norm ` W ) ` B ) e. RR )
19 15 16 18 syl2anc 
 |-  ( ( W e. NrmMod /\ A e. K /\ B e. V ) -> ( ( norm ` W ) ` B ) e. RR )
20 19 recnd 
 |-  ( ( W e. NrmMod /\ A e. K /\ B e. V ) -> ( ( norm ` W ) ` B ) e. CC )
21 13 20 mul0ord 
 |-  ( ( W e. NrmMod /\ A e. K /\ B e. V ) -> ( ( ( ( norm ` F ) ` A ) x. ( ( norm ` W ) ` B ) ) = 0 <-> ( ( ( norm ` F ) ` A ) = 0 \/ ( ( norm ` W ) ` B ) = 0 ) ) )
22 1 17 2 4 5 10 nmvs 
 |-  ( ( W e. NrmMod /\ A e. K /\ B e. V ) -> ( ( norm ` W ) ` ( A .x. B ) ) = ( ( ( norm ` F ) ` A ) x. ( ( norm ` W ) ` B ) ) )
23 22 eqeq1d 
 |-  ( ( W e. NrmMod /\ A e. K /\ B e. V ) -> ( ( ( norm ` W ) ` ( A .x. B ) ) = 0 <-> ( ( ( norm ` F ) ` A ) x. ( ( norm ` W ) ` B ) ) = 0 ) )
24 nlmlmod 
 |-  ( W e. NrmMod -> W e. LMod )
25 1 4 2 5 lmodvscl 
 |-  ( ( W e. LMod /\ A e. K /\ B e. V ) -> ( A .x. B ) e. V )
26 24 25 syl3an1 
 |-  ( ( W e. NrmMod /\ A e. K /\ B e. V ) -> ( A .x. B ) e. V )
27 1 17 3 nmeq0 
 |-  ( ( W e. NrmGrp /\ ( A .x. B ) e. V ) -> ( ( ( norm ` W ) ` ( A .x. B ) ) = 0 <-> ( A .x. B ) = .0. ) )
28 15 26 27 syl2anc 
 |-  ( ( W e. NrmMod /\ A e. K /\ B e. V ) -> ( ( ( norm ` W ) ` ( A .x. B ) ) = 0 <-> ( A .x. B ) = .0. ) )
29 23 28 bitr3d 
 |-  ( ( W e. NrmMod /\ A e. K /\ B e. V ) -> ( ( ( ( norm ` F ) ` A ) x. ( ( norm ` W ) ` B ) ) = 0 <-> ( A .x. B ) = .0. ) )
30 5 10 6 nmeq0 
 |-  ( ( F e. NrmGrp /\ A e. K ) -> ( ( ( norm ` F ) ` A ) = 0 <-> A = O ) )
31 8 9 30 syl2anc 
 |-  ( ( W e. NrmMod /\ A e. K /\ B e. V ) -> ( ( ( norm ` F ) ` A ) = 0 <-> A = O ) )
32 1 17 3 nmeq0 
 |-  ( ( W e. NrmGrp /\ B e. V ) -> ( ( ( norm ` W ) ` B ) = 0 <-> B = .0. ) )
33 15 16 32 syl2anc 
 |-  ( ( W e. NrmMod /\ A e. K /\ B e. V ) -> ( ( ( norm ` W ) ` B ) = 0 <-> B = .0. ) )
34 31 33 orbi12d 
 |-  ( ( W e. NrmMod /\ A e. K /\ B e. V ) -> ( ( ( ( norm ` F ) ` A ) = 0 \/ ( ( norm ` W ) ` B ) = 0 ) <-> ( A = O \/ B = .0. ) ) )
35 21 29 34 3bitr3d 
 |-  ( ( W e. NrmMod /\ A e. K /\ B e. V ) -> ( ( A .x. B ) = .0. <-> ( A = O \/ B = .0. ) ) )