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