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	$$⊢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$$
	frlmssuvc2.l	$$⊢\phi \to L\in \left(I\setminus J\right)$$
	frlmssuvc2.x	$$⊢\phi \to X\in \left(K\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
Assertion	frlmssuvc2	$$⊢\phi \to \neg 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		frlmssuvc2.l	$$⊢\phi \to L\in \left(I\setminus J\right)$$
12		frlmssuvc2.x	$$⊢\phi \to X\in \left(K\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
13		fveq2	$$⊢x=L\to \left(X\underset{\dot{}}{·}U\left(L\right)\right)\left(x\right)=\left(X\underset{\dot{}}{·}U\left(L\right)\right)\left(L\right)$$
14	13	neeq1d	$$⊢x=L\to \left(\left(X\underset{\dot{}}{·}U\left(L\right)\right)\left(x\right)\ne \underset{\dot{}}{0}\leftrightarrow \left(X\underset{\dot{}}{·}U\left(L\right)\right)\left(L\right)\ne \underset{\dot{}}{0}\right)$$
15	11	eldifad	$$⊢\phi \to L\in I$$
16	12	eldifad	$$⊢\phi \to X\in K$$
17	2 1 3	uvcff	$$⊢\left(R\in \mathrm{Ring}\wedge I\in V\right)\to U:I⟶B$$
18	8 9 17	syl2anc	$$⊢\phi \to U:I⟶B$$
19	18 15	ffvelrnd	$$⊢\phi \to U\left(L\right)\in B$$
20		eqid	$$⊢{\cdot }_R={\cdot }_R$$
21	1 3 4 9 16 19 15 5 20	frlmvscaval	$$⊢\phi \to \left(X\underset{\dot{}}{·}U\left(L\right)\right)\left(L\right)=X{\cdot }_{R}U\left(L\right)\left(L\right)$$
22		eqid	$$⊢1_R=1_R$$
23	2 8 9 15 22	uvcvv1	$$⊢\phi \to U\left(L\right)\left(L\right)=1_R$$
24	23	oveq2d	$$⊢\phi \to X{\cdot }_{R}U\left(L\right)\left(L\right)=X{\cdot }_R{1}_R$$
25	4 20 22	ringridm	$$⊢\left(R\in \mathrm{Ring}\wedge X\in K\right)\to X{\cdot }_R{1}_R=X$$
26	8 16 25	syl2anc	$$⊢\phi \to X{\cdot }_R{1}_R=X$$
27	21 24 26	3eqtrd	$$⊢\phi \to \left(X\underset{\dot{}}{·}U\left(L\right)\right)\left(L\right)=X$$
28		eldifsni	$$⊢X\in \left(K\setminus \left\{\underset{\dot{}}{0}\right\}\right)\to X\ne \underset{\dot{}}{0}$$
29	12 28	syl	$$⊢\phi \to X\ne \underset{\dot{}}{0}$$
30	27 29	eqnetrd	$$⊢\phi \to \left(X\underset{\dot{}}{·}U\left(L\right)\right)\left(L\right)\ne \underset{\dot{}}{0}$$
31	14 15 30	elrabd	$$⊢\phi \to L\in \left\{x\in I|\left(X\underset{\dot{}}{·}U\left(L\right)\right)\left(x\right)\ne \underset{\dot{}}{0}\right\}$$
32	11	eldifbd	$$⊢\phi \to \neg L\in J$$
33		nelss	$$⊢\left(L\in \left\{x\in I|\left(X\underset{\dot{}}{·}U\left(L\right)\right)\left(x\right)\ne \underset{\dot{}}{0}\right\}\wedge \neg L\in J\right)\to \neg \left\{x\in I|\left(X\underset{\dot{}}{·}U\left(L\right)\right)\left(x\right)\ne \underset{\dot{}}{0}\right\}\subseteq J$$
34	31 32 33	syl2anc	$$⊢\phi \to \neg \left\{x\in I|\left(X\underset{\dot{}}{·}U\left(L\right)\right)\left(x\right)\ne \underset{\dot{}}{0}\right\}\subseteq J$$
35	1	frlmlmod	$$⊢\left(R\in \mathrm{Ring}\wedge I\in V\right)\to F\in \mathrm{LMod}$$
36	8 9 35	syl2anc	$$⊢\phi \to F\in \mathrm{LMod}$$
37	1	frlmsca	$$⊢\left(R\in \mathrm{Ring}\wedge I\in V\right)\to R=\mathrm{Scalar}\left(F\right)$$
38	8 9 37	syl2anc	$$⊢\phi \to R=\mathrm{Scalar}\left(F\right)$$
39	38	fveq2d	$$⊢\phi \to {\mathrm{Base}}_R={\mathrm{Base}}_{\mathrm{Scalar}\left(F\right)}$$
40	4 39	syl5eq	$$⊢\phi \to K={\mathrm{Base}}_{\mathrm{Scalar}\left(F\right)}$$
41	16 40	eleqtrd	$$⊢\phi \to X\in {\mathrm{Base}}_{\mathrm{Scalar}\left(F\right)}$$
42		eqid	$$⊢\mathrm{Scalar}\left(F\right)=\mathrm{Scalar}\left(F\right)$$
43		eqid	$$⊢{\mathrm{Base}}_{\mathrm{Scalar}\left(F\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left(F\right)}$$
44	3 42 5 43	lmodvscl	$$⊢\left(F\in \mathrm{LMod}\wedge X\in {\mathrm{Base}}_{\mathrm{Scalar}\left(F\right)}\wedge U\left(L\right)\in B\right)\to X\underset{\dot{}}{·}U\left(L\right)\in B$$
45	36 41 19 44	syl3anc	$$⊢\phi \to X\underset{\dot{}}{·}U\left(L\right)\in B$$
46	1 4 3	frlmbasf	$$⊢\left(I\in V\wedge X\underset{\dot{}}{·}U\left(L\right)\in B\right)\to \left(X\underset{\dot{}}{·}U\left(L\right)\right):I⟶K$$
47	9 45 46	syl2anc	$$⊢\phi \to \left(X\underset{\dot{}}{·}U\left(L\right)\right):I⟶K$$
48	47	ffnd	$$⊢\phi \to \left(X\underset{\dot{}}{·}U\left(L\right)\right)FnI$$
49	6	fvexi	$$⊢\underset{\dot{}}{0}\in \mathrm{V}$$
50	49	a1i	$$⊢\phi \to \underset{\dot{}}{0}\in \mathrm{V}$$
51		suppvalfn	$$⊢\left(\left(X\underset{\dot{}}{·}U\left(L\right)\right)FnI\wedge I\in V\wedge \underset{\dot{}}{0}\in \mathrm{V}\right)\to \left(X\underset{\dot{}}{·}U\left(L\right)\right)\mathrm{supp}\underset{\dot{}}{0}=\left\{x\in I|\left(X\underset{\dot{}}{·}U\left(L\right)\right)\left(x\right)\ne \underset{\dot{}}{0}\right\}$$
52	48 9 50 51	syl3anc	$$⊢\phi \to \left(X\underset{\dot{}}{·}U\left(L\right)\right)\mathrm{supp}\underset{\dot{}}{0}=\left\{x\in I|\left(X\underset{\dot{}}{·}U\left(L\right)\right)\left(x\right)\ne \underset{\dot{}}{0}\right\}$$
53	52	sseq1d	$$⊢\phi \to \left(\left(X\underset{\dot{}}{·}U\left(L\right)\right)\mathrm{supp}\underset{\dot{}}{0}\subseteq J\leftrightarrow \left\{x\in I|\left(X\underset{\dot{}}{·}U\left(L\right)\right)\left(x\right)\ne \underset{\dot{}}{0}\right\}\subseteq J\right)$$
54	34 53	mtbird	$$⊢\phi \to \neg \left(X\underset{\dot{}}{·}U\left(L\right)\right)\mathrm{supp}\underset{\dot{}}{0}\subseteq J$$
55	54	intnand	$$⊢\phi \to \neg \left(X\underset{\dot{}}{·}U\left(L\right)\in B\wedge \left(X\underset{\dot{}}{·}U\left(L\right)\right)\mathrm{supp}\underset{\dot{}}{0}\subseteq J\right)$$
56		oveq1	$$⊢x=X\underset{\dot{}}{·}U\left(L\right)\to x\mathrm{supp}\underset{\dot{}}{0}=\left(X\underset{\dot{}}{·}U\left(L\right)\right)\mathrm{supp}\underset{\dot{}}{0}$$
57	56	sseq1d	$$⊢x=X\underset{\dot{}}{·}U\left(L\right)\to \left(x\mathrm{supp}\underset{\dot{}}{0}\subseteq J\leftrightarrow \left(X\underset{\dot{}}{·}U\left(L\right)\right)\mathrm{supp}\underset{\dot{}}{0}\subseteq J\right)$$
58	57 7	elrab2	$$⊢X\underset{\dot{}}{·}U\left(L\right)\in C\leftrightarrow \left(X\underset{\dot{}}{·}U\left(L\right)\in B\wedge \left(X\underset{\dot{}}{·}U\left(L\right)\right)\mathrm{supp}\underset{\dot{}}{0}\subseteq J\right)$$
59	55 58	sylnibr	$$⊢\phi \to \neg X\underset{\dot{}}{·}U\left(L\right)\in C$$