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 eleq1 
 |-  ( y = z -> ( y e. ( C I D ) <-> z e. ( C I D ) ) )
44 oveq2 
 |-  ( y = z -> ( C .- y ) = ( C .- z ) )
45 44 eqeq2d 
 |-  ( y = z -> ( ( A .- B ) = ( C .- y ) <-> ( A .- B ) = ( C .- z ) ) )
46 43 45 anbi12d 
 |-  ( y = z -> ( ( y e. ( C I D ) /\ ( A .- B ) = ( C .- y ) ) <-> ( z e. ( C I D ) /\ ( A .- B ) = ( C .- z ) ) ) )
47 46 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 ) ) )
48 47 bilani 
 |-  ( ( 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 ) ) )
49 42 48 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 ) ) )
50 5 ad2antrr 
 |-  ( ( ( ph /\ z e. P ) /\ ( B e. ( A I z ) /\ ( A .- z ) = ( C .- D ) ) ) -> G e. TarskiG )
51 6 ad2antrr 
 |-  ( ( ( ph /\ z e. P ) /\ ( B e. ( A I z ) /\ ( A .- z ) = ( C .- D ) ) ) -> A e. P )
52 simplr 
 |-  ( ( ( ph /\ z e. P ) /\ ( B e. ( A I z ) /\ ( A .- z ) = ( C .- D ) ) ) -> z e. P )
53 7 ad2antrr 
 |-  ( ( ( ph /\ z e. P ) /\ ( B e. ( A I z ) /\ ( A .- z ) = ( C .- D ) ) ) -> B e. P )
54 8 ad2antrr 
 |-  ( ( ( ph /\ z e. P ) /\ ( B e. ( A I z ) /\ ( A .- z ) = ( C .- D ) ) ) -> C e. P )
55 9 ad2antrr 
 |-  ( ( ( ph /\ z e. P ) /\ ( B e. ( A I z ) /\ ( A .- z ) = ( C .- D ) ) ) -> D e. P )
56 simprl 
 |-  ( ( ( ph /\ z e. P ) /\ ( B e. ( A I z ) /\ ( A .- z ) = ( C .- D ) ) ) -> B e. ( A I z ) )
57 1 11 3 50 51 53 52 56 btwncolg3 
 |-  ( ( ( ph /\ z e. P ) /\ ( B e. ( A I z ) /\ ( A .- z ) = ( C .- D ) ) ) -> ( z e. ( A ( LineG ` G ) B ) \/ A = B ) )
58 simprr 
 |-  ( ( ( ph /\ z e. P ) /\ ( B e. ( A I z ) /\ ( A .- z ) = ( C .- D ) ) ) -> ( A .- z ) = ( C .- D ) )
59 1 11 3 50 51 52 53 16 54 55 2 57 58 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 "> )
60 50 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 )
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 "> ) -> A e. P )
62 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 "> ) -> B e. P )
63 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 "> ) -> z e. P )
64 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 "> ) -> C e. P )
65 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 )
66 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 "> ) -> D e. P )
67 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 "> )
68 1 2 3 16 60 61 63 62 64 66 65 67 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 "> )
69 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 ) ) )
70 69 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 ) )
71 1 2 3 16 60 61 62 63 64 65 66 68 70 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 ) )
72 1 2 3 16 60 61 63 62 64 66 65 67 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 ) )
73 1 2 3 60 62 61 65 64 72 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 ) )
74 71 73 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 ) ) )
75 74 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 ) ) ) )
76 75 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 ) ) ) )
77 59 76 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 ) ) )
78 77 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 ) ) )
79 oveq2 
 |-  ( x = z -> ( A I x ) = ( A I z ) )
80 79 eleq2d 
 |-  ( x = z -> ( B e. ( A I x ) <-> B e. ( A I z ) ) )
81 oveq2 
 |-  ( x = z -> ( A .- x ) = ( A .- z ) )
82 81 eqeq1d 
 |-  ( x = z -> ( ( A .- x ) = ( C .- D ) <-> ( A .- z ) = ( C .- D ) ) )
83 80 82 anbi12d 
 |-  ( x = z -> ( ( B e. ( A I x ) /\ ( A .- x ) = ( C .- D ) ) <-> ( B e. ( A I z ) /\ ( A .- z ) = ( C .- D ) ) ) )
84 83 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 ) ) )
85 84 bilani 
 |-  ( ( 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 ) ) )
86 78 85 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 ) ) )
87 49 86 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 ) ) ) )
88 10 87 bitrd 
 |-  ( ph -> ( ( A .- B ) .<_ ( C .- D ) <-> E. x e. P ( B e. ( A I x ) /\ ( A .- x ) = ( C .- D ) ) ) )