This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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