Metamath Proof Explorer


Definition df-lplanes

Description: Define the set of all "lattice planes" (lattice elements which cover a line) in a Hilbert lattice k , in other words all elements of height 3 (or lattice dimension 3 or projective dimension 2). (Contributed by NM, 16-Jun-2012)

Ref Expression
Assertion df-lplanes LPlanes = ( 𝑘 ∈ V ↦ { 𝑥 ∈ ( Base ‘ 𝑘 ) ∣ ∃ 𝑝 ∈ ( LLines ‘ 𝑘 ) 𝑝 ( ⋖ ‘ 𝑘 ) 𝑥 } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 clpl LPlanes
1 vk 𝑘
2 cvv V
3 vx 𝑥
4 cbs Base
5 1 cv 𝑘
6 5 4 cfv ( Base ‘ 𝑘 )
7 vp 𝑝
8 clln LLines
9 5 8 cfv ( LLines ‘ 𝑘 )
10 7 cv 𝑝
11 ccvr
12 5 11 cfv ( ⋖ ‘ 𝑘 )
13 3 cv 𝑥
14 10 13 12 wbr 𝑝 ( ⋖ ‘ 𝑘 ) 𝑥
15 14 7 9 wrex 𝑝 ∈ ( LLines ‘ 𝑘 ) 𝑝 ( ⋖ ‘ 𝑘 ) 𝑥
16 15 3 6 crab { 𝑥 ∈ ( Base ‘ 𝑘 ) ∣ ∃ 𝑝 ∈ ( LLines ‘ 𝑘 ) 𝑝 ( ⋖ ‘ 𝑘 ) 𝑥 }
17 1 2 16 cmpt ( 𝑘 ∈ V ↦ { 𝑥 ∈ ( Base ‘ 𝑘 ) ∣ ∃ 𝑝 ∈ ( LLines ‘ 𝑘 ) 𝑝 ( ⋖ ‘ 𝑘 ) 𝑥 } )
18 0 17 wceq LPlanes = ( 𝑘 ∈ V ↦ { 𝑥 ∈ ( Base ‘ 𝑘 ) ∣ ∃ 𝑝 ∈ ( LLines ‘ 𝑘 ) 𝑝 ( ⋖ ‘ 𝑘 ) 𝑥 } )