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

Metamath Proof Explorer

Theorem lssvs0or

Description: If a scalar product belongs to a subspace, either the scalar component is zero or the vector component also belongs to the subspace. (Contributed by NM, 5-Apr-2015)

Ref Expression
Hypotheses lssvs0or.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
lssvs0or.t ⊢ · = ( ·𝑠 ‘ 𝑊 )
lssvs0or.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
lssvs0or.k ⊢ 𝐾 = ( Base ‘ 𝐹 )
lssvs0or.o ⊢ 0 = ( 0g ‘ 𝐹 )
lssvs0or.s ⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
lssvs0or.w ⊢ ( 𝜑 → 𝑊 ∈ LVec )
lssvs0or.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑆 )
lssvs0or.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
lssvs0or.a ⊢ ( 𝜑 → 𝐴 ∈ 𝐾 )
Assertion lssvs0or ( 𝜑 → ( ( 𝐴 · 𝑋 ) ∈ 𝑈 ↔ ( 𝐴 = 0 ∨ 𝑋 ∈ 𝑈 ) ) )

Proof

Step Hyp Ref Expression
1 lssvs0or.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
2 lssvs0or.t ⊢ · = ( ·𝑠 ‘ 𝑊 )
3 lssvs0or.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
4 lssvs0or.k ⊢ 𝐾 = ( Base ‘ 𝐹 )
5 lssvs0or.o ⊢ 0 = ( 0g ‘ 𝐹 )
6 lssvs0or.s ⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
7 lssvs0or.w ⊢ ( 𝜑 → 𝑊 ∈ LVec )
8 lssvs0or.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑆 )
9 lssvs0or.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
10 lssvs0or.a ⊢ ( 𝜑 → 𝐴 ∈ 𝐾 )
11 3 lvecdrng ⊢ ( 𝑊 ∈ LVec → 𝐹 ∈ DivRing )
12 7 11 syl ⊢ ( 𝜑 → 𝐹 ∈ DivRing )
13 12 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝐴 · 𝑋 ) ∈ 𝑈 ) ∧ 𝐴 ≠ 0 ) → 𝐹 ∈ DivRing )
14 10 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝐴 · 𝑋 ) ∈ 𝑈 ) ∧ 𝐴 ≠ 0 ) → 𝐴 ∈ 𝐾 )
15 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝐴 · 𝑋 ) ∈ 𝑈 ) ∧ 𝐴 ≠ 0 ) → 𝐴 ≠ 0 )
16 eqid ⊢ ( .r ‘ 𝐹 ) = ( .r ‘ 𝐹 )
17 eqid ⊢ ( 1r ‘ 𝐹 ) = ( 1r ‘ 𝐹 )
18 eqid ⊢ ( invr ‘ 𝐹 ) = ( invr ‘ 𝐹 )
19 4 5 16 17 18 drnginvrl ⊢ ( ( 𝐹 ∈ DivRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐴 ≠ 0 ) → ( ( ( invr ‘ 𝐹 ) ‘ 𝐴 ) ( .r ‘ 𝐹 ) 𝐴 ) = ( 1r ‘ 𝐹 ) )
20 13 14 15 19 syl3anc ⊢ ( ( ( 𝜑 ∧ ( 𝐴 · 𝑋 ) ∈ 𝑈 ) ∧ 𝐴 ≠ 0 ) → ( ( ( invr ‘ 𝐹 ) ‘ 𝐴 ) ( .r ‘ 𝐹 ) 𝐴 ) = ( 1r ‘ 𝐹 ) )
21 20 oveq1d ⊢ ( ( ( 𝜑 ∧ ( 𝐴 · 𝑋 ) ∈ 𝑈 ) ∧ 𝐴 ≠ 0 ) → ( ( ( ( invr ‘ 𝐹 ) ‘ 𝐴 ) ( .r ‘ 𝐹 ) 𝐴 ) · 𝑋 ) = ( ( 1r ‘ 𝐹 ) · 𝑋 ) )
22 lveclmod ⊢ ( 𝑊 ∈ LVec → 𝑊 ∈ LMod )
23 7 22 syl ⊢ ( 𝜑 → 𝑊 ∈ LMod )
24 23 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝐴 · 𝑋 ) ∈ 𝑈 ) ∧ 𝐴 ≠ 0 ) → 𝑊 ∈ LMod )
25 4 5 18 drnginvrcl ⊢ ( ( 𝐹 ∈ DivRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐴 ≠ 0 ) → ( ( invr ‘ 𝐹 ) ‘ 𝐴 ) ∈ 𝐾 )
26 13 14 15 25 syl3anc ⊢ ( ( ( 𝜑 ∧ ( 𝐴 · 𝑋 ) ∈ 𝑈 ) ∧ 𝐴 ≠ 0 ) → ( ( invr ‘ 𝐹 ) ‘ 𝐴 ) ∈ 𝐾 )
27 9 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝐴 · 𝑋 ) ∈ 𝑈 ) ∧ 𝐴 ≠ 0 ) → 𝑋 ∈ 𝑉 )
28 1 3 2 4 16 lmodvsass ⊢ ( ( 𝑊 ∈ LMod ∧ ( ( ( invr ‘ 𝐹 ) ‘ 𝐴 ) ∈ 𝐾 ∧ 𝐴 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉 ) ) → ( ( ( ( invr ‘ 𝐹 ) ‘ 𝐴 ) ( .r ‘ 𝐹 ) 𝐴 ) · 𝑋 ) = ( ( ( invr ‘ 𝐹 ) ‘ 𝐴 ) · ( 𝐴 · 𝑋 ) ) )
29 24 26 14 27 28 syl13anc ⊢ ( ( ( 𝜑 ∧ ( 𝐴 · 𝑋 ) ∈ 𝑈 ) ∧ 𝐴 ≠ 0 ) → ( ( ( ( invr ‘ 𝐹 ) ‘ 𝐴 ) ( .r ‘ 𝐹 ) 𝐴 ) · 𝑋 ) = ( ( ( invr ‘ 𝐹 ) ‘ 𝐴 ) · ( 𝐴 · 𝑋 ) ) )
30 1 3 2 17 lmodvs1 ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) → ( ( 1r ‘ 𝐹 ) · 𝑋 ) = 𝑋 )
31 24 27 30 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝐴 · 𝑋 ) ∈ 𝑈 ) ∧ 𝐴 ≠ 0 ) → ( ( 1r ‘ 𝐹 ) · 𝑋 ) = 𝑋 )
32 21 29 31 3eqtr3rd ⊢ ( ( ( 𝜑 ∧ ( 𝐴 · 𝑋 ) ∈ 𝑈 ) ∧ 𝐴 ≠ 0 ) → 𝑋 = ( ( ( invr ‘ 𝐹 ) ‘ 𝐴 ) · ( 𝐴 · 𝑋 ) ) )
33 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝐴 · 𝑋 ) ∈ 𝑈 ) ∧ 𝐴 ≠ 0 ) → 𝑈 ∈ 𝑆 )
34 simplr ⊢ ( ( ( 𝜑 ∧ ( 𝐴 · 𝑋 ) ∈ 𝑈 ) ∧ 𝐴 ≠ 0 ) → ( 𝐴 · 𝑋 ) ∈ 𝑈 )
35 3 2 4 6 lssvscl ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) ∧ ( ( ( invr ‘ 𝐹 ) ‘ 𝐴 ) ∈ 𝐾 ∧ ( 𝐴 · 𝑋 ) ∈ 𝑈 ) ) → ( ( ( invr ‘ 𝐹 ) ‘ 𝐴 ) · ( 𝐴 · 𝑋 ) ) ∈ 𝑈 )
36 24 33 26 34 35 syl22anc ⊢ ( ( ( 𝜑 ∧ ( 𝐴 · 𝑋 ) ∈ 𝑈 ) ∧ 𝐴 ≠ 0 ) → ( ( ( invr ‘ 𝐹 ) ‘ 𝐴 ) · ( 𝐴 · 𝑋 ) ) ∈ 𝑈 )
37 32 36 eqeltrd ⊢ ( ( ( 𝜑 ∧ ( 𝐴 · 𝑋 ) ∈ 𝑈 ) ∧ 𝐴 ≠ 0 ) → 𝑋 ∈ 𝑈 )
38 37 ex ⊢ ( ( 𝜑 ∧ ( 𝐴 · 𝑋 ) ∈ 𝑈 ) → ( 𝐴 ≠ 0 → 𝑋 ∈ 𝑈 ) )
39 38 necon1bd ⊢ ( ( 𝜑 ∧ ( 𝐴 · 𝑋 ) ∈ 𝑈 ) → ( ¬ 𝑋 ∈ 𝑈 → 𝐴 = 0 ) )
40 39 orrd ⊢ ( ( 𝜑 ∧ ( 𝐴 · 𝑋 ) ∈ 𝑈 ) → ( 𝑋 ∈ 𝑈 ∨ 𝐴 = 0 ) )
41 40 orcomd ⊢ ( ( 𝜑 ∧ ( 𝐴 · 𝑋 ) ∈ 𝑈 ) → ( 𝐴 = 0 ∨ 𝑋 ∈ 𝑈 ) )
42 oveq1 ⊢ ( 𝐴 = 0 → ( 𝐴 · 𝑋 ) = ( 0 · 𝑋 ) )
43 42 adantl ⊢ ( ( 𝜑 ∧ 𝐴 = 0 ) → ( 𝐴 · 𝑋 ) = ( 0 · 𝑋 ) )
44 eqid ⊢ ( 0g ‘ 𝑊 ) = ( 0g ‘ 𝑊 )
45 1 3 2 5 44 lmod0vs ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) → ( 0 · 𝑋 ) = ( 0g ‘ 𝑊 ) )
46 23 9 45 syl2anc ⊢ ( 𝜑 → ( 0 · 𝑋 ) = ( 0g ‘ 𝑊 ) )
47 44 6 lss0cl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) → ( 0g ‘ 𝑊 ) ∈ 𝑈 )
48 23 8 47 syl2anc ⊢ ( 𝜑 → ( 0g ‘ 𝑊 ) ∈ 𝑈 )
49 46 48 eqeltrd ⊢ ( 𝜑 → ( 0 · 𝑋 ) ∈ 𝑈 )
50 49 adantr ⊢ ( ( 𝜑 ∧ 𝐴 = 0 ) → ( 0 · 𝑋 ) ∈ 𝑈 )
51 43 50 eqeltrd ⊢ ( ( 𝜑 ∧ 𝐴 = 0 ) → ( 𝐴 · 𝑋 ) ∈ 𝑈 )
52 23 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑈 ) → 𝑊 ∈ LMod )
53 8 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑈 ) → 𝑈 ∈ 𝑆 )
54 10 adantr ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑈 ) → 𝐴 ∈ 𝐾 )
55 simpr ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑈 ) → 𝑋 ∈ 𝑈 )
56 3 2 4 6 lssvscl ⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) ∧ ( 𝐴 ∈ 𝐾 ∧ 𝑋 ∈ 𝑈 ) ) → ( 𝐴 · 𝑋 ) ∈ 𝑈 )
57 52 53 54 55 56 syl22anc ⊢ ( ( 𝜑 ∧ 𝑋 ∈ 𝑈 ) → ( 𝐴 · 𝑋 ) ∈ 𝑈 )
58 51 57 jaodan ⊢ ( ( 𝜑 ∧ ( 𝐴 = 0 ∨ 𝑋 ∈ 𝑈 ) ) → ( 𝐴 · 𝑋 ) ∈ 𝑈 )
59 41 58 impbida ⊢ ( 𝜑 → ( ( 𝐴 · 𝑋 ) ∈ 𝑈 ↔ ( 𝐴 = 0 ∨ 𝑋 ∈ 𝑈 ) ) )