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	|- LHyp = ( k e. _V |-> { x e. ( Base ` k ) | x (

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		clh	|- LHyp
1		vk	|- k
2		cvv	|- _V
3		vx	|- x
4		cbs	|- Base
5	1	cv	|- k
6	5 4	cfv	|- ( Base ` k )
7	3	cv	|- x
8		ccvr	|-
9	5 8	cfv	|- (
10		cp1	|- 1.
11	5 10	cfv	|- ( 1. ` k )
12	7 11 9	wbr	|- x (
13	12 3 6	crab	|- { x e. ( Base ` k ) | x (
14	1 2 13	cmpt	|- ( k e. _V |-> { x e. ( Base ` k ) | x (
15	0 14	wceq	|- LHyp = ( k e. _V |-> { x e. ( Base ` k ) | x (