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

Definition df-lplanes 30370
 Description: Define the set of all "lattice planes" (lattice elements which cover a line) in a Hilbert lattice , 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
Distinct variable group:   ,,

Detailed syntax breakdown of Definition df-lplanes
StepHypRef Expression
1 clpl 30363 . 2
2 vk . . 3
3 cvv 2958 . . 3
4 vp . . . . . . 7
54cv 1652 . . . . . 6
6 vx . . . . . . 7
76cv 1652 . . . . . 6
82cv 1652 . . . . . . 7
9 ccvr 30134 . . . . . . 7
108, 9cfv 5457 . . . . . 6
115, 7, 10wbr 4215 . . . . 5
12 clln 30362 . . . . . 6
138, 12cfv 5457 . . . . 5
1411, 4, 13wrex 2708 . . . 4
15 cbs 13474 . . . . 5
168, 15cfv 5457 . . . 4
1714, 6, 16crab 2711 . . 3
182, 3, 17cmpt 4269 . 2
191, 18wceq 1653 1
 Colors of variables: wff set class This definition is referenced by:  lplnset  30400
 Copyright terms: Public domain W3C validator