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 = ( Base ` W )
	lspprat.s	\|- S = ( LSubSp ` W )
	lspprat.n	\|- N = ( LSpan ` W )
	lspprat.w	\|- ( ph -> W e. LVec )
	lspprat.u	\|- ( ph -> U e. S )
	lspprat.x	\|- ( ph -> X e. V )
	lspprat.y	\|- ( ph -> Y e. V )
	lspprat.p	\|- ( ph -> U C. ( N ` { X , Y } ) )
	lsppratlem1.o	\|- .0. = ( 0g ` W )
	lsppratlem1.x2	\|- ( ph -> x e. ( U \ { .0. } ) )
	lsppratlem1.y2	\|- ( ph -> y e. ( U \ ( N ` { x } ) ) )
	lsppratlem2.x1	\|- ( ph -> X e. ( N ` { x , y } ) )
	lsppratlem2.y1	\|- ( ph -> Y e. ( N ` { x , y } ) )
Assertion	lsppratlem2	\|- ( ph -> ( N ` { X , Y } ) C_ U )

Proof

Step	Hyp	Ref	Expression
1		lspprat.v	\|- V = ( Base ` W )
2		lspprat.s	\|- S = ( LSubSp ` W )
3		lspprat.n	\|- N = ( LSpan ` W )
4		lspprat.w	\|- ( ph -> W e. LVec )
5		lspprat.u	\|- ( ph -> U e. S )
6		lspprat.x	\|- ( ph -> X e. V )
7		lspprat.y	\|- ( ph -> Y e. V )
8		lspprat.p	\|- ( ph -> U C. ( N ` { X , Y } ) )
9		lsppratlem1.o	\|- .0. = ( 0g ` W )
10		lsppratlem1.x2	\|- ( ph -> x e. ( U \ { .0. } ) )
11		lsppratlem1.y2	\|- ( ph -> y e. ( U \ ( N ` { x } ) ) )
12		lsppratlem2.x1	\|- ( ph -> X e. ( N ` { x , y } ) )
13		lsppratlem2.y1	\|- ( ph -> Y e. ( N ` { x , y } ) )
14		lveclmod	\|- ( W e. LVec -> W e. LMod )
15	4 14	syl	\|- ( ph -> W e. LMod )
16	10	eldifad	\|- ( ph -> x e. U )
17	11	eldifad	\|- ( ph -> y e. U )
18	16 17	prssd	\|- ( ph -> { x , y } C_ U )
19	1 2	lssss	\|- ( U e. S -> U C_ V )
20	5 19	syl	\|- ( ph -> U C_ V )
21	18 20	sstrd	\|- ( ph -> { x , y } C_ V )
22	1 2 3	lspcl	\|- ( ( W e. LMod /\ { x , y } C_ V ) -> ( N ` { x , y } ) e. S )
23	15 21 22	syl2anc	\|- ( ph -> ( N ` { x , y } ) e. S )
24	2 3 15 23 12 13	lspprss	\|- ( ph -> ( N ` { X , Y } ) C_ ( N ` { x , y } ) )
25	2 3 15 5 16 17	lspprss	\|- ( ph -> ( N ` { x , y } ) C_ U )
26	24 25	sstrd	\|- ( ph -> ( N ` { X , Y } ) C_ U )

Metamath Proof Explorer

Theorem lsppratlem2

Proof