Proof of Theorem lpssat
| Step | Hyp | Ref
| Expression |
| 1 | | lpssat.l |
. . . 4
⊢ (𝜑 → 𝑇 ⊊ 𝑈) |
| 2 | | dfpss3 4089 |
. . . . 5
⊢ (𝑇 ⊊ 𝑈 ↔ (𝑇 ⊆ 𝑈 ∧ ¬ 𝑈 ⊆ 𝑇)) |
| 3 | 2 | simprbi 496 |
. . . 4
⊢ (𝑇 ⊊ 𝑈 → ¬ 𝑈 ⊆ 𝑇) |
| 4 | 1, 3 | syl 17 |
. . 3
⊢ (𝜑 → ¬ 𝑈 ⊆ 𝑇) |
| 5 | | iman 401 |
. . . . 5
⊢ ((𝑞 ⊆ 𝑈 → 𝑞 ⊆ 𝑇) ↔ ¬ (𝑞 ⊆ 𝑈 ∧ ¬ 𝑞 ⊆ 𝑇)) |
| 6 | 5 | ralbii 3093 |
. . . 4
⊢
(∀𝑞 ∈
𝐴 (𝑞 ⊆ 𝑈 → 𝑞 ⊆ 𝑇) ↔ ∀𝑞 ∈ 𝐴 ¬ (𝑞 ⊆ 𝑈 ∧ ¬ 𝑞 ⊆ 𝑇)) |
| 7 | | ss2rab 4071 |
. . . . 5
⊢ ({𝑞 ∈ 𝐴 ∣ 𝑞 ⊆ 𝑈} ⊆ {𝑞 ∈ 𝐴 ∣ 𝑞 ⊆ 𝑇} ↔ ∀𝑞 ∈ 𝐴 (𝑞 ⊆ 𝑈 → 𝑞 ⊆ 𝑇)) |
| 8 | | lpssat.w |
. . . . . . . . 9
⊢ (𝜑 → 𝑊 ∈ LMod) |
| 9 | 8 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ {𝑞 ∈ 𝐴 ∣ 𝑞 ⊆ 𝑈} ⊆ {𝑞 ∈ 𝐴 ∣ 𝑞 ⊆ 𝑇}) → 𝑊 ∈ LMod) |
| 10 | | lpssat.s |
. . . . . . . . . . . 12
⊢ 𝑆 = (LSubSp‘𝑊) |
| 11 | | lpssat.a |
. . . . . . . . . . . 12
⊢ 𝐴 = (LSAtoms‘𝑊) |
| 12 | 10, 11 | lsatlss 38997 |
. . . . . . . . . . 11
⊢ (𝑊 ∈ LMod → 𝐴 ⊆ 𝑆) |
| 13 | | rabss2 4078 |
. . . . . . . . . . 11
⊢ (𝐴 ⊆ 𝑆 → {𝑞 ∈ 𝐴 ∣ 𝑞 ⊆ 𝑇} ⊆ {𝑞 ∈ 𝑆 ∣ 𝑞 ⊆ 𝑇}) |
| 14 | | uniss 4915 |
. . . . . . . . . . 11
⊢ ({𝑞 ∈ 𝐴 ∣ 𝑞 ⊆ 𝑇} ⊆ {𝑞 ∈ 𝑆 ∣ 𝑞 ⊆ 𝑇} → ∪ {𝑞 ∈ 𝐴 ∣ 𝑞 ⊆ 𝑇} ⊆ ∪
{𝑞 ∈ 𝑆 ∣ 𝑞 ⊆ 𝑇}) |
| 15 | 8, 12, 13, 14 | 4syl 19 |
. . . . . . . . . 10
⊢ (𝜑 → ∪ {𝑞
∈ 𝐴 ∣ 𝑞 ⊆ 𝑇} ⊆ ∪
{𝑞 ∈ 𝑆 ∣ 𝑞 ⊆ 𝑇}) |
| 16 | | lpssat.t |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑇 ∈ 𝑆) |
| 17 | | unimax 4944 |
. . . . . . . . . . . 12
⊢ (𝑇 ∈ 𝑆 → ∪ {𝑞 ∈ 𝑆 ∣ 𝑞 ⊆ 𝑇} = 𝑇) |
| 18 | 16, 17 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → ∪ {𝑞
∈ 𝑆 ∣ 𝑞 ⊆ 𝑇} = 𝑇) |
| 19 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢
(Base‘𝑊) =
(Base‘𝑊) |
| 20 | 19, 10 | lssss 20934 |
. . . . . . . . . . . 12
⊢ (𝑇 ∈ 𝑆 → 𝑇 ⊆ (Base‘𝑊)) |
| 21 | 16, 20 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑇 ⊆ (Base‘𝑊)) |
| 22 | 18, 21 | eqsstrd 4018 |
. . . . . . . . . 10
⊢ (𝜑 → ∪ {𝑞
∈ 𝑆 ∣ 𝑞 ⊆ 𝑇} ⊆ (Base‘𝑊)) |
| 23 | 15, 22 | sstrd 3994 |
. . . . . . . . 9
⊢ (𝜑 → ∪ {𝑞
∈ 𝐴 ∣ 𝑞 ⊆ 𝑇} ⊆ (Base‘𝑊)) |
| 24 | 23 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ {𝑞 ∈ 𝐴 ∣ 𝑞 ⊆ 𝑈} ⊆ {𝑞 ∈ 𝐴 ∣ 𝑞 ⊆ 𝑇}) → ∪
{𝑞 ∈ 𝐴 ∣ 𝑞 ⊆ 𝑇} ⊆ (Base‘𝑊)) |
| 25 | | uniss 4915 |
. . . . . . . . 9
⊢ ({𝑞 ∈ 𝐴 ∣ 𝑞 ⊆ 𝑈} ⊆ {𝑞 ∈ 𝐴 ∣ 𝑞 ⊆ 𝑇} → ∪ {𝑞 ∈ 𝐴 ∣ 𝑞 ⊆ 𝑈} ⊆ ∪
{𝑞 ∈ 𝐴 ∣ 𝑞 ⊆ 𝑇}) |
| 26 | 25 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ {𝑞 ∈ 𝐴 ∣ 𝑞 ⊆ 𝑈} ⊆ {𝑞 ∈ 𝐴 ∣ 𝑞 ⊆ 𝑇}) → ∪
{𝑞 ∈ 𝐴 ∣ 𝑞 ⊆ 𝑈} ⊆ ∪
{𝑞 ∈ 𝐴 ∣ 𝑞 ⊆ 𝑇}) |
| 27 | | eqid 2737 |
. . . . . . . . 9
⊢
(LSpan‘𝑊) =
(LSpan‘𝑊) |
| 28 | 19, 27 | lspss 20982 |
. . . . . . . 8
⊢ ((𝑊 ∈ LMod ∧ ∪ {𝑞
∈ 𝐴 ∣ 𝑞 ⊆ 𝑇} ⊆ (Base‘𝑊) ∧ ∪ {𝑞 ∈ 𝐴 ∣ 𝑞 ⊆ 𝑈} ⊆ ∪
{𝑞 ∈ 𝐴 ∣ 𝑞 ⊆ 𝑇}) → ((LSpan‘𝑊)‘∪ {𝑞 ∈ 𝐴 ∣ 𝑞 ⊆ 𝑈}) ⊆ ((LSpan‘𝑊)‘∪ {𝑞 ∈ 𝐴 ∣ 𝑞 ⊆ 𝑇})) |
| 29 | 9, 24, 26, 28 | syl3anc 1373 |
. . . . . . 7
⊢ ((𝜑 ∧ {𝑞 ∈ 𝐴 ∣ 𝑞 ⊆ 𝑈} ⊆ {𝑞 ∈ 𝐴 ∣ 𝑞 ⊆ 𝑇}) → ((LSpan‘𝑊)‘∪ {𝑞 ∈ 𝐴 ∣ 𝑞 ⊆ 𝑈}) ⊆ ((LSpan‘𝑊)‘∪ {𝑞 ∈ 𝐴 ∣ 𝑞 ⊆ 𝑇})) |
| 30 | | lpssat.u |
. . . . . . . . 9
⊢ (𝜑 → 𝑈 ∈ 𝑆) |
| 31 | 10, 27, 11 | lssats 39013 |
. . . . . . . . 9
⊢ ((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) → 𝑈 = ((LSpan‘𝑊)‘∪ {𝑞 ∈ 𝐴 ∣ 𝑞 ⊆ 𝑈})) |
| 32 | 8, 30, 31 | syl2anc 584 |
. . . . . . . 8
⊢ (𝜑 → 𝑈 = ((LSpan‘𝑊)‘∪ {𝑞 ∈ 𝐴 ∣ 𝑞 ⊆ 𝑈})) |
| 33 | 32 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ {𝑞 ∈ 𝐴 ∣ 𝑞 ⊆ 𝑈} ⊆ {𝑞 ∈ 𝐴 ∣ 𝑞 ⊆ 𝑇}) → 𝑈 = ((LSpan‘𝑊)‘∪ {𝑞 ∈ 𝐴 ∣ 𝑞 ⊆ 𝑈})) |
| 34 | 10, 27, 11 | lssats 39013 |
. . . . . . . . 9
⊢ ((𝑊 ∈ LMod ∧ 𝑇 ∈ 𝑆) → 𝑇 = ((LSpan‘𝑊)‘∪ {𝑞 ∈ 𝐴 ∣ 𝑞 ⊆ 𝑇})) |
| 35 | 8, 16, 34 | syl2anc 584 |
. . . . . . . 8
⊢ (𝜑 → 𝑇 = ((LSpan‘𝑊)‘∪ {𝑞 ∈ 𝐴 ∣ 𝑞 ⊆ 𝑇})) |
| 36 | 35 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ {𝑞 ∈ 𝐴 ∣ 𝑞 ⊆ 𝑈} ⊆ {𝑞 ∈ 𝐴 ∣ 𝑞 ⊆ 𝑇}) → 𝑇 = ((LSpan‘𝑊)‘∪ {𝑞 ∈ 𝐴 ∣ 𝑞 ⊆ 𝑇})) |
| 37 | 29, 33, 36 | 3sstr4d 4039 |
. . . . . 6
⊢ ((𝜑 ∧ {𝑞 ∈ 𝐴 ∣ 𝑞 ⊆ 𝑈} ⊆ {𝑞 ∈ 𝐴 ∣ 𝑞 ⊆ 𝑇}) → 𝑈 ⊆ 𝑇) |
| 38 | 37 | ex 412 |
. . . . 5
⊢ (𝜑 → ({𝑞 ∈ 𝐴 ∣ 𝑞 ⊆ 𝑈} ⊆ {𝑞 ∈ 𝐴 ∣ 𝑞 ⊆ 𝑇} → 𝑈 ⊆ 𝑇)) |
| 39 | 7, 38 | biimtrrid 243 |
. . . 4
⊢ (𝜑 → (∀𝑞 ∈ 𝐴 (𝑞 ⊆ 𝑈 → 𝑞 ⊆ 𝑇) → 𝑈 ⊆ 𝑇)) |
| 40 | 6, 39 | biimtrrid 243 |
. . 3
⊢ (𝜑 → (∀𝑞 ∈ 𝐴 ¬ (𝑞 ⊆ 𝑈 ∧ ¬ 𝑞 ⊆ 𝑇) → 𝑈 ⊆ 𝑇)) |
| 41 | 4, 40 | mtod 198 |
. 2
⊢ (𝜑 → ¬ ∀𝑞 ∈ 𝐴 ¬ (𝑞 ⊆ 𝑈 ∧ ¬ 𝑞 ⊆ 𝑇)) |
| 42 | | dfrex2 3073 |
. 2
⊢
(∃𝑞 ∈
𝐴 (𝑞 ⊆ 𝑈 ∧ ¬ 𝑞 ⊆ 𝑇) ↔ ¬ ∀𝑞 ∈ 𝐴 ¬ (𝑞 ⊆ 𝑈 ∧ ¬ 𝑞 ⊆ 𝑇)) |
| 43 | 41, 42 | sylibr 234 |
1
⊢ (𝜑 → ∃𝑞 ∈ 𝐴 (𝑞 ⊆ 𝑈 ∧ ¬ 𝑞 ⊆ 𝑇)) |