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