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 𝑉 = ( Base ‘ 𝑊 )
nlmmul0or.s · = ( ·𝑠𝑊 )
nlmmul0or.z 0 = ( 0g𝑊 )
nlmmul0or.f 𝐹 = ( Scalar ‘ 𝑊 )
nlmmul0or.k 𝐾 = ( Base ‘ 𝐹 )
nlmmul0or.o 𝑂 = ( 0g𝐹 )
Assertion nlmmul0or ( ( 𝑊 ∈ NrmMod ∧ 𝐴𝐾𝐵𝑉 ) → ( ( 𝐴 · 𝐵 ) = 0 ↔ ( 𝐴 = 𝑂𝐵 = 0 ) ) )

Proof

Step Hyp Ref Expression
1 nlmmul0or.v 𝑉 = ( Base ‘ 𝑊 )
2 nlmmul0or.s · = ( ·𝑠𝑊 )
3 nlmmul0or.z 0 = ( 0g𝑊 )
4 nlmmul0or.f 𝐹 = ( Scalar ‘ 𝑊 )
5 nlmmul0or.k 𝐾 = ( Base ‘ 𝐹 )
6 nlmmul0or.o 𝑂 = ( 0g𝐹 )
7 4 nlmngp2 ( 𝑊 ∈ NrmMod → 𝐹 ∈ NrmGrp )
8 7 3ad2ant1 ( ( 𝑊 ∈ NrmMod ∧ 𝐴𝐾𝐵𝑉 ) → 𝐹 ∈ NrmGrp )
9 simp2 ( ( 𝑊 ∈ NrmMod ∧ 𝐴𝐾𝐵𝑉 ) → 𝐴𝐾 )
10 eqid ( norm ‘ 𝐹 ) = ( norm ‘ 𝐹 )
11 5 10 nmcl ( ( 𝐹 ∈ NrmGrp ∧ 𝐴𝐾 ) → ( ( norm ‘ 𝐹 ) ‘ 𝐴 ) ∈ ℝ )
12 8 9 11 syl2anc ( ( 𝑊 ∈ NrmMod ∧ 𝐴𝐾𝐵𝑉 ) → ( ( norm ‘ 𝐹 ) ‘ 𝐴 ) ∈ ℝ )
13 12 recnd ( ( 𝑊 ∈ NrmMod ∧ 𝐴𝐾𝐵𝑉 ) → ( ( norm ‘ 𝐹 ) ‘ 𝐴 ) ∈ ℂ )
14 nlmngp ( 𝑊 ∈ NrmMod → 𝑊 ∈ NrmGrp )
15 14 3ad2ant1 ( ( 𝑊 ∈ NrmMod ∧ 𝐴𝐾𝐵𝑉 ) → 𝑊 ∈ NrmGrp )
16 simp3 ( ( 𝑊 ∈ NrmMod ∧ 𝐴𝐾𝐵𝑉 ) → 𝐵𝑉 )
17 eqid ( norm ‘ 𝑊 ) = ( norm ‘ 𝑊 )
18 1 17 nmcl ( ( 𝑊 ∈ NrmGrp ∧ 𝐵𝑉 ) → ( ( norm ‘ 𝑊 ) ‘ 𝐵 ) ∈ ℝ )
19 15 16 18 syl2anc ( ( 𝑊 ∈ NrmMod ∧ 𝐴𝐾𝐵𝑉 ) → ( ( norm ‘ 𝑊 ) ‘ 𝐵 ) ∈ ℝ )
20 19 recnd ( ( 𝑊 ∈ NrmMod ∧ 𝐴𝐾𝐵𝑉 ) → ( ( norm ‘ 𝑊 ) ‘ 𝐵 ) ∈ ℂ )
21 13 20 mul0ord ( ( 𝑊 ∈ NrmMod ∧ 𝐴𝐾𝐵𝑉 ) → ( ( ( ( norm ‘ 𝐹 ) ‘ 𝐴 ) · ( ( norm ‘ 𝑊 ) ‘ 𝐵 ) ) = 0 ↔ ( ( ( norm ‘ 𝐹 ) ‘ 𝐴 ) = 0 ∨ ( ( norm ‘ 𝑊 ) ‘ 𝐵 ) = 0 ) ) )
22 1 17 2 4 5 10 nmvs ( ( 𝑊 ∈ NrmMod ∧ 𝐴𝐾𝐵𝑉 ) → ( ( norm ‘ 𝑊 ) ‘ ( 𝐴 · 𝐵 ) ) = ( ( ( norm ‘ 𝐹 ) ‘ 𝐴 ) · ( ( norm ‘ 𝑊 ) ‘ 𝐵 ) ) )
23 22 eqeq1d ( ( 𝑊 ∈ NrmMod ∧ 𝐴𝐾𝐵𝑉 ) → ( ( ( norm ‘ 𝑊 ) ‘ ( 𝐴 · 𝐵 ) ) = 0 ↔ ( ( ( norm ‘ 𝐹 ) ‘ 𝐴 ) · ( ( norm ‘ 𝑊 ) ‘ 𝐵 ) ) = 0 ) )
24 nlmlmod ( 𝑊 ∈ NrmMod → 𝑊 ∈ LMod )
25 1 4 2 5 lmodvscl ( ( 𝑊 ∈ LMod ∧ 𝐴𝐾𝐵𝑉 ) → ( 𝐴 · 𝐵 ) ∈ 𝑉 )
26 24 25 syl3an1 ( ( 𝑊 ∈ NrmMod ∧ 𝐴𝐾𝐵𝑉 ) → ( 𝐴 · 𝐵 ) ∈ 𝑉 )
27 1 17 3 nmeq0 ( ( 𝑊 ∈ NrmGrp ∧ ( 𝐴 · 𝐵 ) ∈ 𝑉 ) → ( ( ( norm ‘ 𝑊 ) ‘ ( 𝐴 · 𝐵 ) ) = 0 ↔ ( 𝐴 · 𝐵 ) = 0 ) )
28 15 26 27 syl2anc ( ( 𝑊 ∈ NrmMod ∧ 𝐴𝐾𝐵𝑉 ) → ( ( ( norm ‘ 𝑊 ) ‘ ( 𝐴 · 𝐵 ) ) = 0 ↔ ( 𝐴 · 𝐵 ) = 0 ) )
29 23 28 bitr3d ( ( 𝑊 ∈ NrmMod ∧ 𝐴𝐾𝐵𝑉 ) → ( ( ( ( norm ‘ 𝐹 ) ‘ 𝐴 ) · ( ( norm ‘ 𝑊 ) ‘ 𝐵 ) ) = 0 ↔ ( 𝐴 · 𝐵 ) = 0 ) )
30 5 10 6 nmeq0 ( ( 𝐹 ∈ NrmGrp ∧ 𝐴𝐾 ) → ( ( ( norm ‘ 𝐹 ) ‘ 𝐴 ) = 0 ↔ 𝐴 = 𝑂 ) )
31 8 9 30 syl2anc ( ( 𝑊 ∈ NrmMod ∧ 𝐴𝐾𝐵𝑉 ) → ( ( ( norm ‘ 𝐹 ) ‘ 𝐴 ) = 0 ↔ 𝐴 = 𝑂 ) )
32 1 17 3 nmeq0 ( ( 𝑊 ∈ NrmGrp ∧ 𝐵𝑉 ) → ( ( ( norm ‘ 𝑊 ) ‘ 𝐵 ) = 0 ↔ 𝐵 = 0 ) )
33 15 16 32 syl2anc ( ( 𝑊 ∈ NrmMod ∧ 𝐴𝐾𝐵𝑉 ) → ( ( ( norm ‘ 𝑊 ) ‘ 𝐵 ) = 0 ↔ 𝐵 = 0 ) )
34 31 33 orbi12d ( ( 𝑊 ∈ NrmMod ∧ 𝐴𝐾𝐵𝑉 ) → ( ( ( ( norm ‘ 𝐹 ) ‘ 𝐴 ) = 0 ∨ ( ( norm ‘ 𝑊 ) ‘ 𝐵 ) = 0 ) ↔ ( 𝐴 = 𝑂𝐵 = 0 ) ) )
35 21 29 34 3bitr3d ( ( 𝑊 ∈ NrmMod ∧ 𝐴𝐾𝐵𝑉 ) → ( ( 𝐴 · 𝐵 ) = 0 ↔ ( 𝐴 = 𝑂𝐵 = 0 ) ) )