Definition df-lhyp 38009

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

Step	Hyp	Ref	Expression
1		clh 38005	. 2 class LHyp
2		vk	. . 3 setvar 𝑘
3		cvv 3433	. . 3 class V
4		vx	. . . . . 6 setvar 𝑥
5	4	cv 1538	. . . . 5 class 𝑥
6	2	cv 1538	. . . . . 6 class 𝑘
7		cp1 18151	. . . . . 6 class 1.
8	6, 7	cfv 6437	. . . . 5 class (1.‘𝑘)
9		ccvr 37283	. . . . . 6 class ⋖
10	6, 9	cfv 6437	. . . . 5 class ( ⋖ ‘𝑘)
11	5, 8, 10	wbr 5075	. . . 4 wff 𝑥( ⋖ ‘𝑘)(1.‘𝑘)
12		cbs 16921	. . . . 5 class Base
13	6, 12	cfv 6437	. . . 4 class (Base‘𝑘)
14	11, 4, 13	crab 3069	. . 3 class {𝑥 ∈ (Base‘𝑘) ∣ 𝑥( ⋖ ‘𝑘)(1.‘𝑘)}
15	2, 3, 14	cmpt 5158	. 2 class (𝑘 ∈ V ↦ {𝑥 ∈ (Base‘𝑘) ∣ 𝑥( ⋖ ‘𝑘)(1.‘𝑘)})
16	1, 15	wceq 1539	1 wff LHyp = (𝑘 ∈ V ↦ {𝑥 ∈ (Base‘𝑘) ∣ 𝑥( ⋖ ‘𝑘)(1.‘𝑘)})

This definition is referenced by:  lhpset  38016