This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 = ( 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 )