Metamath Proof Explorer

Theorem legbtwn

Description: Deduce betweenness from "less than" relation. Corresponds loosely to Proposition 6.13 of Schwabhauser p. 45. (Contributed by Thierry Arnoux, 25-Aug-2019)

Ref Expression
Hypotheses legval.p 
|- P = ( Base ` G )
legval.d 
|- .- = ( dist ` G )
legval.i 
|- I = ( Itv ` G )
legval.l 
|- .<_ = ( leG ` G )
legval.g 
|- ( ph -> G e. TarskiG )
legid.a 
|- ( ph -> A e. P )
legid.b 
|- ( ph -> B e. P )
legtrd.c 
|- ( ph -> C e. P )
legtrd.d 
|- ( ph -> D e. P )
legbtwn.1 
|- ( ph -> ( A e. ( C I B ) \/ B e. ( C I A ) ) )
legbtwn.2 
|- ( ph -> ( C .- A ) .<_ ( C .- B ) )
Assertion legbtwn 
|- ( ph -> A e. ( C I B ) )

Proof

Step Hyp Ref Expression
1 legval.p 
 |-  P = ( Base ` G )
2 legval.d 
 |-  .- = ( dist ` G )
3 legval.i 
 |-  I = ( Itv ` G )
4 legval.l 
 |-  .<_ = ( leG ` G )
5 legval.g 
 |-  ( ph -> G e. TarskiG )
6 legid.a 
 |-  ( ph -> A e. P )
7 legid.b 
 |-  ( ph -> B e. P )
8 legtrd.c 
 |-  ( ph -> C e. P )
9 legtrd.d 
 |-  ( ph -> D e. P )
10 legbtwn.1 
 |-  ( ph -> ( A e. ( C I B ) \/ B e. ( C I A ) ) )
11 legbtwn.2 
 |-  ( ph -> ( C .- A ) .<_ ( C .- B ) )
12 simpr 
 |-  ( ( ph /\ A e. ( C I B ) ) -> A e. ( C I B ) )
13 5 adantr 
 |-  ( ( ph /\ B e. ( C I A ) ) -> G e. TarskiG )
14 6 adantr 
 |-  ( ( ph /\ B e. ( C I A ) ) -> A e. P )
15 7 adantr 
 |-  ( ( ph /\ B e. ( C I A ) ) -> B e. P )
16 8 adantr 
 |-  ( ( ph /\ B e. ( C I A ) ) -> C e. P )
17 simpr 
 |-  ( ( ph /\ B e. ( C I A ) ) -> B e. ( C I A ) )
18 1 2 3 13 16 15 14 17 tgbtwncom 
 |-  ( ( ph /\ B e. ( C I A ) ) -> B e. ( A I C ) )
19 1 2 3 13 15 16 tgbtwntriv1 
 |-  ( ( ph /\ B e. ( C I A ) ) -> B e. ( B I C ) )
20 11 adantr 
 |-  ( ( ph /\ B e. ( C I A ) ) -> ( C .- A ) .<_ ( C .- B ) )
21 1 2 3 4 13 16 15 14 17 btwnleg 
 |-  ( ( ph /\ B e. ( C I A ) ) -> ( C .- B ) .<_ ( C .- A ) )
22 1 2 3 4 13 16 14 16 15 20 21 legtri3 
 |-  ( ( ph /\ B e. ( C I A ) ) -> ( C .- A ) = ( C .- B ) )
23 1 2 3 13 16 14 16 15 22 tgcgrcomlr 
 |-  ( ( ph /\ B e. ( C I A ) ) -> ( A .- C ) = ( B .- C ) )
24 eqidd 
 |-  ( ( ph /\ B e. ( C I A ) ) -> ( B .- C ) = ( B .- C ) )
25 1 2 3 13 14 15 16 15 15 16 18 19 23 24 tgcgrsub 
 |-  ( ( ph /\ B e. ( C I A ) ) -> ( A .- B ) = ( B .- B ) )
26 1 2 3 13 14 15 15 25 axtgcgrid 
 |-  ( ( ph /\ B e. ( C I A ) ) -> A = B )
27 26 17 eqeltrd 
 |-  ( ( ph /\ B e. ( C I A ) ) -> A e. ( C I A ) )
28 26 oveq2d 
 |-  ( ( ph /\ B e. ( C I A ) ) -> ( C I A ) = ( C I B ) )
29 27 28 eleqtrd 
 |-  ( ( ph /\ B e. ( C I A ) ) -> A e. ( C I B ) )
30 12 29 10 mpjaodan 
 |-  ( ph -> A e. ( C I B ) )