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

Theorem llnn0 37280
Description: A lattice line is nonzero. (Contributed by NM, 15-Jul-2012.)
Hypotheses
Ref Expression
llnn0.z 0 = (0.‘𝐾)
llnn0.n 𝑁 = (LLines‘𝐾)
Assertion
Ref Expression
llnn0 ((𝐾 ∈ HL ∧ 𝑋𝑁) → 𝑋0 )

Proof of Theorem llnn0
Dummy variable 𝑝 is distinct from all other variables.
StepHypRef Expression
1 eqid 2738 . . . . 5 (Atoms‘𝐾) = (Atoms‘𝐾)
21atex 37170 . . . 4 (𝐾 ∈ HL → (Atoms‘𝐾) ≠ ∅)
3 n0 4270 . . . 4 ((Atoms‘𝐾) ≠ ∅ ↔ ∃𝑝 𝑝 ∈ (Atoms‘𝐾))
42, 3sylib 221 . . 3 (𝐾 ∈ HL → ∃𝑝 𝑝 ∈ (Atoms‘𝐾))
54adantr 484 . 2 ((𝐾 ∈ HL ∧ 𝑋𝑁) → ∃𝑝 𝑝 ∈ (Atoms‘𝐾))
6 eqid 2738 . . . . 5 (le‘𝐾) = (le‘𝐾)
7 llnn0.n . . . . 5 𝑁 = (LLines‘𝐾)
86, 1, 7llnnleat 37277 . . . 4 ((𝐾 ∈ HL ∧ 𝑋𝑁𝑝 ∈ (Atoms‘𝐾)) → ¬ 𝑋(le‘𝐾)𝑝)
983expa 1120 . . 3 (((𝐾 ∈ HL ∧ 𝑋𝑁) ∧ 𝑝 ∈ (Atoms‘𝐾)) → ¬ 𝑋(le‘𝐾)𝑝)
10 hlop 37126 . . . . . . 7 (𝐾 ∈ HL → 𝐾 ∈ OP)
1110ad2antrr 726 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑋𝑁) ∧ 𝑝 ∈ (Atoms‘𝐾)) → 𝐾 ∈ OP)
12 eqid 2738 . . . . . . . 8 (Base‘𝐾) = (Base‘𝐾)
1312, 1atbase 37053 . . . . . . 7 (𝑝 ∈ (Atoms‘𝐾) → 𝑝 ∈ (Base‘𝐾))
1413adantl 485 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑋𝑁) ∧ 𝑝 ∈ (Atoms‘𝐾)) → 𝑝 ∈ (Base‘𝐾))
15 llnn0.z . . . . . . 7 0 = (0.‘𝐾)
1612, 6, 15op0le 36950 . . . . . 6 ((𝐾 ∈ OP ∧ 𝑝 ∈ (Base‘𝐾)) → 0 (le‘𝐾)𝑝)
1711, 14, 16syl2anc 587 . . . . 5 (((𝐾 ∈ HL ∧ 𝑋𝑁) ∧ 𝑝 ∈ (Atoms‘𝐾)) → 0 (le‘𝐾)𝑝)
18 breq1 5065 . . . . 5 (𝑋 = 0 → (𝑋(le‘𝐾)𝑝0 (le‘𝐾)𝑝))
1917, 18syl5ibrcom 250 . . . 4 (((𝐾 ∈ HL ∧ 𝑋𝑁) ∧ 𝑝 ∈ (Atoms‘𝐾)) → (𝑋 = 0𝑋(le‘𝐾)𝑝))
2019necon3bd 2955 . . 3 (((𝐾 ∈ HL ∧ 𝑋𝑁) ∧ 𝑝 ∈ (Atoms‘𝐾)) → (¬ 𝑋(le‘𝐾)𝑝𝑋0 ))
219, 20mpd 15 . 2 (((𝐾 ∈ HL ∧ 𝑋𝑁) ∧ 𝑝 ∈ (Atoms‘𝐾)) → 𝑋0 )
225, 21exlimddv 1943 1 ((𝐾 ∈ HL ∧ 𝑋𝑁) → 𝑋0 )
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 399   = wceq 1543  wex 1787  wcel 2111  wne 2941  c0 4246   class class class wbr 5062  cfv 6389  Basecbs 16773  lecple 16822  0.cp0 17942  OPcops 36936  Atomscatm 37027  HLchlt 37114  LLinesclln 37255
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2159  ax-12 2176  ax-ext 2709  ax-rep 5188  ax-sep 5201  ax-nul 5208  ax-pow 5267  ax-pr 5331  ax-un 7532
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2072  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2887  df-ne 2942  df-ral 3067  df-rex 3068  df-reu 3069  df-rab 3071  df-v 3417  df-sbc 3704  df-csb 3821  df-dif 3878  df-un 3880  df-in 3882  df-ss 3892  df-nul 4247  df-if 4449  df-pw 4524  df-sn 4551  df-pr 4553  df-op 4557  df-uni 4829  df-iun 4915  df-br 5063  df-opab 5125  df-mpt 5145  df-id 5464  df-xp 5566  df-rel 5567  df-cnv 5568  df-co 5569  df-dm 5570  df-rn 5571  df-res 5572  df-ima 5573  df-iota 6347  df-fun 6391  df-fn 6392  df-f 6393  df-f1 6394  df-fo 6395  df-f1o 6396  df-fv 6397  df-riota 7179  df-ov 7225  df-oprab 7226  df-proset 17815  df-poset 17833  df-plt 17849  df-lub 17865  df-glb 17866  df-join 17867  df-meet 17868  df-p0 17944  df-p1 17945  df-lat 17951  df-clat 18018  df-oposet 36940  df-ol 36942  df-oml 36943  df-covers 37030  df-ats 37031  df-atl 37062  df-cvlat 37086  df-hlat 37115  df-llines 37262
This theorem is referenced by:  2llnm3N  37333  cdleme22b  38105
  Copyright terms: Public domain W3C validator