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

Definition df-lhyp 35592
 Description: Define the set of lattice hyperplanes, which are all lattice elements covered by 1 (i.e. all co-atoms). We call them "hyperplanes" instead of "co-atoms" in analogy with projective geometry hyperplanes. (Contributed by NM, 11-May-2012.)
Assertion
Ref Expression
df-lhyp LHyp = (𝑘 ∈ V ↦ {𝑥 ∈ (Base‘𝑘) ∣ 𝑥( ⋖ ‘𝑘)(1.‘𝑘)})
Distinct variable group:   𝑥,𝑘

Detailed syntax breakdown of Definition df-lhyp
StepHypRef Expression
1 clh 35588 . 2 class LHyp
2 vk . . 3 setvar 𝑘
3 cvv 3231 . . 3 class V
4 vx . . . . . 6 setvar 𝑥
54cv 1522 . . . . 5 class 𝑥
62cv 1522 . . . . . 6 class 𝑘
7 cp1 17085 . . . . . 6 class 1.
86, 7cfv 5926 . . . . 5 class (1.‘𝑘)
9 ccvr 34867 . . . . . 6 class
106, 9cfv 5926 . . . . 5 class ( ⋖ ‘𝑘)
115, 8, 10wbr 4685 . . . 4 wff 𝑥( ⋖ ‘𝑘)(1.‘𝑘)
12 cbs 15904 . . . . 5 class Base
136, 12cfv 5926 . . . 4 class (Base‘𝑘)
1411, 4, 13crab 2945 . . 3 class {𝑥 ∈ (Base‘𝑘) ∣ 𝑥( ⋖ ‘𝑘)(1.‘𝑘)}
152, 3, 14cmpt 4762 . 2 class (𝑘 ∈ V ↦ {𝑥 ∈ (Base‘𝑘) ∣ 𝑥( ⋖ ‘𝑘)(1.‘𝑘)})
161, 15wceq 1523 1 wff LHyp = (𝑘 ∈ V ↦ {𝑥 ∈ (Base‘𝑘) ∣ 𝑥( ⋖ ‘𝑘)(1.‘𝑘)})
 Colors of variables: wff setvar class This definition is referenced by:  lhpset  35599
 Copyright terms: Public domain W3C validator