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