Theorem frlmssuvc1

Description: A scalar multiple of a unit vector included in a support-restriction subspace is 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	⊢ ( 𝜑 → 𝐽 ⊆ 𝐼 )
	frlmssuvc1.l	⊢ ( 𝜑 → 𝐿 ∈ 𝐽 )
	frlmssuvc1.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐾 )
Assertion	frlmssuvc1	⊢ ( 𝜑 → ( 𝑋 · ( 𝑈 ‘ 𝐿 ) ) ∈ 𝐶 )

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		frlmssuvc1.l	⊢ ( 𝜑 → 𝐿 ∈ 𝐽 )
12		frlmssuvc1.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐾 )
13	1	frlmlmod	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ) → 𝐹 ∈ LMod )
14	8 9 13	syl2anc	⊢ ( 𝜑 → 𝐹 ∈ LMod )
15		eqid	⊢ ( LSubSp ‘ 𝐹 ) = ( LSubSp ‘ 𝐹 )
16	1 15 3 6 7	frlmsslss2	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ) → 𝐶 ∈ ( LSubSp ‘ 𝐹 ) )
17	8 9 10 16	syl3anc	⊢ ( 𝜑 → 𝐶 ∈ ( LSubSp ‘ 𝐹 ) )
18	1	frlmsca	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ) → 𝑅 = ( Scalar ‘ 𝐹 ) )
19	8 9 18	syl2anc	⊢ ( 𝜑 → 𝑅 = ( Scalar ‘ 𝐹 ) )
20	19	fveq2d	⊢ ( 𝜑 → ( Base ‘ 𝑅 ) = ( Base ‘ ( Scalar ‘ 𝐹 ) ) )
21	4 20	syl5eq	⊢ ( 𝜑 → 𝐾 = ( Base ‘ ( Scalar ‘ 𝐹 ) ) )
22	12 21	eleqtrd	⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ ( Scalar ‘ 𝐹 ) ) )
23	2 1 3	uvcff	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑉 ) → 𝑈 : 𝐼 ⟶ 𝐵 )
24	8 9 23	syl2anc	⊢ ( 𝜑 → 𝑈 : 𝐼 ⟶ 𝐵 )
25	10 11	sseldd	⊢ ( 𝜑 → 𝐿 ∈ 𝐼 )
26	24 25	ffvelrnd	⊢ ( 𝜑 → ( 𝑈 ‘ 𝐿 ) ∈ 𝐵 )
27	1 4 3	frlmbasf	⊢ ( ( 𝐼 ∈ 𝑉 ∧ ( 𝑈 ‘ 𝐿 ) ∈ 𝐵 ) → ( 𝑈 ‘ 𝐿 ) : 𝐼 ⟶ 𝐾 )
28	9 26 27	syl2anc	⊢ ( 𝜑 → ( 𝑈 ‘ 𝐿 ) : 𝐼 ⟶ 𝐾 )
29	8	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∖ 𝐽 ) ) → 𝑅 ∈ Ring )
30	9	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∖ 𝐽 ) ) → 𝐼 ∈ 𝑉 )
31	25	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∖ 𝐽 ) ) → 𝐿 ∈ 𝐼 )
32		eldifi	⊢ ( 𝑥 ∈ ( 𝐼 ∖ 𝐽 ) → 𝑥 ∈ 𝐼 )
33	32	adantl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∖ 𝐽 ) ) → 𝑥 ∈ 𝐼 )
34		disjdif	⊢ ( 𝐽 ∩ ( 𝐼 ∖ 𝐽 ) ) = ∅
35		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∖ 𝐽 ) ) → 𝑥 ∈ ( 𝐼 ∖ 𝐽 ) )
36		disjne	⊢ ( ( ( 𝐽 ∩ ( 𝐼 ∖ 𝐽 ) ) = ∅ ∧ 𝐿 ∈ 𝐽 ∧ 𝑥 ∈ ( 𝐼 ∖ 𝐽 ) ) → 𝐿 ≠ 𝑥 )
37	34 11 35 36	mp3an2ani	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∖ 𝐽 ) ) → 𝐿 ≠ 𝑥 )
38	2 29 30 31 33 37 6	uvcvv0	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐼 ∖ 𝐽 ) ) → ( ( 𝑈 ‘ 𝐿 ) ‘ 𝑥 ) = 0 )
39	28 38	suppss	⊢ ( 𝜑 → ( ( 𝑈 ‘ 𝐿 ) supp 0 ) ⊆ 𝐽 )
40		oveq1	⊢ ( 𝑥 = ( 𝑈 ‘ 𝐿 ) → ( 𝑥 supp 0 ) = ( ( 𝑈 ‘ 𝐿 ) supp 0 ) )
41	40	sseq1d	⊢ ( 𝑥 = ( 𝑈 ‘ 𝐿 ) → ( ( 𝑥 supp 0 ) ⊆ 𝐽 ↔ ( ( 𝑈 ‘ 𝐿 ) supp 0 ) ⊆ 𝐽 ) )
42	41 7	elrab2	⊢ ( ( 𝑈 ‘ 𝐿 ) ∈ 𝐶 ↔ ( ( 𝑈 ‘ 𝐿 ) ∈ 𝐵 ∧ ( ( 𝑈 ‘ 𝐿 ) supp 0 ) ⊆ 𝐽 ) )
43	26 39 42	sylanbrc	⊢ ( 𝜑 → ( 𝑈 ‘ 𝐿 ) ∈ 𝐶 )
44		eqid	⊢ ( Scalar ‘ 𝐹 ) = ( Scalar ‘ 𝐹 )
45		eqid	⊢ ( Base ‘ ( Scalar ‘ 𝐹 ) ) = ( Base ‘ ( Scalar ‘ 𝐹 ) )
46	44 5 45 15	lssvscl	⊢ ( ( ( 𝐹 ∈ LMod ∧ 𝐶 ∈ ( LSubSp ‘ 𝐹 ) ) ∧ ( 𝑋 ∈ ( Base ‘ ( Scalar ‘ 𝐹 ) ) ∧ ( 𝑈 ‘ 𝐿 ) ∈ 𝐶 ) ) → ( 𝑋 · ( 𝑈 ‘ 𝐿 ) ) ∈ 𝐶 )
47	14 17 22 43 46	syl22anc	⊢ ( 𝜑 → ( 𝑋 · ( 𝑈 ‘ 𝐿 ) ) ∈ 𝐶 )