Metamath Proof Explorer


Theorem btwnhl2

Description: Deduce half-line from betweenness. (Contributed by Thierry Arnoux, 4-Mar-2020)

Ref Expression
Hypotheses ishlg.p
|- P = ( Base ` G )
ishlg.i
|- I = ( Itv ` G )
ishlg.k
|- K = ( hlG ` G )
ishlg.a
|- ( ph -> A e. P )
ishlg.b
|- ( ph -> B e. P )
ishlg.c
|- ( ph -> C e. P )
hlln.1
|- ( ph -> G e. TarskiG )
hltr.d
|- ( ph -> D e. P )
btwnhl1.1
|- ( ph -> C e. ( A I B ) )
btwnhl1.2
|- ( ph -> A =/= B )
btwnhl2.3
|- ( ph -> C =/= B )
Assertion btwnhl2
|- ( ph -> C ( K ` B ) A )

Proof

Step Hyp Ref Expression
1 ishlg.p
 |-  P = ( Base ` G )
2 ishlg.i
 |-  I = ( Itv ` G )
3 ishlg.k
 |-  K = ( hlG ` G )
4 ishlg.a
 |-  ( ph -> A e. P )
5 ishlg.b
 |-  ( ph -> B e. P )
6 ishlg.c
 |-  ( ph -> C e. P )
7 hlln.1
 |-  ( ph -> G e. TarskiG )
8 hltr.d
 |-  ( ph -> D e. P )
9 btwnhl1.1
 |-  ( ph -> C e. ( A I B ) )
10 btwnhl1.2
 |-  ( ph -> A =/= B )
11 btwnhl2.3
 |-  ( ph -> C =/= B )
12 eqid
 |-  ( dist ` G ) = ( dist ` G )
13 1 12 2 7 4 6 5 9 tgbtwncom
 |-  ( ph -> C e. ( B I A ) )
14 13 orcd
 |-  ( ph -> ( C e. ( B I A ) \/ A e. ( B I C ) ) )
15 1 2 3 6 4 5 7 ishlg
 |-  ( ph -> ( C ( K ` B ) A <-> ( C =/= B /\ A =/= B /\ ( C e. ( B I A ) \/ A e. ( B I C ) ) ) ) )
16 11 10 14 15 mpbir3and
 |-  ( ph -> C ( K ` B ) A )