Metamath Proof Explorer

Theorem legov2

Description: An equivalent definition of the less-than relationship. Definition 5.5 of Schwabhauser p. 41. (Contributed by Thierry Arnoux, 21-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 )
legov.a 
|- ( ph -> A e. P )
legov.b 
|- ( ph -> B e. P )
legov.c 
|- ( ph -> C e. P )
legov.d 
|- ( ph -> D e. P )
Assertion legov2 
|- ( ph -> ( ( A .- B ) .<_ ( C .- D ) <-> E. x e. P ( B e. ( A I x ) /\ ( A .- x ) = ( C .- D ) ) ) )

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 legov.a 
 |-  ( ph -> A e. P )
7 legov.b 
 |-  ( ph -> B e. P )
8 legov.c 
 |-  ( ph -> C e. P )
9 legov.d 
 |-  ( ph -> D e. P )
10 1 2 3 4 5 6 7 8 9 legov 
 |-  ( ph -> ( ( A .- B ) .<_ ( C .- D ) <-> E. y e. P ( y e. ( C I D ) /\ ( A .- B ) = ( C .- y ) ) ) )
11 eqid 
 |-  ( LineG ` G ) = ( LineG ` G )
12 5 ad2antrr 
 |-  ( ( ( ph /\ z e. P ) /\ ( z e. ( C I D ) /\ ( A .- B ) = ( C .- z ) ) ) -> G e. TarskiG )
13 8 ad2antrr 
 |-  ( ( ( ph /\ z e. P ) /\ ( z e. ( C I D ) /\ ( A .- B ) = ( C .- z ) ) ) -> C e. P )
14 simplr 
 |-  ( ( ( ph /\ z e. P ) /\ ( z e. ( C I D ) /\ ( A .- B ) = ( C .- z ) ) ) -> z e. P )
15 9 ad2antrr 
 |-  ( ( ( ph /\ z e. P ) /\ ( z e. ( C I D ) /\ ( A .- B ) = ( C .- z ) ) ) -> D e. P )
16 eqid 
 |-  ( cgrG ` G ) = ( cgrG ` G )
17 6 ad2antrr 
 |-  ( ( ( ph /\ z e. P ) /\ ( z e. ( C I D ) /\ ( A .- B ) = ( C .- z ) ) ) -> A e. P )
18 7 ad2antrr 
 |-  ( ( ( ph /\ z e. P ) /\ ( z e. ( C I D ) /\ ( A .- B ) = ( C .- z ) ) ) -> B e. P )
19 simprl 
 |-  ( ( ( ph /\ z e. P ) /\ ( z e. ( C I D ) /\ ( A .- B ) = ( C .- z ) ) ) -> z e. ( C I D ) )
20 1 11 3 12 13 15 14 19 btwncolg1 
 |-  ( ( ( ph /\ z e. P ) /\ ( z e. ( C I D ) /\ ( A .- B ) = ( C .- z ) ) ) -> ( z e. ( C ( LineG ` G ) D ) \/ C = D ) )
21 simprr 
 |-  ( ( ( ph /\ z e. P ) /\ ( z e. ( C I D ) /\ ( A .- B ) = ( C .- z ) ) ) -> ( A .- B ) = ( C .- z ) )
22 21 eqcomd 
 |-  ( ( ( ph /\ z e. P ) /\ ( z e. ( C I D ) /\ ( A .- B ) = ( C .- z ) ) ) -> ( C .- z ) = ( A .- B ) )
23 1 11 3 12 13 14 15 16 17 18 2 20 22 lnext 
 |-  ( ( ( ph /\ z e. P ) /\ ( z e. ( C I D ) /\ ( A .- B ) = ( C .- z ) ) ) -> E. x e. P <" C z D "> ( cgrG ` G ) <" A B x "> )
24 12 ad2antrr 
 |-  ( ( ( ( ( ph /\ z e. P ) /\ ( z e. ( C I D ) /\ ( A .- B ) = ( C .- z ) ) ) /\ x e. P ) /\ <" C z D "> ( cgrG ` G ) <" A B x "> ) -> G e. TarskiG )
25 13 ad2antrr 
 |-  ( ( ( ( ( ph /\ z e. P ) /\ ( z e. ( C I D ) /\ ( A .- B ) = ( C .- z ) ) ) /\ x e. P ) /\ <" C z D "> ( cgrG ` G ) <" A B x "> ) -> C e. P )
26 14 ad2antrr 
 |-  ( ( ( ( ( ph /\ z e. P ) /\ ( z e. ( C I D ) /\ ( A .- B ) = ( C .- z ) ) ) /\ x e. P ) /\ <" C z D "> ( cgrG ` G ) <" A B x "> ) -> z e. P )
27 15 ad2antrr 
 |-  ( ( ( ( ( ph /\ z e. P ) /\ ( z e. ( C I D ) /\ ( A .- B ) = ( C .- z ) ) ) /\ x e. P ) /\ <" C z D "> ( cgrG ` G ) <" A B x "> ) -> D e. P )
28 17 ad2antrr 
 |-  ( ( ( ( ( ph /\ z e. P ) /\ ( z e. ( C I D ) /\ ( A .- B ) = ( C .- z ) ) ) /\ x e. P ) /\ <" C z D "> ( cgrG ` G ) <" A B x "> ) -> A e. P )
29 18 ad2antrr 
 |-  ( ( ( ( ( ph /\ z e. P ) /\ ( z e. ( C I D ) /\ ( A .- B ) = ( C .- z ) ) ) /\ x e. P ) /\ <" C z D "> ( cgrG ` G ) <" A B x "> ) -> B e. P )
30 simplr 
 |-  ( ( ( ( ( ph /\ z e. P ) /\ ( z e. ( C I D ) /\ ( A .- B ) = ( C .- z ) ) ) /\ x e. P ) /\ <" C z D "> ( cgrG ` G ) <" A B x "> ) -> x e. P )
31 simpr 
 |-  ( ( ( ( ( ph /\ z e. P ) /\ ( z e. ( C I D ) /\ ( A .- B ) = ( C .- z ) ) ) /\ x e. P ) /\ <" C z D "> ( cgrG ` G ) <" A B x "> ) -> <" C z D "> ( cgrG ` G ) <" A B x "> )
32 simpllr 
 |-  ( ( ( ( ( ph /\ z e. P ) /\ ( z e. ( C I D ) /\ ( A .- B ) = ( C .- z ) ) ) /\ x e. P ) /\ <" C z D "> ( cgrG ` G ) <" A B x "> ) -> ( z e. ( C I D ) /\ ( A .- B ) = ( C .- z ) ) )
33 32 simpld 
 |-  ( ( ( ( ( ph /\ z e. P ) /\ ( z e. ( C I D ) /\ ( A .- B ) = ( C .- z ) ) ) /\ x e. P ) /\ <" C z D "> ( cgrG ` G ) <" A B x "> ) -> z e. ( C I D ) )
34 1 2 3 16 24 25 26 27 28 29 30 31 33 tgbtwnxfr 
 |-  ( ( ( ( ( ph /\ z e. P ) /\ ( z e. ( C I D ) /\ ( A .- B ) = ( C .- z ) ) ) /\ x e. P ) /\ <" C z D "> ( cgrG ` G ) <" A B x "> ) -> B e. ( A I x ) )
35 1 2 3 16 24 25 26 27 28 29 30 31 trgcgrcom 
 |-  ( ( ( ( ( ph /\ z e. P ) /\ ( z e. ( C I D ) /\ ( A .- B ) = ( C .- z ) ) ) /\ x e. P ) /\ <" C z D "> ( cgrG ` G ) <" A B x "> ) -> <" A B x "> ( cgrG ` G ) <" C z D "> )
36 1 2 3 16 24 28 29 30 25 26 27 35 cgr3simp3 
 |-  ( ( ( ( ( ph /\ z e. P ) /\ ( z e. ( C I D ) /\ ( A .- B ) = ( C .- z ) ) ) /\ x e. P ) /\ <" C z D "> ( cgrG ` G ) <" A B x "> ) -> ( x .- A ) = ( D .- C ) )
37 1 2 3 24 30 28 27 25 36 tgcgrcomlr 
 |-  ( ( ( ( ( ph /\ z e. P ) /\ ( z e. ( C I D ) /\ ( A .- B ) = ( C .- z ) ) ) /\ x e. P ) /\ <" C z D "> ( cgrG ` G ) <" A B x "> ) -> ( A .- x ) = ( C .- D ) )
38 34 37 jca 
 |-  ( ( ( ( ( ph /\ z e. P ) /\ ( z e. ( C I D ) /\ ( A .- B ) = ( C .- z ) ) ) /\ x e. P ) /\ <" C z D "> ( cgrG ` G ) <" A B x "> ) -> ( B e. ( A I x ) /\ ( A .- x ) = ( C .- D ) ) )
39 38 ex 
 |-  ( ( ( ( ph /\ z e. P ) /\ ( z e. ( C I D ) /\ ( A .- B ) = ( C .- z ) ) ) /\ x e. P ) -> ( <" C z D "> ( cgrG ` G ) <" A B x "> -> ( B e. ( A I x ) /\ ( A .- x ) = ( C .- D ) ) ) )
40 39 reximdva 
 |-  ( ( ( ph /\ z e. P ) /\ ( z e. ( C I D ) /\ ( A .- B ) = ( C .- z ) ) ) -> ( E. x e. P <" C z D "> ( cgrG ` G ) <" A B x "> -> E. x e. P ( B e. ( A I x ) /\ ( A .- x ) = ( C .- D ) ) ) )
41 23 40 mpd 
 |-  ( ( ( ph /\ z e. P ) /\ ( z e. ( C I D ) /\ ( A .- B ) = ( C .- z ) ) ) -> E. x e. P ( B e. ( A I x ) /\ ( A .- x ) = ( C .- D ) ) )
42 41 adantllr 
 |-  ( ( ( ( ph /\ E. y e. P ( y e. ( C I D ) /\ ( A .- B ) = ( C .- y ) ) ) /\ z e. P ) /\ ( z e. ( C I D ) /\ ( A .- B ) = ( C .- z ) ) ) -> E. x e. P ( B e. ( A I x ) /\ ( A .- x ) = ( C .- D ) ) )
43 simpr 
 |-  ( ( ph /\ E. y e. P ( y e. ( C I D ) /\ ( A .- B ) = ( C .- y ) ) ) -> E. y e. P ( y e. ( C I D ) /\ ( A .- B ) = ( C .- y ) ) )
44 eleq1 
 |-  ( y = z -> ( y e. ( C I D ) <-> z e. ( C I D ) ) )
45 oveq2 
 |-  ( y = z -> ( C .- y ) = ( C .- z ) )
46 45 eqeq2d 
 |-  ( y = z -> ( ( A .- B ) = ( C .- y ) <-> ( A .- B ) = ( C .- z ) ) )
47 44 46 anbi12d 
 |-  ( y = z -> ( ( y e. ( C I D ) /\ ( A .- B ) = ( C .- y ) ) <-> ( z e. ( C I D ) /\ ( A .- B ) = ( C .- z ) ) ) )
48 47 cbvrexvw 
 |-  ( E. y e. P ( y e. ( C I D ) /\ ( A .- B ) = ( C .- y ) ) <-> E. z e. P ( z e. ( C I D ) /\ ( A .- B ) = ( C .- z ) ) )
49 43 48 sylib 
 |-  ( ( ph /\ E. y e. P ( y e. ( C I D ) /\ ( A .- B ) = ( C .- y ) ) ) -> E. z e. P ( z e. ( C I D ) /\ ( A .- B ) = ( C .- z ) ) )
50 42 49 r19.29a 
 |-  ( ( ph /\ E. y e. P ( y e. ( C I D ) /\ ( A .- B ) = ( C .- y ) ) ) -> E. x e. P ( B e. ( A I x ) /\ ( A .- x ) = ( C .- D ) ) )
51 5 ad2antrr 
 |-  ( ( ( ph /\ z e. P ) /\ ( B e. ( A I z ) /\ ( A .- z ) = ( C .- D ) ) ) -> G e. TarskiG )
52 6 ad2antrr 
 |-  ( ( ( ph /\ z e. P ) /\ ( B e. ( A I z ) /\ ( A .- z ) = ( C .- D ) ) ) -> A e. P )
53 simplr 
 |-  ( ( ( ph /\ z e. P ) /\ ( B e. ( A I z ) /\ ( A .- z ) = ( C .- D ) ) ) -> z e. P )
54 7 ad2antrr 
 |-  ( ( ( ph /\ z e. P ) /\ ( B e. ( A I z ) /\ ( A .- z ) = ( C .- D ) ) ) -> B e. P )
55 8 ad2antrr 
 |-  ( ( ( ph /\ z e. P ) /\ ( B e. ( A I z ) /\ ( A .- z ) = ( C .- D ) ) ) -> C e. P )
56 9 ad2antrr 
 |-  ( ( ( ph /\ z e. P ) /\ ( B e. ( A I z ) /\ ( A .- z ) = ( C .- D ) ) ) -> D e. P )
57 simprl 
 |-  ( ( ( ph /\ z e. P ) /\ ( B e. ( A I z ) /\ ( A .- z ) = ( C .- D ) ) ) -> B e. ( A I z ) )
58 1 11 3 51 52 54 53 57 btwncolg3 
 |-  ( ( ( ph /\ z e. P ) /\ ( B e. ( A I z ) /\ ( A .- z ) = ( C .- D ) ) ) -> ( z e. ( A ( LineG ` G ) B ) \/ A = B ) )
59 simprr 
 |-  ( ( ( ph /\ z e. P ) /\ ( B e. ( A I z ) /\ ( A .- z ) = ( C .- D ) ) ) -> ( A .- z ) = ( C .- D ) )
60 1 11 3 51 52 53 54 16 55 56 2 58 59 lnext 
 |-  ( ( ( ph /\ z e. P ) /\ ( B e. ( A I z ) /\ ( A .- z ) = ( C .- D ) ) ) -> E. y e. P <" A z B "> ( cgrG ` G ) <" C D y "> )
61 51 ad2antrr 
 |-  ( ( ( ( ( ph /\ z e. P ) /\ ( B e. ( A I z ) /\ ( A .- z ) = ( C .- D ) ) ) /\ y e. P ) /\ <" A z B "> ( cgrG ` G ) <" C D y "> ) -> G e. TarskiG )
62 52 ad2antrr 
 |-  ( ( ( ( ( ph /\ z e. P ) /\ ( B e. ( A I z ) /\ ( A .- z ) = ( C .- D ) ) ) /\ y e. P ) /\ <" A z B "> ( cgrG ` G ) <" C D y "> ) -> A e. P )
63 54 ad2antrr 
 |-  ( ( ( ( ( ph /\ z e. P ) /\ ( B e. ( A I z ) /\ ( A .- z ) = ( C .- D ) ) ) /\ y e. P ) /\ <" A z B "> ( cgrG ` G ) <" C D y "> ) -> B e. P )
64 53 ad2antrr 
 |-  ( ( ( ( ( ph /\ z e. P ) /\ ( B e. ( A I z ) /\ ( A .- z ) = ( C .- D ) ) ) /\ y e. P ) /\ <" A z B "> ( cgrG ` G ) <" C D y "> ) -> z e. P )
65 55 ad2antrr 
 |-  ( ( ( ( ( ph /\ z e. P ) /\ ( B e. ( A I z ) /\ ( A .- z ) = ( C .- D ) ) ) /\ y e. P ) /\ <" A z B "> ( cgrG ` G ) <" C D y "> ) -> C e. P )
66 simplr 
 |-  ( ( ( ( ( ph /\ z e. P ) /\ ( B e. ( A I z ) /\ ( A .- z ) = ( C .- D ) ) ) /\ y e. P ) /\ <" A z B "> ( cgrG ` G ) <" C D y "> ) -> y e. P )
67 56 ad2antrr 
 |-  ( ( ( ( ( ph /\ z e. P ) /\ ( B e. ( A I z ) /\ ( A .- z ) = ( C .- D ) ) ) /\ y e. P ) /\ <" A z B "> ( cgrG ` G ) <" C D y "> ) -> D e. P )
68 simpr 
 |-  ( ( ( ( ( ph /\ z e. P ) /\ ( B e. ( A I z ) /\ ( A .- z ) = ( C .- D ) ) ) /\ y e. P ) /\ <" A z B "> ( cgrG ` G ) <" C D y "> ) -> <" A z B "> ( cgrG ` G ) <" C D y "> )
69 1 2 3 16 61 62 64 63 65 67 66 68 cgr3swap23 
 |-  ( ( ( ( ( ph /\ z e. P ) /\ ( B e. ( A I z ) /\ ( A .- z ) = ( C .- D ) ) ) /\ y e. P ) /\ <" A z B "> ( cgrG ` G ) <" C D y "> ) -> <" A B z "> ( cgrG ` G ) <" C y D "> )
70 simpllr 
 |-  ( ( ( ( ( ph /\ z e. P ) /\ ( B e. ( A I z ) /\ ( A .- z ) = ( C .- D ) ) ) /\ y e. P ) /\ <" A z B "> ( cgrG ` G ) <" C D y "> ) -> ( B e. ( A I z ) /\ ( A .- z ) = ( C .- D ) ) )
71 70 simpld 
 |-  ( ( ( ( ( ph /\ z e. P ) /\ ( B e. ( A I z ) /\ ( A .- z ) = ( C .- D ) ) ) /\ y e. P ) /\ <" A z B "> ( cgrG ` G ) <" C D y "> ) -> B e. ( A I z ) )
72 1 2 3 16 61 62 63 64 65 66 67 69 71 tgbtwnxfr 
 |-  ( ( ( ( ( ph /\ z e. P ) /\ ( B e. ( A I z ) /\ ( A .- z ) = ( C .- D ) ) ) /\ y e. P ) /\ <" A z B "> ( cgrG ` G ) <" C D y "> ) -> y e. ( C I D ) )
73 1 2 3 16 61 62 64 63 65 67 66 68 cgr3simp3 
 |-  ( ( ( ( ( ph /\ z e. P ) /\ ( B e. ( A I z ) /\ ( A .- z ) = ( C .- D ) ) ) /\ y e. P ) /\ <" A z B "> ( cgrG ` G ) <" C D y "> ) -> ( B .- A ) = ( y .- C ) )
74 1 2 3 61 63 62 66 65 73 tgcgrcomlr 
 |-  ( ( ( ( ( ph /\ z e. P ) /\ ( B e. ( A I z ) /\ ( A .- z ) = ( C .- D ) ) ) /\ y e. P ) /\ <" A z B "> ( cgrG ` G ) <" C D y "> ) -> ( A .- B ) = ( C .- y ) )
75 72 74 jca 
 |-  ( ( ( ( ( ph /\ z e. P ) /\ ( B e. ( A I z ) /\ ( A .- z ) = ( C .- D ) ) ) /\ y e. P ) /\ <" A z B "> ( cgrG ` G ) <" C D y "> ) -> ( y e. ( C I D ) /\ ( A .- B ) = ( C .- y ) ) )
76 75 ex 
 |-  ( ( ( ( ph /\ z e. P ) /\ ( B e. ( A I z ) /\ ( A .- z ) = ( C .- D ) ) ) /\ y e. P ) -> ( <" A z B "> ( cgrG ` G ) <" C D y "> -> ( y e. ( C I D ) /\ ( A .- B ) = ( C .- y ) ) ) )
77 76 reximdva 
 |-  ( ( ( ph /\ z e. P ) /\ ( B e. ( A I z ) /\ ( A .- z ) = ( C .- D ) ) ) -> ( E. y e. P <" A z B "> ( cgrG ` G ) <" C D y "> -> E. y e. P ( y e. ( C I D ) /\ ( A .- B ) = ( C .- y ) ) ) )
78 60 77 mpd 
 |-  ( ( ( ph /\ z e. P ) /\ ( B e. ( A I z ) /\ ( A .- z ) = ( C .- D ) ) ) -> E. y e. P ( y e. ( C I D ) /\ ( A .- B ) = ( C .- y ) ) )
79 78 adantllr 
 |-  ( ( ( ( ph /\ E. x e. P ( B e. ( A I x ) /\ ( A .- x ) = ( C .- D ) ) ) /\ z e. P ) /\ ( B e. ( A I z ) /\ ( A .- z ) = ( C .- D ) ) ) -> E. y e. P ( y e. ( C I D ) /\ ( A .- B ) = ( C .- y ) ) )
80 simpr 
 |-  ( ( ph /\ E. x e. P ( B e. ( A I x ) /\ ( A .- x ) = ( C .- D ) ) ) -> E. x e. P ( B e. ( A I x ) /\ ( A .- x ) = ( C .- D ) ) )
81 oveq2 
 |-  ( x = z -> ( A I x ) = ( A I z ) )
82 81 eleq2d 
 |-  ( x = z -> ( B e. ( A I x ) <-> B e. ( A I z ) ) )
83 oveq2 
 |-  ( x = z -> ( A .- x ) = ( A .- z ) )
84 83 eqeq1d 
 |-  ( x = z -> ( ( A .- x ) = ( C .- D ) <-> ( A .- z ) = ( C .- D ) ) )
85 82 84 anbi12d 
 |-  ( x = z -> ( ( B e. ( A I x ) /\ ( A .- x ) = ( C .- D ) ) <-> ( B e. ( A I z ) /\ ( A .- z ) = ( C .- D ) ) ) )
86 85 cbvrexvw 
 |-  ( E. x e. P ( B e. ( A I x ) /\ ( A .- x ) = ( C .- D ) ) <-> E. z e. P ( B e. ( A I z ) /\ ( A .- z ) = ( C .- D ) ) )
87 80 86 sylib 
 |-  ( ( ph /\ E. x e. P ( B e. ( A I x ) /\ ( A .- x ) = ( C .- D ) ) ) -> E. z e. P ( B e. ( A I z ) /\ ( A .- z ) = ( C .- D ) ) )
88 79 87 r19.29a 
 |-  ( ( ph /\ E. x e. P ( B e. ( A I x ) /\ ( A .- x ) = ( C .- D ) ) ) -> E. y e. P ( y e. ( C I D ) /\ ( A .- B ) = ( C .- y ) ) )
89 50 88 impbida 
 |-  ( ph -> ( E. y e. P ( y e. ( C I D ) /\ ( A .- B ) = ( C .- y ) ) <-> E. x e. P ( B e. ( A I x ) /\ ( A .- x ) = ( C .- D ) ) ) )
90 10 89 bitrd 
 |-  ( ph -> ( ( A .- B ) .<_ ( C .- D ) <-> E. x e. P ( B e. ( A I x ) /\ ( A .- x ) = ( C .- D ) ) ) )