Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  llncvrlpln Structured version   Visualization version   GIF version

Theorem llncvrlpln 36087
Description: An element covering a lattice line is a lattice plane and vice-versa. (Contributed by NM, 26-Jun-2012.)
Hypotheses
Ref Expression
llncvrlpln.b 𝐵 = (Base‘𝐾)
llncvrlpln.c 𝐶 = ( ⋖ ‘𝐾)
llncvrlpln.n 𝑁 = (LLines‘𝐾)
llncvrlpln.p 𝑃 = (LPlanes‘𝐾)
Assertion
Ref Expression
llncvrlpln (((𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵) ∧ 𝑋𝐶𝑌) → (𝑋𝑁𝑌𝑃))

Proof of Theorem llncvrlpln
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 simpll1 1192 . . 3 ((((𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵) ∧ 𝑋𝐶𝑌) ∧ 𝑋𝑁) → 𝐾 ∈ HL)
2 simpll3 1194 . . 3 ((((𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵) ∧ 𝑋𝐶𝑌) ∧ 𝑋𝑁) → 𝑌𝐵)
3 simpr 477 . . 3 ((((𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵) ∧ 𝑋𝐶𝑌) ∧ 𝑋𝑁) → 𝑋𝑁)
4 simplr 756 . . 3 ((((𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵) ∧ 𝑋𝐶𝑌) ∧ 𝑋𝑁) → 𝑋𝐶𝑌)
5 llncvrlpln.b . . . 4 𝐵 = (Base‘𝐾)
6 llncvrlpln.c . . . 4 𝐶 = ( ⋖ ‘𝐾)
7 llncvrlpln.n . . . 4 𝑁 = (LLines‘𝐾)
8 llncvrlpln.p . . . 4 𝑃 = (LPlanes‘𝐾)
95, 6, 7, 8lplni 36061 . . 3 (((𝐾 ∈ HL ∧ 𝑌𝐵𝑋𝑁) ∧ 𝑋𝐶𝑌) → 𝑌𝑃)
101, 2, 3, 4, 9syl31anc 1353 . 2 ((((𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵) ∧ 𝑋𝐶𝑌) ∧ 𝑋𝑁) → 𝑌𝑃)
11 simpll1 1192 . . . 4 ((((𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵) ∧ 𝑋𝐶𝑌) ∧ 𝑌𝑃) → 𝐾 ∈ HL)
12 simpll2 1193 . . . 4 ((((𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵) ∧ 𝑋𝐶𝑌) ∧ 𝑌𝑃) → 𝑋𝐵)
13 eqid 2772 . . . . . . 7 (Atoms‘𝐾) = (Atoms‘𝐾)
1413, 8lplnneat 36074 . . . . . 6 ((𝐾 ∈ HL ∧ 𝑌𝑃) → ¬ 𝑌 ∈ (Atoms‘𝐾))
1511, 14sylancom 579 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵) ∧ 𝑋𝐶𝑌) ∧ 𝑌𝑃) → ¬ 𝑌 ∈ (Atoms‘𝐾))
16 simplr 756 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵) ∧ 𝑋𝐶𝑌) ∧ 𝑌𝑃) → 𝑋𝐶𝑌)
17 breq1 4926 . . . . . . . 8 (𝑋 = (0.‘𝐾) → (𝑋𝐶𝑌 ↔ (0.‘𝐾)𝐶𝑌))
1816, 17syl5ibcom 237 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵) ∧ 𝑋𝐶𝑌) ∧ 𝑌𝑃) → (𝑋 = (0.‘𝐾) → (0.‘𝐾)𝐶𝑌))
19 simpll3 1194 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵) ∧ 𝑋𝐶𝑌) ∧ 𝑌𝑃) → 𝑌𝐵)
20 eqid 2772 . . . . . . . . 9 (0.‘𝐾) = (0.‘𝐾)
215, 20, 6, 13isat2 35816 . . . . . . . 8 ((𝐾 ∈ HL ∧ 𝑌𝐵) → (𝑌 ∈ (Atoms‘𝐾) ↔ (0.‘𝐾)𝐶𝑌))
2211, 19, 21syl2anc 576 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵) ∧ 𝑋𝐶𝑌) ∧ 𝑌𝑃) → (𝑌 ∈ (Atoms‘𝐾) ↔ (0.‘𝐾)𝐶𝑌))
2318, 22sylibrd 251 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵) ∧ 𝑋𝐶𝑌) ∧ 𝑌𝑃) → (𝑋 = (0.‘𝐾) → 𝑌 ∈ (Atoms‘𝐾)))
2423necon3bd 2975 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵) ∧ 𝑋𝐶𝑌) ∧ 𝑌𝑃) → (¬ 𝑌 ∈ (Atoms‘𝐾) → 𝑋 ≠ (0.‘𝐾)))
2515, 24mpd 15 . . . 4 ((((𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵) ∧ 𝑋𝐶𝑌) ∧ 𝑌𝑃) → 𝑋 ≠ (0.‘𝐾))
267, 8lplnnelln 36075 . . . . . 6 ((𝐾 ∈ HL ∧ 𝑌𝑃) → ¬ 𝑌𝑁)
2711, 26sylancom 579 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵) ∧ 𝑋𝐶𝑌) ∧ 𝑌𝑃) → ¬ 𝑌𝑁)
285, 6, 13, 7atcvrlln 36049 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵) ∧ 𝑋𝐶𝑌) → (𝑋 ∈ (Atoms‘𝐾) ↔ 𝑌𝑁))
2928adantr 473 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵) ∧ 𝑋𝐶𝑌) ∧ 𝑌𝑃) → (𝑋 ∈ (Atoms‘𝐾) ↔ 𝑌𝑁))
3027, 29mtbird 317 . . . 4 ((((𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵) ∧ 𝑋𝐶𝑌) ∧ 𝑌𝑃) → ¬ 𝑋 ∈ (Atoms‘𝐾))
31 eqid 2772 . . . . 5 (le‘𝐾) = (le‘𝐾)
325, 31, 20, 13, 7llnle 36047 . . . 4 (((𝐾 ∈ HL ∧ 𝑋𝐵) ∧ (𝑋 ≠ (0.‘𝐾) ∧ ¬ 𝑋 ∈ (Atoms‘𝐾))) → ∃𝑧𝑁 𝑧(le‘𝐾)𝑋)
3311, 12, 25, 30, 32syl22anc 826 . . 3 ((((𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵) ∧ 𝑋𝐶𝑌) ∧ 𝑌𝑃) → ∃𝑧𝑁 𝑧(le‘𝐾)𝑋)
34 simpr3 1176 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵) ∧ 𝑋𝐶𝑌) ∧ (𝑌𝑃𝑧𝑁𝑧(le‘𝐾)𝑋)) → 𝑧(le‘𝐾)𝑋)
35 simpll1 1192 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵) ∧ 𝑋𝐶𝑌) ∧ (𝑌𝑃𝑧𝑁𝑧(le‘𝐾)𝑋)) → 𝐾 ∈ HL)
36 hlop 35891 . . . . . . . . . 10 (𝐾 ∈ HL → 𝐾 ∈ OP)
3735, 36syl 17 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵) ∧ 𝑋𝐶𝑌) ∧ (𝑌𝑃𝑧𝑁𝑧(le‘𝐾)𝑋)) → 𝐾 ∈ OP)
38 simpr2 1175 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵) ∧ 𝑋𝐶𝑌) ∧ (𝑌𝑃𝑧𝑁𝑧(le‘𝐾)𝑋)) → 𝑧𝑁)
395, 7llnbase 36038 . . . . . . . . . 10 (𝑧𝑁𝑧𝐵)
4038, 39syl 17 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵) ∧ 𝑋𝐶𝑌) ∧ (𝑌𝑃𝑧𝑁𝑧(le‘𝐾)𝑋)) → 𝑧𝐵)
41 simpll2 1193 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵) ∧ 𝑋𝐶𝑌) ∧ (𝑌𝑃𝑧𝑁𝑧(le‘𝐾)𝑋)) → 𝑋𝐵)
42 simpll3 1194 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵) ∧ 𝑋𝐶𝑌) ∧ (𝑌𝑃𝑧𝑁𝑧(le‘𝐾)𝑋)) → 𝑌𝐵)
43 simpr1 1174 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵) ∧ 𝑋𝐶𝑌) ∧ (𝑌𝑃𝑧𝑁𝑧(le‘𝐾)𝑋)) → 𝑌𝑃)
445, 31, 6cvrle 35807 . . . . . . . . . . . 12 (((𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵) ∧ 𝑋𝐶𝑌) → 𝑋(le‘𝐾)𝑌)
4544adantr 473 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵) ∧ 𝑋𝐶𝑌) ∧ (𝑌𝑃𝑧𝑁𝑧(le‘𝐾)𝑋)) → 𝑋(le‘𝐾)𝑌)
46 hlpos 35895 . . . . . . . . . . . . 13 (𝐾 ∈ HL → 𝐾 ∈ Poset)
4735, 46syl 17 . . . . . . . . . . . 12 ((((𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵) ∧ 𝑋𝐶𝑌) ∧ (𝑌𝑃𝑧𝑁𝑧(le‘𝐾)𝑋)) → 𝐾 ∈ Poset)
485, 31postr 17411 . . . . . . . . . . . 12 ((𝐾 ∈ Poset ∧ (𝑧𝐵𝑋𝐵𝑌𝐵)) → ((𝑧(le‘𝐾)𝑋𝑋(le‘𝐾)𝑌) → 𝑧(le‘𝐾)𝑌))
4947, 40, 41, 42, 48syl13anc 1352 . . . . . . . . . . 11 ((((𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵) ∧ 𝑋𝐶𝑌) ∧ (𝑌𝑃𝑧𝑁𝑧(le‘𝐾)𝑋)) → ((𝑧(le‘𝐾)𝑋𝑋(le‘𝐾)𝑌) → 𝑧(le‘𝐾)𝑌))
5034, 45, 49mp2and 686 . . . . . . . . . 10 ((((𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵) ∧ 𝑋𝐶𝑌) ∧ (𝑌𝑃𝑧𝑁𝑧(le‘𝐾)𝑋)) → 𝑧(le‘𝐾)𝑌)
5131, 6, 7, 8llncvrlpln2 36086 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑧𝑁𝑌𝑃) ∧ 𝑧(le‘𝐾)𝑌) → 𝑧𝐶𝑌)
5235, 38, 43, 50, 51syl31anc 1353 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵) ∧ 𝑋𝐶𝑌) ∧ (𝑌𝑃𝑧𝑁𝑧(le‘𝐾)𝑋)) → 𝑧𝐶𝑌)
53 simplr 756 . . . . . . . . 9 ((((𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵) ∧ 𝑋𝐶𝑌) ∧ (𝑌𝑃𝑧𝑁𝑧(le‘𝐾)𝑋)) → 𝑋𝐶𝑌)
545, 31, 6cvrcmp2 35813 . . . . . . . . 9 ((𝐾 ∈ OP ∧ (𝑧𝐵𝑋𝐵𝑌𝐵) ∧ (𝑧𝐶𝑌𝑋𝐶𝑌)) → (𝑧(le‘𝐾)𝑋𝑧 = 𝑋))
5537, 40, 41, 42, 52, 53, 54syl132anc 1368 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵) ∧ 𝑋𝐶𝑌) ∧ (𝑌𝑃𝑧𝑁𝑧(le‘𝐾)𝑋)) → (𝑧(le‘𝐾)𝑋𝑧 = 𝑋))
5634, 55mpbid 224 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵) ∧ 𝑋𝐶𝑌) ∧ (𝑌𝑃𝑧𝑁𝑧(le‘𝐾)𝑋)) → 𝑧 = 𝑋)
5756, 38eqeltrrd 2861 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵) ∧ 𝑋𝐶𝑌) ∧ (𝑌𝑃𝑧𝑁𝑧(le‘𝐾)𝑋)) → 𝑋𝑁)
58573exp2 1334 . . . . 5 (((𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵) ∧ 𝑋𝐶𝑌) → (𝑌𝑃 → (𝑧𝑁 → (𝑧(le‘𝐾)𝑋𝑋𝑁))))
5958imp 398 . . . 4 ((((𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵) ∧ 𝑋𝐶𝑌) ∧ 𝑌𝑃) → (𝑧𝑁 → (𝑧(le‘𝐾)𝑋𝑋𝑁)))
6059rexlimdv 3222 . . 3 ((((𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵) ∧ 𝑋𝐶𝑌) ∧ 𝑌𝑃) → (∃𝑧𝑁 𝑧(le‘𝐾)𝑋𝑋𝑁))
6133, 60mpd 15 . 2 ((((𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵) ∧ 𝑋𝐶𝑌) ∧ 𝑌𝑃) → 𝑋𝑁)
6210, 61impbida 788 1 (((𝐾 ∈ HL ∧ 𝑋𝐵𝑌𝐵) ∧ 𝑋𝐶𝑌) → (𝑋𝑁𝑌𝑃))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 198  wa 387  w3a 1068   = wceq 1507  wcel 2048  wne 2961  wrex 3083   class class class wbr 4923  cfv 6182  Basecbs 16329  lecple 16418  Posetcpo 17398  0.cp0 17495  OPcops 35701  ccvr 35791  Atomscatm 35792  HLchlt 35879  LLinesclln 36020  LPlanesclpl 36021
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1964  ax-8 2050  ax-9 2057  ax-10 2077  ax-11 2091  ax-12 2104  ax-13 2299  ax-ext 2745  ax-rep 5043  ax-sep 5054  ax-nul 5061  ax-pow 5113  ax-pr 5180  ax-un 7273
This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2014  df-mo 2544  df-eu 2580  df-clab 2754  df-cleq 2765  df-clel 2840  df-nfc 2912  df-ne 2962  df-ral 3087  df-rex 3088  df-reu 3089  df-rab 3091  df-v 3411  df-sbc 3678  df-csb 3783  df-dif 3828  df-un 3830  df-in 3832  df-ss 3839  df-nul 4174  df-if 4345  df-pw 4418  df-sn 4436  df-pr 4438  df-op 4442  df-uni 4707  df-iun 4788  df-br 4924  df-opab 4986  df-mpt 5003  df-id 5305  df-xp 5406  df-rel 5407  df-cnv 5408  df-co 5409  df-dm 5410  df-rn 5411  df-res 5412  df-ima 5413  df-iota 6146  df-fun 6184  df-fn 6185  df-f 6186  df-f1 6187  df-fo 6188  df-f1o 6189  df-fv 6190  df-riota 6931  df-ov 6973  df-oprab 6974  df-proset 17386  df-poset 17404  df-plt 17416  df-lub 17432  df-glb 17433  df-join 17434  df-meet 17435  df-p0 17497  df-lat 17504  df-clat 17566  df-oposet 35705  df-ol 35707  df-oml 35708  df-covers 35795  df-ats 35796  df-atl 35827  df-cvlat 35851  df-hlat 35880  df-llines 36027  df-lplanes 36028
This theorem is referenced by:  2lplnmN  36088  2llnmj  36089  lplncvrlvol  36145  2lplnm2N  36150  2lplnmj  36151
  Copyright terms: Public domain W3C validator