# Metamath Proof Explorer

## 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 ${setvar}{k}$
2 cvv ${class}\mathrm{V}$
3 vx ${setvar}{x}$
4 cbs ${class}\mathrm{Base}$
5 1 cv ${setvar}{k}$
6 5 4 cfv ${class}{\mathrm{Base}}_{{k}}$
7 3 cv ${setvar}{x}$
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 ${wff}{x}{⋖}_{{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)$