Database
ELEMENTARY GEOMETRY
Tarskian Geometry
Colinearity
btwncolg3
Next ⟩
colcom
Metamath Proof Explorer
Ascii
Unicode
Theorem
btwncolg3
Description:
Betweenness implies colinearity.
(Contributed by
Thierry Arnoux
, 28-Mar-2019)
Ref
Expression
Hypotheses
tglngval.p
⊢
P
=
Base
G
tglngval.l
⊢
L
=
Line
𝒢
⁡
G
tglngval.i
⊢
I
=
Itv
⁡
G
tglngval.g
⊢
φ
→
G
∈
𝒢
Tarski
tglngval.x
⊢
φ
→
X
∈
P
tglngval.y
⊢
φ
→
Y
∈
P
tgcolg.z
⊢
φ
→
Z
∈
P
btwncolg3.z
⊢
φ
→
Y
∈
X
I
Z
Assertion
btwncolg3
⊢
φ
→
Z
∈
X
L
Y
∨
X
=
Y
Proof
Step
Hyp
Ref
Expression
1
tglngval.p
⊢
P
=
Base
G
2
tglngval.l
⊢
L
=
Line
𝒢
⁡
G
3
tglngval.i
⊢
I
=
Itv
⁡
G
4
tglngval.g
⊢
φ
→
G
∈
𝒢
Tarski
5
tglngval.x
⊢
φ
→
X
∈
P
6
tglngval.y
⊢
φ
→
Y
∈
P
7
tgcolg.z
⊢
φ
→
Z
∈
P
8
btwncolg3.z
⊢
φ
→
Y
∈
X
I
Z
9
8
3mix3d
⊢
φ
→
Z
∈
X
I
Y
∨
X
∈
Z
I
Y
∨
Y
∈
X
I
Z
10
1
2
3
4
5
6
7
tgcolg
⊢
φ
→
Z
∈
X
L
Y
∨
X
=
Y
↔
Z
∈
X
I
Y
∨
X
∈
Z
I
Y
∨
Y
∈
X
I
Z
11
9
10
mpbird
⊢
φ
→
Z
∈
X
L
Y
∨
X
=
Y