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

Theorem islpln3 37852
Description: The predicate "is a lattice plane". (Contributed by NM, 17-Jun-2012.)
Hypotheses
Ref Expression
islpln3.b 𝐵 = (Base‘𝐾)
islpln3.l = (le‘𝐾)
islpln3.j = (join‘𝐾)
islpln3.a 𝐴 = (Atoms‘𝐾)
islpln3.n 𝑁 = (LLines‘𝐾)
islpln3.p 𝑃 = (LPlanes‘𝐾)
Assertion
Ref Expression
islpln3 ((𝐾 ∈ HL ∧ 𝑋𝐵) → (𝑋𝑃 ↔ ∃𝑦𝑁𝑝𝐴𝑝 𝑦𝑋 = (𝑦 𝑝))))
Distinct variable groups:   𝐴,𝑝   𝑦,𝑝,𝐵   𝐾,𝑝,𝑦   ,𝑝   𝑁,𝑝,𝑦   𝑋,𝑝,𝑦
Allowed substitution hints:   𝐴(𝑦)   𝑃(𝑦,𝑝)   (𝑦,𝑝)   (𝑦)

Proof of Theorem islpln3
StepHypRef Expression
1 islpln3.b . . 3 𝐵 = (Base‘𝐾)
2 eqid 2736 . . 3 ( ⋖ ‘𝐾) = ( ⋖ ‘𝐾)
3 islpln3.n . . 3 𝑁 = (LLines‘𝐾)
4 islpln3.p . . 3 𝑃 = (LPlanes‘𝐾)
51, 2, 3, 4islpln4 37850 . 2 ((𝐾 ∈ HL ∧ 𝑋𝐵) → (𝑋𝑃 ↔ ∃𝑦𝑁 𝑦( ⋖ ‘𝐾)𝑋))
6 simpll 764 . . . . 5 (((𝐾 ∈ HL ∧ 𝑋𝐵) ∧ 𝑦𝑁) → 𝐾 ∈ HL)
71, 3llnbase 37828 . . . . . 6 (𝑦𝑁𝑦𝐵)
87adantl 482 . . . . 5 (((𝐾 ∈ HL ∧ 𝑋𝐵) ∧ 𝑦𝑁) → 𝑦𝐵)
9 simplr 766 . . . . 5 (((𝐾 ∈ HL ∧ 𝑋𝐵) ∧ 𝑦𝑁) → 𝑋𝐵)
10 islpln3.l . . . . . 6 = (le‘𝐾)
11 islpln3.j . . . . . 6 = (join‘𝐾)
12 islpln3.a . . . . . 6 𝐴 = (Atoms‘𝐾)
131, 10, 11, 2, 12cvrval3 37732 . . . . 5 ((𝐾 ∈ HL ∧ 𝑦𝐵𝑋𝐵) → (𝑦( ⋖ ‘𝐾)𝑋 ↔ ∃𝑝𝐴𝑝 𝑦 ∧ (𝑦 𝑝) = 𝑋)))
146, 8, 9, 13syl3anc 1370 . . . 4 (((𝐾 ∈ HL ∧ 𝑋𝐵) ∧ 𝑦𝑁) → (𝑦( ⋖ ‘𝐾)𝑋 ↔ ∃𝑝𝐴𝑝 𝑦 ∧ (𝑦 𝑝) = 𝑋)))
15 eqcom 2743 . . . . . . 7 ((𝑦 𝑝) = 𝑋𝑋 = (𝑦 𝑝))
1615a1i 11 . . . . . 6 ((((𝐾 ∈ HL ∧ 𝑋𝐵) ∧ 𝑦𝑁) ∧ 𝑝𝐴) → ((𝑦 𝑝) = 𝑋𝑋 = (𝑦 𝑝)))
1716anbi2d 629 . . . . 5 ((((𝐾 ∈ HL ∧ 𝑋𝐵) ∧ 𝑦𝑁) ∧ 𝑝𝐴) → ((¬ 𝑝 𝑦 ∧ (𝑦 𝑝) = 𝑋) ↔ (¬ 𝑝 𝑦𝑋 = (𝑦 𝑝))))
1817rexbidva 3169 . . . 4 (((𝐾 ∈ HL ∧ 𝑋𝐵) ∧ 𝑦𝑁) → (∃𝑝𝐴𝑝 𝑦 ∧ (𝑦 𝑝) = 𝑋) ↔ ∃𝑝𝐴𝑝 𝑦𝑋 = (𝑦 𝑝))))
1914, 18bitrd 278 . . 3 (((𝐾 ∈ HL ∧ 𝑋𝐵) ∧ 𝑦𝑁) → (𝑦( ⋖ ‘𝐾)𝑋 ↔ ∃𝑝𝐴𝑝 𝑦𝑋 = (𝑦 𝑝))))
2019rexbidva 3169 . 2 ((𝐾 ∈ HL ∧ 𝑋𝐵) → (∃𝑦𝑁 𝑦( ⋖ ‘𝐾)𝑋 ↔ ∃𝑦𝑁𝑝𝐴𝑝 𝑦𝑋 = (𝑦 𝑝))))
215, 20bitrd 278 1 ((𝐾 ∈ HL ∧ 𝑋𝐵) → (𝑋𝑃 ↔ ∃𝑦𝑁𝑝𝐴𝑝 𝑦𝑋 = (𝑦 𝑝))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396   = wceq 1540  wcel 2105  wrex 3070   class class class wbr 5093  cfv 6480  (class class class)co 7338  Basecbs 17010  lecple 17067  joincjn 18127  ccvr 37580  Atomscatm 37581  HLchlt 37668  LLinesclln 37810  LPlanesclpl 37811
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2707  ax-rep 5230  ax-sep 5244  ax-nul 5251  ax-pow 5309  ax-pr 5373  ax-un 7651
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2886  df-ne 2941  df-ral 3062  df-rex 3071  df-reu 3350  df-rab 3404  df-v 3443  df-sbc 3728  df-csb 3844  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4271  df-if 4475  df-pw 4550  df-sn 4575  df-pr 4577  df-op 4581  df-uni 4854  df-iun 4944  df-br 5094  df-opab 5156  df-mpt 5177  df-id 5519  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-iota 6432  df-fun 6482  df-fn 6483  df-f 6484  df-f1 6485  df-fo 6486  df-f1o 6487  df-fv 6488  df-riota 7294  df-ov 7341  df-oprab 7342  df-proset 18111  df-poset 18129  df-plt 18146  df-lub 18162  df-glb 18163  df-join 18164  df-meet 18165  df-p0 18241  df-lat 18248  df-clat 18315  df-oposet 37494  df-ol 37496  df-oml 37497  df-covers 37584  df-ats 37585  df-atl 37616  df-cvlat 37640  df-hlat 37669  df-llines 37817  df-lplanes 37818
This theorem is referenced by:  islpln5  37854  lplnexllnN  37883
  Copyright terms: Public domain W3C validator