Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Norm Megill
Projective geometries based on Hilbert lattices
isline
Next ⟩
islinei
Metamath Proof Explorer
Ascii
Unicode
Theorem
isline
Description:
The predicate "is a line".
(Contributed by
NM
, 19-Sep-2011)
Ref
Expression
Hypotheses
isline.l
⊢
≤
˙
=
≤
K
isline.j
⊢
∨
˙
=
join
⁡
K
isline.a
⊢
A
=
Atoms
⁡
K
isline.n
⊢
N
=
Lines
⁡
K
Assertion
isline
⊢
K
∈
D
→
X
∈
N
↔
∃
q
∈
A
∃
r
∈
A
q
≠
r
∧
X
=
p
∈
A
|
p
≤
˙
q
∨
˙
r
Proof
Step
Hyp
Ref
Expression
1
isline.l
⊢
≤
˙
=
≤
K
2
isline.j
⊢
∨
˙
=
join
⁡
K
3
isline.a
⊢
A
=
Atoms
⁡
K
4
isline.n
⊢
N
=
Lines
⁡
K
5
1
2
3
4
lineset
⊢
K
∈
D
→
N
=
x
|
∃
q
∈
A
∃
r
∈
A
q
≠
r
∧
x
=
p
∈
A
|
p
≤
˙
q
∨
˙
r
6
5
eleq2d
⊢
K
∈
D
→
X
∈
N
↔
X
∈
x
|
∃
q
∈
A
∃
r
∈
A
q
≠
r
∧
x
=
p
∈
A
|
p
≤
˙
q
∨
˙
r
7
3
fvexi
⊢
A
∈
V
8
7
rabex
⊢
p
∈
A
|
p
≤
˙
q
∨
˙
r
∈
V
9
eleq1
⊢
X
=
p
∈
A
|
p
≤
˙
q
∨
˙
r
→
X
∈
V
↔
p
∈
A
|
p
≤
˙
q
∨
˙
r
∈
V
10
8
9
mpbiri
⊢
X
=
p
∈
A
|
p
≤
˙
q
∨
˙
r
→
X
∈
V
11
10
adantl
⊢
q
≠
r
∧
X
=
p
∈
A
|
p
≤
˙
q
∨
˙
r
→
X
∈
V
12
11
a1i
⊢
q
∈
A
∧
r
∈
A
→
q
≠
r
∧
X
=
p
∈
A
|
p
≤
˙
q
∨
˙
r
→
X
∈
V
13
12
rexlimivv
⊢
∃
q
∈
A
∃
r
∈
A
q
≠
r
∧
X
=
p
∈
A
|
p
≤
˙
q
∨
˙
r
→
X
∈
V
14
eqeq1
⊢
x
=
X
→
x
=
p
∈
A
|
p
≤
˙
q
∨
˙
r
↔
X
=
p
∈
A
|
p
≤
˙
q
∨
˙
r
15
14
anbi2d
⊢
x
=
X
→
q
≠
r
∧
x
=
p
∈
A
|
p
≤
˙
q
∨
˙
r
↔
q
≠
r
∧
X
=
p
∈
A
|
p
≤
˙
q
∨
˙
r
16
15
2rexbidv
⊢
x
=
X
→
∃
q
∈
A
∃
r
∈
A
q
≠
r
∧
x
=
p
∈
A
|
p
≤
˙
q
∨
˙
r
↔
∃
q
∈
A
∃
r
∈
A
q
≠
r
∧
X
=
p
∈
A
|
p
≤
˙
q
∨
˙
r
17
13
16
elab3
⊢
X
∈
x
|
∃
q
∈
A
∃
r
∈
A
q
≠
r
∧
x
=
p
∈
A
|
p
≤
˙
q
∨
˙
r
↔
∃
q
∈
A
∃
r
∈
A
q
≠
r
∧
X
=
p
∈
A
|
p
≤
˙
q
∨
˙
r
18
6
17
bitrdi
⊢
K
∈
D
→
X
∈
N
↔
∃
q
∈
A
∃
r
∈
A
q
≠
r
∧
X
=
p
∈
A
|
p
≤
˙
q
∨
˙
r