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 ˙