Metamath Proof Explorer

Theorem legov

Description: Value of the less-than relationship. Definition 5.4 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 legov 
|- ( ph -> ( ( A .- B ) .<_ ( C .- D ) <-> E. z e. P ( z e. ( C I D ) /\ ( A .- B ) = ( C .- z ) ) ) )

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 legval 
 |-  ( ph -> .<_ = { <. e , f >. | E. x e. P E. y e. P ( f = ( x .- y ) /\ E. z e. P ( z e. ( x I y ) /\ e = ( x .- z ) ) ) } )
11 10 breqd 
 |-  ( ph -> ( ( A .- B ) .<_ ( C .- D ) <-> ( A .- B ) { <. e , f >. | E. x e. P E. y e. P ( f = ( x .- y ) /\ E. z e. P ( z e. ( x I y ) /\ e = ( x .- z ) ) ) } ( C .- D ) ) )
12 ovex 
 |-  ( A .- B ) e. _V
13 ovex 
 |-  ( C .- D ) e. _V
14 simpr 
 |-  ( ( e = ( A .- B ) /\ f = ( C .- D ) ) -> f = ( C .- D ) )
15 14 eqeq1d 
 |-  ( ( e = ( A .- B ) /\ f = ( C .- D ) ) -> ( f = ( x .- y ) <-> ( C .- D ) = ( x .- y ) ) )
16 simpl 
 |-  ( ( e = ( A .- B ) /\ f = ( C .- D ) ) -> e = ( A .- B ) )
17 16 eqeq1d 
 |-  ( ( e = ( A .- B ) /\ f = ( C .- D ) ) -> ( e = ( x .- z ) <-> ( A .- B ) = ( x .- z ) ) )
18 17 anbi2d 
 |-  ( ( e = ( A .- B ) /\ f = ( C .- D ) ) -> ( ( z e. ( x I y ) /\ e = ( x .- z ) ) <-> ( z e. ( x I y ) /\ ( A .- B ) = ( x .- z ) ) ) )
19 18 rexbidv 
 |-  ( ( e = ( A .- B ) /\ f = ( C .- D ) ) -> ( E. z e. P ( z e. ( x I y ) /\ e = ( x .- z ) ) <-> E. z e. P ( z e. ( x I y ) /\ ( A .- B ) = ( x .- z ) ) ) )
20 15 19 anbi12d 
 |-  ( ( e = ( A .- B ) /\ f = ( C .- D ) ) -> ( ( f = ( x .- y ) /\ E. z e. P ( z e. ( x I y ) /\ e = ( x .- z ) ) ) <-> ( ( C .- D ) = ( x .- y ) /\ E. z e. P ( z e. ( x I y ) /\ ( A .- B ) = ( x .- z ) ) ) ) )
21 20 2rexbidv 
 |-  ( ( e = ( A .- B ) /\ f = ( C .- D ) ) -> ( E. x e. P E. y e. P ( f = ( x .- y ) /\ E. z e. P ( z e. ( x I y ) /\ e = ( x .- z ) ) ) <-> E. x e. P E. y e. P ( ( C .- D ) = ( x .- y ) /\ E. z e. P ( z e. ( x I y ) /\ ( A .- B ) = ( x .- z ) ) ) ) )
22 eqid 
 |-  { <. e , f >. | E. x e. P E. y e. P ( f = ( x .- y ) /\ E. z e. P ( z e. ( x I y ) /\ e = ( x .- z ) ) ) } = { <. e , f >. | E. x e. P E. y e. P ( f = ( x .- y ) /\ E. z e. P ( z e. ( x I y ) /\ e = ( x .- z ) ) ) }
23 12 13 21 22 braba 
 |-  ( ( A .- B ) { <. e , f >. | E. x e. P E. y e. P ( f = ( x .- y ) /\ E. z e. P ( z e. ( x I y ) /\ e = ( x .- z ) ) ) } ( C .- D ) <-> E. x e. P E. y e. P ( ( C .- D ) = ( x .- y ) /\ E. z e. P ( z e. ( x I y ) /\ ( A .- B ) = ( x .- z ) ) ) )
24 11 23 bitrdi 
 |-  ( ph -> ( ( A .- B ) .<_ ( C .- D ) <-> E. x e. P E. y e. P ( ( C .- D ) = ( x .- y ) /\ E. z e. P ( z e. ( x I y ) /\ ( A .- B ) = ( x .- z ) ) ) ) )
25 anass 
 |-  ( ( ( ( ( ph /\ c e. P ) /\ d e. P ) /\ ( C .- D ) = ( c .- d ) ) /\ E. z e. P ( z e. ( c I d ) /\ ( A .- B ) = ( c .- z ) ) ) <-> ( ( ( ph /\ c e. P ) /\ d e. P ) /\ ( ( C .- D ) = ( c .- d ) /\ E. z e. P ( z e. ( c I d ) /\ ( A .- B ) = ( c .- z ) ) ) ) )
26 25 anbi1i 
 |-  ( ( ( ( ( ( ph /\ c e. P ) /\ d e. P ) /\ ( C .- D ) = ( c .- d ) ) /\ E. z e. P ( z e. ( c I d ) /\ ( A .- B ) = ( c .- z ) ) ) /\ x e. P ) <-> ( ( ( ( ph /\ c e. P ) /\ d e. P ) /\ ( ( C .- D ) = ( c .- d ) /\ E. z e. P ( z e. ( c I d ) /\ ( A .- B ) = ( c .- z ) ) ) ) /\ x e. P ) )
27 eqid 
 |-  ( cgrG ` G ) = ( cgrG ` G )
28 5 ad5antr 
 |-  ( ( ( ( ( ( ph /\ c e. P ) /\ d e. P ) /\ ( C .- D ) = ( c .- d ) ) /\ x e. P ) /\ ( x e. ( c I d ) /\ ( A .- B ) = ( c .- x ) ) ) -> G e. TarskiG )
29 28 adantr 
 |-  ( ( ( ( ( ( ( ph /\ c e. P ) /\ d e. P ) /\ ( C .- D ) = ( c .- d ) ) /\ x e. P ) /\ ( x e. ( c I d ) /\ ( A .- B ) = ( c .- x ) ) ) /\ ( z e. P /\ <" c d x "> ( cgrG ` G ) <" C D z "> ) ) -> G e. TarskiG )
30 simp-5r 
 |-  ( ( ( ( ( ( ph /\ c e. P ) /\ d e. P ) /\ ( C .- D ) = ( c .- d ) ) /\ x e. P ) /\ ( x e. ( c I d ) /\ ( A .- B ) = ( c .- x ) ) ) -> c e. P )
31 30 adantr 
 |-  ( ( ( ( ( ( ( ph /\ c e. P ) /\ d e. P ) /\ ( C .- D ) = ( c .- d ) ) /\ x e. P ) /\ ( x e. ( c I d ) /\ ( A .- B ) = ( c .- x ) ) ) /\ ( z e. P /\ <" c d x "> ( cgrG ` G ) <" C D z "> ) ) -> c e. P )
32 simpllr 
 |-  ( ( ( ( ( ( ( ph /\ c e. P ) /\ d e. P ) /\ ( C .- D ) = ( c .- d ) ) /\ x e. P ) /\ ( x e. ( c I d ) /\ ( A .- B ) = ( c .- x ) ) ) /\ ( z e. P /\ <" c d x "> ( cgrG ` G ) <" C D z "> ) ) -> x e. P )
33 simp-4r 
 |-  ( ( ( ( ( ( ph /\ c e. P ) /\ d e. P ) /\ ( C .- D ) = ( c .- d ) ) /\ x e. P ) /\ ( x e. ( c I d ) /\ ( A .- B ) = ( c .- x ) ) ) -> d e. P )
34 33 adantr 
 |-  ( ( ( ( ( ( ( ph /\ c e. P ) /\ d e. P ) /\ ( C .- D ) = ( c .- d ) ) /\ x e. P ) /\ ( x e. ( c I d ) /\ ( A .- B ) = ( c .- x ) ) ) /\ ( z e. P /\ <" c d x "> ( cgrG ` G ) <" C D z "> ) ) -> d e. P )
35 8 ad5antr 
 |-  ( ( ( ( ( ( ph /\ c e. P ) /\ d e. P ) /\ ( C .- D ) = ( c .- d ) ) /\ x e. P ) /\ ( x e. ( c I d ) /\ ( A .- B ) = ( c .- x ) ) ) -> C e. P )
36 35 adantr 
 |-  ( ( ( ( ( ( ( ph /\ c e. P ) /\ d e. P ) /\ ( C .- D ) = ( c .- d ) ) /\ x e. P ) /\ ( x e. ( c I d ) /\ ( A .- B ) = ( c .- x ) ) ) /\ ( z e. P /\ <" c d x "> ( cgrG ` G ) <" C D z "> ) ) -> C e. P )
37 simprl 
 |-  ( ( ( ( ( ( ( ph /\ c e. P ) /\ d e. P ) /\ ( C .- D ) = ( c .- d ) ) /\ x e. P ) /\ ( x e. ( c I d ) /\ ( A .- B ) = ( c .- x ) ) ) /\ ( z e. P /\ <" c d x "> ( cgrG ` G ) <" C D z "> ) ) -> z e. P )
38 9 ad5antr 
 |-  ( ( ( ( ( ( ph /\ c e. P ) /\ d e. P ) /\ ( C .- D ) = ( c .- d ) ) /\ x e. P ) /\ ( x e. ( c I d ) /\ ( A .- B ) = ( c .- x ) ) ) -> D e. P )
39 38 adantr 
 |-  ( ( ( ( ( ( ( ph /\ c e. P ) /\ d e. P ) /\ ( C .- D ) = ( c .- d ) ) /\ x e. P ) /\ ( x e. ( c I d ) /\ ( A .- B ) = ( c .- x ) ) ) /\ ( z e. P /\ <" c d x "> ( cgrG ` G ) <" C D z "> ) ) -> D e. P )
40 simprr 
 |-  ( ( ( ( ( ( ( ph /\ c e. P ) /\ d e. P ) /\ ( C .- D ) = ( c .- d ) ) /\ x e. P ) /\ ( x e. ( c I d ) /\ ( A .- B ) = ( c .- x ) ) ) /\ ( z e. P /\ <" c d x "> ( cgrG ` G ) <" C D z "> ) ) -> <" c d x "> ( cgrG ` G ) <" C D z "> )
41 1 2 3 27 29 31 34 32 36 39 37 40 cgr3swap23 
 |-  ( ( ( ( ( ( ( ph /\ c e. P ) /\ d e. P ) /\ ( C .- D ) = ( c .- d ) ) /\ x e. P ) /\ ( x e. ( c I d ) /\ ( A .- B ) = ( c .- x ) ) ) /\ ( z e. P /\ <" c d x "> ( cgrG ` G ) <" C D z "> ) ) -> <" c x d "> ( cgrG ` G ) <" C z D "> )
42 simprl 
 |-  ( ( ( ( ( ( ph /\ c e. P ) /\ d e. P ) /\ ( C .- D ) = ( c .- d ) ) /\ x e. P ) /\ ( x e. ( c I d ) /\ ( A .- B ) = ( c .- x ) ) ) -> x e. ( c I d ) )
43 42 adantr 
 |-  ( ( ( ( ( ( ( ph /\ c e. P ) /\ d e. P ) /\ ( C .- D ) = ( c .- d ) ) /\ x e. P ) /\ ( x e. ( c I d ) /\ ( A .- B ) = ( c .- x ) ) ) /\ ( z e. P /\ <" c d x "> ( cgrG ` G ) <" C D z "> ) ) -> x e. ( c I d ) )
44 1 2 3 27 29 31 32 34 36 37 39 41 43 tgbtwnxfr 
 |-  ( ( ( ( ( ( ( ph /\ c e. P ) /\ d e. P ) /\ ( C .- D ) = ( c .- d ) ) /\ x e. P ) /\ ( x e. ( c I d ) /\ ( A .- B ) = ( c .- x ) ) ) /\ ( z e. P /\ <" c d x "> ( cgrG ` G ) <" C D z "> ) ) -> z e. ( C I D ) )
45 simplrr 
 |-  ( ( ( ( ( ( ( ph /\ c e. P ) /\ d e. P ) /\ ( C .- D ) = ( c .- d ) ) /\ x e. P ) /\ ( x e. ( c I d ) /\ ( A .- B ) = ( c .- x ) ) ) /\ ( z e. P /\ <" c d x "> ( cgrG ` G ) <" C D z "> ) ) -> ( A .- B ) = ( c .- x ) )
46 1 2 3 27 29 31 32 34 36 37 39 41 cgr3simp1 
 |-  ( ( ( ( ( ( ( ph /\ c e. P ) /\ d e. P ) /\ ( C .- D ) = ( c .- d ) ) /\ x e. P ) /\ ( x e. ( c I d ) /\ ( A .- B ) = ( c .- x ) ) ) /\ ( z e. P /\ <" c d x "> ( cgrG ` G ) <" C D z "> ) ) -> ( c .- x ) = ( C .- z ) )
47 45 46 eqtrd 
 |-  ( ( ( ( ( ( ( ph /\ c e. P ) /\ d e. P ) /\ ( C .- D ) = ( c .- d ) ) /\ x e. P ) /\ ( x e. ( c I d ) /\ ( A .- B ) = ( c .- x ) ) ) /\ ( z e. P /\ <" c d x "> ( cgrG ` G ) <" C D z "> ) ) -> ( A .- B ) = ( C .- z ) )
48 44 47 jca 
 |-  ( ( ( ( ( ( ( ph /\ c e. P ) /\ d e. P ) /\ ( C .- D ) = ( c .- d ) ) /\ x e. P ) /\ ( x e. ( c I d ) /\ ( A .- B ) = ( c .- x ) ) ) /\ ( z e. P /\ <" c d x "> ( cgrG ` G ) <" C D z "> ) ) -> ( z e. ( C I D ) /\ ( A .- B ) = ( C .- z ) ) )
49 eqid 
 |-  ( LineG ` G ) = ( LineG ` G )
50 simplr 
 |-  ( ( ( ( ( ( ph /\ c e. P ) /\ d e. P ) /\ ( C .- D ) = ( c .- d ) ) /\ x e. P ) /\ ( x e. ( c I d ) /\ ( A .- B ) = ( c .- x ) ) ) -> x e. P )
51 1 49 3 28 30 50 33 42 btwncolg3 
 |-  ( ( ( ( ( ( ph /\ c e. P ) /\ d e. P ) /\ ( C .- D ) = ( c .- d ) ) /\ x e. P ) /\ ( x e. ( c I d ) /\ ( A .- B ) = ( c .- x ) ) ) -> ( d e. ( c ( LineG ` G ) x ) \/ c = x ) )
52 simpllr 
 |-  ( ( ( ( ( ( ph /\ c e. P ) /\ d e. P ) /\ ( C .- D ) = ( c .- d ) ) /\ x e. P ) /\ ( x e. ( c I d ) /\ ( A .- B ) = ( c .- x ) ) ) -> ( C .- D ) = ( c .- d ) )
53 52 eqcomd 
 |-  ( ( ( ( ( ( ph /\ c e. P ) /\ d e. P ) /\ ( C .- D ) = ( c .- d ) ) /\ x e. P ) /\ ( x e. ( c I d ) /\ ( A .- B ) = ( c .- x ) ) ) -> ( c .- d ) = ( C .- D ) )
54 1 49 3 28 30 33 50 27 35 38 2 51 53 lnext 
 |-  ( ( ( ( ( ( ph /\ c e. P ) /\ d e. P ) /\ ( C .- D ) = ( c .- d ) ) /\ x e. P ) /\ ( x e. ( c I d ) /\ ( A .- B ) = ( c .- x ) ) ) -> E. z e. P <" c d x "> ( cgrG ` G ) <" C D z "> )
55 48 54 reximddv 
 |-  ( ( ( ( ( ( ph /\ c e. P ) /\ d e. P ) /\ ( C .- D ) = ( c .- d ) ) /\ x e. P ) /\ ( x e. ( c I d ) /\ ( A .- B ) = ( c .- x ) ) ) -> E. z e. P ( z e. ( C I D ) /\ ( A .- B ) = ( C .- z ) ) )
56 55 adantllr 
 |-  ( ( ( ( ( ( ( ph /\ c e. P ) /\ d e. P ) /\ ( C .- D ) = ( c .- d ) ) /\ E. z e. P ( z e. ( c I d ) /\ ( A .- B ) = ( c .- z ) ) ) /\ x e. P ) /\ ( x e. ( c I d ) /\ ( A .- B ) = ( c .- x ) ) ) -> E. z e. P ( z e. ( C I D ) /\ ( A .- B ) = ( C .- z ) ) )
57 26 56 sylanbr 
 |-  ( ( ( ( ( ( ph /\ c e. P ) /\ d e. P ) /\ ( ( C .- D ) = ( c .- d ) /\ E. z e. P ( z e. ( c I d ) /\ ( A .- B ) = ( c .- z ) ) ) ) /\ x e. P ) /\ ( x e. ( c I d ) /\ ( A .- B ) = ( c .- x ) ) ) -> E. z e. P ( z e. ( C I D ) /\ ( A .- B ) = ( C .- z ) ) )
58 simprr 
 |-  ( ( ( ( ph /\ c e. P ) /\ d e. P ) /\ ( ( C .- D ) = ( c .- d ) /\ E. z e. P ( z e. ( c I d ) /\ ( A .- B ) = ( c .- z ) ) ) ) -> E. z e. P ( z e. ( c I d ) /\ ( A .- B ) = ( c .- z ) ) )
59 eleq1w 
 |-  ( x = z -> ( x e. ( c I d ) <-> z e. ( c I d ) ) )
60 oveq2 
 |-  ( x = z -> ( c .- x ) = ( c .- z ) )
61 60 eqeq2d 
 |-  ( x = z -> ( ( A .- B ) = ( c .- x ) <-> ( A .- B ) = ( c .- z ) ) )
62 59 61 anbi12d 
 |-  ( x = z -> ( ( x e. ( c I d ) /\ ( A .- B ) = ( c .- x ) ) <-> ( z e. ( c I d ) /\ ( A .- B ) = ( c .- z ) ) ) )
63 62 cbvrexvw 
 |-  ( E. x e. P ( x e. ( c I d ) /\ ( A .- B ) = ( c .- x ) ) <-> E. z e. P ( z e. ( c I d ) /\ ( A .- B ) = ( c .- z ) ) )
64 58 63 sylibr 
 |-  ( ( ( ( ph /\ c e. P ) /\ d e. P ) /\ ( ( C .- D ) = ( c .- d ) /\ E. z e. P ( z e. ( c I d ) /\ ( A .- B ) = ( c .- z ) ) ) ) -> E. x e. P ( x e. ( c I d ) /\ ( A .- B ) = ( c .- x ) ) )
65 57 64 r19.29a 
 |-  ( ( ( ( ph /\ c e. P ) /\ d e. P ) /\ ( ( C .- D ) = ( c .- d ) /\ E. z e. P ( z e. ( c I d ) /\ ( A .- B ) = ( c .- z ) ) ) ) -> E. z e. P ( z e. ( C I D ) /\ ( A .- B ) = ( C .- z ) ) )
66 65 adantl3r 
 |-  ( ( ( ( ( ph /\ E. x e. P E. y e. P ( ( C .- D ) = ( x .- y ) /\ E. z e. P ( z e. ( x I y ) /\ ( A .- B ) = ( x .- z ) ) ) ) /\ c e. P ) /\ d e. P ) /\ ( ( C .- D ) = ( c .- d ) /\ E. z e. P ( z e. ( c I d ) /\ ( A .- B ) = ( c .- z ) ) ) ) -> E. z e. P ( z e. ( C I D ) /\ ( A .- B ) = ( C .- z ) ) )
67 simpr 
 |-  ( ( ph /\ E. x e. P E. y e. P ( ( C .- D ) = ( x .- y ) /\ E. z e. P ( z e. ( x I y ) /\ ( A .- B ) = ( x .- z ) ) ) ) -> E. x e. P E. y e. P ( ( C .- D ) = ( x .- y ) /\ E. z e. P ( z e. ( x I y ) /\ ( A .- B ) = ( x .- z ) ) ) )
68 oveq1 
 |-  ( c = x -> ( c .- d ) = ( x .- d ) )
69 68 eqeq2d 
 |-  ( c = x -> ( ( C .- D ) = ( c .- d ) <-> ( C .- D ) = ( x .- d ) ) )
70 oveq1 
 |-  ( c = x -> ( c I d ) = ( x I d ) )
71 70 eleq2d 
 |-  ( c = x -> ( z e. ( c I d ) <-> z e. ( x I d ) ) )
72 oveq1 
 |-  ( c = x -> ( c .- z ) = ( x .- z ) )
73 72 eqeq2d 
 |-  ( c = x -> ( ( A .- B ) = ( c .- z ) <-> ( A .- B ) = ( x .- z ) ) )
74 71 73 anbi12d 
 |-  ( c = x -> ( ( z e. ( c I d ) /\ ( A .- B ) = ( c .- z ) ) <-> ( z e. ( x I d ) /\ ( A .- B ) = ( x .- z ) ) ) )
75 74 rexbidv 
 |-  ( c = x -> ( E. z e. P ( z e. ( c I d ) /\ ( A .- B ) = ( c .- z ) ) <-> E. z e. P ( z e. ( x I d ) /\ ( A .- B ) = ( x .- z ) ) ) )
76 69 75 anbi12d 
 |-  ( c = x -> ( ( ( C .- D ) = ( c .- d ) /\ E. z e. P ( z e. ( c I d ) /\ ( A .- B ) = ( c .- z ) ) ) <-> ( ( C .- D ) = ( x .- d ) /\ E. z e. P ( z e. ( x I d ) /\ ( A .- B ) = ( x .- z ) ) ) ) )
77 oveq2 
 |-  ( d = y -> ( x .- d ) = ( x .- y ) )
78 77 eqeq2d 
 |-  ( d = y -> ( ( C .- D ) = ( x .- d ) <-> ( C .- D ) = ( x .- y ) ) )
79 oveq2 
 |-  ( d = y -> ( x I d ) = ( x I y ) )
80 79 eleq2d 
 |-  ( d = y -> ( z e. ( x I d ) <-> z e. ( x I y ) ) )
81 80 anbi1d 
 |-  ( d = y -> ( ( z e. ( x I d ) /\ ( A .- B ) = ( x .- z ) ) <-> ( z e. ( x I y ) /\ ( A .- B ) = ( x .- z ) ) ) )
82 81 rexbidv 
 |-  ( d = y -> ( E. z e. P ( z e. ( x I d ) /\ ( A .- B ) = ( x .- z ) ) <-> E. z e. P ( z e. ( x I y ) /\ ( A .- B ) = ( x .- z ) ) ) )
83 78 82 anbi12d 
 |-  ( d = y -> ( ( ( C .- D ) = ( x .- d ) /\ E. z e. P ( z e. ( x I d ) /\ ( A .- B ) = ( x .- z ) ) ) <-> ( ( C .- D ) = ( x .- y ) /\ E. z e. P ( z e. ( x I y ) /\ ( A .- B ) = ( x .- z ) ) ) ) )
84 76 83 cbvrex2vw 
 |-  ( E. c e. P E. d e. P ( ( C .- D ) = ( c .- d ) /\ E. z e. P ( z e. ( c I d ) /\ ( A .- B ) = ( c .- z ) ) ) <-> E. x e. P E. y e. P ( ( C .- D ) = ( x .- y ) /\ E. z e. P ( z e. ( x I y ) /\ ( A .- B ) = ( x .- z ) ) ) )
85 67 84 sylibr 
 |-  ( ( ph /\ E. x e. P E. y e. P ( ( C .- D ) = ( x .- y ) /\ E. z e. P ( z e. ( x I y ) /\ ( A .- B ) = ( x .- z ) ) ) ) -> E. c e. P E. d e. P ( ( C .- D ) = ( c .- d ) /\ E. z e. P ( z e. ( c I d ) /\ ( A .- B ) = ( c .- z ) ) ) )
86 66 85 r19.29vva 
 |-  ( ( ph /\ E. x e. P E. y e. P ( ( C .- D ) = ( x .- y ) /\ E. z e. P ( z e. ( x I y ) /\ ( A .- B ) = ( x .- z ) ) ) ) -> E. z e. P ( z e. ( C I D ) /\ ( A .- B ) = ( C .- z ) ) )
87 8 adantr 
 |-  ( ( ph /\ E. z e. P ( z e. ( C I D ) /\ ( A .- B ) = ( C .- z ) ) ) -> C e. P )
88 9 adantr 
 |-  ( ( ph /\ E. z e. P ( z e. ( C I D ) /\ ( A .- B ) = ( C .- z ) ) ) -> D e. P )
89 eqidd 
 |-  ( ( ph /\ E. z e. P ( z e. ( C I D ) /\ ( A .- B ) = ( C .- z ) ) ) -> ( C .- D ) = ( C .- D ) )
90 simpr 
 |-  ( ( ph /\ E. z e. P ( z e. ( C I D ) /\ ( A .- B ) = ( C .- z ) ) ) -> E. z e. P ( z e. ( C I D ) /\ ( A .- B ) = ( C .- z ) ) )
91 oveq1 
 |-  ( x = C -> ( x .- y ) = ( C .- y ) )
92 91 eqeq2d 
 |-  ( x = C -> ( ( C .- D ) = ( x .- y ) <-> ( C .- D ) = ( C .- y ) ) )
93 oveq1 
 |-  ( x = C -> ( x I y ) = ( C I y ) )
94 93 eleq2d 
 |-  ( x = C -> ( z e. ( x I y ) <-> z e. ( C I y ) ) )
95 oveq1 
 |-  ( x = C -> ( x .- z ) = ( C .- z ) )
96 95 eqeq2d 
 |-  ( x = C -> ( ( A .- B ) = ( x .- z ) <-> ( A .- B ) = ( C .- z ) ) )
97 94 96 anbi12d 
 |-  ( x = C -> ( ( z e. ( x I y ) /\ ( A .- B ) = ( x .- z ) ) <-> ( z e. ( C I y ) /\ ( A .- B ) = ( C .- z ) ) ) )
98 97 rexbidv 
 |-  ( x = C -> ( E. z e. P ( z e. ( x I y ) /\ ( A .- B ) = ( x .- z ) ) <-> E. z e. P ( z e. ( C I y ) /\ ( A .- B ) = ( C .- z ) ) ) )
99 92 98 anbi12d 
 |-  ( x = C -> ( ( ( C .- D ) = ( x .- y ) /\ E. z e. P ( z e. ( x I y ) /\ ( A .- B ) = ( x .- z ) ) ) <-> ( ( C .- D ) = ( C .- y ) /\ E. z e. P ( z e. ( C I y ) /\ ( A .- B ) = ( C .- z ) ) ) ) )
100 oveq2 
 |-  ( y = D -> ( C .- y ) = ( C .- D ) )
101 100 eqeq2d 
 |-  ( y = D -> ( ( C .- D ) = ( C .- y ) <-> ( C .- D ) = ( C .- D ) ) )
102 oveq2 
 |-  ( y = D -> ( C I y ) = ( C I D ) )
103 102 eleq2d 
 |-  ( y = D -> ( z e. ( C I y ) <-> z e. ( C I D ) ) )
104 103 anbi1d 
 |-  ( y = D -> ( ( z e. ( C I y ) /\ ( A .- B ) = ( C .- z ) ) <-> ( z e. ( C I D ) /\ ( A .- B ) = ( C .- z ) ) ) )
105 104 rexbidv 
 |-  ( y = D -> ( E. z e. P ( z e. ( C I y ) /\ ( A .- B ) = ( C .- z ) ) <-> E. z e. P ( z e. ( C I D ) /\ ( A .- B ) = ( C .- z ) ) ) )
106 101 105 anbi12d 
 |-  ( y = D -> ( ( ( C .- D ) = ( C .- y ) /\ E. z e. P ( z e. ( C I y ) /\ ( A .- B ) = ( C .- z ) ) ) <-> ( ( C .- D ) = ( C .- D ) /\ E. z e. P ( z e. ( C I D ) /\ ( A .- B ) = ( C .- z ) ) ) ) )
107 99 106 rspc2ev 
 |-  ( ( C e. P /\ D e. P /\ ( ( C .- D ) = ( C .- D ) /\ E. z e. P ( z e. ( C I D ) /\ ( A .- B ) = ( C .- z ) ) ) ) -> E. x e. P E. y e. P ( ( C .- D ) = ( x .- y ) /\ E. z e. P ( z e. ( x I y ) /\ ( A .- B ) = ( x .- z ) ) ) )
108 87 88 89 90 107 syl112anc 
 |-  ( ( ph /\ E. z e. P ( z e. ( C I D ) /\ ( A .- B ) = ( C .- z ) ) ) -> E. x e. P E. y e. P ( ( C .- D ) = ( x .- y ) /\ E. z e. P ( z e. ( x I y ) /\ ( A .- B ) = ( x .- z ) ) ) )
109 86 108 impbida 
 |-  ( ph -> ( E. x e. P E. y e. P ( ( C .- D ) = ( x .- y ) /\ E. z e. P ( z e. ( x I y ) /\ ( A .- B ) = ( x .- z ) ) ) <-> E. z e. P ( z e. ( C I D ) /\ ( A .- B ) = ( C .- z ) ) ) )
110 24 109 bitrd 
 |-  ( ph -> ( ( A .- B ) .<_ ( C .- D ) <-> E. z e. P ( z e. ( C I D ) /\ ( A .- B ) = ( C .- z ) ) ) )