Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Norm Megill
Projective geometries based on Hilbert lattices
lplnnelln
Next ⟩
lplnn0N
Metamath Proof Explorer
Ascii
Unicode
Theorem
lplnnelln
Description:
No lattice plane is a lattice line.
(Contributed by
NM
, 19-Jun-2012)
Ref
Expression
Hypotheses
lplnnelln.n
⊢
N
=
LLines
⁡
K
lplnnelln.p
⊢
P
=
LPlanes
⁡
K
Assertion
lplnnelln
⊢
K
∈
HL
∧
X
∈
P
→
¬
X
∈
N
Proof
Step
Hyp
Ref
Expression
1
lplnnelln.n
⊢
N
=
LLines
⁡
K
2
lplnnelln.p
⊢
P
=
LPlanes
⁡
K
3
hllat
⊢
K
∈
HL
→
K
∈
Lat
4
eqid
⊢
Base
K
=
Base
K
5
4
2
lplnbase
⊢
X
∈
P
→
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
∈
P
→
X
≤
K
X
9
6
1
2
lplnnlelln
⊢
K
∈
HL
∧
X
∈
P
∧
X
∈
N
→
¬
X
≤
K
X
10
9
3expia
⊢
K
∈
HL
∧
X
∈
P
→
X
∈
N
→
¬
X
≤
K
X
11
8
10
mt2d
⊢
K
∈
HL
∧
X
∈
P
→
¬
X
∈
N