Metamath Proof Explorer


Theorem btwnlng1

Description: Betweenness implies colinearity. (Contributed by Thierry Arnoux, 28-Mar-2019)

Ref Expression
Hypotheses btwnlng1.p P = Base G
btwnlng1.i I = Itv G
btwnlng1.l L = Line 𝒢 G
btwnlng1.g φ G 𝒢 Tarski
btwnlng1.x φ X P
btwnlng1.y φ Y P
btwnlng1.z φ Z P
btwnlng1.d φ X Y
btwnlng1.1 φ Z X I Y
Assertion btwnlng1 φ Z X L Y

Proof

Step Hyp Ref Expression
1 btwnlng1.p P = Base G
2 btwnlng1.i I = Itv G
3 btwnlng1.l L = Line 𝒢 G
4 btwnlng1.g φ G 𝒢 Tarski
5 btwnlng1.x φ X P
6 btwnlng1.y φ Y P
7 btwnlng1.z φ Z P
8 btwnlng1.d φ X Y
9 btwnlng1.1 φ Z X I Y
10 9 3mix1d φ Z X I Y X Z I Y Y X I Z
11 1 3 2 4 5 6 8 7 tgellng φ Z X L Y Z X I Y X Z I Y Y X I Z
12 10 11 mpbird φ Z X L Y