Definition df-lhyp 30470

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

Distinct variable group:   x, k

Detailed syntax breakdown of Definition df-lhyp

Step	Hyp	Ref	Expression
1		clh 30466	. 2 class LHyp
2		vk	. . 3 set k
3		cvv 2916	. . 3 class _V
4		vx	. . . . . 6 set x
5	4	cv 1648	. . . . 5 class x
6	2	cv 1648	. . . . . 6 class k
7		cp1 14422	. . . . . 6 class 1.
8	6, 7	cfv 5413	. . . . 5 class ( 1. ` k )
9		ccvr 29745	. . . . . 6 class <o
10	6, 9	cfv 5413	. . . . 5 class ( <o ` k )
11	5, 8, 10	wbr 4172	. . . 4 wff x ( <o ` k ) ( 1. ` k )
12		cbs 13424	. . . . 5 class Base
13	6, 12	cfv 5413	. . . 4 class ( Base ` k )
14	11, 4, 13	crab 2670	. . 3 class { x e. ( Base ` k ) | x ( <o ` k ) ( 1. ` k ) }
15	2, 3, 14	cmpt 4226	. 2 class ( k e. _V |-> { x e. ( Base ` k ) | x ( <o ` k ) ( 1. ` k ) } )
16	1, 15	wceq 1649	1 wff LHyp = ( k e. _V |-> { x e. ( Base ` k ) | x ( <o ` k ) ( 1. ` k ) } )

This definition is referenced by:  lhpset  30477