Metamath Proof Explorer


Theorem btwncolg2

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
btwncolg2.z φ X Z I Y
Assertion btwncolg2 φ 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 btwncolg2.z φ X Z I Y
9 8 3mix2d φ 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