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