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

Definition df-lplanes 38674
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 LPlanes = (π‘˜ ∈ V ↦ {π‘₯ ∈ (Baseβ€˜π‘˜) ∣ βˆƒπ‘ ∈ (LLinesβ€˜π‘˜)𝑝( β‹– β€˜π‘˜)π‘₯})
Distinct variable group:   π‘˜,𝑝,π‘₯

Detailed syntax breakdown of Definition df-lplanes
StepHypRef Expression
1 clpl 38667 . 2 class LPlanes
2 vk . . 3 setvar π‘˜
3 cvv 3473 . . 3 class V
4 vp . . . . . . 7 setvar 𝑝
54cv 1539 . . . . . 6 class 𝑝
6 vx . . . . . . 7 setvar π‘₯
76cv 1539 . . . . . 6 class π‘₯
82cv 1539 . . . . . . 7 class π‘˜
9 ccvr 38436 . . . . . . 7 class β‹–
108, 9cfv 6544 . . . . . 6 class ( β‹– β€˜π‘˜)
115, 7, 10wbr 5149 . . . . 5 wff 𝑝( β‹– β€˜π‘˜)π‘₯
12 clln 38666 . . . . . 6 class LLines
138, 12cfv 6544 . . . . 5 class (LLinesβ€˜π‘˜)
1411, 4, 13wrex 3069 . . . 4 wff βˆƒπ‘ ∈ (LLinesβ€˜π‘˜)𝑝( β‹– β€˜π‘˜)π‘₯
15 cbs 17149 . . . . 5 class Base
168, 15cfv 6544 . . . 4 class (Baseβ€˜π‘˜)
1714, 6, 16crab 3431 . . 3 class {π‘₯ ∈ (Baseβ€˜π‘˜) ∣ βˆƒπ‘ ∈ (LLinesβ€˜π‘˜)𝑝( β‹– β€˜π‘˜)π‘₯}
182, 3, 17cmpt 5232 . 2 class (π‘˜ ∈ V ↦ {π‘₯ ∈ (Baseβ€˜π‘˜) ∣ βˆƒπ‘ ∈ (LLinesβ€˜π‘˜)𝑝( β‹– β€˜π‘˜)π‘₯})
191, 18wceq 1540 1 wff LPlanes = (π‘˜ ∈ V ↦ {π‘₯ ∈ (Baseβ€˜π‘˜) ∣ βˆƒπ‘ ∈ (LLinesβ€˜π‘˜)𝑝( β‹– β€˜π‘˜)π‘₯})
Colors of variables: wff setvar class
This definition is referenced by:  lplnset  38704
  Copyright terms: Public domain W3C validator