Metamath Proof Explorer

Theorem legtrd

Description: Transitivity of the less-than relationship. Proposition 5.8 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 )
legtrd.e 
|- ( ph -> E e. P )
legtrd.f 
|- ( ph -> F e. P )
legtrd.1 
|- ( ph -> ( A .- B ) .<_ ( C .- D ) )
legtrd.2 
|- ( ph -> ( C .- D ) .<_ ( E .- F ) )
Assertion legtrd 
|- ( ph -> ( A .- B ) .<_ ( E .- F ) )

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 legtrd.e 
 |-  ( ph -> E e. P )
11 legtrd.f 
 |-  ( ph -> F e. P )
12 legtrd.1 
 |-  ( ph -> ( A .- B ) .<_ ( C .- D ) )
13 legtrd.2 
 |-  ( ph -> ( C .- D ) .<_ ( E .- F ) )
14 eqid 
 |-  ( LineG ` G ) = ( LineG ` G )
15 5 ad4antr 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ ( x e. ( C I D ) /\ ( A .- B ) = ( C .- x ) ) ) /\ y e. P ) /\ ( y e. ( E I F ) /\ ( C .- D ) = ( E .- y ) ) ) -> G e. TarskiG )
16 8 ad4antr 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ ( x e. ( C I D ) /\ ( A .- B ) = ( C .- x ) ) ) /\ y e. P ) /\ ( y e. ( E I F ) /\ ( C .- D ) = ( E .- y ) ) ) -> C e. P )
17 9 ad4antr 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ ( x e. ( C I D ) /\ ( A .- B ) = ( C .- x ) ) ) /\ y e. P ) /\ ( y e. ( E I F ) /\ ( C .- D ) = ( E .- y ) ) ) -> D e. P )
18 simp-4r 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ ( x e. ( C I D ) /\ ( A .- B ) = ( C .- x ) ) ) /\ y e. P ) /\ ( y e. ( E I F ) /\ ( C .- D ) = ( E .- y ) ) ) -> x e. P )
19 eqid 
 |-  ( cgrG ` G ) = ( cgrG ` G )
20 10 ad4antr 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ ( x e. ( C I D ) /\ ( A .- B ) = ( C .- x ) ) ) /\ y e. P ) /\ ( y e. ( E I F ) /\ ( C .- D ) = ( E .- y ) ) ) -> E e. P )
21 simplr 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ ( x e. ( C I D ) /\ ( A .- B ) = ( C .- x ) ) ) /\ y e. P ) /\ ( y e. ( E I F ) /\ ( C .- D ) = ( E .- y ) ) ) -> y e. P )
22 simpllr 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ ( x e. ( C I D ) /\ ( A .- B ) = ( C .- x ) ) ) /\ y e. P ) /\ ( y e. ( E I F ) /\ ( C .- D ) = ( E .- y ) ) ) -> ( x e. ( C I D ) /\ ( A .- B ) = ( C .- x ) ) )
23 22 simpld 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ ( x e. ( C I D ) /\ ( A .- B ) = ( C .- x ) ) ) /\ y e. P ) /\ ( y e. ( E I F ) /\ ( C .- D ) = ( E .- y ) ) ) -> x e. ( C I D ) )
24 1 14 3 15 16 18 17 23 btwncolg3 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ ( x e. ( C I D ) /\ ( A .- B ) = ( C .- x ) ) ) /\ y e. P ) /\ ( y e. ( E I F ) /\ ( C .- D ) = ( E .- y ) ) ) -> ( D e. ( C ( LineG ` G ) x ) \/ C = x ) )
25 simprr 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ ( x e. ( C I D ) /\ ( A .- B ) = ( C .- x ) ) ) /\ y e. P ) /\ ( y e. ( E I F ) /\ ( C .- D ) = ( E .- y ) ) ) -> ( C .- D ) = ( E .- y ) )
26 1 14 3 15 16 17 18 19 20 21 2 24 25 lnext 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ ( x e. ( C I D ) /\ ( A .- B ) = ( C .- x ) ) ) /\ y e. P ) /\ ( y e. ( E I F ) /\ ( C .- D ) = ( E .- y ) ) ) -> E. z e. P <" C D x "> ( cgrG ` G ) <" E y z "> )
27 15 ad2antrr 
 |-  ( ( ( ( ( ( ( ph /\ x e. P ) /\ ( x e. ( C I D ) /\ ( A .- B ) = ( C .- x ) ) ) /\ y e. P ) /\ ( y e. ( E I F ) /\ ( C .- D ) = ( E .- y ) ) ) /\ z e. P ) /\ <" C D x "> ( cgrG ` G ) <" E y z "> ) -> G e. TarskiG )
28 20 ad2antrr 
 |-  ( ( ( ( ( ( ( ph /\ x e. P ) /\ ( x e. ( C I D ) /\ ( A .- B ) = ( C .- x ) ) ) /\ y e. P ) /\ ( y e. ( E I F ) /\ ( C .- D ) = ( E .- y ) ) ) /\ z e. P ) /\ <" C D x "> ( cgrG ` G ) <" E y z "> ) -> E e. P )
29 simplr 
 |-  ( ( ( ( ( ( ( ph /\ x e. P ) /\ ( x e. ( C I D ) /\ ( A .- B ) = ( C .- x ) ) ) /\ y e. P ) /\ ( y e. ( E I F ) /\ ( C .- D ) = ( E .- y ) ) ) /\ z e. P ) /\ <" C D x "> ( cgrG ` G ) <" E y z "> ) -> z e. P )
30 simp-4r 
 |-  ( ( ( ( ( ( ( ph /\ x e. P ) /\ ( x e. ( C I D ) /\ ( A .- B ) = ( C .- x ) ) ) /\ y e. P ) /\ ( y e. ( E I F ) /\ ( C .- D ) = ( E .- y ) ) ) /\ z e. P ) /\ <" C D x "> ( cgrG ` G ) <" E y z "> ) -> y e. P )
31 11 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ x e. P ) /\ ( x e. ( C I D ) /\ ( A .- B ) = ( C .- x ) ) ) /\ y e. P ) /\ ( y e. ( E I F ) /\ ( C .- D ) = ( E .- y ) ) ) /\ z e. P ) /\ <" C D x "> ( cgrG ` G ) <" E y z "> ) -> F e. P )
32 16 ad2antrr 
 |-  ( ( ( ( ( ( ( ph /\ x e. P ) /\ ( x e. ( C I D ) /\ ( A .- B ) = ( C .- x ) ) ) /\ y e. P ) /\ ( y e. ( E I F ) /\ ( C .- D ) = ( E .- y ) ) ) /\ z e. P ) /\ <" C D x "> ( cgrG ` G ) <" E y z "> ) -> C e. P )
33 18 ad2antrr 
 |-  ( ( ( ( ( ( ( ph /\ x e. P ) /\ ( x e. ( C I D ) /\ ( A .- B ) = ( C .- x ) ) ) /\ y e. P ) /\ ( y e. ( E I F ) /\ ( C .- D ) = ( E .- y ) ) ) /\ z e. P ) /\ <" C D x "> ( cgrG ` G ) <" E y z "> ) -> x e. P )
34 17 ad2antrr 
 |-  ( ( ( ( ( ( ( ph /\ x e. P ) /\ ( x e. ( C I D ) /\ ( A .- B ) = ( C .- x ) ) ) /\ y e. P ) /\ ( y e. ( E I F ) /\ ( C .- D ) = ( E .- y ) ) ) /\ z e. P ) /\ <" C D x "> ( cgrG ` G ) <" E y z "> ) -> D e. P )
35 simpr 
 |-  ( ( ( ( ( ( ( ph /\ x e. P ) /\ ( x e. ( C I D ) /\ ( A .- B ) = ( C .- x ) ) ) /\ y e. P ) /\ ( y e. ( E I F ) /\ ( C .- D ) = ( E .- y ) ) ) /\ z e. P ) /\ <" C D x "> ( cgrG ` G ) <" E y z "> ) -> <" C D x "> ( cgrG ` G ) <" E y z "> )
36 1 2 3 19 27 32 34 33 28 30 29 35 cgr3swap23 
 |-  ( ( ( ( ( ( ( ph /\ x e. P ) /\ ( x e. ( C I D ) /\ ( A .- B ) = ( C .- x ) ) ) /\ y e. P ) /\ ( y e. ( E I F ) /\ ( C .- D ) = ( E .- y ) ) ) /\ z e. P ) /\ <" C D x "> ( cgrG ` G ) <" E y z "> ) -> <" C x D "> ( cgrG ` G ) <" E z y "> )
37 23 ad2antrr 
 |-  ( ( ( ( ( ( ( ph /\ x e. P ) /\ ( x e. ( C I D ) /\ ( A .- B ) = ( C .- x ) ) ) /\ y e. P ) /\ ( y e. ( E I F ) /\ ( C .- D ) = ( E .- y ) ) ) /\ z e. P ) /\ <" C D x "> ( cgrG ` G ) <" E y z "> ) -> x e. ( C I D ) )
38 1 2 3 19 27 32 33 34 28 29 30 36 37 tgbtwnxfr 
 |-  ( ( ( ( ( ( ( ph /\ x e. P ) /\ ( x e. ( C I D ) /\ ( A .- B ) = ( C .- x ) ) ) /\ y e. P ) /\ ( y e. ( E I F ) /\ ( C .- D ) = ( E .- y ) ) ) /\ z e. P ) /\ <" C D x "> ( cgrG ` G ) <" E y z "> ) -> z e. ( E I y ) )
39 simpllr 
 |-  ( ( ( ( ( ( ( ph /\ x e. P ) /\ ( x e. ( C I D ) /\ ( A .- B ) = ( C .- x ) ) ) /\ y e. P ) /\ ( y e. ( E I F ) /\ ( C .- D ) = ( E .- y ) ) ) /\ z e. P ) /\ <" C D x "> ( cgrG ` G ) <" E y z "> ) -> ( y e. ( E I F ) /\ ( C .- D ) = ( E .- y ) ) )
40 39 simpld 
 |-  ( ( ( ( ( ( ( ph /\ x e. P ) /\ ( x e. ( C I D ) /\ ( A .- B ) = ( C .- x ) ) ) /\ y e. P ) /\ ( y e. ( E I F ) /\ ( C .- D ) = ( E .- y ) ) ) /\ z e. P ) /\ <" C D x "> ( cgrG ` G ) <" E y z "> ) -> y e. ( E I F ) )
41 1 2 3 27 28 29 30 31 38 40 tgbtwnexch 
 |-  ( ( ( ( ( ( ( ph /\ x e. P ) /\ ( x e. ( C I D ) /\ ( A .- B ) = ( C .- x ) ) ) /\ y e. P ) /\ ( y e. ( E I F ) /\ ( C .- D ) = ( E .- y ) ) ) /\ z e. P ) /\ <" C D x "> ( cgrG ` G ) <" E y z "> ) -> z e. ( E I F ) )
42 simp-5r 
 |-  ( ( ( ( ( ( ( ph /\ x e. P ) /\ ( x e. ( C I D ) /\ ( A .- B ) = ( C .- x ) ) ) /\ y e. P ) /\ ( y e. ( E I F ) /\ ( C .- D ) = ( E .- y ) ) ) /\ z e. P ) /\ <" C D x "> ( cgrG ` G ) <" E y z "> ) -> ( x e. ( C I D ) /\ ( A .- B ) = ( C .- x ) ) )
43 42 simprd 
 |-  ( ( ( ( ( ( ( ph /\ x e. P ) /\ ( x e. ( C I D ) /\ ( A .- B ) = ( C .- x ) ) ) /\ y e. P ) /\ ( y e. ( E I F ) /\ ( C .- D ) = ( E .- y ) ) ) /\ z e. P ) /\ <" C D x "> ( cgrG ` G ) <" E y z "> ) -> ( A .- B ) = ( C .- x ) )
44 1 2 3 19 27 32 33 34 28 29 30 36 cgr3simp1 
 |-  ( ( ( ( ( ( ( ph /\ x e. P ) /\ ( x e. ( C I D ) /\ ( A .- B ) = ( C .- x ) ) ) /\ y e. P ) /\ ( y e. ( E I F ) /\ ( C .- D ) = ( E .- y ) ) ) /\ z e. P ) /\ <" C D x "> ( cgrG ` G ) <" E y z "> ) -> ( C .- x ) = ( E .- z ) )
45 43 44 eqtrd 
 |-  ( ( ( ( ( ( ( ph /\ x e. P ) /\ ( x e. ( C I D ) /\ ( A .- B ) = ( C .- x ) ) ) /\ y e. P ) /\ ( y e. ( E I F ) /\ ( C .- D ) = ( E .- y ) ) ) /\ z e. P ) /\ <" C D x "> ( cgrG ` G ) <" E y z "> ) -> ( A .- B ) = ( E .- z ) )
46 41 45 jca 
 |-  ( ( ( ( ( ( ( ph /\ x e. P ) /\ ( x e. ( C I D ) /\ ( A .- B ) = ( C .- x ) ) ) /\ y e. P ) /\ ( y e. ( E I F ) /\ ( C .- D ) = ( E .- y ) ) ) /\ z e. P ) /\ <" C D x "> ( cgrG ` G ) <" E y z "> ) -> ( z e. ( E I F ) /\ ( A .- B ) = ( E .- z ) ) )
47 46 ex 
 |-  ( ( ( ( ( ( ph /\ x e. P ) /\ ( x e. ( C I D ) /\ ( A .- B ) = ( C .- x ) ) ) /\ y e. P ) /\ ( y e. ( E I F ) /\ ( C .- D ) = ( E .- y ) ) ) /\ z e. P ) -> ( <" C D x "> ( cgrG ` G ) <" E y z "> -> ( z e. ( E I F ) /\ ( A .- B ) = ( E .- z ) ) ) )
48 47 reximdva 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ ( x e. ( C I D ) /\ ( A .- B ) = ( C .- x ) ) ) /\ y e. P ) /\ ( y e. ( E I F ) /\ ( C .- D ) = ( E .- y ) ) ) -> ( E. z e. P <" C D x "> ( cgrG ` G ) <" E y z "> -> E. z e. P ( z e. ( E I F ) /\ ( A .- B ) = ( E .- z ) ) ) )
49 26 48 mpd 
 |-  ( ( ( ( ( ph /\ x e. P ) /\ ( x e. ( C I D ) /\ ( A .- B ) = ( C .- x ) ) ) /\ y e. P ) /\ ( y e. ( E I F ) /\ ( C .- D ) = ( E .- y ) ) ) -> E. z e. P ( z e. ( E I F ) /\ ( A .- B ) = ( E .- z ) ) )
50 1 2 3 4 5 8 9 10 11 legov 
 |-  ( ph -> ( ( C .- D ) .<_ ( E .- F ) <-> E. y e. P ( y e. ( E I F ) /\ ( C .- D ) = ( E .- y ) ) ) )
51 13 50 mpbid 
 |-  ( ph -> E. y e. P ( y e. ( E I F ) /\ ( C .- D ) = ( E .- y ) ) )
52 51 ad2antrr 
 |-  ( ( ( ph /\ x e. P ) /\ ( x e. ( C I D ) /\ ( A .- B ) = ( C .- x ) ) ) -> E. y e. P ( y e. ( E I F ) /\ ( C .- D ) = ( E .- y ) ) )
53 49 52 r19.29a 
 |-  ( ( ( ph /\ x e. P ) /\ ( x e. ( C I D ) /\ ( A .- B ) = ( C .- x ) ) ) -> E. z e. P ( z e. ( E I F ) /\ ( A .- B ) = ( E .- z ) ) )
54 1 2 3 4 5 6 7 8 9 legov 
 |-  ( ph -> ( ( A .- B ) .<_ ( C .- D ) <-> E. x e. P ( x e. ( C I D ) /\ ( A .- B ) = ( C .- x ) ) ) )
55 12 54 mpbid 
 |-  ( ph -> E. x e. P ( x e. ( C I D ) /\ ( A .- B ) = ( C .- x ) ) )
56 53 55 r19.29a 
 |-  ( ph -> E. z e. P ( z e. ( E I F ) /\ ( A .- B ) = ( E .- z ) ) )
57 1 2 3 4 5 6 7 10 11 legov 
 |-  ( ph -> ( ( A .- B ) .<_ ( E .- F ) <-> E. z e. P ( z e. ( E I F ) /\ ( A .- B ) = ( E .- z ) ) ) )
58 56 57 mpbird 
 |-  ( ph -> ( A .- B ) .<_ ( E .- F ) )