Metamath Proof Explorer

Theorem lsppratlem3

Description: Lemma for lspprat . In the first case of lsppratlem1 , since x e/ ( N(/) ) , also Y e. ( N{ x } ) , and since y e. ( N{ X , Y } ) C_ ( N{ X , x } ) and y e/ ( N{ x } ) , we have X e. ( N{ x , y } ) as desired. (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 } ) ) )
lsppratlem3.x3 
|- ( ph -> x e. ( N ` { Y } ) )
Assertion lsppratlem3 
|- ( 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 lsppratlem3.x3 
 |-  ( ph -> x e. ( N ` { Y } ) )
13 lveclmod 
 |-  ( W e. LVec -> W e. LMod )
14 4 13 syl 
 |-  ( ph -> W e. LMod )
15 7 snssd 
 |-  ( ph -> { Y } C_ V )
16 1 3 lspssv 
 |-  ( ( W e. LMod /\ { Y } C_ V ) -> ( N ` { Y } ) C_ V )
17 14 15 16 syl2anc 
 |-  ( ph -> ( N ` { Y } ) C_ V )
18 17 12 sseldd 
 |-  ( ph -> x e. V )
19 18 snssd 
 |-  ( ph -> { x } C_ V )
20 8 pssssd 
 |-  ( ph -> U C_ ( N ` { X , Y } ) )
21 6 snssd 
 |-  ( ph -> { X } C_ V )
22 19 21 unssd 
 |-  ( ph -> ( { x } u. { X } ) C_ V )
23 1 2 3 lspcl 
 |-  ( ( W e. LMod /\ ( { x } u. { X } ) C_ V ) -> ( N ` ( { x } u. { X } ) ) e. S )
24 14 22 23 syl2anc 
 |-  ( ph -> ( N ` ( { x } u. { X } ) ) e. S )
25 df-pr 
 |-  { X , Y } = ( { X } u. { Y } )
26 1 3 lspssid 
 |-  ( ( W e. LMod /\ ( { x } u. { X } ) C_ V ) -> ( { x } u. { X } ) C_ ( N ` ( { x } u. { X } ) ) )
27 14 22 26 syl2anc 
 |-  ( ph -> ( { x } u. { X } ) C_ ( N ` ( { x } u. { X } ) ) )
28 27 unssbd 
 |-  ( ph -> { X } C_ ( N ` ( { x } u. { X } ) ) )
29 ssun1 
 |-  { x } C_ ( { x } u. { X } )
30 29 a1i 
 |-  ( ph -> { x } C_ ( { x } u. { X } ) )
31 1 3 lspss 
 |-  ( ( W e. LMod /\ ( { x } u. { X } ) C_ V /\ { x } C_ ( { x } u. { X } ) ) -> ( N ` { x } ) C_ ( N ` ( { x } u. { X } ) ) )
32 14 22 30 31 syl3anc 
 |-  ( ph -> ( N ` { x } ) C_ ( N ` ( { x } u. { X } ) ) )
33 0ss 
 |-  (/) C_ V
34 33 a1i 
 |-  ( ph -> (/) C_ V )
35 uncom 
 |-  ( (/) u. { Y } ) = ( { Y } u. (/) )
36 un0 
 |-  ( { Y } u. (/) ) = { Y }
37 35 36 eqtri 
 |-  ( (/) u. { Y } ) = { Y }
38 37 fveq2i 
 |-  ( N ` ( (/) u. { Y } ) ) = ( N ` { Y } )
39 12 38 eleqtrrdi 
 |-  ( ph -> x e. ( N ` ( (/) u. { Y } ) ) )
40 10 eldifbd 
 |-  ( ph -> -. x e. { .0. } )
41 9 3 lsp0 
 |-  ( W e. LMod -> ( N ` (/) ) = { .0. } )
42 14 41 syl 
 |-  ( ph -> ( N ` (/) ) = { .0. } )
43 40 42 neleqtrrd 
 |-  ( ph -> -. x e. ( N ` (/) ) )
44 39 43 eldifd 
 |-  ( ph -> x e. ( ( N ` ( (/) u. { Y } ) ) \ ( N ` (/) ) ) )
45 1 2 3 lspsolv 
 |-  ( ( W e. LVec /\ ( (/) C_ V /\ Y e. V /\ x e. ( ( N ` ( (/) u. { Y } ) ) \ ( N ` (/) ) ) ) ) -> Y e. ( N ` ( (/) u. { x } ) ) )
46 4 34 7 44 45 syl13anc 
 |-  ( ph -> Y e. ( N ` ( (/) u. { x } ) ) )
47 uncom 
 |-  ( (/) u. { x } ) = ( { x } u. (/) )
48 un0 
 |-  ( { x } u. (/) ) = { x }
49 47 48 eqtri 
 |-  ( (/) u. { x } ) = { x }
50 49 fveq2i 
 |-  ( N ` ( (/) u. { x } ) ) = ( N ` { x } )
51 46 50 eleqtrdi 
 |-  ( ph -> Y e. ( N ` { x } ) )
52 32 51 sseldd 
 |-  ( ph -> Y e. ( N ` ( { x } u. { X } ) ) )
53 52 snssd 
 |-  ( ph -> { Y } C_ ( N ` ( { x } u. { X } ) ) )
54 28 53 unssd 
 |-  ( ph -> ( { X } u. { Y } ) C_ ( N ` ( { x } u. { X } ) ) )
55 25 54 eqsstrid 
 |-  ( ph -> { X , Y } C_ ( N ` ( { x } u. { X } ) ) )
56 2 3 lspssp 
 |-  ( ( W e. LMod /\ ( N ` ( { x } u. { X } ) ) e. S /\ { X , Y } C_ ( N ` ( { x } u. { X } ) ) ) -> ( N ` { X , Y } ) C_ ( N ` ( { x } u. { X } ) ) )
57 14 24 55 56 syl3anc 
 |-  ( ph -> ( N ` { X , Y } ) C_ ( N ` ( { x } u. { X } ) ) )
58 20 57 sstrd 
 |-  ( ph -> U C_ ( N ` ( { x } u. { X } ) ) )
59 58 ssdifd 
 |-  ( ph -> ( U \ ( N ` { x } ) ) C_ ( ( N ` ( { x } u. { X } ) ) \ ( N ` { x } ) ) )
60 59 11 sseldd 
 |-  ( ph -> y e. ( ( N ` ( { x } u. { X } ) ) \ ( N ` { x } ) ) )
61 1 2 3 lspsolv 
 |-  ( ( W e. LVec /\ ( { x } C_ V /\ X e. V /\ y e. ( ( N ` ( { x } u. { X } ) ) \ ( N ` { x } ) ) ) ) -> X e. ( N ` ( { x } u. { y } ) ) )
62 4 19 6 60 61 syl13anc 
 |-  ( ph -> X e. ( N ` ( { x } u. { y } ) ) )
63 df-pr 
 |-  { x , y } = ( { x } u. { y } )
64 63 fveq2i 
 |-  ( N ` { x , y } ) = ( N ` ( { x } u. { y } ) )
65 62 64 eleqtrrdi 
 |-  ( ph -> X e. ( N ` { x , y } ) )
66 1 2 lssss 
 |-  ( U e. S -> U C_ V )
67 5 66 syl 
 |-  ( ph -> U C_ V )
68 67 ssdifssd 
 |-  ( ph -> ( U \ ( N ` { x } ) ) C_ V )
69 68 11 sseldd 
 |-  ( ph -> y e. V )
70 18 69 prssd 
 |-  ( ph -> { x , y } C_ V )
71 snsspr1 
 |-  { x } C_ { x , y }
72 71 a1i 
 |-  ( ph -> { x } C_ { x , y } )
73 1 3 lspss 
 |-  ( ( W e. LMod /\ { x , y } C_ V /\ { x } C_ { x , y } ) -> ( N ` { x } ) C_ ( N ` { x , y } ) )
74 14 70 72 73 syl3anc 
 |-  ( ph -> ( N ` { x } ) C_ ( N ` { x , y } ) )
75 74 51 sseldd 
 |-  ( ph -> Y e. ( N ` { x , y } ) )
76 65 75 jca 
 |-  ( ph -> ( X e. ( N ` { x , y } ) /\ Y e. ( N ` { x , y } ) ) )