Proof of Theorem 4atexlemcnd
| Step | Hyp | Ref
| Expression |
| 1 | | 4thatlem.ph |
. . . 4
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑆 ∈ 𝐴 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ∧ (𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅)) ∧ (𝑇 ∈ 𝐴 ∧ (𝑈 ∨ 𝑇) = (𝑉 ∨ 𝑇))) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ (𝑃 ∨ 𝑄)))) |
| 2 | | 4thatlem0.l |
. . . 4
⊢ ≤ =
(le‘𝐾) |
| 3 | | 4thatlem0.j |
. . . 4
⊢ ∨ =
(join‘𝐾) |
| 4 | | 4thatlem0.m |
. . . 4
⊢ ∧ =
(meet‘𝐾) |
| 5 | | 4thatlem0.a |
. . . 4
⊢ 𝐴 = (Atoms‘𝐾) |
| 6 | | 4thatlem0.h |
. . . 4
⊢ 𝐻 = (LHyp‘𝐾) |
| 7 | | 4thatlem0.u |
. . . 4
⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊) |
| 8 | | 4thatlem0.v |
. . . 4
⊢ 𝑉 = ((𝑃 ∨ 𝑆) ∧ 𝑊) |
| 9 | 1, 2, 3, 4, 5, 6, 7, 8 | 4atexlemtlw 40069 |
. . 3
⊢ (𝜑 → 𝑇 ≤ 𝑊) |
| 10 | | 4thatlem0.c |
. . . 4
⊢ 𝐶 = ((𝑄 ∨ 𝑇) ∧ (𝑃 ∨ 𝑆)) |
| 11 | 1, 2, 3, 4, 5, 6, 7, 8, 10 | 4atexlemnclw 40072 |
. . 3
⊢ (𝜑 → ¬ 𝐶 ≤ 𝑊) |
| 12 | | nbrne2 5163 |
. . 3
⊢ ((𝑇 ≤ 𝑊 ∧ ¬ 𝐶 ≤ 𝑊) → 𝑇 ≠ 𝐶) |
| 13 | 9, 11, 12 | syl2anc 584 |
. 2
⊢ (𝜑 → 𝑇 ≠ 𝐶) |
| 14 | 1 | 4atexlemk 40049 |
. . . . . . . . 9
⊢ (𝜑 → 𝐾 ∈ HL) |
| 15 | 1 | 4atexlemq 40053 |
. . . . . . . . 9
⊢ (𝜑 → 𝑄 ∈ 𝐴) |
| 16 | 1 | 4atexlemt 40055 |
. . . . . . . . 9
⊢ (𝜑 → 𝑇 ∈ 𝐴) |
| 17 | 3, 5 | hlatjcom 39369 |
. . . . . . . . 9
⊢ ((𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) → (𝑄 ∨ 𝑇) = (𝑇 ∨ 𝑄)) |
| 18 | 14, 15, 16, 17 | syl3anc 1373 |
. . . . . . . 8
⊢ (𝜑 → (𝑄 ∨ 𝑇) = (𝑇 ∨ 𝑄)) |
| 19 | | simp221 1315 |
. . . . . . . . . 10
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑆 ∈ 𝐴 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ∧ (𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅)) ∧ (𝑇 ∈ 𝐴 ∧ (𝑈 ∨ 𝑇) = (𝑉 ∨ 𝑇))) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ (𝑃 ∨ 𝑄))) → 𝑅 ∈ 𝐴) |
| 20 | 1, 19 | sylbi 217 |
. . . . . . . . 9
⊢ (𝜑 → 𝑅 ∈ 𝐴) |
| 21 | 3, 5 | hlatjcom 39369 |
. . . . . . . . 9
⊢ ((𝐾 ∈ HL ∧ 𝑅 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) → (𝑅 ∨ 𝑇) = (𝑇 ∨ 𝑅)) |
| 22 | 14, 20, 16, 21 | syl3anc 1373 |
. . . . . . . 8
⊢ (𝜑 → (𝑅 ∨ 𝑇) = (𝑇 ∨ 𝑅)) |
| 23 | 18, 22 | oveq12d 7449 |
. . . . . . 7
⊢ (𝜑 → ((𝑄 ∨ 𝑇) ∧ (𝑅 ∨ 𝑇)) = ((𝑇 ∨ 𝑄) ∧ (𝑇 ∨ 𝑅))) |
| 24 | 1 | 4atexlemkc 40060 |
. . . . . . . . 9
⊢ (𝜑 → 𝐾 ∈ CvLat) |
| 25 | 1 | 4atexlemp 40052 |
. . . . . . . . 9
⊢ (𝜑 → 𝑃 ∈ 𝐴) |
| 26 | 1 | 4atexlempnq 40057 |
. . . . . . . . 9
⊢ (𝜑 → 𝑃 ≠ 𝑄) |
| 27 | | simp223 1317 |
. . . . . . . . . 10
⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑆 ∈ 𝐴 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ∧ (𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅)) ∧ (𝑇 ∈ 𝐴 ∧ (𝑈 ∨ 𝑇) = (𝑉 ∨ 𝑇))) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ (𝑃 ∨ 𝑄))) → (𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅)) |
| 28 | 1, 27 | sylbi 217 |
. . . . . . . . 9
⊢ (𝜑 → (𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅)) |
| 29 | 5, 3 | cvlsupr6 39348 |
. . . . . . . . . 10
⊢ ((𝐾 ∈ CvLat ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ (𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅))) → 𝑅 ≠ 𝑄) |
| 30 | 29 | necomd 2996 |
. . . . . . . . 9
⊢ ((𝐾 ∈ CvLat ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ (𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅))) → 𝑄 ≠ 𝑅) |
| 31 | 24, 25, 15, 20, 26, 28, 30 | syl132anc 1390 |
. . . . . . . 8
⊢ (𝜑 → 𝑄 ≠ 𝑅) |
| 32 | 1, 2, 3, 4, 5, 6, 7, 8 | 4atexlemntlpq 40070 |
. . . . . . . . 9
⊢ (𝜑 → ¬ 𝑇 ≤ (𝑃 ∨ 𝑄)) |
| 33 | 5, 3 | cvlsupr7 39349 |
. . . . . . . . . . . 12
⊢ ((𝐾 ∈ CvLat ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ (𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅))) → (𝑃 ∨ 𝑄) = (𝑅 ∨ 𝑄)) |
| 34 | 24, 25, 15, 20, 26, 28, 33 | syl132anc 1390 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑃 ∨ 𝑄) = (𝑅 ∨ 𝑄)) |
| 35 | 3, 5 | hlatjcom 39369 |
. . . . . . . . . . . 12
⊢ ((𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) → (𝑄 ∨ 𝑅) = (𝑅 ∨ 𝑄)) |
| 36 | 14, 15, 20, 35 | syl3anc 1373 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑄 ∨ 𝑅) = (𝑅 ∨ 𝑄)) |
| 37 | 34, 36 | eqtr4d 2780 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑃 ∨ 𝑄) = (𝑄 ∨ 𝑅)) |
| 38 | 37 | breq2d 5155 |
. . . . . . . . 9
⊢ (𝜑 → (𝑇 ≤ (𝑃 ∨ 𝑄) ↔ 𝑇 ≤ (𝑄 ∨ 𝑅))) |
| 39 | 32, 38 | mtbid 324 |
. . . . . . . 8
⊢ (𝜑 → ¬ 𝑇 ≤ (𝑄 ∨ 𝑅)) |
| 40 | 2, 3, 4, 5 | 2llnma2 39791 |
. . . . . . . 8
⊢ ((𝐾 ∈ HL ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑄 ≠ 𝑅 ∧ ¬ 𝑇 ≤ (𝑄 ∨ 𝑅))) → ((𝑇 ∨ 𝑄) ∧ (𝑇 ∨ 𝑅)) = 𝑇) |
| 41 | 14, 15, 20, 16, 31, 39, 40 | syl132anc 1390 |
. . . . . . 7
⊢ (𝜑 → ((𝑇 ∨ 𝑄) ∧ (𝑇 ∨ 𝑅)) = 𝑇) |
| 42 | 23, 41 | eqtr2d 2778 |
. . . . . 6
⊢ (𝜑 → 𝑇 = ((𝑄 ∨ 𝑇) ∧ (𝑅 ∨ 𝑇))) |
| 43 | 42 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝐶 = 𝐷) → 𝑇 = ((𝑄 ∨ 𝑇) ∧ (𝑅 ∨ 𝑇))) |
| 44 | 1 | 4atexlemkl 40059 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐾 ∈ Lat) |
| 45 | 1, 3, 5 | 4atexlemqtb 40063 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑄 ∨ 𝑇) ∈ (Base‘𝐾)) |
| 46 | 1, 3, 5 | 4atexlempsb 40062 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑃 ∨ 𝑆) ∈ (Base‘𝐾)) |
| 47 | | eqid 2737 |
. . . . . . . . . . 11
⊢
(Base‘𝐾) =
(Base‘𝐾) |
| 48 | 47, 2, 4 | latmle1 18509 |
. . . . . . . . . 10
⊢ ((𝐾 ∈ Lat ∧ (𝑄 ∨ 𝑇) ∈ (Base‘𝐾) ∧ (𝑃 ∨ 𝑆) ∈ (Base‘𝐾)) → ((𝑄 ∨ 𝑇) ∧ (𝑃 ∨ 𝑆)) ≤ (𝑄 ∨ 𝑇)) |
| 49 | 44, 45, 46, 48 | syl3anc 1373 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑄 ∨ 𝑇) ∧ (𝑃 ∨ 𝑆)) ≤ (𝑄 ∨ 𝑇)) |
| 50 | 10, 49 | eqbrtrid 5178 |
. . . . . . . 8
⊢ (𝜑 → 𝐶 ≤ (𝑄 ∨ 𝑇)) |
| 51 | 50 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐶 = 𝐷) → 𝐶 ≤ (𝑄 ∨ 𝑇)) |
| 52 | | simpr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐶 = 𝐷) → 𝐶 = 𝐷) |
| 53 | | 4thatlem0.d |
. . . . . . . . . 10
⊢ 𝐷 = ((𝑅 ∨ 𝑇) ∧ (𝑃 ∨ 𝑆)) |
| 54 | 47, 3, 5 | hlatjcl 39368 |
. . . . . . . . . . . 12
⊢ ((𝐾 ∈ HL ∧ 𝑅 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) → (𝑅 ∨ 𝑇) ∈ (Base‘𝐾)) |
| 55 | 14, 20, 16, 54 | syl3anc 1373 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑅 ∨ 𝑇) ∈ (Base‘𝐾)) |
| 56 | 47, 2, 4 | latmle1 18509 |
. . . . . . . . . . 11
⊢ ((𝐾 ∈ Lat ∧ (𝑅 ∨ 𝑇) ∈ (Base‘𝐾) ∧ (𝑃 ∨ 𝑆) ∈ (Base‘𝐾)) → ((𝑅 ∨ 𝑇) ∧ (𝑃 ∨ 𝑆)) ≤ (𝑅 ∨ 𝑇)) |
| 57 | 44, 55, 46, 56 | syl3anc 1373 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑅 ∨ 𝑇) ∧ (𝑃 ∨ 𝑆)) ≤ (𝑅 ∨ 𝑇)) |
| 58 | 53, 57 | eqbrtrid 5178 |
. . . . . . . . 9
⊢ (𝜑 → 𝐷 ≤ (𝑅 ∨ 𝑇)) |
| 59 | 58 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐶 = 𝐷) → 𝐷 ≤ (𝑅 ∨ 𝑇)) |
| 60 | 52, 59 | eqbrtrd 5165 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐶 = 𝐷) → 𝐶 ≤ (𝑅 ∨ 𝑇)) |
| 61 | 1, 2, 3, 4, 5, 6, 7, 8, 10 | 4atexlemc 40071 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐶 ∈ 𝐴) |
| 62 | 47, 5 | atbase 39290 |
. . . . . . . . . 10
⊢ (𝐶 ∈ 𝐴 → 𝐶 ∈ (Base‘𝐾)) |
| 63 | 61, 62 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝐶 ∈ (Base‘𝐾)) |
| 64 | 47, 2, 4 | latlem12 18511 |
. . . . . . . . 9
⊢ ((𝐾 ∈ Lat ∧ (𝐶 ∈ (Base‘𝐾) ∧ (𝑄 ∨ 𝑇) ∈ (Base‘𝐾) ∧ (𝑅 ∨ 𝑇) ∈ (Base‘𝐾))) → ((𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑇)) ↔ 𝐶 ≤ ((𝑄 ∨ 𝑇) ∧ (𝑅 ∨ 𝑇)))) |
| 65 | 44, 63, 45, 55, 64 | syl13anc 1374 |
. . . . . . . 8
⊢ (𝜑 → ((𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑇)) ↔ 𝐶 ≤ ((𝑄 ∨ 𝑇) ∧ (𝑅 ∨ 𝑇)))) |
| 66 | 65 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐶 = 𝐷) → ((𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑇)) ↔ 𝐶 ≤ ((𝑄 ∨ 𝑇) ∧ (𝑅 ∨ 𝑇)))) |
| 67 | 51, 60, 66 | mpbi2and 712 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐶 = 𝐷) → 𝐶 ≤ ((𝑄 ∨ 𝑇) ∧ (𝑅 ∨ 𝑇))) |
| 68 | | hlatl 39361 |
. . . . . . . . 9
⊢ (𝐾 ∈ HL → 𝐾 ∈ AtLat) |
| 69 | 14, 68 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝐾 ∈ AtLat) |
| 70 | 42, 16 | eqeltrrd 2842 |
. . . . . . . 8
⊢ (𝜑 → ((𝑄 ∨ 𝑇) ∧ (𝑅 ∨ 𝑇)) ∈ 𝐴) |
| 71 | 2, 5 | atcmp 39312 |
. . . . . . . 8
⊢ ((𝐾 ∈ AtLat ∧ 𝐶 ∈ 𝐴 ∧ ((𝑄 ∨ 𝑇) ∧ (𝑅 ∨ 𝑇)) ∈ 𝐴) → (𝐶 ≤ ((𝑄 ∨ 𝑇) ∧ (𝑅 ∨ 𝑇)) ↔ 𝐶 = ((𝑄 ∨ 𝑇) ∧ (𝑅 ∨ 𝑇)))) |
| 72 | 69, 61, 70, 71 | syl3anc 1373 |
. . . . . . 7
⊢ (𝜑 → (𝐶 ≤ ((𝑄 ∨ 𝑇) ∧ (𝑅 ∨ 𝑇)) ↔ 𝐶 = ((𝑄 ∨ 𝑇) ∧ (𝑅 ∨ 𝑇)))) |
| 73 | 72 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐶 = 𝐷) → (𝐶 ≤ ((𝑄 ∨ 𝑇) ∧ (𝑅 ∨ 𝑇)) ↔ 𝐶 = ((𝑄 ∨ 𝑇) ∧ (𝑅 ∨ 𝑇)))) |
| 74 | 67, 73 | mpbid 232 |
. . . . 5
⊢ ((𝜑 ∧ 𝐶 = 𝐷) → 𝐶 = ((𝑄 ∨ 𝑇) ∧ (𝑅 ∨ 𝑇))) |
| 75 | 43, 74 | eqtr4d 2780 |
. . . 4
⊢ ((𝜑 ∧ 𝐶 = 𝐷) → 𝑇 = 𝐶) |
| 76 | 75 | ex 412 |
. . 3
⊢ (𝜑 → (𝐶 = 𝐷 → 𝑇 = 𝐶)) |
| 77 | 76 | necon3d 2961 |
. 2
⊢ (𝜑 → (𝑇 ≠ 𝐶 → 𝐶 ≠ 𝐷)) |
| 78 | 13, 77 | mpd 15 |
1
⊢ (𝜑 → 𝐶 ≠ 𝐷) |