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