Step |
Hyp |
Ref |
Expression |
1 |
|
lssats.s |
⊢ 𝑆 = ( LSubSp ‘ 𝑊 ) |
2 |
|
lssats.n |
⊢ 𝑁 = ( LSpan ‘ 𝑊 ) |
3 |
|
lssats.a |
⊢ 𝐴 = ( LSAtoms ‘ 𝑊 ) |
4 |
|
eleq1 |
⊢ ( 𝑦 = ( 0g ‘ 𝑊 ) → ( 𝑦 ∈ ( 𝑁 ‘ ∪ { 𝑥 ∈ 𝐴 ∣ 𝑥 ⊆ 𝑈 } ) ↔ ( 0g ‘ 𝑊 ) ∈ ( 𝑁 ‘ ∪ { 𝑥 ∈ 𝐴 ∣ 𝑥 ⊆ 𝑈 } ) ) ) |
5 |
|
simplll |
⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) ∧ 𝑦 ∈ 𝑈 ) ∧ 𝑦 ≠ ( 0g ‘ 𝑊 ) ) → 𝑊 ∈ LMod ) |
6 |
|
simpllr |
⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) ∧ 𝑦 ∈ 𝑈 ) ∧ 𝑦 ≠ ( 0g ‘ 𝑊 ) ) → 𝑈 ∈ 𝑆 ) |
7 |
|
simplr |
⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) ∧ 𝑦 ∈ 𝑈 ) ∧ 𝑦 ≠ ( 0g ‘ 𝑊 ) ) → 𝑦 ∈ 𝑈 ) |
8 |
|
eqid |
⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 ) |
9 |
8 1
|
lssel |
⊢ ( ( 𝑈 ∈ 𝑆 ∧ 𝑦 ∈ 𝑈 ) → 𝑦 ∈ ( Base ‘ 𝑊 ) ) |
10 |
6 7 9
|
syl2anc |
⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) ∧ 𝑦 ∈ 𝑈 ) ∧ 𝑦 ≠ ( 0g ‘ 𝑊 ) ) → 𝑦 ∈ ( Base ‘ 𝑊 ) ) |
11 |
8 1 2
|
lspsncl |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ) → ( 𝑁 ‘ { 𝑦 } ) ∈ 𝑆 ) |
12 |
5 10 11
|
syl2anc |
⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) ∧ 𝑦 ∈ 𝑈 ) ∧ 𝑦 ≠ ( 0g ‘ 𝑊 ) ) → ( 𝑁 ‘ { 𝑦 } ) ∈ 𝑆 ) |
13 |
1 2
|
lspid |
⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑁 ‘ { 𝑦 } ) ∈ 𝑆 ) → ( 𝑁 ‘ ( 𝑁 ‘ { 𝑦 } ) ) = ( 𝑁 ‘ { 𝑦 } ) ) |
14 |
5 12 13
|
syl2anc |
⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) ∧ 𝑦 ∈ 𝑈 ) ∧ 𝑦 ≠ ( 0g ‘ 𝑊 ) ) → ( 𝑁 ‘ ( 𝑁 ‘ { 𝑦 } ) ) = ( 𝑁 ‘ { 𝑦 } ) ) |
15 |
1 3
|
lsatlss |
⊢ ( 𝑊 ∈ LMod → 𝐴 ⊆ 𝑆 ) |
16 |
15
|
adantr |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) → 𝐴 ⊆ 𝑆 ) |
17 |
|
rabss2 |
⊢ ( 𝐴 ⊆ 𝑆 → { 𝑥 ∈ 𝐴 ∣ 𝑥 ⊆ 𝑈 } ⊆ { 𝑥 ∈ 𝑆 ∣ 𝑥 ⊆ 𝑈 } ) |
18 |
|
uniss |
⊢ ( { 𝑥 ∈ 𝐴 ∣ 𝑥 ⊆ 𝑈 } ⊆ { 𝑥 ∈ 𝑆 ∣ 𝑥 ⊆ 𝑈 } → ∪ { 𝑥 ∈ 𝐴 ∣ 𝑥 ⊆ 𝑈 } ⊆ ∪ { 𝑥 ∈ 𝑆 ∣ 𝑥 ⊆ 𝑈 } ) |
19 |
16 17 18
|
3syl |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) → ∪ { 𝑥 ∈ 𝐴 ∣ 𝑥 ⊆ 𝑈 } ⊆ ∪ { 𝑥 ∈ 𝑆 ∣ 𝑥 ⊆ 𝑈 } ) |
20 |
|
unimax |
⊢ ( 𝑈 ∈ 𝑆 → ∪ { 𝑥 ∈ 𝑆 ∣ 𝑥 ⊆ 𝑈 } = 𝑈 ) |
21 |
8 1
|
lssss |
⊢ ( 𝑈 ∈ 𝑆 → 𝑈 ⊆ ( Base ‘ 𝑊 ) ) |
22 |
20 21
|
eqsstrd |
⊢ ( 𝑈 ∈ 𝑆 → ∪ { 𝑥 ∈ 𝑆 ∣ 𝑥 ⊆ 𝑈 } ⊆ ( Base ‘ 𝑊 ) ) |
23 |
22
|
adantl |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) → ∪ { 𝑥 ∈ 𝑆 ∣ 𝑥 ⊆ 𝑈 } ⊆ ( Base ‘ 𝑊 ) ) |
24 |
19 23
|
sstrd |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) → ∪ { 𝑥 ∈ 𝐴 ∣ 𝑥 ⊆ 𝑈 } ⊆ ( Base ‘ 𝑊 ) ) |
25 |
24
|
ad2antrr |
⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) ∧ 𝑦 ∈ 𝑈 ) ∧ 𝑦 ≠ ( 0g ‘ 𝑊 ) ) → ∪ { 𝑥 ∈ 𝐴 ∣ 𝑥 ⊆ 𝑈 } ⊆ ( Base ‘ 𝑊 ) ) |
26 |
|
simpr |
⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) ∧ 𝑦 ∈ 𝑈 ) ∧ 𝑦 ≠ ( 0g ‘ 𝑊 ) ) → 𝑦 ≠ ( 0g ‘ 𝑊 ) ) |
27 |
|
eqid |
⊢ ( 0g ‘ 𝑊 ) = ( 0g ‘ 𝑊 ) |
28 |
8 2 27 3
|
lsatlspsn2 |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ∧ 𝑦 ≠ ( 0g ‘ 𝑊 ) ) → ( 𝑁 ‘ { 𝑦 } ) ∈ 𝐴 ) |
29 |
5 10 26 28
|
syl3anc |
⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) ∧ 𝑦 ∈ 𝑈 ) ∧ 𝑦 ≠ ( 0g ‘ 𝑊 ) ) → ( 𝑁 ‘ { 𝑦 } ) ∈ 𝐴 ) |
30 |
1 2 5 6 7
|
lspsnel5a |
⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) ∧ 𝑦 ∈ 𝑈 ) ∧ 𝑦 ≠ ( 0g ‘ 𝑊 ) ) → ( 𝑁 ‘ { 𝑦 } ) ⊆ 𝑈 ) |
31 |
|
sseq1 |
⊢ ( 𝑥 = ( 𝑁 ‘ { 𝑦 } ) → ( 𝑥 ⊆ 𝑈 ↔ ( 𝑁 ‘ { 𝑦 } ) ⊆ 𝑈 ) ) |
32 |
31
|
elrab |
⊢ ( ( 𝑁 ‘ { 𝑦 } ) ∈ { 𝑥 ∈ 𝐴 ∣ 𝑥 ⊆ 𝑈 } ↔ ( ( 𝑁 ‘ { 𝑦 } ) ∈ 𝐴 ∧ ( 𝑁 ‘ { 𝑦 } ) ⊆ 𝑈 ) ) |
33 |
29 30 32
|
sylanbrc |
⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) ∧ 𝑦 ∈ 𝑈 ) ∧ 𝑦 ≠ ( 0g ‘ 𝑊 ) ) → ( 𝑁 ‘ { 𝑦 } ) ∈ { 𝑥 ∈ 𝐴 ∣ 𝑥 ⊆ 𝑈 } ) |
34 |
|
elssuni |
⊢ ( ( 𝑁 ‘ { 𝑦 } ) ∈ { 𝑥 ∈ 𝐴 ∣ 𝑥 ⊆ 𝑈 } → ( 𝑁 ‘ { 𝑦 } ) ⊆ ∪ { 𝑥 ∈ 𝐴 ∣ 𝑥 ⊆ 𝑈 } ) |
35 |
33 34
|
syl |
⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) ∧ 𝑦 ∈ 𝑈 ) ∧ 𝑦 ≠ ( 0g ‘ 𝑊 ) ) → ( 𝑁 ‘ { 𝑦 } ) ⊆ ∪ { 𝑥 ∈ 𝐴 ∣ 𝑥 ⊆ 𝑈 } ) |
36 |
8 2
|
lspss |
⊢ ( ( 𝑊 ∈ LMod ∧ ∪ { 𝑥 ∈ 𝐴 ∣ 𝑥 ⊆ 𝑈 } ⊆ ( Base ‘ 𝑊 ) ∧ ( 𝑁 ‘ { 𝑦 } ) ⊆ ∪ { 𝑥 ∈ 𝐴 ∣ 𝑥 ⊆ 𝑈 } ) → ( 𝑁 ‘ ( 𝑁 ‘ { 𝑦 } ) ) ⊆ ( 𝑁 ‘ ∪ { 𝑥 ∈ 𝐴 ∣ 𝑥 ⊆ 𝑈 } ) ) |
37 |
5 25 35 36
|
syl3anc |
⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) ∧ 𝑦 ∈ 𝑈 ) ∧ 𝑦 ≠ ( 0g ‘ 𝑊 ) ) → ( 𝑁 ‘ ( 𝑁 ‘ { 𝑦 } ) ) ⊆ ( 𝑁 ‘ ∪ { 𝑥 ∈ 𝐴 ∣ 𝑥 ⊆ 𝑈 } ) ) |
38 |
14 37
|
eqsstrrd |
⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) ∧ 𝑦 ∈ 𝑈 ) ∧ 𝑦 ≠ ( 0g ‘ 𝑊 ) ) → ( 𝑁 ‘ { 𝑦 } ) ⊆ ( 𝑁 ‘ ∪ { 𝑥 ∈ 𝐴 ∣ 𝑥 ⊆ 𝑈 } ) ) |
39 |
8 2
|
lspsnid |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ) → 𝑦 ∈ ( 𝑁 ‘ { 𝑦 } ) ) |
40 |
5 10 39
|
syl2anc |
⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) ∧ 𝑦 ∈ 𝑈 ) ∧ 𝑦 ≠ ( 0g ‘ 𝑊 ) ) → 𝑦 ∈ ( 𝑁 ‘ { 𝑦 } ) ) |
41 |
38 40
|
sseldd |
⊢ ( ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) ∧ 𝑦 ∈ 𝑈 ) ∧ 𝑦 ≠ ( 0g ‘ 𝑊 ) ) → 𝑦 ∈ ( 𝑁 ‘ ∪ { 𝑥 ∈ 𝐴 ∣ 𝑥 ⊆ 𝑈 } ) ) |
42 |
|
simpll |
⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) ∧ 𝑦 ∈ 𝑈 ) → 𝑊 ∈ LMod ) |
43 |
8 1 2
|
lspcl |
⊢ ( ( 𝑊 ∈ LMod ∧ ∪ { 𝑥 ∈ 𝐴 ∣ 𝑥 ⊆ 𝑈 } ⊆ ( Base ‘ 𝑊 ) ) → ( 𝑁 ‘ ∪ { 𝑥 ∈ 𝐴 ∣ 𝑥 ⊆ 𝑈 } ) ∈ 𝑆 ) |
44 |
24 43
|
syldan |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) → ( 𝑁 ‘ ∪ { 𝑥 ∈ 𝐴 ∣ 𝑥 ⊆ 𝑈 } ) ∈ 𝑆 ) |
45 |
44
|
adantr |
⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) ∧ 𝑦 ∈ 𝑈 ) → ( 𝑁 ‘ ∪ { 𝑥 ∈ 𝐴 ∣ 𝑥 ⊆ 𝑈 } ) ∈ 𝑆 ) |
46 |
27 1
|
lss0cl |
⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑁 ‘ ∪ { 𝑥 ∈ 𝐴 ∣ 𝑥 ⊆ 𝑈 } ) ∈ 𝑆 ) → ( 0g ‘ 𝑊 ) ∈ ( 𝑁 ‘ ∪ { 𝑥 ∈ 𝐴 ∣ 𝑥 ⊆ 𝑈 } ) ) |
47 |
42 45 46
|
syl2anc |
⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) ∧ 𝑦 ∈ 𝑈 ) → ( 0g ‘ 𝑊 ) ∈ ( 𝑁 ‘ ∪ { 𝑥 ∈ 𝐴 ∣ 𝑥 ⊆ 𝑈 } ) ) |
48 |
4 41 47
|
pm2.61ne |
⊢ ( ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) ∧ 𝑦 ∈ 𝑈 ) → 𝑦 ∈ ( 𝑁 ‘ ∪ { 𝑥 ∈ 𝐴 ∣ 𝑥 ⊆ 𝑈 } ) ) |
49 |
48
|
ex |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) → ( 𝑦 ∈ 𝑈 → 𝑦 ∈ ( 𝑁 ‘ ∪ { 𝑥 ∈ 𝐴 ∣ 𝑥 ⊆ 𝑈 } ) ) ) |
50 |
49
|
ssrdv |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) → 𝑈 ⊆ ( 𝑁 ‘ ∪ { 𝑥 ∈ 𝐴 ∣ 𝑥 ⊆ 𝑈 } ) ) |
51 |
|
simpl |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) → 𝑊 ∈ LMod ) |
52 |
8 2
|
lspss |
⊢ ( ( 𝑊 ∈ LMod ∧ ∪ { 𝑥 ∈ 𝑆 ∣ 𝑥 ⊆ 𝑈 } ⊆ ( Base ‘ 𝑊 ) ∧ ∪ { 𝑥 ∈ 𝐴 ∣ 𝑥 ⊆ 𝑈 } ⊆ ∪ { 𝑥 ∈ 𝑆 ∣ 𝑥 ⊆ 𝑈 } ) → ( 𝑁 ‘ ∪ { 𝑥 ∈ 𝐴 ∣ 𝑥 ⊆ 𝑈 } ) ⊆ ( 𝑁 ‘ ∪ { 𝑥 ∈ 𝑆 ∣ 𝑥 ⊆ 𝑈 } ) ) |
53 |
51 23 19 52
|
syl3anc |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) → ( 𝑁 ‘ ∪ { 𝑥 ∈ 𝐴 ∣ 𝑥 ⊆ 𝑈 } ) ⊆ ( 𝑁 ‘ ∪ { 𝑥 ∈ 𝑆 ∣ 𝑥 ⊆ 𝑈 } ) ) |
54 |
20
|
adantl |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) → ∪ { 𝑥 ∈ 𝑆 ∣ 𝑥 ⊆ 𝑈 } = 𝑈 ) |
55 |
54
|
fveq2d |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) → ( 𝑁 ‘ ∪ { 𝑥 ∈ 𝑆 ∣ 𝑥 ⊆ 𝑈 } ) = ( 𝑁 ‘ 𝑈 ) ) |
56 |
1 2
|
lspid |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) → ( 𝑁 ‘ 𝑈 ) = 𝑈 ) |
57 |
55 56
|
eqtrd |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) → ( 𝑁 ‘ ∪ { 𝑥 ∈ 𝑆 ∣ 𝑥 ⊆ 𝑈 } ) = 𝑈 ) |
58 |
53 57
|
sseqtrd |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) → ( 𝑁 ‘ ∪ { 𝑥 ∈ 𝐴 ∣ 𝑥 ⊆ 𝑈 } ) ⊆ 𝑈 ) |
59 |
50 58
|
eqssd |
⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) → 𝑈 = ( 𝑁 ‘ ∪ { 𝑥 ∈ 𝐴 ∣ 𝑥 ⊆ 𝑈 } ) ) |