Metamath Proof Explorer

Theorem frlmssuvc2

Description: A nonzero scalar multiple of a unit vector not included in a support-restriction subspace is not included in the subspace. (Contributed by Stefan O'Rear, 5-Feb-2015) (Revised by AV, 24-Jun-2019)

Ref Expression
Hypotheses frlmssuvc1.f ⊢ 𝐹 = ( 𝑅 freeLMod 𝐼 )
frlmssuvc1.u ⊢ 𝑈 = ( 𝑅 unitVec 𝐼 )
frlmssuvc1.b ⊢ 𝐵 = ( Base ‘ 𝐹 )
frlmssuvc1.k ⊢ 𝐾 = ( Base ‘ 𝑅 )
frlmssuvc1.t ⊢ · = ( ·𝑠 ‘ 𝐹 )
frlmssuvc1.z ⊢ 0 = ( 0g ‘ 𝑅 )
frlmssuvc1.c ⊢ 𝐶 = { 𝑥 ∈ 𝐵 ∣ ( 𝑥 supp 0 ) ⊆ 𝐽 }
frlmssuvc1.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
frlmssuvc1.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
frlmssuvc1.j ⊢ ( 𝜑 → 𝐽 ⊆ 𝐼 )
frlmssuvc2.l ⊢ ( 𝜑 → 𝐿 ∈ ( 𝐼 ∖ 𝐽 ) )
frlmssuvc2.x ⊢ ( 𝜑 → 𝑋 ∈ ( 𝐾 ∖ { 0 } ) )
Assertion frlmssuvc2 ( 𝜑 → ¬ ( 𝑋 · ( 𝑈 ‘ 𝐿 ) ) ∈ 𝐶 )

Proof

Step Hyp Ref Expression
1 frlmssuvc1.f ⊢ 𝐹 = ( 𝑅 freeLMod 𝐼 )
2 frlmssuvc1.u ⊢ 𝑈 = ( 𝑅 unitVec 𝐼 )
3 frlmssuvc1.b ⊢ 𝐵 = ( Base ‘ 𝐹 )
4 frlmssuvc1.k ⊢ 𝐾 = ( Base ‘ 𝑅 )
5 frlmssuvc1.t ⊢ · = ( ·𝑠 ‘ 𝐹 )
6 frlmssuvc1.z ⊢ 0 = ( 0g ‘ 𝑅 )
7 frlmssuvc1.c ⊢ 𝐶 = { 𝑥 ∈ 𝐵 ∣ ( 𝑥 supp 0 ) ⊆ 𝐽 }
8 frlmssuvc1.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
9 frlmssuvc1.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
10 frlmssuvc1.j ⊢ ( 𝜑 → 𝐽 ⊆ 𝐼 )
11 frlmssuvc2.l ⊢ ( 𝜑 → 𝐿 ∈ ( 𝐼 ∖ 𝐽 ) )
12 frlmssuvc2.x ⊢ ( 𝜑 → 𝑋 ∈ ( 𝐾 ∖ { 0 } ) )
13 fveq2 ⊢ ( 𝑥 = 𝐿 → ( ( 𝑋 · ( 𝑈 ‘ 𝐿 ) ) ‘ 𝑥 ) = ( ( 𝑋 · ( 𝑈 ‘ 𝐿 ) ) ‘ 𝐿 ) )
14 13 neeq1d ⊢ ( 𝑥 = 𝐿 → ( ( ( 𝑋 · ( 𝑈 ‘ 𝐿 ) ) ‘ 𝑥 ) ≠ 0 ↔ ( ( 𝑋 · ( 𝑈 ‘ 𝐿 ) ) ‘ 𝐿 ) ≠ 0 ) )
15 11 eldifad ⊢ ( 𝜑 → 𝐿 ∈ 𝐼 )
16 12 eldifad ⊢ ( 𝜑 → 𝑋 ∈ 𝐾 )
17 2 1 3 uvcff ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ) → 𝑈 : 𝐼 ⟶ 𝐵 )
18 8 9 17 syl2anc ⊢ ( 𝜑 → 𝑈 : 𝐼 ⟶ 𝐵 )
19 18 15 ffvelrnd ⊢ ( 𝜑 → ( 𝑈 ‘ 𝐿 ) ∈ 𝐵 )
20 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
21 1 3 4 9 16 19 15 5 20 frlmvscaval ⊢ ( 𝜑 → ( ( 𝑋 · ( 𝑈 ‘ 𝐿 ) ) ‘ 𝐿 ) = ( 𝑋 ( .r ‘ 𝑅 ) ( ( 𝑈 ‘ 𝐿 ) ‘ 𝐿 ) ) )
22 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
23 2 8 9 15 22 uvcvv1 ⊢ ( 𝜑 → ( ( 𝑈 ‘ 𝐿 ) ‘ 𝐿 ) = ( 1r ‘ 𝑅 ) )
24 23 oveq2d ⊢ ( 𝜑 → ( 𝑋 ( .r ‘ 𝑅 ) ( ( 𝑈 ‘ 𝐿 ) ‘ 𝐿 ) ) = ( 𝑋 ( .r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) )
25 4 20 22 ringridm ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐾 ) → ( 𝑋 ( .r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) = 𝑋 )
26 8 16 25 syl2anc ⊢ ( 𝜑 → ( 𝑋 ( .r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) = 𝑋 )
27 21 24 26 3eqtrd ⊢ ( 𝜑 → ( ( 𝑋 · ( 𝑈 ‘ 𝐿 ) ) ‘ 𝐿 ) = 𝑋 )
28 eldifsni ⊢ ( 𝑋 ∈ ( 𝐾 ∖ { 0 } ) → 𝑋 ≠ 0 )
29 12 28 syl ⊢ ( 𝜑 → 𝑋 ≠ 0 )
30 27 29 eqnetrd ⊢ ( 𝜑 → ( ( 𝑋 · ( 𝑈 ‘ 𝐿 ) ) ‘ 𝐿 ) ≠ 0 )
31 14 15 30 elrabd ⊢ ( 𝜑 → 𝐿 ∈ { 𝑥 ∈ 𝐼 ∣ ( ( 𝑋 · ( 𝑈 ‘ 𝐿 ) ) ‘ 𝑥 ) ≠ 0 } )
32 11 eldifbd ⊢ ( 𝜑 → ¬ 𝐿 ∈ 𝐽 )
33 nelss ⊢ ( ( 𝐿 ∈ { 𝑥 ∈ 𝐼 ∣ ( ( 𝑋 · ( 𝑈 ‘ 𝐿 ) ) ‘ 𝑥 ) ≠ 0 } ∧ ¬ 𝐿 ∈ 𝐽 ) → ¬ { 𝑥 ∈ 𝐼 ∣ ( ( 𝑋 · ( 𝑈 ‘ 𝐿 ) ) ‘ 𝑥 ) ≠ 0 } ⊆ 𝐽 )
34 31 32 33 syl2anc ⊢ ( 𝜑 → ¬ { 𝑥 ∈ 𝐼 ∣ ( ( 𝑋 · ( 𝑈 ‘ 𝐿 ) ) ‘ 𝑥 ) ≠ 0 } ⊆ 𝐽 )
35 1 frlmlmod ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ) → 𝐹 ∈ LMod )
36 8 9 35 syl2anc ⊢ ( 𝜑 → 𝐹 ∈ LMod )
37 1 frlmsca ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ) → 𝑅 = ( Scalar ‘ 𝐹 ) )
38 8 9 37 syl2anc ⊢ ( 𝜑 → 𝑅 = ( Scalar ‘ 𝐹 ) )
39 38 fveq2d ⊢ ( 𝜑 → ( Base ‘ 𝑅 ) = ( Base ‘ ( Scalar ‘ 𝐹 ) ) )
40 4 39 syl5eq ⊢ ( 𝜑 → 𝐾 = ( Base ‘ ( Scalar ‘ 𝐹 ) ) )
41 16 40 eleqtrd ⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ ( Scalar ‘ 𝐹 ) ) )
42 eqid ⊢ ( Scalar ‘ 𝐹 ) = ( Scalar ‘ 𝐹 )
43 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝐹 ) ) = ( Base ‘ ( Scalar ‘ 𝐹 ) )
44 3 42 5 43 lmodvscl ⊢ ( ( 𝐹 ∈ LMod ∧ 𝑋 ∈ ( Base ‘ ( Scalar ‘ 𝐹 ) ) ∧ ( 𝑈 ‘ 𝐿 ) ∈ 𝐵 ) → ( 𝑋 · ( 𝑈 ‘ 𝐿 ) ) ∈ 𝐵 )
45 36 41 19 44 syl3anc ⊢ ( 𝜑 → ( 𝑋 · ( 𝑈 ‘ 𝐿 ) ) ∈ 𝐵 )
46 1 4 3 frlmbasf ⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑋 · ( 𝑈 ‘ 𝐿 ) ) ∈ 𝐵 ) → ( 𝑋 · ( 𝑈 ‘ 𝐿 ) ) : 𝐼 ⟶ 𝐾 )
47 9 45 46 syl2anc ⊢ ( 𝜑 → ( 𝑋 · ( 𝑈 ‘ 𝐿 ) ) : 𝐼 ⟶ 𝐾 )
48 47 ffnd ⊢ ( 𝜑 → ( 𝑋 · ( 𝑈 ‘ 𝐿 ) ) Fn 𝐼 )
49 6 fvexi ⊢ 0 ∈ V
50 49 a1i ⊢ ( 𝜑 → 0 ∈ V )
51 suppvalfn ⊢ ( ( ( 𝑋 · ( 𝑈 ‘ 𝐿 ) ) Fn 𝐼 ∧ 𝐼 ∈ 𝑉 ∧ 0 ∈ V ) → ( ( 𝑋 · ( 𝑈 ‘ 𝐿 ) ) supp 0 ) = { 𝑥 ∈ 𝐼 ∣ ( ( 𝑋 · ( 𝑈 ‘ 𝐿 ) ) ‘ 𝑥 ) ≠ 0 } )
52 48 9 50 51 syl3anc ⊢ ( 𝜑 → ( ( 𝑋 · ( 𝑈 ‘ 𝐿 ) ) supp 0 ) = { 𝑥 ∈ 𝐼 ∣ ( ( 𝑋 · ( 𝑈 ‘ 𝐿 ) ) ‘ 𝑥 ) ≠ 0 } )
53 52 sseq1d ⊢ ( 𝜑 → ( ( ( 𝑋 · ( 𝑈 ‘ 𝐿 ) ) supp 0 ) ⊆ 𝐽 ↔ { 𝑥 ∈ 𝐼 ∣ ( ( 𝑋 · ( 𝑈 ‘ 𝐿 ) ) ‘ 𝑥 ) ≠ 0 } ⊆ 𝐽 ) )
54 34 53 mtbird ⊢ ( 𝜑 → ¬ ( ( 𝑋 · ( 𝑈 ‘ 𝐿 ) ) supp 0 ) ⊆ 𝐽 )
55 54 intnand ⊢ ( 𝜑 → ¬ ( ( 𝑋 · ( 𝑈 ‘ 𝐿 ) ) ∈ 𝐵 ∧ ( ( 𝑋 · ( 𝑈 ‘ 𝐿 ) ) supp 0 ) ⊆ 𝐽 ) )
56 oveq1 ⊢ ( 𝑥 = ( 𝑋 · ( 𝑈 ‘ 𝐿 ) ) → ( 𝑥 supp 0 ) = ( ( 𝑋 · ( 𝑈 ‘ 𝐿 ) ) supp 0 ) )
57 56 sseq1d ⊢ ( 𝑥 = ( 𝑋 · ( 𝑈 ‘ 𝐿 ) ) → ( ( 𝑥 supp 0 ) ⊆ 𝐽 ↔ ( ( 𝑋 · ( 𝑈 ‘ 𝐿 ) ) supp 0 ) ⊆ 𝐽 ) )
58 57 7 elrab2 ⊢ ( ( 𝑋 · ( 𝑈 ‘ 𝐿 ) ) ∈ 𝐶 ↔ ( ( 𝑋 · ( 𝑈 ‘ 𝐿 ) ) ∈ 𝐵 ∧ ( ( 𝑋 · ( 𝑈 ‘ 𝐿 ) ) supp 0 ) ⊆ 𝐽 ) )
59 55 58 sylnibr ⊢ ( 𝜑 → ¬ ( 𝑋 · ( 𝑈 ‘ 𝐿 ) ) ∈ 𝐶 )