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	ffvelcdmd	⊢ ( 𝜑 → ( 𝑈 ‘ 𝐿 ) ∈ 𝐵 )
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	eqtrid	⊢ ( 𝜑 → 𝐾 = ( 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	⊢ ( 𝜑 → ¬ ( 𝑋 · ( 𝑈 ‘ 𝐿 ) ) ∈ 𝐶 )