Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Norm Megill
Projective geometries based on Hilbert lattices
2atneat
Next ⟩
llnn0
Metamath Proof Explorer
Ascii
Unicode
Theorem
2atneat
Description:
The join of two distinct atoms is not an atom.
(Contributed by
NM
, 12-Oct-2012)
Ref
Expression
Hypotheses
2atneat.j
⊢
∨
˙
=
join
⁡
K
2atneat.a
⊢
A
=
Atoms
⁡
K
Assertion
2atneat
⊢
K
∈
HL
∧
P
∈
A
∧
Q
∈
A
∧
P
≠
Q
→
¬
P
∨
˙
Q
∈
A
Proof
Step
Hyp
Ref
Expression
1
2atneat.j
⊢
∨
˙
=
join
⁡
K
2
2atneat.a
⊢
A
=
Atoms
⁡
K
3
simpl
⊢
K
∈
HL
∧
P
∈
A
∧
Q
∈
A
∧
P
≠
Q
→
K
∈
HL
4
simpr1
⊢
K
∈
HL
∧
P
∈
A
∧
Q
∈
A
∧
P
≠
Q
→
P
∈
A
5
simpr2
⊢
K
∈
HL
∧
P
∈
A
∧
Q
∈
A
∧
P
≠
Q
→
Q
∈
A
6
simpr3
⊢
K
∈
HL
∧
P
∈
A
∧
Q
∈
A
∧
P
≠
Q
→
P
≠
Q
7
eqid
⊢
LLines
⁡
K
=
LLines
⁡
K
8
1
2
7
llni2
⊢
K
∈
HL
∧
P
∈
A
∧
Q
∈
A
∧
P
≠
Q
→
P
∨
˙
Q
∈
LLines
⁡
K
9
3
4
5
6
8
syl31anc
⊢
K
∈
HL
∧
P
∈
A
∧
Q
∈
A
∧
P
≠
Q
→
P
∨
˙
Q
∈
LLines
⁡
K
10
2
7
llnneat
⊢
K
∈
HL
∧
P
∨
˙
Q
∈
LLines
⁡
K
→
¬
P
∨
˙
Q
∈
A
11
9
10
syldan
⊢
K
∈
HL
∧
P
∈
A
∧
Q
∈
A
∧
P
≠
Q
→
¬
P
∨
˙
Q
∈
A