Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Norm Megill
Projective geometries based on Hilbert lattices
lvolnelpln
Next ⟩
lvoln0N
Metamath Proof Explorer
Ascii
Unicode
Theorem
lvolnelpln
Description:
No lattice volume is a lattice plane.
(Contributed by
NM
, 19-Jun-2012)
Ref
Expression
Hypotheses
lvolnelpln.p
⊢
P
=
LPlanes
⁡
K
lvolnelpln.v
⊢
V
=
LVols
⁡
K
Assertion
lvolnelpln
⊢
K
∈
HL
∧
X
∈
V
→
¬
X
∈
P
Proof
Step
Hyp
Ref
Expression
1
lvolnelpln.p
⊢
P
=
LPlanes
⁡
K
2
lvolnelpln.v
⊢
V
=
LVols
⁡
K
3
hllat
⊢
K
∈
HL
→
K
∈
Lat
4
eqid
⊢
Base
K
=
Base
K
5
4
2
lvolbase
⊢
X
∈
V
→
X
∈
Base
K
6
eqid
⊢
≤
K
=
≤
K
7
4
6
latref
⊢
K
∈
Lat
∧
X
∈
Base
K
→
X
≤
K
X
8
3
5
7
syl2an
⊢
K
∈
HL
∧
X
∈
V
→
X
≤
K
X
9
6
1
2
lvolnlelpln
⊢
K
∈
HL
∧
X
∈
V
∧
X
∈
P
→
¬
X
≤
K
X
10
9
3expia
⊢
K
∈
HL
∧
X
∈
V
→
X
∈
P
→
¬
X
≤
K
X
11
8
10
mt2d
⊢
K
∈
HL
∧
X
∈
V
→
¬
X
∈
P