Metamath Proof Explorer


Theorem btwnlng2

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 = ( LineG ` G )
btwnlng1.g
|- ( ph -> G e. TarskiG )
btwnlng1.x
|- ( ph -> X e. P )
btwnlng1.y
|- ( ph -> Y e. P )
btwnlng1.z
|- ( ph -> Z e. P )
btwnlng1.d
|- ( ph -> X =/= Y )
btwnlng2.1
|- ( ph -> X e. ( Z I Y ) )
Assertion btwnlng2
|- ( ph -> Z e. ( X L Y ) )

Proof

Step Hyp Ref Expression
1 btwnlng1.p
 |-  P = ( Base ` G )
2 btwnlng1.i
 |-  I = ( Itv ` G )
3 btwnlng1.l
 |-  L = ( LineG ` G )
4 btwnlng1.g
 |-  ( ph -> G e. TarskiG )
5 btwnlng1.x
 |-  ( ph -> X e. P )
6 btwnlng1.y
 |-  ( ph -> Y e. P )
7 btwnlng1.z
 |-  ( ph -> Z e. P )
8 btwnlng1.d
 |-  ( ph -> X =/= Y )
9 btwnlng2.1
 |-  ( ph -> X e. ( Z I Y ) )
10 9 3mix2d
 |-  ( ph -> ( Z e. ( X I Y ) \/ X e. ( Z I Y ) \/ Y e. ( X I Z ) ) )
11 1 3 2 4 5 6 8 7 tgellng
 |-  ( ph -> ( Z e. ( X L Y ) <-> ( Z e. ( X I Y ) \/ X e. ( Z I Y ) \/ Y e. ( X I Z ) ) ) )
12 10 11 mpbird
 |-  ( ph -> Z e. ( X L Y ) )