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