Definition df-lhyp 39990

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 39986	. 2 class LHyp
2		vk	. . 3 setvar 𝑘
3		cvv 3480	. . 3 class V
4		vx	. . . . . 6 setvar 𝑥
5	4	cv 1539	. . . . 5 class 𝑥
6	2	cv 1539	. . . . . 6 class 𝑘
7		cp1 18469	. . . . . 6 class 1.
8	6, 7	cfv 6561	. . . . 5 class (1.‘𝑘)
9		ccvr 39263	. . . . . 6 class ⋖
10	6, 9	cfv 6561	. . . . 5 class ( ⋖ ‘𝑘)
11	5, 8, 10	wbr 5143	. . . 4 wff 𝑥( ⋖ ‘𝑘)(1.‘𝑘)
12		cbs 17247	. . . . 5 class Base
13	6, 12	cfv 6561	. . . 4 class (Base‘𝑘)
14	11, 4, 13	crab 3436	. . 3 class {𝑥 ∈ (Base‘𝑘) ∣ 𝑥( ⋖ ‘𝑘)(1.‘𝑘)}
15	2, 3, 14	cmpt 5225	. 2 class (𝑘 ∈ V ↦ {𝑥 ∈ (Base‘𝑘) ∣ 𝑥( ⋖ ‘𝑘)(1.‘𝑘)})
16	1, 15	wceq 1540	1 wff LHyp = (𝑘 ∈ V ↦ {𝑥 ∈ (Base‘𝑘) ∣ 𝑥( ⋖ ‘𝑘)(1.‘𝑘)})

This definition is referenced by:  lhpset  39997