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

Theorem lplnbase 35342
Description: A lattice plane is a lattice element. (Contributed by NM, 17-Jun-2012.)
Hypotheses
Ref Expression
lplnbase.b 𝐵 = (Base‘𝐾)
lplnbase.p 𝑃 = (LPlanes‘𝐾)
Assertion
Ref Expression
lplnbase (𝑋𝑃𝑋𝐵)

Proof of Theorem lplnbase
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 n0i 4065 . . . 4 (𝑋𝑃 → ¬ 𝑃 = ∅)
2 lplnbase.p . . . . 5 𝑃 = (LPlanes‘𝐾)
32eqeq1i 2774 . . . 4 (𝑃 = ∅ ↔ (LPlanes‘𝐾) = ∅)
41, 3sylnib 317 . . 3 (𝑋𝑃 → ¬ (LPlanes‘𝐾) = ∅)
5 fvprc 6325 . . 3 𝐾 ∈ V → (LPlanes‘𝐾) = ∅)
64, 5nsyl2 144 . 2 (𝑋𝑃𝐾 ∈ V)
7 lplnbase.b . . . 4 𝐵 = (Base‘𝐾)
8 eqid 2769 . . . 4 ( ⋖ ‘𝐾) = ( ⋖ ‘𝐾)
9 eqid 2769 . . . 4 (LLines‘𝐾) = (LLines‘𝐾)
107, 8, 9, 2islpln 35338 . . 3 (𝐾 ∈ V → (𝑋𝑃 ↔ (𝑋𝐵 ∧ ∃𝑥 ∈ (LLines‘𝐾)𝑥( ⋖ ‘𝐾)𝑋)))
1110simprbda 651 . 2 ((𝐾 ∈ V ∧ 𝑋𝑃) → 𝑋𝐵)
126, 11mpancom 703 1 (𝑋𝑃𝑋𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1629  wcel 2143  wrex 3060  Vcvv 3348  c0 4060   class class class wbr 4783  cfv 6030  Basecbs 16070  ccvr 35071  LLinesclln 35299  LPlanesclpl 35300
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1868  ax-4 1883  ax-5 1989  ax-6 2055  ax-7 2091  ax-8 2145  ax-9 2152  ax-10 2172  ax-11 2188  ax-12 2201  ax-13 2406  ax-ext 2749  ax-sep 4911  ax-nul 4919  ax-pow 4970  ax-pr 5033
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1071  df-tru 1632  df-ex 1851  df-nf 1856  df-sb 2048  df-eu 2620  df-mo 2621  df-clab 2756  df-cleq 2762  df-clel 2765  df-nfc 2900  df-ral 3064  df-rex 3065  df-rab 3068  df-v 3350  df-sbc 3585  df-dif 3723  df-un 3725  df-in 3727  df-ss 3734  df-nul 4061  df-if 4223  df-sn 4314  df-pr 4316  df-op 4320  df-uni 4572  df-br 4784  df-opab 4844  df-mpt 4861  df-id 5156  df-xp 5254  df-rel 5255  df-cnv 5256  df-co 5257  df-dm 5258  df-iota 5993  df-fun 6032  df-fv 6038  df-lplanes 35307
This theorem is referenced by:  islpln2  35344  llnmlplnN  35347  lplnnle2at  35349  lplnneat  35353  lplnnelln  35354  llncvrlpln2  35365  2lplnmN  35367  lplncmp  35370  lplnexatN  35371  lplnexllnN  35372  2llnjaN  35374  islvol3  35384  lvoli3  35385  lvolnle3at  35390  lplncvrlvol2  35423  lplncvrlvol  35424  lvolcmp  35425  2lplnm2N  35429  2lplnmj  35430  dalemyeb  35457  dalem10  35481  dalem16  35487  dalem44  35524  dalem55  35535
  Copyright terms: Public domain W3C validator