MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  legov Structured version   Visualization version   Unicode version
Theorem legov 25480
Description: Value of the less-than relationship. Definition 5.4 of [Schwabhauser] p. 41. (Contributed by Thierry Arnoux, 21-Jun-2019.)
Hypotheses
Ref Expression
legval.p |- P = ( Base ` G )
legval.d |- .- = ( dist ` G )
legval.i |- I = (Itv ` G )
legval.l |- .<_ = (≤G ` 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
Ref Expression
legov |- ( ph -> ( ( A .- B ) .<_ ( C .- D ) <-> E. z e. P ( z e. ( C I D ) /\ ( A .- B ) = ( C .- z ) ) ) )
Distinct variable groups:   z, .-   z, A   z, B   z, C   z, D   z, I   z, P   z, G   ph, z
Allowed substitution hint:   .<_ ( z)
Proof of Theorem legov
Dummy variables c d e f x y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 legval.p . . . . 5 |- P = ( Base ` G )
2 legval.d . . . . 5 |- .- = ( dist ` G )
3 legval.i . . . . 5 |- I = (Itv ` G )
4 legval.l . . . . 5 |- .<_ = (≤G ` G )
5 legval.g . . . . 5 |- ( ph -> G e. TarskiG )
61, 2, 3, 4, 5legval 25479 . . . 4 |- ( 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 ) ) ) } )
76breqd 4664 . . 3 |- ( 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 ) ) )
8 ovex 6678 . . . 4 |- ( A .- B ) e. _V
9 ovex 6678 . . . 4 |- ( C .- D ) e. _V
10 simpr 477 . . . . . . 7 |- ( ( e = ( A .- B ) /\ f = ( C .- D ) ) -> f = ( C .- D ) )
1110eqeq1d 2624 . . . . . 6 |- ( ( e = ( A .- B ) /\ f = ( C .- D ) ) -> ( f = ( x .- y ) <-> ( C .- D ) = ( x .- y ) ) )
12 simpl 473 . . . . . . . . 9 |- ( ( e = ( A .- B ) /\ f = ( C .- D ) ) -> e = ( A .- B ) )
1312eqeq1d 2624 . . . . . . . 8 |- ( ( e = ( A .- B ) /\ f = ( C .- D ) ) -> ( e = ( x .- z ) <-> ( A .- B ) = ( x .- z ) ) )
1413anbi2d 740 . . . . . . 7 |- ( ( e = ( A .- B ) /\ f = ( C .- D ) ) -> ( ( z e. ( x I y ) /\ e = ( x .- z ) ) <-> ( z e. ( x I y ) /\ ( A .- B ) = ( x .- z ) ) ) )
1514rexbidv 3052 . . . . . 6 |- ( ( 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 ) ) ) )
1611, 15anbi12d 747 . . . . 5 |- ( ( 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 ) ) ) ) )
17162rexbidv 3057 . . . 4 |- ( ( 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 ) ) ) ) )
18 eqid 2622 . . . 4 |- { <. 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 ) ) ) }
198, 9, 17, 18braba 4992 . . 3 |- ( ( 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 ) ) ) )
207, 19syl6bb 276 . 2 |- ( 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 ) ) ) ) )
21 anass 681 . . . . . . . 8 |- ( ( ( ( ( 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 ) ) ) ) )
2221anbi1i 731 . . . . . . 7 |- ( ( ( ( ( ( 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 ) )
23 eqid 2622 . . . . . . . . . . 11 |- (cgrG ` G ) = (cgrG ` G )
245ad5antr 770 . . . . . . . . . . . 12 |- ( ( ( ( ( ( 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 )
2524adantr 481 . . . . . . . . . . 11 |- ( ( ( ( ( ( ( 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 )
26 simp-5r 809 . . . . . . . . . . . 12 |- ( ( ( ( ( ( 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 )
2726adantr 481 . . . . . . . . . . 11 |- ( ( ( ( ( ( ( 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 )
28 simpllr 799 . . . . . . . . . . 11 |- ( ( ( ( ( ( ( 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 )
29 simp-4r 807 . . . . . . . . . . . 12 |- ( ( ( ( ( ( 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 )
3029adantr 481 . . . . . . . . . . 11 |- ( ( ( ( ( ( ( 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 )
31 legov.c . . . . . . . . . . . . 13 |- ( ph -> C e. P )
3231ad5antr 770 . . . . . . . . . . . 12 |- ( ( ( ( ( ( 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 )
3332adantr 481 . . . . . . . . . . 11 |- ( ( ( ( ( ( ( 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 )
34 simprl 794 . . . . . . . . . . 11 |- ( ( ( ( ( ( ( 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 )
35 legov.d . . . . . . . . . . . . 13 |- ( ph -> D e. P )
3635ad5antr 770 . . . . . . . . . . . 12 |- ( ( ( ( ( ( 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 )
3736adantr 481 . . . . . . . . . . 11 |- ( ( ( ( ( ( ( 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 )
38 simprr 796 . . . . . . . . . . . 12 |- ( ( ( ( ( ( ( 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 "> )
391, 2, 3, 23, 25, 27, 30, 28, 33, 37, 34, 38cgr3swap23 25419 . . . . . . . . . . 11 |- ( ( ( ( ( ( ( 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 "> )
40 simprl 794 . . . . . . . . . . . 12 |- ( ( ( ( ( ( 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 ) )
4140adantr 481 . . . . . . . . . . 11 |- ( ( ( ( ( ( ( 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 ) )
421, 2, 3, 23, 25, 27, 28, 30, 33, 34, 37, 39, 41tgbtwnxfr 25425 . . . . . . . . . 10 |- ( ( ( ( ( ( ( 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 ) )
43 simplrr 801 . . . . . . . . . . 11 |- ( ( ( ( ( ( ( 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 ) )
441, 2, 3, 23, 25, 27, 28, 30, 33, 34, 37, 39cgr3simp1 25415 . . . . . . . . . . 11 |- ( ( ( ( ( ( ( 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 ) )
4543, 44eqtrd 2656 . . . . . . . . . 10 |- ( ( ( ( ( ( ( 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 ) )
4642, 45jca 554 . . . . . . . . 9 |- ( ( ( ( ( ( ( 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 ) ) )
47 eqid 2622 . . . . . . . . . 10 |- (LineG ` G ) = (LineG ` G )
48 simplr 792 . . . . . . . . . 10 |- ( ( ( ( ( ( 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 )
491, 47, 3, 24, 26, 48, 29, 40btwncolg3 25452 . . . . . . . . . 10 |- ( ( ( ( ( ( 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 ) )
50 simpllr 799 . . . . . . . . . . 11 |- ( ( ( ( ( ( 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 ) )
5150eqcomd 2628 . . . . . . . . . 10 |- ( ( ( ( ( ( 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 ) )
521, 47, 3, 24, 26, 29, 48, 23, 32, 36, 2, 49, 51lnext 25462 . . . . . . . . 9 |- ( ( ( ( ( ( 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 "> )
5346, 52reximddv 3018 . . . . . . . 8 |- ( ( ( ( ( ( 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 ) ) )
5453adantllr 755 . . . . . . 7 |- ( ( ( ( ( ( ( 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 ) ) )
5522, 54sylanbr 490 . . . . . 6 |- ( ( ( ( ( ( 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 ) ) )
56 simprr 796 . . . . . . 7 |- ( ( ( ( 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 ) ) )
57 eleq1 2689 . . . . . . . . 9 |- ( x = z -> ( x e. ( c I d ) <-> z e. ( c I d ) ) )
58 oveq2 6658 . . . . . . . . . 10 |- ( x = z -> ( c .- x ) = ( c .- z ) )
5958eqeq2d 2632 . . . . . . . . 9 |- ( x = z -> ( ( A .- B ) = ( c .- x ) <-> ( A .- B ) = ( c .- z ) ) )
6057, 59anbi12d 747 . . . . . . . 8 |- ( x = z -> ( ( x e. ( c I d ) /\ ( A .- B ) = ( c .- x ) ) <-> ( z e. ( c I d ) /\ ( A .- B ) = ( c .- z ) ) ) )
6160cbvrexv 3172 . . . . . . 7 |- ( 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 ) ) )
6256, 61sylibr 224 . . . . . 6 |- ( ( ( ( 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 ) ) )
6355, 62r19.29a 3078 . . . . 5 |- ( ( ( ( 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 ) ) )
6463adantl3r 786 . . . 4 |- ( ( ( ( ( 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 ) ) )
65 simpr 477 . . . . 5 |- ( ( 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 ) ) ) )
66 oveq1 6657 . . . . . . . 8 |- ( c = x -> ( c .- d ) = ( x .- d ) )
6766eqeq2d 2632 . . . . . . 7 |- ( c = x -> ( ( C .- D ) = ( c .- d ) <-> ( C .- D ) = ( x .- d ) ) )
68 oveq1 6657 . . . . . . . . . 10 |- ( c = x -> ( c I d ) = ( x I d ) )
6968eleq2d 2687 . . . . . . . . 9 |- ( c = x -> ( z e. ( c I d ) <-> z e. ( x I d ) ) )
70 oveq1 6657 . . . . . . . . . 10 |- ( c = x -> ( c .- z ) = ( x .- z ) )
7170eqeq2d 2632 . . . . . . . . 9 |- ( c = x -> ( ( A .- B ) = ( c .- z ) <-> ( A .- B ) = ( x .- z ) ) )
7269, 71anbi12d 747 . . . . . . . 8 |- ( c = x -> ( ( z e. ( c I d ) /\ ( A .- B ) = ( c .- z ) ) <-> ( z e. ( x I d ) /\ ( A .- B ) = ( x .- z ) ) ) )
7372rexbidv 3052 . . . . . . 7 |- ( 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 ) ) ) )
7467, 73anbi12d 747 . . . . . 6 |- ( 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 ) ) ) ) )
75 oveq2 6658 . . . . . . . 8 |- ( d = y -> ( x .- d ) = ( x .- y ) )
7675eqeq2d 2632 . . . . . . 7 |- ( d = y -> ( ( C .- D ) = ( x .- d ) <-> ( C .- D ) = ( x .- y ) ) )
77 oveq2 6658 . . . . . . . . . 10 |- ( d = y -> ( x I d ) = ( x I y ) )
7877eleq2d 2687 . . . . . . . . 9 |- ( d = y -> ( z e. ( x I d ) <-> z e. ( x I y ) ) )
7978anbi1d 741 . . . . . . . 8 |- ( d = y -> ( ( z e. ( x I d ) /\ ( A .- B ) = ( x .- z ) ) <-> ( z e. ( x I y ) /\ ( A .- B ) = ( x .- z ) ) ) )
8079rexbidv 3052 . . . . . . 7 |- ( 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 ) ) ) )
8176, 80anbi12d 747 . . . . . 6 |- ( 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 ) ) ) ) )
8274, 81cbvrex2v 3180 . . . . 5 |- ( 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 ) ) ) )
8365, 82sylibr 224 . . . 4 |- ( ( 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 ) ) ) )
8464, 83r19.29vva 3081 . . 3 |- ( ( 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 ) ) )
8531adantr 481 . . . 4 |- ( ( ph /\ E. z e. P ( z e. ( C I D ) /\ ( A .- B ) = ( C .- z ) ) ) -> C e. P )
8635adantr 481 . . . 4 |- ( ( ph /\ E. z e. P ( z e. ( C I D ) /\ ( A .- B ) = ( C .- z ) ) ) -> D e. P )
87 eqidd 2623 . . . 4 |- ( ( ph /\ E. z e. P ( z e. ( C I D ) /\ ( A .- B ) = ( C .- z ) ) ) -> ( C .- D ) = ( C .- D ) )
88 simpr 477 . . . 4 |- ( ( 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 ) ) )
89 oveq1 6657 . . . . . . 7 |- ( x = C -> ( x .- y ) = ( C .- y ) )
9089eqeq2d 2632 . . . . . 6 |- ( x = C -> ( ( C .- D ) = ( x .- y ) <-> ( C .- D ) = ( C .- y ) ) )
91 oveq1 6657 . . . . . . . . 9 |- ( x = C -> ( x I y ) = ( C I y ) )
9291eleq2d 2687 . . . . . . . 8 |- ( x = C -> ( z e. ( x I y ) <-> z e. ( C I y ) ) )
93 oveq1 6657 . . . . . . . . 9 |- ( x = C -> ( x .- z ) = ( C .- z ) )
9493eqeq2d 2632 . . . . . . . 8 |- ( x = C -> ( ( A .- B ) = ( x .- z ) <-> ( A .- B ) = ( C .- z ) ) )
9592, 94anbi12d 747 . . . . . . 7 |- ( x = C -> ( ( z e. ( x I y ) /\ ( A .- B ) = ( x .- z ) ) <-> ( z e. ( C I y ) /\ ( A .- B ) = ( C .- z ) ) ) )
9695rexbidv 3052 . . . . . 6 |- ( 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 ) ) ) )
9790, 96anbi12d 747 . . . . 5 |- ( 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 ) ) ) ) )
98 oveq2 6658 . . . . . . 7 |- ( y = D -> ( C .- y ) = ( C .- D ) )
9998eqeq2d 2632 . . . . . 6 |- ( y = D -> ( ( C .- D ) = ( C .- y ) <-> ( C .- D ) = ( C .- D ) ) )
100 oveq2 6658 . . . . . . . . 9 |- ( y = D -> ( C I y ) = ( C I D ) )
101100eleq2d 2687 . . . . . . . 8 |- ( y = D -> ( z e. ( C I y ) <-> z e. ( C I D ) ) )
102101anbi1d 741 . . . . . . 7 |- ( y = D -> ( ( z e. ( C I y ) /\ ( A .- B ) = ( C .- z ) ) <-> ( z e. ( C I D ) /\ ( A .- B ) = ( C .- z ) ) ) )
103102rexbidv 3052 . . . . . 6 |- ( 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 ) ) ) )
10499, 103anbi12d 747 . . . . 5 |- ( 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 ) ) ) ) )
10597, 104rspc2ev 3324 . . . 4 |- ( ( 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 ) ) ) )
10685, 86, 87, 88, 105syl112anc 1330 . . 3 |- ( ( 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 ) ) ) )
10784, 106impbida 877 . 2 |- ( 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 ) ) ) )
10820, 107bitrd 268 1 |- ( ph -> ( ( A .- B ) .<_ ( C .- D ) <-> E. z e. P ( z e. ( C I D ) /\ ( A .- B ) = ( C .- z ) ) ) )
Colors of variables: wff setvar class
Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384   = wceq 1483   e. wcel 1990   E.wrex 2913   class class class wbr 4653   {copab 4712   ` cfv 5888  (class class class)co 6650   <"cs3 13587   Basecbs 15857   distcds 15950  TarskiGcstrkg 25329  Itvcitv 25335  LineGclng 25336  cgrGccgrg 25405  ≤Gcleg 25477
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-cnex 9992  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-mulcom 10000  ax-addass 10001  ax-mulass 10002  ax-distr 10003  ax-i2m1 10004  ax-1ne0 10005  ax-1rid 10006  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009  ax-pre-lttri 10010  ax-pre-lttrn 10011  ax-pre-ltadd 10012  ax-pre-mulgt0 10013
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-int 4476  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-om 7066  df-1st 7168  df-2nd 7169  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-1o 7560  df-oadd 7564  df-er 7742  df-pm 7860  df-en 7956  df-dom 7957  df-sdom 7958  df-fin 7959  df-card 8765  df-cda 8990  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080  df-sub 10268  df-neg 10269  df-nn 11021  df-2 11079  df-3 11080  df-n0 11293  df-xnn0 11364  df-z 11378  df-uz 11688  df-fz 12327  df-fzo 12466  df-hash 13118  df-word 13299  df-concat 13301  df-s1 13302  df-s2 13593  df-s3 13594  df-trkgc 25347  df-trkgb 25348  df-trkgcb 25349  df-trkg 25352  df-cgrg 25406  df-leg 25478
This theorem is referenced by:  legov2  25481  legid  25482  btwnleg  25483  legtrd  25484  legtri3  25485  legtrid  25486  leg0  25487  mideulem  25628  opphllem3  25641
  Copyright terms: Public domain W3C validator