Metamath Proof Explorer

Theorem legtrid

Description: Trichotomy law for the less-than relationship. Proposition 5.10 of Schwabhauser p. 42. (Contributed by Thierry Arnoux, 27-Jun-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 )
Assertion legtrid 
|- ( ph -> ( ( A .- B ) .<_ ( C .- D ) \/ ( C .- D ) .<_ ( A .- 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 5 adantr 
 |-  ( ( ph /\ ( # ` P ) = 1 ) -> G e. TarskiG )
11 6 adantr 
 |-  ( ( ph /\ ( # ` P ) = 1 ) -> A e. P )
12 7 adantr 
 |-  ( ( ph /\ ( # ` P ) = 1 ) -> B e. P )
13 1 2 3 4 10 11 12 legid 
 |-  ( ( ph /\ ( # ` P ) = 1 ) -> ( A .- B ) .<_ ( A .- B ) )
14 8 adantr 
 |-  ( ( ph /\ ( # ` P ) = 1 ) -> C e. P )
15 simpr 
 |-  ( ( ph /\ ( # ` P ) = 1 ) -> ( # ` P ) = 1 )
16 9 adantr 
 |-  ( ( ph /\ ( # ` P ) = 1 ) -> D e. P )
17 1 2 3 10 11 12 14 15 16 tgldim0cgr 
 |-  ( ( ph /\ ( # ` P ) = 1 ) -> ( A .- B ) = ( C .- D ) )
18 13 17 breqtrd 
 |-  ( ( ph /\ ( # ` P ) = 1 ) -> ( A .- B ) .<_ ( C .- D ) )
19 18 orcd 
 |-  ( ( ph /\ ( # ` P ) = 1 ) -> ( ( A .- B ) .<_ ( C .- D ) \/ ( C .- D ) .<_ ( A .- B ) ) )
20 5 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. P ) /\ ( A e. ( B I x ) /\ A =/= x ) ) /\ ( y e. P /\ ( A e. ( x I y ) /\ ( A .- y ) = ( C .- D ) ) ) ) -> G e. TarskiG )
21 simplr 
 |-  ( ( ( ph /\ x e. P ) /\ ( A e. ( B I x ) /\ A =/= x ) ) -> x e. P )
22 21 adantr 
 |-  ( ( ( ( ph /\ x e. P ) /\ ( A e. ( B I x ) /\ A =/= x ) ) /\ ( y e. P /\ ( A e. ( x I y ) /\ ( A .- y ) = ( C .- D ) ) ) ) -> x e. P )
23 6 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. P ) /\ ( A e. ( B I x ) /\ A =/= x ) ) /\ ( y e. P /\ ( A e. ( x I y ) /\ ( A .- y ) = ( C .- D ) ) ) ) -> A e. P )
24 7 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. P ) /\ ( A e. ( B I x ) /\ A =/= x ) ) /\ ( y e. P /\ ( A e. ( x I y ) /\ ( A .- y ) = ( C .- D ) ) ) ) -> B e. P )
25 simprl 
 |-  ( ( ( ( ph /\ x e. P ) /\ ( A e. ( B I x ) /\ A =/= x ) ) /\ ( y e. P /\ ( A e. ( x I y ) /\ ( A .- y ) = ( C .- D ) ) ) ) -> y e. P )
26 simplrr 
 |-  ( ( ( ( ph /\ x e. P ) /\ ( A e. ( B I x ) /\ A =/= x ) ) /\ ( y e. P /\ ( A e. ( x I y ) /\ ( A .- y ) = ( C .- D ) ) ) ) -> A =/= x )
27 26 necomd 
 |-  ( ( ( ( ph /\ x e. P ) /\ ( A e. ( B I x ) /\ A =/= x ) ) /\ ( y e. P /\ ( A e. ( x I y ) /\ ( A .- y ) = ( C .- D ) ) ) ) -> x =/= A )
28 simplrl 
 |-  ( ( ( ( ph /\ x e. P ) /\ ( A e. ( B I x ) /\ A =/= x ) ) /\ ( y e. P /\ ( A e. ( x I y ) /\ ( A .- y ) = ( C .- D ) ) ) ) -> A e. ( B I x ) )
29 1 2 3 20 24 23 22 28 tgbtwncom 
 |-  ( ( ( ( ph /\ x e. P ) /\ ( A e. ( B I x ) /\ A =/= x ) ) /\ ( y e. P /\ ( A e. ( x I y ) /\ ( A .- y ) = ( C .- D ) ) ) ) -> A e. ( x I B ) )
30 simprrl 
 |-  ( ( ( ( ph /\ x e. P ) /\ ( A e. ( B I x ) /\ A =/= x ) ) /\ ( y e. P /\ ( A e. ( x I y ) /\ ( A .- y ) = ( C .- D ) ) ) ) -> A e. ( x I y ) )
31 1 3 20 22 23 24 25 27 29 30 tgbtwnconn2 
 |-  ( ( ( ( ph /\ x e. P ) /\ ( A e. ( B I x ) /\ A =/= x ) ) /\ ( y e. P /\ ( A e. ( x I y ) /\ ( A .- y ) = ( C .- D ) ) ) ) -> ( B e. ( A I y ) \/ y e. ( A I B ) ) )
32 simprrr 
 |-  ( ( ( ( ph /\ x e. P ) /\ ( A e. ( B I x ) /\ A =/= x ) ) /\ ( y e. P /\ ( A e. ( x I y ) /\ ( A .- y ) = ( C .- D ) ) ) ) -> ( A .- y ) = ( C .- D ) )
33 31 32 jca 
 |-  ( ( ( ( ph /\ x e. P ) /\ ( A e. ( B I x ) /\ A =/= x ) ) /\ ( y e. P /\ ( A e. ( x I y ) /\ ( A .- y ) = ( C .- D ) ) ) ) -> ( ( B e. ( A I y ) \/ y e. ( A I B ) ) /\ ( A .- y ) = ( C .- D ) ) )
34 5 ad2antrr 
 |-  ( ( ( ph /\ x e. P ) /\ ( A e. ( B I x ) /\ A =/= x ) ) -> G e. TarskiG )
35 6 ad2antrr 
 |-  ( ( ( ph /\ x e. P ) /\ ( A e. ( B I x ) /\ A =/= x ) ) -> A e. P )
36 8 ad2antrr 
 |-  ( ( ( ph /\ x e. P ) /\ ( A e. ( B I x ) /\ A =/= x ) ) -> C e. P )
37 9 ad2antrr 
 |-  ( ( ( ph /\ x e. P ) /\ ( A e. ( B I x ) /\ A =/= x ) ) -> D e. P )
38 1 2 3 34 21 35 36 37 axtgsegcon 
 |-  ( ( ( ph /\ x e. P ) /\ ( A e. ( B I x ) /\ A =/= x ) ) -> E. y e. P ( A e. ( x I y ) /\ ( A .- y ) = ( C .- D ) ) )
39 33 38 reximddv 
 |-  ( ( ( ph /\ x e. P ) /\ ( A e. ( B I x ) /\ A =/= x ) ) -> E. y e. P ( ( B e. ( A I y ) \/ y e. ( A I B ) ) /\ ( A .- y ) = ( C .- D ) ) )
40 39 adantllr 
 |-  ( ( ( ( ph /\ 2 <_ ( # ` P ) ) /\ x e. P ) /\ ( A e. ( B I x ) /\ A =/= x ) ) -> E. y e. P ( ( B e. ( A I y ) \/ y e. ( A I B ) ) /\ ( A .- y ) = ( C .- D ) ) )
41 5 adantr 
 |-  ( ( ph /\ 2 <_ ( # ` P ) ) -> G e. TarskiG )
42 7 adantr 
 |-  ( ( ph /\ 2 <_ ( # ` P ) ) -> B e. P )
43 6 adantr 
 |-  ( ( ph /\ 2 <_ ( # ` P ) ) -> A e. P )
44 simpr 
 |-  ( ( ph /\ 2 <_ ( # ` P ) ) -> 2 <_ ( # ` P ) )
45 1 2 3 41 42 43 44 tgbtwndiff 
 |-  ( ( ph /\ 2 <_ ( # ` P ) ) -> E. x e. P ( A e. ( B I x ) /\ A =/= x ) )
46 40 45 r19.29a 
 |-  ( ( ph /\ 2 <_ ( # ` P ) ) -> E. y e. P ( ( B e. ( A I y ) \/ y e. ( A I B ) ) /\ ( A .- y ) = ( C .- D ) ) )
47 andir 
 |-  ( ( ( B e. ( A I y ) \/ y e. ( A I B ) ) /\ ( A .- y ) = ( C .- D ) ) <-> ( ( B e. ( A I y ) /\ ( A .- y ) = ( C .- D ) ) \/ ( y e. ( A I B ) /\ ( A .- y ) = ( C .- D ) ) ) )
48 eqcom 
 |-  ( ( A .- y ) = ( C .- D ) <-> ( C .- D ) = ( A .- y ) )
49 48 anbi2i 
 |-  ( ( y e. ( A I B ) /\ ( A .- y ) = ( C .- D ) ) <-> ( y e. ( A I B ) /\ ( C .- D ) = ( A .- y ) ) )
50 49 orbi2i 
 |-  ( ( ( B e. ( A I y ) /\ ( A .- y ) = ( C .- D ) ) \/ ( y e. ( A I B ) /\ ( A .- y ) = ( C .- D ) ) ) <-> ( ( B e. ( A I y ) /\ ( A .- y ) = ( C .- D ) ) \/ ( y e. ( A I B ) /\ ( C .- D ) = ( A .- y ) ) ) )
51 47 50 bitri 
 |-  ( ( ( B e. ( A I y ) \/ y e. ( A I B ) ) /\ ( A .- y ) = ( C .- D ) ) <-> ( ( B e. ( A I y ) /\ ( A .- y ) = ( C .- D ) ) \/ ( y e. ( A I B ) /\ ( C .- D ) = ( A .- y ) ) ) )
52 51 rexbii 
 |-  ( E. y e. P ( ( B e. ( A I y ) \/ y e. ( A I B ) ) /\ ( A .- y ) = ( C .- D ) ) <-> E. y e. P ( ( B e. ( A I y ) /\ ( A .- y ) = ( C .- D ) ) \/ ( y e. ( A I B ) /\ ( C .- D ) = ( A .- y ) ) ) )
53 r19.43 
 |-  ( E. y e. P ( ( B e. ( A I y ) /\ ( A .- y ) = ( C .- D ) ) \/ ( y e. ( A I B ) /\ ( C .- D ) = ( A .- y ) ) ) <-> ( E. y e. P ( B e. ( A I y ) /\ ( A .- y ) = ( C .- D ) ) \/ E. y e. P ( y e. ( A I B ) /\ ( C .- D ) = ( A .- y ) ) ) )
54 52 53 bitri 
 |-  ( E. y e. P ( ( B e. ( A I y ) \/ y e. ( A I B ) ) /\ ( A .- y ) = ( C .- D ) ) <-> ( E. y e. P ( B e. ( A I y ) /\ ( A .- y ) = ( C .- D ) ) \/ E. y e. P ( y e. ( A I B ) /\ ( C .- D ) = ( A .- y ) ) ) )
55 46 54 sylib 
 |-  ( ( ph /\ 2 <_ ( # ` P ) ) -> ( E. y e. P ( B e. ( A I y ) /\ ( A .- y ) = ( C .- D ) ) \/ E. y e. P ( y e. ( A I B ) /\ ( C .- D ) = ( A .- y ) ) ) )
56 1 2 3 4 5 6 7 8 9 legov2 
 |-  ( ph -> ( ( A .- B ) .<_ ( C .- D ) <-> E. y e. P ( B e. ( A I y ) /\ ( A .- y ) = ( C .- D ) ) ) )
57 1 2 3 4 5 8 9 6 7 legov 
 |-  ( ph -> ( ( C .- D ) .<_ ( A .- B ) <-> E. y e. P ( y e. ( A I B ) /\ ( C .- D ) = ( A .- y ) ) ) )
58 56 57 orbi12d 
 |-  ( ph -> ( ( ( A .- B ) .<_ ( C .- D ) \/ ( C .- D ) .<_ ( A .- B ) ) <-> ( E. y e. P ( B e. ( A I y ) /\ ( A .- y ) = ( C .- D ) ) \/ E. y e. P ( y e. ( A I B ) /\ ( C .- D ) = ( A .- y ) ) ) ) )
59 58 adantr 
 |-  ( ( ph /\ 2 <_ ( # ` P ) ) -> ( ( ( A .- B ) .<_ ( C .- D ) \/ ( C .- D ) .<_ ( A .- B ) ) <-> ( E. y e. P ( B e. ( A I y ) /\ ( A .- y ) = ( C .- D ) ) \/ E. y e. P ( y e. ( A I B ) /\ ( C .- D ) = ( A .- y ) ) ) ) )
60 55 59 mpbird 
 |-  ( ( ph /\ 2 <_ ( # ` P ) ) -> ( ( A .- B ) .<_ ( C .- D ) \/ ( C .- D ) .<_ ( A .- B ) ) )
61 1 6 tgldimor 
 |-  ( ph -> ( ( # ` P ) = 1 \/ 2 <_ ( # ` P ) ) )
62 19 60 61 mpjaodan 
 |-  ( ph -> ( ( A .- B ) .<_ ( C .- D ) \/ ( C .- D ) .<_ ( A .- B ) ) )