Step |
Hyp |
Ref |
Expression |
1 |
|
lssats.s |
|- S = ( LSubSp ` W ) |
2 |
|
lssats.n |
|- N = ( LSpan ` W ) |
3 |
|
lssats.a |
|- A = ( LSAtoms ` W ) |
4 |
|
eleq1 |
|- ( y = ( 0g ` W ) -> ( y e. ( N ` U. { x e. A | x C_ U } ) <-> ( 0g ` W ) e. ( N ` U. { x e. A | x C_ U } ) ) ) |
5 |
|
simplll |
|- ( ( ( ( W e. LMod /\ U e. S ) /\ y e. U ) /\ y =/= ( 0g ` W ) ) -> W e. LMod ) |
6 |
|
simpllr |
|- ( ( ( ( W e. LMod /\ U e. S ) /\ y e. U ) /\ y =/= ( 0g ` W ) ) -> U e. S ) |
7 |
|
simplr |
|- ( ( ( ( W e. LMod /\ U e. S ) /\ y e. U ) /\ y =/= ( 0g ` W ) ) -> y e. U ) |
8 |
|
eqid |
|- ( Base ` W ) = ( Base ` W ) |
9 |
8 1
|
lssel |
|- ( ( U e. S /\ y e. U ) -> y e. ( Base ` W ) ) |
10 |
6 7 9
|
syl2anc |
|- ( ( ( ( W e. LMod /\ U e. S ) /\ y e. U ) /\ y =/= ( 0g ` W ) ) -> y e. ( Base ` W ) ) |
11 |
8 1 2
|
lspsncl |
|- ( ( W e. LMod /\ y e. ( Base ` W ) ) -> ( N ` { y } ) e. S ) |
12 |
5 10 11
|
syl2anc |
|- ( ( ( ( W e. LMod /\ U e. S ) /\ y e. U ) /\ y =/= ( 0g ` W ) ) -> ( N ` { y } ) e. S ) |
13 |
1 2
|
lspid |
|- ( ( W e. LMod /\ ( N ` { y } ) e. S ) -> ( N ` ( N ` { y } ) ) = ( N ` { y } ) ) |
14 |
5 12 13
|
syl2anc |
|- ( ( ( ( W e. LMod /\ U e. S ) /\ y e. U ) /\ y =/= ( 0g ` W ) ) -> ( N ` ( N ` { y } ) ) = ( N ` { y } ) ) |
15 |
1 3
|
lsatlss |
|- ( W e. LMod -> A C_ S ) |
16 |
15
|
adantr |
|- ( ( W e. LMod /\ U e. S ) -> A C_ S ) |
17 |
|
rabss2 |
|- ( A C_ S -> { x e. A | x C_ U } C_ { x e. S | x C_ U } ) |
18 |
|
uniss |
|- ( { x e. A | x C_ U } C_ { x e. S | x C_ U } -> U. { x e. A | x C_ U } C_ U. { x e. S | x C_ U } ) |
19 |
16 17 18
|
3syl |
|- ( ( W e. LMod /\ U e. S ) -> U. { x e. A | x C_ U } C_ U. { x e. S | x C_ U } ) |
20 |
|
unimax |
|- ( U e. S -> U. { x e. S | x C_ U } = U ) |
21 |
8 1
|
lssss |
|- ( U e. S -> U C_ ( Base ` W ) ) |
22 |
20 21
|
eqsstrd |
|- ( U e. S -> U. { x e. S | x C_ U } C_ ( Base ` W ) ) |
23 |
22
|
adantl |
|- ( ( W e. LMod /\ U e. S ) -> U. { x e. S | x C_ U } C_ ( Base ` W ) ) |
24 |
19 23
|
sstrd |
|- ( ( W e. LMod /\ U e. S ) -> U. { x e. A | x C_ U } C_ ( Base ` W ) ) |
25 |
24
|
ad2antrr |
|- ( ( ( ( W e. LMod /\ U e. S ) /\ y e. U ) /\ y =/= ( 0g ` W ) ) -> U. { x e. A | x C_ U } C_ ( Base ` W ) ) |
26 |
|
simpr |
|- ( ( ( ( W e. LMod /\ U e. S ) /\ y e. U ) /\ y =/= ( 0g ` W ) ) -> y =/= ( 0g ` W ) ) |
27 |
|
eqid |
|- ( 0g ` W ) = ( 0g ` W ) |
28 |
8 2 27 3
|
lsatlspsn2 |
|- ( ( W e. LMod /\ y e. ( Base ` W ) /\ y =/= ( 0g ` W ) ) -> ( N ` { y } ) e. A ) |
29 |
5 10 26 28
|
syl3anc |
|- ( ( ( ( W e. LMod /\ U e. S ) /\ y e. U ) /\ y =/= ( 0g ` W ) ) -> ( N ` { y } ) e. A ) |
30 |
1 2 5 6 7
|
lspsnel5a |
|- ( ( ( ( W e. LMod /\ U e. S ) /\ y e. U ) /\ y =/= ( 0g ` W ) ) -> ( N ` { y } ) C_ U ) |
31 |
|
sseq1 |
|- ( x = ( N ` { y } ) -> ( x C_ U <-> ( N ` { y } ) C_ U ) ) |
32 |
31
|
elrab |
|- ( ( N ` { y } ) e. { x e. A | x C_ U } <-> ( ( N ` { y } ) e. A /\ ( N ` { y } ) C_ U ) ) |
33 |
29 30 32
|
sylanbrc |
|- ( ( ( ( W e. LMod /\ U e. S ) /\ y e. U ) /\ y =/= ( 0g ` W ) ) -> ( N ` { y } ) e. { x e. A | x C_ U } ) |
34 |
|
elssuni |
|- ( ( N ` { y } ) e. { x e. A | x C_ U } -> ( N ` { y } ) C_ U. { x e. A | x C_ U } ) |
35 |
33 34
|
syl |
|- ( ( ( ( W e. LMod /\ U e. S ) /\ y e. U ) /\ y =/= ( 0g ` W ) ) -> ( N ` { y } ) C_ U. { x e. A | x C_ U } ) |
36 |
8 2
|
lspss |
|- ( ( W e. LMod /\ U. { x e. A | x C_ U } C_ ( Base ` W ) /\ ( N ` { y } ) C_ U. { x e. A | x C_ U } ) -> ( N ` ( N ` { y } ) ) C_ ( N ` U. { x e. A | x C_ U } ) ) |
37 |
5 25 35 36
|
syl3anc |
|- ( ( ( ( W e. LMod /\ U e. S ) /\ y e. U ) /\ y =/= ( 0g ` W ) ) -> ( N ` ( N ` { y } ) ) C_ ( N ` U. { x e. A | x C_ U } ) ) |
38 |
14 37
|
eqsstrrd |
|- ( ( ( ( W e. LMod /\ U e. S ) /\ y e. U ) /\ y =/= ( 0g ` W ) ) -> ( N ` { y } ) C_ ( N ` U. { x e. A | x C_ U } ) ) |
39 |
8 2
|
lspsnid |
|- ( ( W e. LMod /\ y e. ( Base ` W ) ) -> y e. ( N ` { y } ) ) |
40 |
5 10 39
|
syl2anc |
|- ( ( ( ( W e. LMod /\ U e. S ) /\ y e. U ) /\ y =/= ( 0g ` W ) ) -> y e. ( N ` { y } ) ) |
41 |
38 40
|
sseldd |
|- ( ( ( ( W e. LMod /\ U e. S ) /\ y e. U ) /\ y =/= ( 0g ` W ) ) -> y e. ( N ` U. { x e. A | x C_ U } ) ) |
42 |
|
simpll |
|- ( ( ( W e. LMod /\ U e. S ) /\ y e. U ) -> W e. LMod ) |
43 |
8 1 2
|
lspcl |
|- ( ( W e. LMod /\ U. { x e. A | x C_ U } C_ ( Base ` W ) ) -> ( N ` U. { x e. A | x C_ U } ) e. S ) |
44 |
24 43
|
syldan |
|- ( ( W e. LMod /\ U e. S ) -> ( N ` U. { x e. A | x C_ U } ) e. S ) |
45 |
44
|
adantr |
|- ( ( ( W e. LMod /\ U e. S ) /\ y e. U ) -> ( N ` U. { x e. A | x C_ U } ) e. S ) |
46 |
27 1
|
lss0cl |
|- ( ( W e. LMod /\ ( N ` U. { x e. A | x C_ U } ) e. S ) -> ( 0g ` W ) e. ( N ` U. { x e. A | x C_ U } ) ) |
47 |
42 45 46
|
syl2anc |
|- ( ( ( W e. LMod /\ U e. S ) /\ y e. U ) -> ( 0g ` W ) e. ( N ` U. { x e. A | x C_ U } ) ) |
48 |
4 41 47
|
pm2.61ne |
|- ( ( ( W e. LMod /\ U e. S ) /\ y e. U ) -> y e. ( N ` U. { x e. A | x C_ U } ) ) |
49 |
48
|
ex |
|- ( ( W e. LMod /\ U e. S ) -> ( y e. U -> y e. ( N ` U. { x e. A | x C_ U } ) ) ) |
50 |
49
|
ssrdv |
|- ( ( W e. LMod /\ U e. S ) -> U C_ ( N ` U. { x e. A | x C_ U } ) ) |
51 |
|
simpl |
|- ( ( W e. LMod /\ U e. S ) -> W e. LMod ) |
52 |
8 2
|
lspss |
|- ( ( W e. LMod /\ U. { x e. S | x C_ U } C_ ( Base ` W ) /\ U. { x e. A | x C_ U } C_ U. { x e. S | x C_ U } ) -> ( N ` U. { x e. A | x C_ U } ) C_ ( N ` U. { x e. S | x C_ U } ) ) |
53 |
51 23 19 52
|
syl3anc |
|- ( ( W e. LMod /\ U e. S ) -> ( N ` U. { x e. A | x C_ U } ) C_ ( N ` U. { x e. S | x C_ U } ) ) |
54 |
20
|
adantl |
|- ( ( W e. LMod /\ U e. S ) -> U. { x e. S | x C_ U } = U ) |
55 |
54
|
fveq2d |
|- ( ( W e. LMod /\ U e. S ) -> ( N ` U. { x e. S | x C_ U } ) = ( N ` U ) ) |
56 |
1 2
|
lspid |
|- ( ( W e. LMod /\ U e. S ) -> ( N ` U ) = U ) |
57 |
55 56
|
eqtrd |
|- ( ( W e. LMod /\ U e. S ) -> ( N ` U. { x e. S | x C_ U } ) = U ) |
58 |
53 57
|
sseqtrd |
|- ( ( W e. LMod /\ U e. S ) -> ( N ` U. { x e. A | x C_ U } ) C_ U ) |
59 |
50 58
|
eqssd |
|- ( ( W e. LMod /\ U e. S ) -> U = ( N ` U. { x e. A | x C_ U } ) ) |