Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Norm Megill
Projective geometries based on Hilbert lattices
islln
Next ⟩
islln4
Metamath Proof Explorer
Ascii
Unicode
Theorem
islln
Description:
The predicate "is a lattice line".
(Contributed by
NM
, 16-Jun-2012)
Ref
Expression
Hypotheses
llnset.b
⊢
B
=
Base
K
llnset.c
⊢
C
=
⋖
K
llnset.a
⊢
A
=
Atoms
⁡
K
llnset.n
⊢
N
=
LLines
⁡
K
Assertion
islln
⊢
K
∈
D
→
X
∈
N
↔
X
∈
B
∧
∃
p
∈
A
p
C
X
Proof
Step
Hyp
Ref
Expression
1
llnset.b
⊢
B
=
Base
K
2
llnset.c
⊢
C
=
⋖
K
3
llnset.a
⊢
A
=
Atoms
⁡
K
4
llnset.n
⊢
N
=
LLines
⁡
K
5
1
2
3
4
llnset
⊢
K
∈
D
→
N
=
x
∈
B
|
∃
p
∈
A
p
C
x
6
5
eleq2d
⊢
K
∈
D
→
X
∈
N
↔
X
∈
x
∈
B
|
∃
p
∈
A
p
C
x
7
breq2
⊢
x
=
X
→
p
C
x
↔
p
C
X
8
7
rexbidv
⊢
x
=
X
→
∃
p
∈
A
p
C
x
↔
∃
p
∈
A
p
C
X
9
8
elrab
⊢
X
∈
x
∈
B
|
∃
p
∈
A
p
C
x
↔
X
∈
B
∧
∃
p
∈
A
p
C
X
10
6
9
bitrdi
⊢
K
∈
D
→
X
∈
N
↔
X
∈
B
∧
∃
p
∈
A
p
C
X