Metamath Proof Explorer


Definition df-lvols

Description: Define the set of all 3-dimensional "lattice volumes" (lattice elements which cover a plane) in a Hilbert lattice k , in other words all elements of height 4 (or lattice dimension 4 or projective dimension 3). (Contributed by NM, 1-Jul-2012)

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

Detailed syntax breakdown

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