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 · ˙ = W
nlmmul0or.z 0 ˙ = 0 W
nlmmul0or.f F = Scalar W
nlmmul0or.k K = Base F
nlmmul0or.o O = 0 F
Assertion nlmmul0or W NrmMod A K B V A · ˙ B = 0 ˙ A = O B = 0 ˙

Proof

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