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