This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem lvecvs0or

Description: If a scalar product is zero, one of its factors must be zero. ( hvmul0or analog.) (Contributed by NM, 2-Jul-2014)

Ref Expression
Hypotheses lvecmul0or.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
lvecmul0or.s ⊢ · = ( ·𝑠 ‘ 𝑊 )
lvecmul0or.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
lvecmul0or.k ⊢ 𝐾 = ( Base ‘ 𝐹 )
lvecmul0or.o ⊢ 𝑂 = ( 0g ‘ 𝐹 )
lvecmul0or.z ⊢ 0 = ( 0g ‘ 𝑊 )
lvecmul0or.w ⊢ ( 𝜑 → 𝑊 ∈ LVec )
lvecmul0or.a ⊢ ( 𝜑 → 𝐴 ∈ 𝐾 )
lvecmul0or.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
Assertion lvecvs0or ( 𝜑 → ( ( 𝐴 · 𝑋 ) = 0 ↔ ( 𝐴 = 𝑂 ∨ 𝑋 = 0 ) ) )

Proof

Step Hyp Ref Expression
1 lvecmul0or.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
2 lvecmul0or.s ⊢ · = ( ·𝑠 ‘ 𝑊 )
3 lvecmul0or.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
4 lvecmul0or.k ⊢ 𝐾 = ( Base ‘ 𝐹 )
5 lvecmul0or.o ⊢ 𝑂 = ( 0g ‘ 𝐹 )
6 lvecmul0or.z ⊢ 0 = ( 0g ‘ 𝑊 )
7 lvecmul0or.w ⊢ ( 𝜑 → 𝑊 ∈ LVec )
8 lvecmul0or.a ⊢ ( 𝜑 → 𝐴 ∈ 𝐾 )
9 lvecmul0or.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
10 df-ne ⊢ ( 𝐴 ≠ 𝑂 ↔ ¬ 𝐴 = 𝑂 )
11 oveq2 ⊢ ( ( 𝐴 · 𝑋 ) = 0 → ( ( ( invr ‘ 𝐹 ) ‘ 𝐴 ) · ( 𝐴 · 𝑋 ) ) = ( ( ( invr ‘ 𝐹 ) ‘ 𝐴 ) · 0 ) )
12 11 ad2antlr ⊢ ( ( ( 𝜑 ∧ ( 𝐴 · 𝑋 ) = 0 ) ∧ 𝐴 ≠ 𝑂 ) → ( ( ( invr ‘ 𝐹 ) ‘ 𝐴 ) · ( 𝐴 · 𝑋 ) ) = ( ( ( invr ‘ 𝐹 ) ‘ 𝐴 ) · 0 ) )
13 7 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝑂 ) → 𝑊 ∈ LVec )
14 3 lvecdrng ⊢ ( 𝑊 ∈ LVec → 𝐹 ∈ DivRing )
15 13 14 syl ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝑂 ) → 𝐹 ∈ DivRing )
16 8 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝑂 ) → 𝐴 ∈ 𝐾 )
17 simpr ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝑂 ) → 𝐴 ≠ 𝑂 )
18 eqid ⊢ ( .r ‘ 𝐹 ) = ( .r ‘ 𝐹 )
19 eqid ⊢ ( 1r ‘ 𝐹 ) = ( 1r ‘ 𝐹 )
20 eqid ⊢ ( invr ‘ 𝐹 ) = ( invr ‘ 𝐹 )
21 4 5 18 19 20 drnginvrl ⊢ ( ( 𝐹 ∈ DivRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐴 ≠ 𝑂 ) → ( ( ( invr ‘ 𝐹 ) ‘ 𝐴 ) ( .r ‘ 𝐹 ) 𝐴 ) = ( 1r ‘ 𝐹 ) )
22 15 16 17 21 syl3anc ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝑂 ) → ( ( ( invr ‘ 𝐹 ) ‘ 𝐴 ) ( .r ‘ 𝐹 ) 𝐴 ) = ( 1r ‘ 𝐹 ) )
23 22 oveq1d ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝑂 ) → ( ( ( ( invr ‘ 𝐹 ) ‘ 𝐴 ) ( .r ‘ 𝐹 ) 𝐴 ) · 𝑋 ) = ( ( 1r ‘ 𝐹 ) · 𝑋 ) )
24 lveclmod ⊢ ( 𝑊 ∈ LVec → 𝑊 ∈ LMod )
25 7 24 syl ⊢ ( 𝜑 → 𝑊 ∈ LMod )
26 25 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝑂 ) → 𝑊 ∈ LMod )
27 4 5 20 drnginvrcl ⊢ ( ( 𝐹 ∈ DivRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐴 ≠ 𝑂 ) → ( ( invr ‘ 𝐹 ) ‘ 𝐴 ) ∈ 𝐾 )
28 15 16 17 27 syl3anc ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝑂 ) → ( ( invr ‘ 𝐹 ) ‘ 𝐴 ) ∈ 𝐾 )
29 9 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝑂 ) → 𝑋 ∈ 𝑉 )
30 1 3 2 4 18 lmodvsass ⊢ ( ( 𝑊 ∈ LMod ∧ ( ( ( invr ‘ 𝐹 ) ‘ 𝐴 ) ∈ 𝐾 ∧ 𝐴 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ) → ( ( ( ( invr ‘ 𝐹 ) ‘ 𝐴 ) ( .r ‘ 𝐹 ) 𝐴 ) · 𝑋 ) = ( ( ( invr ‘ 𝐹 ) ‘ 𝐴 ) · ( 𝐴 · 𝑋 ) ) )
31 26 28 16 29 30 syl13anc ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝑂 ) → ( ( ( ( invr ‘ 𝐹 ) ‘ 𝐴 ) ( .r ‘ 𝐹 ) 𝐴 ) · 𝑋 ) = ( ( ( invr ‘ 𝐹 ) ‘ 𝐴 ) · ( 𝐴 · 𝑋 ) ) )
32 1 3 2 19 lmodvs1 ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) → ( ( 1r ‘ 𝐹 ) · 𝑋 ) = 𝑋 )
33 25 9 32 syl2anc ⊢ ( 𝜑 → ( ( 1r ‘ 𝐹 ) · 𝑋 ) = 𝑋 )
34 33 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝑂 ) → ( ( 1r ‘ 𝐹 ) · 𝑋 ) = 𝑋 )
35 23 31 34 3eqtr3d ⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝑂 ) → ( ( ( invr ‘ 𝐹 ) ‘ 𝐴 ) · ( 𝐴 · 𝑋 ) ) = 𝑋 )
36 35 adantlr ⊢ ( ( ( 𝜑 ∧ ( 𝐴 · 𝑋 ) = 0 ) ∧ 𝐴 ≠ 𝑂 ) → ( ( ( invr ‘ 𝐹 ) ‘ 𝐴 ) · ( 𝐴 · 𝑋 ) ) = 𝑋 )
37 25 adantr ⊢ ( ( 𝜑 ∧ ( 𝐴 · 𝑋 ) = 0 ) → 𝑊 ∈ LMod )
38 37 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝐴 · 𝑋 ) = 0 ) ∧ 𝐴 ≠ 𝑂 ) → 𝑊 ∈ LMod )
39 28 adantlr ⊢ ( ( ( 𝜑 ∧ ( 𝐴 · 𝑋 ) = 0 ) ∧ 𝐴 ≠ 𝑂 ) → ( ( invr ‘ 𝐹 ) ‘ 𝐴 ) ∈ 𝐾 )
40 3 2 4 6 lmodvs0 ⊢ ( ( 𝑊 ∈ LMod ∧ ( ( invr ‘ 𝐹 ) ‘ 𝐴 ) ∈ 𝐾 ) → ( ( ( invr ‘ 𝐹 ) ‘ 𝐴 ) · 0 ) = 0 )
41 38 39 40 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝐴 · 𝑋 ) = 0 ) ∧ 𝐴 ≠ 𝑂 ) → ( ( ( invr ‘ 𝐹 ) ‘ 𝐴 ) · 0 ) = 0 )
42 12 36 41 3eqtr3d ⊢ ( ( ( 𝜑 ∧ ( 𝐴 · 𝑋 ) = 0 ) ∧ 𝐴 ≠ 𝑂 ) → 𝑋 = 0 )
43 42 ex ⊢ ( ( 𝜑 ∧ ( 𝐴 · 𝑋 ) = 0 ) → ( 𝐴 ≠ 𝑂 → 𝑋 = 0 ) )
44 10 43 biimtrrid ⊢ ( ( 𝜑 ∧ ( 𝐴 · 𝑋 ) = 0 ) → ( ¬ 𝐴 = 𝑂 → 𝑋 = 0 ) )
45 44 orrd ⊢ ( ( 𝜑 ∧ ( 𝐴 · 𝑋 ) = 0 ) → ( 𝐴 = 𝑂 ∨ 𝑋 = 0 ) )
46 45 ex ⊢ ( 𝜑 → ( ( 𝐴 · 𝑋 ) = 0 → ( 𝐴 = 𝑂 ∨ 𝑋 = 0 ) ) )
47 1 3 2 5 6 lmod0vs ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) → ( 𝑂 · 𝑋 ) = 0 )
48 25 9 47 syl2anc ⊢ ( 𝜑 → ( 𝑂 · 𝑋 ) = 0 )
49 oveq1 ⊢ ( 𝐴 = 𝑂 → ( 𝐴 · 𝑋 ) = ( 𝑂 · 𝑋 ) )
50 49 eqeq1d ⊢ ( 𝐴 = 𝑂 → ( ( 𝐴 · 𝑋 ) = 0 ↔ ( 𝑂 · 𝑋 ) = 0 ) )
51 48 50 syl5ibrcom ⊢ ( 𝜑 → ( 𝐴 = 𝑂 → ( 𝐴 · 𝑋 ) = 0 ) )
52 3 2 4 6 lmodvs0 ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐴 ∈ 𝐾 ) → ( 𝐴 · 0 ) = 0 )
53 25 8 52 syl2anc ⊢ ( 𝜑 → ( 𝐴 · 0 ) = 0 )
54 oveq2 ⊢ ( 𝑋 = 0 → ( 𝐴 · 𝑋 ) = ( 𝐴 · 0 ) )
55 54 eqeq1d ⊢ ( 𝑋 = 0 → ( ( 𝐴 · 𝑋 ) = 0 ↔ ( 𝐴 · 0 ) = 0 ) )
56 53 55 syl5ibrcom ⊢ ( 𝜑 → ( 𝑋 = 0 → ( 𝐴 · 𝑋 ) = 0 ) )
57 51 56 jaod ⊢ ( 𝜑 → ( ( 𝐴 = 𝑂 ∨ 𝑋 = 0 ) → ( 𝐴 · 𝑋 ) = 0 ) )
58 46 57 impbid ⊢ ( 𝜑 → ( ( 𝐴 · 𝑋 ) = 0 ↔ ( 𝐴 = 𝑂 ∨ 𝑋 = 0 ) ) )