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 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. ‘ 𝑘 ) } )