Metamath Proof Explorer


Definition df-lplanes

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)

Ref Expression
Assertion df-lplanes
|- LPlanes = ( k e. _V |-> { x e. ( Base ` k ) | E. p e. ( LLines ` k ) p ( 

Detailed syntax breakdown

Step Hyp Ref Expression
0 clpl
 |-  LPlanes
1 vk
 |-  k
2 cvv
 |-  _V
3 vx
 |-  x
4 cbs
 |-  Base
5 1 cv
 |-  k
6 5 4 cfv
 |-  ( Base ` k )
7 vp
 |-  p
8 clln
 |-  LLines
9 5 8 cfv
 |-  ( LLines ` k )
10 7 cv
 |-  p
11 ccvr
 |-  
12 5 11 cfv
 |-  ( 
13 3 cv
 |-  x
14 10 13 12 wbr
 |-  p ( 
15 14 7 9 wrex
 |-  E. p e. ( LLines ` k ) p ( 
16 15 3 6 crab
 |-  { x e. ( Base ` k ) | E. p e. ( LLines ` k ) p ( 
17 1 2 16 cmpt
 |-  ( k e. _V |-> { x e. ( Base ` k ) | E. p e. ( LLines ` k ) p ( 
18 0 17 wceq
 |-  LPlanes = ( k e. _V |-> { x e. ( Base ` k ) | E. p e. ( LLines ` k ) p (