Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Norm Megill
Projective geometries based on Hilbert lattices
df-lvols
Metamath Proof Explorer
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 ‘ 𝑘 ) 𝑝 ( ⋖ ‘ 𝑘 ) 𝑥 } )