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 } ) ) )