Definition df-lhyp 35274

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 35270	. 2 class LHyp
2		vk	. . 3 setvar k
3		cvv 3200	. . 3 class _V
4		vx	. . . . . 6 setvar x
5	4	cv 1482	. . . . 5 class x
6	2	cv 1482	. . . . . 6 class k
7		cp1 17038	. . . . . 6 class 1.
8	6, 7	cfv 5888	. . . . 5 class ( 1. ` k )
9		ccvr 34549	. . . . . 6 class <o
10	6, 9	cfv 5888	. . . . 5 class ( <o ` k )
11	5, 8, 10	wbr 4653	. . . 4 wff x ( <o ` k ) ( 1. ` k )
12		cbs 15857	. . . . 5 class Base
13	6, 12	cfv 5888	. . . 4 class ( Base ` k )
14	11, 4, 13	crab 2916	. . 3 class { x e. ( Base ` k ) | x ( <o ` k ) ( 1. ` k ) }
15	2, 3, 14	cmpt 4729	. 2 class ( k e. _V |-> { x e. ( Base ` k ) | x ( <o ` k ) ( 1. ` k ) } )
16	1, 15	wceq 1483	1 wff LHyp = ( k e. _V |-> { x e. ( Base ` k ) | x ( <o ` k ) ( 1. ` k ) } )

This definition is referenced by:  lhpset  35281