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	$$⊢F=R\mathrm{freeLMod}I$$
	frlmssuvc1.u	$$⊢U=R\mathrm{unitVec}I$$
	frlmssuvc1.b	$$⊢B={\mathrm{Base}}_F$$
	frlmssuvc1.k	$$⊢K={\mathrm{Base}}_R$$
	frlmssuvc1.t	$$⊢\underset{\dot{}}{·}={\cdot }_F$$
	frlmssuvc1.z	$$⊢\underset{\dot{}}{0}=0_R$$
	frlmssuvc1.c	$$⊢C=\left\{x\in B|x\mathrm{supp}\underset{\dot{}}{0}\subseteq J\right\}$$
	frlmssuvc1.r	$$⊢\phi \to R\in \mathrm{Ring}$$
	frlmssuvc1.i	$$⊢\phi \to I\in V$$
	frlmssuvc1.j	$$⊢\phi \to J\subseteq I$$
	frlmssuvc1.l	$$⊢\phi \to L\in J$$
	frlmssuvc1.x	$$⊢\phi \to X\in K$$
Assertion	frlmssuvc1	$$⊢\phi \to X\underset{\dot{}}{·}U\left(L\right)\in C$$

Proof

Step	Hyp	Ref	Expression
1		frlmssuvc1.f	$$⊢F=R\mathrm{freeLMod}I$$
2		frlmssuvc1.u	$$⊢U=R\mathrm{unitVec}I$$
3		frlmssuvc1.b	$$⊢B={\mathrm{Base}}_F$$
4		frlmssuvc1.k	$$⊢K={\mathrm{Base}}_R$$
5		frlmssuvc1.t	$$⊢\underset{\dot{}}{·}={\cdot }_F$$
6		frlmssuvc1.z	$$⊢\underset{\dot{}}{0}=0_R$$
7		frlmssuvc1.c	$$⊢C=\left\{x\in B|x\mathrm{supp}\underset{\dot{}}{0}\subseteq J\right\}$$
8		frlmssuvc1.r	$$⊢\phi \to R\in \mathrm{Ring}$$
9		frlmssuvc1.i	$$⊢\phi \to I\in V$$
10		frlmssuvc1.j	$$⊢\phi \to J\subseteq I$$
11		frlmssuvc1.l	$$⊢\phi \to L\in J$$
12		frlmssuvc1.x	$$⊢\phi \to X\in K$$
13	1	frlmlmod	$$⊢\left(R\in \mathrm{Ring}\wedge I\in V\right)\to F\in \mathrm{LMod}$$
14	8 9 13	syl2anc	$$⊢\phi \to F\in \mathrm{LMod}$$
15		eqid	$$⊢\mathrm{LSubSp}\left(F\right)=\mathrm{LSubSp}\left(F\right)$$
16	1 15 3 6 7	frlmsslss2	$$⊢\left(R\in \mathrm{Ring}\wedge I\in V\wedge J\subseteq I\right)\to C\in \mathrm{LSubSp}\left(F\right)$$
17	8 9 10 16	syl3anc	$$⊢\phi \to C\in \mathrm{LSubSp}\left(F\right)$$
18	1	frlmsca	$$⊢\left(R\in \mathrm{Ring}\wedge I\in V\right)\to R=\mathrm{Scalar}\left(F\right)$$
19	8 9 18	syl2anc	$$⊢\phi \to R=\mathrm{Scalar}\left(F\right)$$
20	19	fveq2d	$$⊢\phi \to {\mathrm{Base}}_R={\mathrm{Base}}_{\mathrm{Scalar}\left(F\right)}$$
21	4 20	syl5eq	$$⊢\phi \to K={\mathrm{Base}}_{\mathrm{Scalar}\left(F\right)}$$
22	12 21	eleqtrd	$$⊢\phi \to X\in {\mathrm{Base}}_{\mathrm{Scalar}\left(F\right)}$$
23	2 1 3	uvcff	$$⊢\left(R\in \mathrm{Ring}\wedge I\in V\right)\to U:I⟶B$$
24	8 9 23	syl2anc	$$⊢\phi \to U:I⟶B$$
25	10 11	sseldd	$$⊢\phi \to L\in I$$
26	24 25	ffvelrnd	$$⊢\phi \to U\left(L\right)\in B$$
27	1 4 3	frlmbasf	$$⊢\left(I\in V\wedge U\left(L\right)\in B\right)\to U\left(L\right):I⟶K$$
28	9 26 27	syl2anc	$$⊢\phi \to U\left(L\right):I⟶K$$
29	8	adantr	$$⊢\left(\phi \wedge x\in \left(I\setminus J\right)\right)\to R\in \mathrm{Ring}$$
30	9	adantr	$$⊢\left(\phi \wedge x\in \left(I\setminus J\right)\right)\to I\in V$$
31	25	adantr	$$⊢\left(\phi \wedge x\in \left(I\setminus J\right)\right)\to L\in I$$
32		eldifi	$$⊢x\in \left(I\setminus J\right)\to x\in I$$
33	32	adantl	$$⊢\left(\phi \wedge x\in \left(I\setminus J\right)\right)\to x\in I$$
34		disjdif	$$⊢J\cap \left(I\setminus J\right)=\varnothing$$
35		simpr	$$⊢\left(\phi \wedge x\in \left(I\setminus J\right)\right)\to x\in \left(I\setminus J\right)$$
36		disjne	$$⊢\left(J\cap \left(I\setminus J\right)=\varnothing \wedge L\in J\wedge x\in \left(I\setminus J\right)\right)\to L\ne x$$
37	34 11 35 36	mp3an2ani	$$⊢\left(\phi \wedge x\in \left(I\setminus J\right)\right)\to L\ne x$$
38	2 29 30 31 33 37 6	uvcvv0	$$⊢\left(\phi \wedge x\in \left(I\setminus J\right)\right)\to U\left(L\right)\left(x\right)=\underset{\dot{}}{0}$$
39	28 38	suppss	$$⊢\phi \to U\left(L\right)\mathrm{supp}\underset{\dot{}}{0}\subseteq J$$
40		oveq1	$$⊢x=U\left(L\right)\to x\mathrm{supp}\underset{\dot{}}{0}=U\left(L\right)\mathrm{supp}\underset{\dot{}}{0}$$
41	40	sseq1d	$$⊢x=U\left(L\right)\to \left(x\mathrm{supp}\underset{\dot{}}{0}\subseteq J\leftrightarrow U\left(L\right)\mathrm{supp}\underset{\dot{}}{0}\subseteq J\right)$$
42	41 7	elrab2	$$⊢U\left(L\right)\in C\leftrightarrow \left(U\left(L\right)\in B\wedge U\left(L\right)\mathrm{supp}\underset{\dot{}}{0}\subseteq J\right)$$
43	26 39 42	sylanbrc	$$⊢\phi \to U\left(L\right)\in C$$
44		eqid	$$⊢\mathrm{Scalar}\left(F\right)=\mathrm{Scalar}\left(F\right)$$
45		eqid	$$⊢{\mathrm{Base}}_{\mathrm{Scalar}\left(F\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left(F\right)}$$
46	44 5 45 15	lssvscl	$$⊢\left(\left(F\in \mathrm{LMod}\wedge C\in \mathrm{LSubSp}\left(F\right)\right)\wedge \left(X\in {\mathrm{Base}}_{\mathrm{Scalar}\left(F\right)}\wedge U\left(L\right)\in C\right)\right)\to X\underset{\dot{}}{·}U\left(L\right)\in C$$
47	14 17 22 43 46	syl22anc	$$⊢\phi \to X\underset{\dot{}}{·}U\left(L\right)\in C$$