Metamath Proof Explorer

Theorem lsppratlem4

Description: Lemma for lspprat . In the second case of lsppratlem1 , y e. ( N{ X , Y } ) C_ ( N{ x , Y } ) and y e/ ( N{ x } ) implies Y e. ( N{ x , y } ) and thus X e. ( N{ x , Y } ) C_ ( N{ x , y } ) as well. (Contributed by NM, 29-Aug-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 } ) ) )
lsppratlem4.x3 
|- ( ph -> X e. ( N ` { x , Y } ) )
Assertion lsppratlem4 
|- ( ph -> ( X e. ( N ` { x , y } ) /\ Y e. ( N ` { x , y } ) ) )

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 lsppratlem4.x3 
 |-  ( ph -> X e. ( N ` { x , Y } ) )
13 lveclmod 
 |-  ( W e. LVec -> W e. LMod )
14 4 13 syl 
 |-  ( ph -> W e. LMod )
15 1 2 lssss 
 |-  ( U e. S -> U C_ V )
16 5 15 syl 
 |-  ( ph -> U C_ V )
17 16 ssdifssd 
 |-  ( ph -> ( U \ { .0. } ) C_ V )
18 17 10 sseldd 
 |-  ( ph -> x e. V )
19 16 ssdifssd 
 |-  ( ph -> ( U \ ( N ` { x } ) ) C_ V )
20 19 11 sseldd 
 |-  ( ph -> y e. V )
21 1 2 3 14 18 20 lspprcl 
 |-  ( ph -> ( N ` { x , y } ) e. S )
22 df-pr 
 |-  { x , Y } = ( { x } u. { Y } )
23 snsspr1 
 |-  { x } C_ { x , y }
24 18 20 prssd 
 |-  ( ph -> { x , y } C_ V )
25 1 3 lspssid 
 |-  ( ( W e. LMod /\ { x , y } C_ V ) -> { x , y } C_ ( N ` { x , y } ) )
26 14 24 25 syl2anc 
 |-  ( ph -> { x , y } C_ ( N ` { x , y } ) )
27 23 26 sstrid 
 |-  ( ph -> { x } C_ ( N ` { x , y } ) )
28 18 snssd 
 |-  ( ph -> { x } C_ V )
29 8 pssssd 
 |-  ( ph -> U C_ ( N ` { X , Y } ) )
30 1 2 3 14 18 7 lspprcl 
 |-  ( ph -> ( N ` { x , Y } ) e. S )
31 df-pr 
 |-  { X , Y } = ( { X } u. { Y } )
32 12 snssd 
 |-  ( ph -> { X } C_ ( N ` { x , Y } ) )
33 snsspr2 
 |-  { Y } C_ { x , Y }
34 18 7 prssd 
 |-  ( ph -> { x , Y } C_ V )
35 1 3 lspssid 
 |-  ( ( W e. LMod /\ { x , Y } C_ V ) -> { x , Y } C_ ( N ` { x , Y } ) )
36 14 34 35 syl2anc 
 |-  ( ph -> { x , Y } C_ ( N ` { x , Y } ) )
37 33 36 sstrid 
 |-  ( ph -> { Y } C_ ( N ` { x , Y } ) )
38 32 37 unssd 
 |-  ( ph -> ( { X } u. { Y } ) C_ ( N ` { x , Y } ) )
39 31 38 eqsstrid 
 |-  ( ph -> { X , Y } C_ ( N ` { x , Y } ) )
40 2 3 lspssp 
 |-  ( ( W e. LMod /\ ( N ` { x , Y } ) e. S /\ { X , Y } C_ ( N ` { x , Y } ) ) -> ( N ` { X , Y } ) C_ ( N ` { x , Y } ) )
41 14 30 39 40 syl3anc 
 |-  ( ph -> ( N ` { X , Y } ) C_ ( N ` { x , Y } ) )
42 29 41 sstrd 
 |-  ( ph -> U C_ ( N ` { x , Y } ) )
43 22 fveq2i 
 |-  ( N ` { x , Y } ) = ( N ` ( { x } u. { Y } ) )
44 42 43 sseqtrdi 
 |-  ( ph -> U C_ ( N ` ( { x } u. { Y } ) ) )
45 44 ssdifd 
 |-  ( ph -> ( U \ ( N ` { x } ) ) C_ ( ( N ` ( { x } u. { Y } ) ) \ ( N ` { x } ) ) )
46 45 11 sseldd 
 |-  ( ph -> y e. ( ( N ` ( { x } u. { Y } ) ) \ ( N ` { x } ) ) )
47 1 2 3 lspsolv 
 |-  ( ( W e. LVec /\ ( { x } C_ V /\ Y e. V /\ y e. ( ( N ` ( { x } u. { Y } ) ) \ ( N ` { x } ) ) ) ) -> Y e. ( N ` ( { x } u. { y } ) ) )
48 4 28 7 46 47 syl13anc 
 |-  ( ph -> Y e. ( N ` ( { x } u. { y } ) ) )
49 df-pr 
 |-  { x , y } = ( { x } u. { y } )
50 49 fveq2i 
 |-  ( N ` { x , y } ) = ( N ` ( { x } u. { y } ) )
51 48 50 eleqtrrdi 
 |-  ( ph -> Y e. ( N ` { x , y } ) )
52 51 snssd 
 |-  ( ph -> { Y } C_ ( N ` { x , y } ) )
53 27 52 unssd 
 |-  ( ph -> ( { x } u. { Y } ) C_ ( N ` { x , y } ) )
54 22 53 eqsstrid 
 |-  ( ph -> { x , Y } C_ ( N ` { x , y } ) )
55 2 3 lspssp 
 |-  ( ( W e. LMod /\ ( N ` { x , y } ) e. S /\ { x , Y } C_ ( N ` { x , y } ) ) -> ( N ` { x , Y } ) C_ ( N ` { x , y } ) )
56 14 21 54 55 syl3anc 
 |-  ( ph -> ( N ` { x , Y } ) C_ ( N ` { x , y } ) )
57 56 12 sseldd 
 |-  ( ph -> X e. ( N ` { x , y } ) )
58 57 51 jca 
 |-  ( ph -> ( X e. ( N ` { x , y } ) /\ Y e. ( N ` { x , y } ) ) )