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 syl5bir ( ( 𝜑 ∧ ( 𝐴 · 𝑋 ) = 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 ) ) )