| Step | Hyp | Ref
| Expression |
| 1 | | simpll1 1213 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋𝐶𝑌) ∧ 𝑋 ∈ 𝑁) → 𝐾 ∈ HL) |
| 2 | | simpll3 1215 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋𝐶𝑌) ∧ 𝑋 ∈ 𝑁) → 𝑌 ∈ 𝐵) |
| 3 | | simpr 484 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋𝐶𝑌) ∧ 𝑋 ∈ 𝑁) → 𝑋 ∈ 𝑁) |
| 4 | | simplr 769 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋𝐶𝑌) ∧ 𝑋 ∈ 𝑁) → 𝑋𝐶𝑌) |
| 5 | | llncvrlpln.b |
. . . 4
⊢ 𝐵 = (Base‘𝐾) |
| 6 | | llncvrlpln.c |
. . . 4
⊢ 𝐶 = ( ⋖ ‘𝐾) |
| 7 | | llncvrlpln.n |
. . . 4
⊢ 𝑁 = (LLines‘𝐾) |
| 8 | | llncvrlpln.p |
. . . 4
⊢ 𝑃 = (LPlanes‘𝐾) |
| 9 | 5, 6, 7, 8 | lplni 39534 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝑁) ∧ 𝑋𝐶𝑌) → 𝑌 ∈ 𝑃) |
| 10 | 1, 2, 3, 4, 9 | syl31anc 1375 |
. 2
⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋𝐶𝑌) ∧ 𝑋 ∈ 𝑁) → 𝑌 ∈ 𝑃) |
| 11 | | simpll1 1213 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋𝐶𝑌) ∧ 𝑌 ∈ 𝑃) → 𝐾 ∈ HL) |
| 12 | | simpll2 1214 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋𝐶𝑌) ∧ 𝑌 ∈ 𝑃) → 𝑋 ∈ 𝐵) |
| 13 | | eqid 2737 |
. . . . . . 7
⊢
(Atoms‘𝐾) =
(Atoms‘𝐾) |
| 14 | 13, 8 | lplnneat 39547 |
. . . . . 6
⊢ ((𝐾 ∈ HL ∧ 𝑌 ∈ 𝑃) → ¬ 𝑌 ∈ (Atoms‘𝐾)) |
| 15 | 11, 14 | sylancom 588 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋𝐶𝑌) ∧ 𝑌 ∈ 𝑃) → ¬ 𝑌 ∈ (Atoms‘𝐾)) |
| 16 | | simplr 769 |
. . . . . . . 8
⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋𝐶𝑌) ∧ 𝑌 ∈ 𝑃) → 𝑋𝐶𝑌) |
| 17 | | breq1 5146 |
. . . . . . . 8
⊢ (𝑋 = (0.‘𝐾) → (𝑋𝐶𝑌 ↔ (0.‘𝐾)𝐶𝑌)) |
| 18 | 16, 17 | syl5ibcom 245 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋𝐶𝑌) ∧ 𝑌 ∈ 𝑃) → (𝑋 = (0.‘𝐾) → (0.‘𝐾)𝐶𝑌)) |
| 19 | | simpll3 1215 |
. . . . . . . 8
⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋𝐶𝑌) ∧ 𝑌 ∈ 𝑃) → 𝑌 ∈ 𝐵) |
| 20 | | eqid 2737 |
. . . . . . . . 9
⊢
(0.‘𝐾) =
(0.‘𝐾) |
| 21 | 5, 20, 6, 13 | isat2 39288 |
. . . . . . . 8
⊢ ((𝐾 ∈ HL ∧ 𝑌 ∈ 𝐵) → (𝑌 ∈ (Atoms‘𝐾) ↔ (0.‘𝐾)𝐶𝑌)) |
| 22 | 11, 19, 21 | syl2anc 584 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋𝐶𝑌) ∧ 𝑌 ∈ 𝑃) → (𝑌 ∈ (Atoms‘𝐾) ↔ (0.‘𝐾)𝐶𝑌)) |
| 23 | 18, 22 | sylibrd 259 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋𝐶𝑌) ∧ 𝑌 ∈ 𝑃) → (𝑋 = (0.‘𝐾) → 𝑌 ∈ (Atoms‘𝐾))) |
| 24 | 23 | necon3bd 2954 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋𝐶𝑌) ∧ 𝑌 ∈ 𝑃) → (¬ 𝑌 ∈ (Atoms‘𝐾) → 𝑋 ≠ (0.‘𝐾))) |
| 25 | 15, 24 | mpd 15 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋𝐶𝑌) ∧ 𝑌 ∈ 𝑃) → 𝑋 ≠ (0.‘𝐾)) |
| 26 | 7, 8 | lplnnelln 39548 |
. . . . . 6
⊢ ((𝐾 ∈ HL ∧ 𝑌 ∈ 𝑃) → ¬ 𝑌 ∈ 𝑁) |
| 27 | 11, 26 | sylancom 588 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋𝐶𝑌) ∧ 𝑌 ∈ 𝑃) → ¬ 𝑌 ∈ 𝑁) |
| 28 | 5, 6, 13, 7 | atcvrlln 39522 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋𝐶𝑌) → (𝑋 ∈ (Atoms‘𝐾) ↔ 𝑌 ∈ 𝑁)) |
| 29 | 28 | adantr 480 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋𝐶𝑌) ∧ 𝑌 ∈ 𝑃) → (𝑋 ∈ (Atoms‘𝐾) ↔ 𝑌 ∈ 𝑁)) |
| 30 | 27, 29 | mtbird 325 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋𝐶𝑌) ∧ 𝑌 ∈ 𝑃) → ¬ 𝑋 ∈ (Atoms‘𝐾)) |
| 31 | | eqid 2737 |
. . . . 5
⊢
(le‘𝐾) =
(le‘𝐾) |
| 32 | 5, 31, 20, 13, 7 | llnle 39520 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵) ∧ (𝑋 ≠ (0.‘𝐾) ∧ ¬ 𝑋 ∈ (Atoms‘𝐾))) → ∃𝑧 ∈ 𝑁 𝑧(le‘𝐾)𝑋) |
| 33 | 11, 12, 25, 30, 32 | syl22anc 839 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋𝐶𝑌) ∧ 𝑌 ∈ 𝑃) → ∃𝑧 ∈ 𝑁 𝑧(le‘𝐾)𝑋) |
| 34 | | simpr3 1197 |
. . . . . . . 8
⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋𝐶𝑌) ∧ (𝑌 ∈ 𝑃 ∧ 𝑧 ∈ 𝑁 ∧ 𝑧(le‘𝐾)𝑋)) → 𝑧(le‘𝐾)𝑋) |
| 35 | | simpll1 1213 |
. . . . . . . . . 10
⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋𝐶𝑌) ∧ (𝑌 ∈ 𝑃 ∧ 𝑧 ∈ 𝑁 ∧ 𝑧(le‘𝐾)𝑋)) → 𝐾 ∈ HL) |
| 36 | | hlop 39363 |
. . . . . . . . . 10
⊢ (𝐾 ∈ HL → 𝐾 ∈ OP) |
| 37 | 35, 36 | syl 17 |
. . . . . . . . 9
⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋𝐶𝑌) ∧ (𝑌 ∈ 𝑃 ∧ 𝑧 ∈ 𝑁 ∧ 𝑧(le‘𝐾)𝑋)) → 𝐾 ∈ OP) |
| 38 | | simpr2 1196 |
. . . . . . . . . 10
⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋𝐶𝑌) ∧ (𝑌 ∈ 𝑃 ∧ 𝑧 ∈ 𝑁 ∧ 𝑧(le‘𝐾)𝑋)) → 𝑧 ∈ 𝑁) |
| 39 | 5, 7 | llnbase 39511 |
. . . . . . . . . 10
⊢ (𝑧 ∈ 𝑁 → 𝑧 ∈ 𝐵) |
| 40 | 38, 39 | syl 17 |
. . . . . . . . 9
⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋𝐶𝑌) ∧ (𝑌 ∈ 𝑃 ∧ 𝑧 ∈ 𝑁 ∧ 𝑧(le‘𝐾)𝑋)) → 𝑧 ∈ 𝐵) |
| 41 | | simpll2 1214 |
. . . . . . . . 9
⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋𝐶𝑌) ∧ (𝑌 ∈ 𝑃 ∧ 𝑧 ∈ 𝑁 ∧ 𝑧(le‘𝐾)𝑋)) → 𝑋 ∈ 𝐵) |
| 42 | | simpll3 1215 |
. . . . . . . . 9
⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋𝐶𝑌) ∧ (𝑌 ∈ 𝑃 ∧ 𝑧 ∈ 𝑁 ∧ 𝑧(le‘𝐾)𝑋)) → 𝑌 ∈ 𝐵) |
| 43 | | simpr1 1195 |
. . . . . . . . . 10
⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋𝐶𝑌) ∧ (𝑌 ∈ 𝑃 ∧ 𝑧 ∈ 𝑁 ∧ 𝑧(le‘𝐾)𝑋)) → 𝑌 ∈ 𝑃) |
| 44 | 5, 31, 6 | cvrle 39279 |
. . . . . . . . . . . 12
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋𝐶𝑌) → 𝑋(le‘𝐾)𝑌) |
| 45 | 44 | adantr 480 |
. . . . . . . . . . 11
⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋𝐶𝑌) ∧ (𝑌 ∈ 𝑃 ∧ 𝑧 ∈ 𝑁 ∧ 𝑧(le‘𝐾)𝑋)) → 𝑋(le‘𝐾)𝑌) |
| 46 | | hlpos 39367 |
. . . . . . . . . . . . 13
⊢ (𝐾 ∈ HL → 𝐾 ∈ Poset) |
| 47 | 35, 46 | syl 17 |
. . . . . . . . . . . 12
⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋𝐶𝑌) ∧ (𝑌 ∈ 𝑃 ∧ 𝑧 ∈ 𝑁 ∧ 𝑧(le‘𝐾)𝑋)) → 𝐾 ∈ Poset) |
| 48 | 5, 31 | postr 18366 |
. . . . . . . . . . . 12
⊢ ((𝐾 ∈ Poset ∧ (𝑧 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → ((𝑧(le‘𝐾)𝑋 ∧ 𝑋(le‘𝐾)𝑌) → 𝑧(le‘𝐾)𝑌)) |
| 49 | 47, 40, 41, 42, 48 | syl13anc 1374 |
. . . . . . . . . . 11
⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋𝐶𝑌) ∧ (𝑌 ∈ 𝑃 ∧ 𝑧 ∈ 𝑁 ∧ 𝑧(le‘𝐾)𝑋)) → ((𝑧(le‘𝐾)𝑋 ∧ 𝑋(le‘𝐾)𝑌) → 𝑧(le‘𝐾)𝑌)) |
| 50 | 34, 45, 49 | mp2and 699 |
. . . . . . . . . 10
⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋𝐶𝑌) ∧ (𝑌 ∈ 𝑃 ∧ 𝑧 ∈ 𝑁 ∧ 𝑧(le‘𝐾)𝑋)) → 𝑧(le‘𝐾)𝑌) |
| 51 | 31, 6, 7, 8 | llncvrlpln2 39559 |
. . . . . . . . . 10
⊢ (((𝐾 ∈ HL ∧ 𝑧 ∈ 𝑁 ∧ 𝑌 ∈ 𝑃) ∧ 𝑧(le‘𝐾)𝑌) → 𝑧𝐶𝑌) |
| 52 | 35, 38, 43, 50, 51 | syl31anc 1375 |
. . . . . . . . 9
⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋𝐶𝑌) ∧ (𝑌 ∈ 𝑃 ∧ 𝑧 ∈ 𝑁 ∧ 𝑧(le‘𝐾)𝑋)) → 𝑧𝐶𝑌) |
| 53 | | simplr 769 |
. . . . . . . . 9
⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋𝐶𝑌) ∧ (𝑌 ∈ 𝑃 ∧ 𝑧 ∈ 𝑁 ∧ 𝑧(le‘𝐾)𝑋)) → 𝑋𝐶𝑌) |
| 54 | 5, 31, 6 | cvrcmp2 39285 |
. . . . . . . . 9
⊢ ((𝐾 ∈ OP ∧ (𝑧 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑧𝐶𝑌 ∧ 𝑋𝐶𝑌)) → (𝑧(le‘𝐾)𝑋 ↔ 𝑧 = 𝑋)) |
| 55 | 37, 40, 41, 42, 52, 53, 54 | syl132anc 1390 |
. . . . . . . 8
⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋𝐶𝑌) ∧ (𝑌 ∈ 𝑃 ∧ 𝑧 ∈ 𝑁 ∧ 𝑧(le‘𝐾)𝑋)) → (𝑧(le‘𝐾)𝑋 ↔ 𝑧 = 𝑋)) |
| 56 | 34, 55 | mpbid 232 |
. . . . . . 7
⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋𝐶𝑌) ∧ (𝑌 ∈ 𝑃 ∧ 𝑧 ∈ 𝑁 ∧ 𝑧(le‘𝐾)𝑋)) → 𝑧 = 𝑋) |
| 57 | 56, 38 | eqeltrrd 2842 |
. . . . . 6
⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋𝐶𝑌) ∧ (𝑌 ∈ 𝑃 ∧ 𝑧 ∈ 𝑁 ∧ 𝑧(le‘𝐾)𝑋)) → 𝑋 ∈ 𝑁) |
| 58 | 57 | 3exp2 1355 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋𝐶𝑌) → (𝑌 ∈ 𝑃 → (𝑧 ∈ 𝑁 → (𝑧(le‘𝐾)𝑋 → 𝑋 ∈ 𝑁)))) |
| 59 | 58 | imp 406 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋𝐶𝑌) ∧ 𝑌 ∈ 𝑃) → (𝑧 ∈ 𝑁 → (𝑧(le‘𝐾)𝑋 → 𝑋 ∈ 𝑁))) |
| 60 | 59 | rexlimdv 3153 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋𝐶𝑌) ∧ 𝑌 ∈ 𝑃) → (∃𝑧 ∈ 𝑁 𝑧(le‘𝐾)𝑋 → 𝑋 ∈ 𝑁)) |
| 61 | 33, 60 | mpd 15 |
. 2
⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋𝐶𝑌) ∧ 𝑌 ∈ 𝑃) → 𝑋 ∈ 𝑁) |
| 62 | 10, 61 | impbida 801 |
1
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋𝐶𝑌) → (𝑋 ∈ 𝑁 ↔ 𝑌 ∈ 𝑃)) |