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 = ( 𝑘 ∈ V ↦ { 𝑥 ∈ ( Base ‘ 𝑘 ) ∣ 𝑥 ( ⋖ ‘ 𝑘 ) ( 1. ‘ 𝑘 ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		clh	⊢ LHyp
1		vk	⊢ 𝑘
2		cvv	⊢ V
3		vx	⊢ 𝑥
4		cbs	⊢ Base
5	1	cv	⊢ 𝑘
6	5 4	cfv	⊢ ( Base ‘ 𝑘 )
7	3	cv	⊢ 𝑥
8		ccvr	⊢ ⋖
9	5 8	cfv	⊢ ( ⋖ ‘ 𝑘 )
10		cp1	⊢ 1.
11	5 10	cfv	⊢ ( 1. ‘ 𝑘 )
12	7 11 9	wbr	⊢ 𝑥 ( ⋖ ‘ 𝑘 ) ( 1. ‘ 𝑘 )
13	12 3 6	crab	⊢ { 𝑥 ∈ ( Base ‘ 𝑘 ) ∣ 𝑥 ( ⋖ ‘ 𝑘 ) ( 1. ‘ 𝑘 ) }
14	1 2 13	cmpt	⊢ ( 𝑘 ∈ V ↦ { 𝑥 ∈ ( Base ‘ 𝑘 ) ∣ 𝑥 ( ⋖ ‘ 𝑘 ) ( 1. ‘ 𝑘 ) } )
15	0 14	wceq	⊢ LHyp = ( 𝑘 ∈ V ↦ { 𝑥 ∈ ( Base ‘ 𝑘 ) ∣ 𝑥 ( ⋖ ‘ 𝑘 ) ( 1. ‘ 𝑘 ) } )