| Step | Hyp | Ref
| Expression |
| 1 | | eleq1 2829 |
. . . . 5
⊢ (𝑦 = (0g‘𝑊) → (𝑦 ∈ (𝑁‘∪ {𝑥 ∈ 𝐴 ∣ 𝑥 ⊆ 𝑈}) ↔ (0g‘𝑊) ∈ (𝑁‘∪ {𝑥 ∈ 𝐴 ∣ 𝑥 ⊆ 𝑈}))) |
| 2 | | simplll 775 |
. . . . . . . 8
⊢ ((((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) ∧ 𝑦 ∈ 𝑈) ∧ 𝑦 ≠ (0g‘𝑊)) → 𝑊 ∈ LMod) |
| 3 | | simpllr 776 |
. . . . . . . . . 10
⊢ ((((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) ∧ 𝑦 ∈ 𝑈) ∧ 𝑦 ≠ (0g‘𝑊)) → 𝑈 ∈ 𝑆) |
| 4 | | simplr 769 |
. . . . . . . . . 10
⊢ ((((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) ∧ 𝑦 ∈ 𝑈) ∧ 𝑦 ≠ (0g‘𝑊)) → 𝑦 ∈ 𝑈) |
| 5 | | eqid 2737 |
. . . . . . . . . . 11
⊢
(Base‘𝑊) =
(Base‘𝑊) |
| 6 | | lssats.s |
. . . . . . . . . . 11
⊢ 𝑆 = (LSubSp‘𝑊) |
| 7 | 5, 6 | lssel 20935 |
. . . . . . . . . 10
⊢ ((𝑈 ∈ 𝑆 ∧ 𝑦 ∈ 𝑈) → 𝑦 ∈ (Base‘𝑊)) |
| 8 | 3, 4, 7 | syl2anc 584 |
. . . . . . . . 9
⊢ ((((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) ∧ 𝑦 ∈ 𝑈) ∧ 𝑦 ≠ (0g‘𝑊)) → 𝑦 ∈ (Base‘𝑊)) |
| 9 | | lssats.n |
. . . . . . . . . 10
⊢ 𝑁 = (LSpan‘𝑊) |
| 10 | 5, 6, 9 | lspsncl 20975 |
. . . . . . . . 9
⊢ ((𝑊 ∈ LMod ∧ 𝑦 ∈ (Base‘𝑊)) → (𝑁‘{𝑦}) ∈ 𝑆) |
| 11 | 2, 8, 10 | syl2anc 584 |
. . . . . . . 8
⊢ ((((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) ∧ 𝑦 ∈ 𝑈) ∧ 𝑦 ≠ (0g‘𝑊)) → (𝑁‘{𝑦}) ∈ 𝑆) |
| 12 | 6, 9 | lspid 20980 |
. . . . . . . 8
⊢ ((𝑊 ∈ LMod ∧ (𝑁‘{𝑦}) ∈ 𝑆) → (𝑁‘(𝑁‘{𝑦})) = (𝑁‘{𝑦})) |
| 13 | 2, 11, 12 | syl2anc 584 |
. . . . . . 7
⊢ ((((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) ∧ 𝑦 ∈ 𝑈) ∧ 𝑦 ≠ (0g‘𝑊)) → (𝑁‘(𝑁‘{𝑦})) = (𝑁‘{𝑦})) |
| 14 | | lssats.a |
. . . . . . . . . . . . 13
⊢ 𝐴 = (LSAtoms‘𝑊) |
| 15 | 6, 14 | lsatlss 38997 |
. . . . . . . . . . . 12
⊢ (𝑊 ∈ LMod → 𝐴 ⊆ 𝑆) |
| 16 | 15 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) → 𝐴 ⊆ 𝑆) |
| 17 | | rabss2 4078 |
. . . . . . . . . . 11
⊢ (𝐴 ⊆ 𝑆 → {𝑥 ∈ 𝐴 ∣ 𝑥 ⊆ 𝑈} ⊆ {𝑥 ∈ 𝑆 ∣ 𝑥 ⊆ 𝑈}) |
| 18 | | uniss 4915 |
. . . . . . . . . . 11
⊢ ({𝑥 ∈ 𝐴 ∣ 𝑥 ⊆ 𝑈} ⊆ {𝑥 ∈ 𝑆 ∣ 𝑥 ⊆ 𝑈} → ∪ {𝑥 ∈ 𝐴 ∣ 𝑥 ⊆ 𝑈} ⊆ ∪
{𝑥 ∈ 𝑆 ∣ 𝑥 ⊆ 𝑈}) |
| 19 | 16, 17, 18 | 3syl 18 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) → ∪ {𝑥 ∈ 𝐴 ∣ 𝑥 ⊆ 𝑈} ⊆ ∪
{𝑥 ∈ 𝑆 ∣ 𝑥 ⊆ 𝑈}) |
| 20 | | unimax 4944 |
. . . . . . . . . . . 12
⊢ (𝑈 ∈ 𝑆 → ∪ {𝑥 ∈ 𝑆 ∣ 𝑥 ⊆ 𝑈} = 𝑈) |
| 21 | 5, 6 | lssss 20934 |
. . . . . . . . . . . 12
⊢ (𝑈 ∈ 𝑆 → 𝑈 ⊆ (Base‘𝑊)) |
| 22 | 20, 21 | eqsstrd 4018 |
. . . . . . . . . . 11
⊢ (𝑈 ∈ 𝑆 → ∪ {𝑥 ∈ 𝑆 ∣ 𝑥 ⊆ 𝑈} ⊆ (Base‘𝑊)) |
| 23 | 22 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) → ∪ {𝑥 ∈ 𝑆 ∣ 𝑥 ⊆ 𝑈} ⊆ (Base‘𝑊)) |
| 24 | 19, 23 | sstrd 3994 |
. . . . . . . . 9
⊢ ((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) → ∪ {𝑥 ∈ 𝐴 ∣ 𝑥 ⊆ 𝑈} ⊆ (Base‘𝑊)) |
| 25 | 24 | ad2antrr 726 |
. . . . . . . 8
⊢ ((((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) ∧ 𝑦 ∈ 𝑈) ∧ 𝑦 ≠ (0g‘𝑊)) → ∪
{𝑥 ∈ 𝐴 ∣ 𝑥 ⊆ 𝑈} ⊆ (Base‘𝑊)) |
| 26 | | simpr 484 |
. . . . . . . . . . 11
⊢ ((((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) ∧ 𝑦 ∈ 𝑈) ∧ 𝑦 ≠ (0g‘𝑊)) → 𝑦 ≠ (0g‘𝑊)) |
| 27 | | eqid 2737 |
. . . . . . . . . . . 12
⊢
(0g‘𝑊) = (0g‘𝑊) |
| 28 | 5, 9, 27, 14 | lsatlspsn2 38993 |
. . . . . . . . . . 11
⊢ ((𝑊 ∈ LMod ∧ 𝑦 ∈ (Base‘𝑊) ∧ 𝑦 ≠ (0g‘𝑊)) → (𝑁‘{𝑦}) ∈ 𝐴) |
| 29 | 2, 8, 26, 28 | syl3anc 1373 |
. . . . . . . . . 10
⊢ ((((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) ∧ 𝑦 ∈ 𝑈) ∧ 𝑦 ≠ (0g‘𝑊)) → (𝑁‘{𝑦}) ∈ 𝐴) |
| 30 | 6, 9, 2, 3, 4 | ellspsn5 20994 |
. . . . . . . . . 10
⊢ ((((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) ∧ 𝑦 ∈ 𝑈) ∧ 𝑦 ≠ (0g‘𝑊)) → (𝑁‘{𝑦}) ⊆ 𝑈) |
| 31 | | sseq1 4009 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝑁‘{𝑦}) → (𝑥 ⊆ 𝑈 ↔ (𝑁‘{𝑦}) ⊆ 𝑈)) |
| 32 | 31 | elrab 3692 |
. . . . . . . . . 10
⊢ ((𝑁‘{𝑦}) ∈ {𝑥 ∈ 𝐴 ∣ 𝑥 ⊆ 𝑈} ↔ ((𝑁‘{𝑦}) ∈ 𝐴 ∧ (𝑁‘{𝑦}) ⊆ 𝑈)) |
| 33 | 29, 30, 32 | sylanbrc 583 |
. . . . . . . . 9
⊢ ((((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) ∧ 𝑦 ∈ 𝑈) ∧ 𝑦 ≠ (0g‘𝑊)) → (𝑁‘{𝑦}) ∈ {𝑥 ∈ 𝐴 ∣ 𝑥 ⊆ 𝑈}) |
| 34 | | elssuni 4937 |
. . . . . . . . 9
⊢ ((𝑁‘{𝑦}) ∈ {𝑥 ∈ 𝐴 ∣ 𝑥 ⊆ 𝑈} → (𝑁‘{𝑦}) ⊆ ∪
{𝑥 ∈ 𝐴 ∣ 𝑥 ⊆ 𝑈}) |
| 35 | 33, 34 | syl 17 |
. . . . . . . 8
⊢ ((((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) ∧ 𝑦 ∈ 𝑈) ∧ 𝑦 ≠ (0g‘𝑊)) → (𝑁‘{𝑦}) ⊆ ∪
{𝑥 ∈ 𝐴 ∣ 𝑥 ⊆ 𝑈}) |
| 36 | 5, 9 | lspss 20982 |
. . . . . . . 8
⊢ ((𝑊 ∈ LMod ∧ ∪ {𝑥
∈ 𝐴 ∣ 𝑥 ⊆ 𝑈} ⊆ (Base‘𝑊) ∧ (𝑁‘{𝑦}) ⊆ ∪
{𝑥 ∈ 𝐴 ∣ 𝑥 ⊆ 𝑈}) → (𝑁‘(𝑁‘{𝑦})) ⊆ (𝑁‘∪ {𝑥 ∈ 𝐴 ∣ 𝑥 ⊆ 𝑈})) |
| 37 | 2, 25, 35, 36 | syl3anc 1373 |
. . . . . . 7
⊢ ((((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) ∧ 𝑦 ∈ 𝑈) ∧ 𝑦 ≠ (0g‘𝑊)) → (𝑁‘(𝑁‘{𝑦})) ⊆ (𝑁‘∪ {𝑥 ∈ 𝐴 ∣ 𝑥 ⊆ 𝑈})) |
| 38 | 13, 37 | eqsstrrd 4019 |
. . . . . 6
⊢ ((((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) ∧ 𝑦 ∈ 𝑈) ∧ 𝑦 ≠ (0g‘𝑊)) → (𝑁‘{𝑦}) ⊆ (𝑁‘∪ {𝑥 ∈ 𝐴 ∣ 𝑥 ⊆ 𝑈})) |
| 39 | 5, 9 | lspsnid 20991 |
. . . . . . 7
⊢ ((𝑊 ∈ LMod ∧ 𝑦 ∈ (Base‘𝑊)) → 𝑦 ∈ (𝑁‘{𝑦})) |
| 40 | 2, 8, 39 | syl2anc 584 |
. . . . . 6
⊢ ((((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) ∧ 𝑦 ∈ 𝑈) ∧ 𝑦 ≠ (0g‘𝑊)) → 𝑦 ∈ (𝑁‘{𝑦})) |
| 41 | 38, 40 | sseldd 3984 |
. . . . 5
⊢ ((((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) ∧ 𝑦 ∈ 𝑈) ∧ 𝑦 ≠ (0g‘𝑊)) → 𝑦 ∈ (𝑁‘∪ {𝑥 ∈ 𝐴 ∣ 𝑥 ⊆ 𝑈})) |
| 42 | | simpll 767 |
. . . . . 6
⊢ (((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) ∧ 𝑦 ∈ 𝑈) → 𝑊 ∈ LMod) |
| 43 | 5, 6, 9 | lspcl 20974 |
. . . . . . . 8
⊢ ((𝑊 ∈ LMod ∧ ∪ {𝑥
∈ 𝐴 ∣ 𝑥 ⊆ 𝑈} ⊆ (Base‘𝑊)) → (𝑁‘∪ {𝑥 ∈ 𝐴 ∣ 𝑥 ⊆ 𝑈}) ∈ 𝑆) |
| 44 | 24, 43 | syldan 591 |
. . . . . . 7
⊢ ((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) → (𝑁‘∪ {𝑥 ∈ 𝐴 ∣ 𝑥 ⊆ 𝑈}) ∈ 𝑆) |
| 45 | 44 | adantr 480 |
. . . . . 6
⊢ (((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) ∧ 𝑦 ∈ 𝑈) → (𝑁‘∪ {𝑥 ∈ 𝐴 ∣ 𝑥 ⊆ 𝑈}) ∈ 𝑆) |
| 46 | 27, 6 | lss0cl 20945 |
. . . . . 6
⊢ ((𝑊 ∈ LMod ∧ (𝑁‘∪ {𝑥
∈ 𝐴 ∣ 𝑥 ⊆ 𝑈}) ∈ 𝑆) → (0g‘𝑊) ∈ (𝑁‘∪ {𝑥 ∈ 𝐴 ∣ 𝑥 ⊆ 𝑈})) |
| 47 | 42, 45, 46 | syl2anc 584 |
. . . . 5
⊢ (((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) ∧ 𝑦 ∈ 𝑈) → (0g‘𝑊) ∈ (𝑁‘∪ {𝑥 ∈ 𝐴 ∣ 𝑥 ⊆ 𝑈})) |
| 48 | 1, 41, 47 | pm2.61ne 3027 |
. . . 4
⊢ (((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) ∧ 𝑦 ∈ 𝑈) → 𝑦 ∈ (𝑁‘∪ {𝑥 ∈ 𝐴 ∣ 𝑥 ⊆ 𝑈})) |
| 49 | 48 | ex 412 |
. . 3
⊢ ((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) → (𝑦 ∈ 𝑈 → 𝑦 ∈ (𝑁‘∪ {𝑥 ∈ 𝐴 ∣ 𝑥 ⊆ 𝑈}))) |
| 50 | 49 | ssrdv 3989 |
. 2
⊢ ((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) → 𝑈 ⊆ (𝑁‘∪ {𝑥 ∈ 𝐴 ∣ 𝑥 ⊆ 𝑈})) |
| 51 | | simpl 482 |
. . . 4
⊢ ((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) → 𝑊 ∈ LMod) |
| 52 | 5, 9 | lspss 20982 |
. . . 4
⊢ ((𝑊 ∈ LMod ∧ ∪ {𝑥
∈ 𝑆 ∣ 𝑥 ⊆ 𝑈} ⊆ (Base‘𝑊) ∧ ∪ {𝑥 ∈ 𝐴 ∣ 𝑥 ⊆ 𝑈} ⊆ ∪
{𝑥 ∈ 𝑆 ∣ 𝑥 ⊆ 𝑈}) → (𝑁‘∪ {𝑥 ∈ 𝐴 ∣ 𝑥 ⊆ 𝑈}) ⊆ (𝑁‘∪ {𝑥 ∈ 𝑆 ∣ 𝑥 ⊆ 𝑈})) |
| 53 | 51, 23, 19, 52 | syl3anc 1373 |
. . 3
⊢ ((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) → (𝑁‘∪ {𝑥 ∈ 𝐴 ∣ 𝑥 ⊆ 𝑈}) ⊆ (𝑁‘∪ {𝑥 ∈ 𝑆 ∣ 𝑥 ⊆ 𝑈})) |
| 54 | 20 | adantl 481 |
. . . . 5
⊢ ((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) → ∪ {𝑥 ∈ 𝑆 ∣ 𝑥 ⊆ 𝑈} = 𝑈) |
| 55 | 54 | fveq2d 6910 |
. . . 4
⊢ ((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) → (𝑁‘∪ {𝑥 ∈ 𝑆 ∣ 𝑥 ⊆ 𝑈}) = (𝑁‘𝑈)) |
| 56 | 6, 9 | lspid 20980 |
. . . 4
⊢ ((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) → (𝑁‘𝑈) = 𝑈) |
| 57 | 55, 56 | eqtrd 2777 |
. . 3
⊢ ((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) → (𝑁‘∪ {𝑥 ∈ 𝑆 ∣ 𝑥 ⊆ 𝑈}) = 𝑈) |
| 58 | 53, 57 | sseqtrd 4020 |
. 2
⊢ ((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) → (𝑁‘∪ {𝑥 ∈ 𝐴 ∣ 𝑥 ⊆ 𝑈}) ⊆ 𝑈) |
| 59 | 50, 58 | eqssd 4001 |
1
⊢ ((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) → 𝑈 = (𝑁‘∪ {𝑥 ∈ 𝐴 ∣ 𝑥 ⊆ 𝑈})) |