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 33599
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 33592 . 2 class LPlanes
2 vk . . 3 setvar 𝑘
3 cvv 3172 . . 3 class V
4 vp . . . . . . 7 setvar 𝑝
54cv 1473 . . . . . 6 class 𝑝
6 vx . . . . . . 7 setvar 𝑥
76cv 1473 . . . . . 6 class 𝑥
82cv 1473 . . . . . . 7 class 𝑘
9 ccvr 33363 . . . . . . 7 class
108, 9cfv 5790 . . . . . 6 class ( ⋖ ‘𝑘)
115, 7, 10wbr 4577 . . . . 5 wff 𝑝( ⋖ ‘𝑘)𝑥
12 clln 33591 . . . . . 6 class LLines
138, 12cfv 5790 . . . . 5 class (LLines‘𝑘)
1411, 4, 13wrex 2896 . . . 4 wff 𝑝 ∈ (LLines‘𝑘)𝑝( ⋖ ‘𝑘)𝑥
15 cbs 15641 . . . . 5 class Base
168, 15cfv 5790 . . . 4 class (Base‘𝑘)
1714, 6, 16crab 2899 . . 3 class {𝑥 ∈ (Base‘𝑘) ∣ ∃𝑝 ∈ (LLines‘𝑘)𝑝( ⋖ ‘𝑘)𝑥}
182, 3, 17cmpt 4637 . 2 class (𝑘 ∈ V ↦ {𝑥 ∈ (Base‘𝑘) ∣ ∃𝑝 ∈ (LLines‘𝑘)𝑝( ⋖ ‘𝑘)𝑥})
191, 18wceq 1474 1 wff LPlanes = (𝑘 ∈ V ↦ {𝑥 ∈ (Base‘𝑘) ∣ ∃𝑝 ∈ (LLines‘𝑘)𝑝( ⋖ ‘𝑘)𝑥})
Colors of variables: wff setvar class
This definition is referenced by:  lplnset  33629
  Copyright terms: Public domain W3C validator