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

Theorem llnexatN 34308
 Description: Given an atom on a line, there is another atom whose join equals the line. (Contributed by NM, 26-Jun-2012.) (New usage is discouraged.)
Hypotheses
Ref Expression
llnexat.l = (le‘𝐾)
llnexat.j = (join‘𝐾)
llnexat.a 𝐴 = (Atoms‘𝐾)
llnexat.n 𝑁 = (LLines‘𝐾)
Assertion
Ref Expression
llnexatN (((𝐾 ∈ HL ∧ 𝑋𝑁𝑃𝐴) ∧ 𝑃 𝑋) → ∃𝑞𝐴 (𝑃𝑞𝑋 = (𝑃 𝑞)))
Distinct variable groups:   𝐴,𝑞   𝐾,𝑞   ,𝑞   𝑁,𝑞   𝑃,𝑞   𝑋,𝑞
Allowed substitution hint:   (𝑞)

Proof of Theorem llnexatN
StepHypRef Expression
1 simp1 1059 . . . 4 ((𝐾 ∈ HL ∧ 𝑋𝑁𝑃𝐴) → 𝐾 ∈ HL)
2 simp3 1061 . . . 4 ((𝐾 ∈ HL ∧ 𝑋𝑁𝑃𝐴) → 𝑃𝐴)
3 simp2 1060 . . . 4 ((𝐾 ∈ HL ∧ 𝑋𝑁𝑃𝐴) → 𝑋𝑁)
41, 2, 33jca 1240 . . 3 ((𝐾 ∈ HL ∧ 𝑋𝑁𝑃𝐴) → (𝐾 ∈ HL ∧ 𝑃𝐴𝑋𝑁))
5 llnexat.l . . . 4 = (le‘𝐾)
6 eqid 2621 . . . 4 ( ⋖ ‘𝐾) = ( ⋖ ‘𝐾)
7 llnexat.a . . . 4 𝐴 = (Atoms‘𝐾)
8 llnexat.n . . . 4 𝑁 = (LLines‘𝐾)
95, 6, 7, 8atcvrlln2 34306 . . 3 (((𝐾 ∈ HL ∧ 𝑃𝐴𝑋𝑁) ∧ 𝑃 𝑋) → 𝑃( ⋖ ‘𝐾)𝑋)
104, 9sylan 488 . 2 (((𝐾 ∈ HL ∧ 𝑋𝑁𝑃𝐴) ∧ 𝑃 𝑋) → 𝑃( ⋖ ‘𝐾)𝑋)
11 simpl1 1062 . . . 4 (((𝐾 ∈ HL ∧ 𝑋𝑁𝑃𝐴) ∧ 𝑃 𝑋) → 𝐾 ∈ HL)
12 simpl3 1064 . . . . 5 (((𝐾 ∈ HL ∧ 𝑋𝑁𝑃𝐴) ∧ 𝑃 𝑋) → 𝑃𝐴)
13 eqid 2621 . . . . . 6 (Base‘𝐾) = (Base‘𝐾)
1413, 7atbase 34077 . . . . 5 (𝑃𝐴𝑃 ∈ (Base‘𝐾))
1512, 14syl 17 . . . 4 (((𝐾 ∈ HL ∧ 𝑋𝑁𝑃𝐴) ∧ 𝑃 𝑋) → 𝑃 ∈ (Base‘𝐾))
16 simpl2 1063 . . . . 5 (((𝐾 ∈ HL ∧ 𝑋𝑁𝑃𝐴) ∧ 𝑃 𝑋) → 𝑋𝑁)
1713, 8llnbase 34296 . . . . 5 (𝑋𝑁𝑋 ∈ (Base‘𝐾))
1816, 17syl 17 . . . 4 (((𝐾 ∈ HL ∧ 𝑋𝑁𝑃𝐴) ∧ 𝑃 𝑋) → 𝑋 ∈ (Base‘𝐾))
19 llnexat.j . . . . 5 = (join‘𝐾)
2013, 5, 19, 6, 7cvrval3 34200 . . . 4 ((𝐾 ∈ HL ∧ 𝑃 ∈ (Base‘𝐾) ∧ 𝑋 ∈ (Base‘𝐾)) → (𝑃( ⋖ ‘𝐾)𝑋 ↔ ∃𝑞𝐴𝑞 𝑃 ∧ (𝑃 𝑞) = 𝑋)))
2111, 15, 18, 20syl3anc 1323 . . 3 (((𝐾 ∈ HL ∧ 𝑋𝑁𝑃𝐴) ∧ 𝑃 𝑋) → (𝑃( ⋖ ‘𝐾)𝑋 ↔ ∃𝑞𝐴𝑞 𝑃 ∧ (𝑃 𝑞) = 𝑋)))
22 simpll1 1098 . . . . . . . 8 ((((𝐾 ∈ HL ∧ 𝑋𝑁𝑃𝐴) ∧ 𝑃 𝑋) ∧ 𝑞𝐴) → 𝐾 ∈ HL)
23 hlatl 34148 . . . . . . . 8 (𝐾 ∈ HL → 𝐾 ∈ AtLat)
2422, 23syl 17 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑋𝑁𝑃𝐴) ∧ 𝑃 𝑋) ∧ 𝑞𝐴) → 𝐾 ∈ AtLat)
25 simpr 477 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑋𝑁𝑃𝐴) ∧ 𝑃 𝑋) ∧ 𝑞𝐴) → 𝑞𝐴)
26 simpll3 1100 . . . . . . 7 ((((𝐾 ∈ HL ∧ 𝑋𝑁𝑃𝐴) ∧ 𝑃 𝑋) ∧ 𝑞𝐴) → 𝑃𝐴)
275, 7atncmp 34100 . . . . . . 7 ((𝐾 ∈ AtLat ∧ 𝑞𝐴𝑃𝐴) → (¬ 𝑞 𝑃𝑞𝑃))
2824, 25, 26, 27syl3anc 1323 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑋𝑁𝑃𝐴) ∧ 𝑃 𝑋) ∧ 𝑞𝐴) → (¬ 𝑞 𝑃𝑞𝑃))
2928anbi1d 740 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑋𝑁𝑃𝐴) ∧ 𝑃 𝑋) ∧ 𝑞𝐴) → ((¬ 𝑞 𝑃 ∧ (𝑃 𝑞) = 𝑋) ↔ (𝑞𝑃 ∧ (𝑃 𝑞) = 𝑋)))
30 necom 2843 . . . . . 6 (𝑞𝑃𝑃𝑞)
31 eqcom 2628 . . . . . 6 ((𝑃 𝑞) = 𝑋𝑋 = (𝑃 𝑞))
3230, 31anbi12i 732 . . . . 5 ((𝑞𝑃 ∧ (𝑃 𝑞) = 𝑋) ↔ (𝑃𝑞𝑋 = (𝑃 𝑞)))
3329, 32syl6bb 276 . . . 4 ((((𝐾 ∈ HL ∧ 𝑋𝑁𝑃𝐴) ∧ 𝑃 𝑋) ∧ 𝑞𝐴) → ((¬ 𝑞 𝑃 ∧ (𝑃 𝑞) = 𝑋) ↔ (𝑃𝑞𝑋 = (𝑃 𝑞))))
3433rexbidva 3042 . . 3 (((𝐾 ∈ HL ∧ 𝑋𝑁𝑃𝐴) ∧ 𝑃 𝑋) → (∃𝑞𝐴𝑞 𝑃 ∧ (𝑃 𝑞) = 𝑋) ↔ ∃𝑞𝐴 (𝑃𝑞𝑋 = (𝑃 𝑞))))
3521, 34bitrd 268 . 2 (((𝐾 ∈ HL ∧ 𝑋𝑁𝑃𝐴) ∧ 𝑃 𝑋) → (𝑃( ⋖ ‘𝐾)𝑋 ↔ ∃𝑞𝐴 (𝑃𝑞𝑋 = (𝑃 𝑞))))
3610, 35mpbid 222 1 (((𝐾 ∈ HL ∧ 𝑋𝑁𝑃𝐴) ∧ 𝑃 𝑋) → ∃𝑞𝐴 (𝑃𝑞𝑋 = (𝑃 𝑞)))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∧ wa 384   ∧ w3a 1036   = wceq 1480   ∈ wcel 1987   ≠ wne 2790  ∃wrex 2908   class class class wbr 4615  ‘cfv 5849  (class class class)co 6607  Basecbs 15784  lecple 15872  joincjn 16868   ⋖ ccvr 34050  Atomscatm 34051  AtLatcal 34052  HLchlt 34138  LLinesclln 34278 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4733  ax-sep 4743  ax-nul 4751  ax-pow 4805  ax-pr 4869  ax-un 6905 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2912  df-rex 2913  df-reu 2914  df-rab 2916  df-v 3188  df-sbc 3419  df-csb 3516  df-dif 3559  df-un 3561  df-in 3563  df-ss 3570  df-nul 3894  df-if 4061  df-pw 4134  df-sn 4151  df-pr 4153  df-op 4157  df-uni 4405  df-iun 4489  df-br 4616  df-opab 4676  df-mpt 4677  df-id 4991  df-xp 5082  df-rel 5083  df-cnv 5084  df-co 5085  df-dm 5086  df-rn 5087  df-res 5088  df-ima 5089  df-iota 5812  df-fun 5851  df-fn 5852  df-f 5853  df-f1 5854  df-fo 5855  df-f1o 5856  df-fv 5857  df-riota 6568  df-ov 6610  df-oprab 6611  df-preset 16852  df-poset 16870  df-plt 16882  df-lub 16898  df-glb 16899  df-join 16900  df-meet 16901  df-p0 16963  df-lat 16970  df-clat 17032  df-oposet 33964  df-ol 33966  df-oml 33967  df-covers 34054  df-ats 34055  df-atl 34086  df-cvlat 34110  df-hlat 34139  df-llines 34285 This theorem is referenced by:  lplnexllnN  34351
 Copyright terms: Public domain W3C validator