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 ) |
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 ) |