Theorem lsppratlem2

Description: Lemma for lspprat . Show that if X and Y are both in ( N{ x , y } ) (which will be our goal for each of the two cases above), then ( N{ X , Y } ) C_ U , contradicting the hypothesis for U . (Contributed by NM, 29-Aug-2014) (Revised by Mario Carneiro, 5-Sep-2014)

	Ref	Expression
Hypotheses	lspprat.v	$$⊢V={\mathrm{Base}}_W$$
	lspprat.s	$$⊢S=\mathrm{LSubSp}\left(W\right)$$
	lspprat.n	$$⊢N=\mathrm{LSpan}\left(W\right)$$
	lspprat.w	$$⊢\phi \to W\in \mathrm{LVec}$$
	lspprat.u	$$⊢\phi \to U\in S$$
	lspprat.x	$$⊢\phi \to X\in V$$
	lspprat.y	$$⊢\phi \to Y\in V$$
	lspprat.p	$$⊢\phi \to U\subset N\left(\left\{X,Y\right\}\right)$$
	lsppratlem1.o	$$⊢\underset{\dot{}}{0}=0_W$$
	lsppratlem1.x2	$$⊢\phi \to x\in \left(U\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
	lsppratlem1.y2	$$⊢\phi \to y\in \left(U\setminus N\left(\left\{x\right\}\right)\right)$$
	lsppratlem2.x1	$$⊢\phi \to X\in N\left(\left\{x,y\right\}\right)$$
	lsppratlem2.y1	$$⊢\phi \to Y\in N\left(\left\{x,y\right\}\right)$$
Assertion	lsppratlem2	$$⊢\phi \to N\left(\left\{X,Y\right\}\right)\subseteq U$$

Proof

Step	Hyp	Ref	Expression
1		lspprat.v	$$⊢V={\mathrm{Base}}_W$$
2		lspprat.s	$$⊢S=\mathrm{LSubSp}\left(W\right)$$
3		lspprat.n	$$⊢N=\mathrm{LSpan}\left(W\right)$$
4		lspprat.w	$$⊢\phi \to W\in \mathrm{LVec}$$
5		lspprat.u	$$⊢\phi \to U\in S$$
6		lspprat.x	$$⊢\phi \to X\in V$$
7		lspprat.y	$$⊢\phi \to Y\in V$$
8		lspprat.p	$$⊢\phi \to U\subset N\left(\left\{X,Y\right\}\right)$$
9		lsppratlem1.o	$$⊢\underset{\dot{}}{0}=0_W$$
10		lsppratlem1.x2	$$⊢\phi \to x\in \left(U\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
11		lsppratlem1.y2	$$⊢\phi \to y\in \left(U\setminus N\left(\left\{x\right\}\right)\right)$$
12		lsppratlem2.x1	$$⊢\phi \to X\in N\left(\left\{x,y\right\}\right)$$
13		lsppratlem2.y1	$$⊢\phi \to Y\in N\left(\left\{x,y\right\}\right)$$
14		lveclmod	$$⊢W\in \mathrm{LVec}\to W\in \mathrm{LMod}$$
15	4 14	syl	$$⊢\phi \to W\in \mathrm{LMod}$$
16	10	eldifad	$$⊢\phi \to x\in U$$
17	11	eldifad	$$⊢\phi \to y\in U$$
18	16 17	prssd	$$⊢\phi \to \left\{x,y\right\}\subseteq U$$
19	1 2	lssss	$$⊢U\in S\to U\subseteq V$$
20	5 19	syl	$$⊢\phi \to U\subseteq V$$
21	18 20	sstrd	$$⊢\phi \to \left\{x,y\right\}\subseteq V$$
22	1 2 3	lspcl	$$⊢\left(W\in \mathrm{LMod}\wedge \left\{x,y\right\}\subseteq V\right)\to N\left(\left\{x,y\right\}\right)\in S$$
23	15 21 22	syl2anc	$$⊢\phi \to N\left(\left\{x,y\right\}\right)\in S$$
24	2 3 15 23 12 13	lspprss	$$⊢\phi \to N\left(\left\{X,Y\right\}\right)\subseteq N\left(\left\{x,y\right\}\right)$$
25	2 3 15 5 16 17	lspprss	$$⊢\phi \to N\left(\left\{x,y\right\}\right)\subseteq U$$
26	24 25	sstrd	$$⊢\phi \to N\left(\left\{X,Y\right\}\right)\subseteq U$$