Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Norm Megill
Projective geometries based on Hilbert lattices
lplnneat
Next ⟩
lplnnelln
Metamath Proof Explorer
Ascii
Unicode
Theorem
lplnneat
Description:
No lattice plane is an atom.
(Contributed by
NM
, 15-Jul-2012)
Ref
Expression
Hypotheses
lplnneat.a
⊢
A
=
Atoms
⁡
K
lplnneat.p
⊢
P
=
LPlanes
⁡
K
Assertion
lplnneat
⊢
K
∈
HL
∧
X
∈
P
→
¬
X
∈
A
Proof
Step
Hyp
Ref
Expression
1
lplnneat.a
⊢
A
=
Atoms
⁡
K
2
lplnneat.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
lplnnleat
⊢
K
∈
HL
∧
X
∈
P
∧
X
∈
A
→
¬
X
≤
K
X
10
9
3expia
⊢
K
∈
HL
∧
X
∈
P
→
X
∈
A
→
¬
X
≤
K
X
11
8
10
mt2d
⊢
K
∈
HL
∧
X
∈
P
→
¬
X
∈
A