Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-lplanes Structured version   Unicode version

Definition df-lplanes 32716
Description: Define the set of all "lattice planes" (lattice elements which cover a line) in a Hilbert lattice  k, in other words all elements of height 3 (or lattice dimension 3 or projective dimension 2). (Contributed by NM, 16-Jun-2012.)
Assertion
Ref Expression
df-lplanes  |-  LPlanes  =  ( k  e.  _V  |->  { x  e.  ( Base `  k )  |  E. p  e.  ( LLines `  k ) p ( 
<o  `  k ) x } )
Distinct variable group:    k, p, x

Detailed syntax breakdown of Definition df-lplanes
StepHypRef Expression
1 clpl 32709 . 2  class  LPlanes
2 vk . . 3  setvar  k
3 cvv 2962 . . 3  class  _V
4 vp . . . . . . 7  setvar  p
54cv 1361 . . . . . 6  class  p
6 vx . . . . . . 7  setvar  x
76cv 1361 . . . . . 6  class  x
82cv 1361 . . . . . . 7  class  k
9 ccvr 32480 . . . . . . 7  class  <o
108, 9cfv 5406 . . . . . 6  class  (  <o  `  k )
115, 7, 10wbr 4280 . . . . 5  wff  p ( 
<o  `  k ) x
12 clln 32708 . . . . . 6  class  LLines
138, 12cfv 5406 . . . . 5  class  ( LLines `  k )
1411, 4, 13wrex 2706 . . . 4  wff  E. p  e.  ( LLines `  k )
p (  <o  `  k
) x
15 cbs 14157 . . . . 5  class  Base
168, 15cfv 5406 . . . 4  class  ( Base `  k )
1714, 6, 16crab 2709 . . 3  class  { x  e.  ( Base `  k
)  |  E. p  e.  ( LLines `  k )
p (  <o  `  k
) x }
182, 3, 17cmpt 4338 . 2  class  ( k  e.  _V  |->  { x  e.  ( Base `  k
)  |  E. p  e.  ( LLines `  k )
p (  <o  `  k
) x } )
191, 18wceq 1362 1  wff  LPlanes  =  ( k  e.  _V  |->  { x  e.  ( Base `  k )  |  E. p  e.  ( LLines `  k ) p ( 
<o  `  k ) x } )
Colors of variables: wff setvar class
This definition is referenced by:  lplnset  32746
  Copyright terms: Public domain W3C validator