Definition df-lhyp

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)

	Ref	Expression
Assertion	df-lhyp	$$⊢\mathrm{LHyp}=\left(k\in \mathrm{V}⟼\left\{x\in {\mathrm{Base}}_k|x{⋖}_k\mathrm{1.}\left(k\right)\right\}\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		clh	$$class\mathrm{LHyp}$$
1		vk	$$setvark$$
2		cvv	$$class\mathrm{V}$$
3		vx	$$setvarx$$
4		cbs	$$class\mathrm{Base}$$
5	1	cv	$$setvark$$
6	5 4	cfv	$$class{\mathrm{Base}}_k$$
7	3	cv	$$setvarx$$
8		ccvr	$$class⋖$$
9	5 8	cfv	$$class{⋖}_k$$
10		cp1	$$class\mathrm{1.}$$
11	5 10	cfv	$$class\mathrm{1.}\left(k\right)$$
12	7 11 9	wbr	$$wffx{⋖}_k\mathrm{1.}\left(k\right)$$
13	12 3 6	crab	$$class\left\{x\in {\mathrm{Base}}_k|x{⋖}_k\mathrm{1.}\left(k\right)\right\}$$
14	1 2 13	cmpt	$$class\left(k\in \mathrm{V}⟼\left\{x\in {\mathrm{Base}}_k|x{⋖}_k\mathrm{1.}\left(k\right)\right\}\right)$$
15	0 14	wceq	$$wff\mathrm{LHyp}=\left(k\in \mathrm{V}⟼\left\{x\in {\mathrm{Base}}_k|x{⋖}_k\mathrm{1.}\left(k\right)\right\}\right)$$