Metamath Proof Explorer

Theorem constrcbvlem

Description: Technical lemma for eliminating the hypothesis of constr0 and co. (Contributed by Thierry Arnoux, 2-Nov-2025)

Ref Expression
Assertion constrcbvlem 
|- rec ( ( z e. _V |-> { y e. CC | ( E. i e. z E. j e. z E. k e. z E. l e. z E. o e. RR E. p e. RR ( y = ( i + ( o x. ( j - i ) ) ) /\ y = ( k + ( p x. ( l - k ) ) ) /\ ( Im ` ( ( * ` ( j - i ) ) x. ( l - k ) ) ) =/= 0 ) \/ E. i e. z E. j e. z E. k e. z E. m e. z E. q e. z E. o e. RR ( y = ( i + ( o x. ( j - i ) ) ) /\ ( abs ` ( y - k ) ) = ( abs ` ( m - q ) ) ) \/ E. i e. z E. j e. z E. k e. z E. l e. z E. m e. z E. q e. z ( i =/= l /\ ( abs ` ( y - i ) ) = ( abs ` ( j - k ) ) /\ ( abs ` ( y - l ) ) = ( abs ` ( m - q ) ) ) ) } ) , { 0 , 1 } ) = rec ( ( s e. _V |-> { x e. CC | ( E. a e. s E. b e. s E. c e. s E. d e. s E. t e. RR E. r e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ x = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) \/ E. a e. s E. b e. s E. c e. s E. e e. s E. f e. s E. t e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) \/ E. a e. s E. b e. s E. c e. s E. d e. s E. e e. s E. f e. s ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) } ) , { 0 , 1 } )

Proof

Step Hyp Ref Expression
1 oveq1 
 |-  ( o = t -> ( o x. ( j - i ) ) = ( t x. ( j - i ) ) )
2 1 oveq2d 
 |-  ( o = t -> ( i + ( o x. ( j - i ) ) ) = ( i + ( t x. ( j - i ) ) ) )
3 2 eqeq2d 
 |-  ( o = t -> ( y = ( i + ( o x. ( j - i ) ) ) <-> y = ( i + ( t x. ( j - i ) ) ) ) )
4 3 3anbi1d 
 |-  ( o = t -> ( ( y = ( i + ( o x. ( j - i ) ) ) /\ y = ( k + ( p x. ( l - k ) ) ) /\ ( Im ` ( ( * ` ( j - i ) ) x. ( l - k ) ) ) =/= 0 ) <-> ( y = ( i + ( t x. ( j - i ) ) ) /\ y = ( k + ( p x. ( l - k ) ) ) /\ ( Im ` ( ( * ` ( j - i ) ) x. ( l - k ) ) ) =/= 0 ) ) )
5 oveq1 
 |-  ( p = r -> ( p x. ( l - k ) ) = ( r x. ( l - k ) ) )
6 5 oveq2d 
 |-  ( p = r -> ( k + ( p x. ( l - k ) ) ) = ( k + ( r x. ( l - k ) ) ) )
7 6 eqeq2d 
 |-  ( p = r -> ( y = ( k + ( p x. ( l - k ) ) ) <-> y = ( k + ( r x. ( l - k ) ) ) ) )
8 7 3anbi2d 
 |-  ( p = r -> ( ( y = ( i + ( t x. ( j - i ) ) ) /\ y = ( k + ( p x. ( l - k ) ) ) /\ ( Im ` ( ( * ` ( j - i ) ) x. ( l - k ) ) ) =/= 0 ) <-> ( y = ( i + ( t x. ( j - i ) ) ) /\ y = ( k + ( r x. ( l - k ) ) ) /\ ( Im ` ( ( * ` ( j - i ) ) x. ( l - k ) ) ) =/= 0 ) ) )
9 4 8 cbvrex2vw 
 |-  ( E. o e. RR E. p e. RR ( y = ( i + ( o x. ( j - i ) ) ) /\ y = ( k + ( p x. ( l - k ) ) ) /\ ( Im ` ( ( * ` ( j - i ) ) x. ( l - k ) ) ) =/= 0 ) <-> E. t e. RR E. r e. RR ( y = ( i + ( t x. ( j - i ) ) ) /\ y = ( k + ( r x. ( l - k ) ) ) /\ ( Im ` ( ( * ` ( j - i ) ) x. ( l - k ) ) ) =/= 0 ) )
10 9 2rexbii 
 |-  ( E. k e. z E. l e. z E. o e. RR E. p e. RR ( y = ( i + ( o x. ( j - i ) ) ) /\ y = ( k + ( p x. ( l - k ) ) ) /\ ( Im ` ( ( * ` ( j - i ) ) x. ( l - k ) ) ) =/= 0 ) <-> E. k e. z E. l e. z E. t e. RR E. r e. RR ( y = ( i + ( t x. ( j - i ) ) ) /\ y = ( k + ( r x. ( l - k ) ) ) /\ ( Im ` ( ( * ` ( j - i ) ) x. ( l - k ) ) ) =/= 0 ) )
11 id 
 |-  ( k = c -> k = c )
12 oveq2 
 |-  ( k = c -> ( l - k ) = ( l - c ) )
13 12 oveq2d 
 |-  ( k = c -> ( r x. ( l - k ) ) = ( r x. ( l - c ) ) )
14 11 13 oveq12d 
 |-  ( k = c -> ( k + ( r x. ( l - k ) ) ) = ( c + ( r x. ( l - c ) ) ) )
15 14 eqeq2d 
 |-  ( k = c -> ( y = ( k + ( r x. ( l - k ) ) ) <-> y = ( c + ( r x. ( l - c ) ) ) ) )
16 12 oveq2d 
 |-  ( k = c -> ( ( * ` ( j - i ) ) x. ( l - k ) ) = ( ( * ` ( j - i ) ) x. ( l - c ) ) )
17 16 fveq2d 
 |-  ( k = c -> ( Im ` ( ( * ` ( j - i ) ) x. ( l - k ) ) ) = ( Im ` ( ( * ` ( j - i ) ) x. ( l - c ) ) ) )
18 17 neeq1d 
 |-  ( k = c -> ( ( Im ` ( ( * ` ( j - i ) ) x. ( l - k ) ) ) =/= 0 <-> ( Im ` ( ( * ` ( j - i ) ) x. ( l - c ) ) ) =/= 0 ) )
19 15 18 3anbi23d 
 |-  ( k = c -> ( ( y = ( i + ( t x. ( j - i ) ) ) /\ y = ( k + ( r x. ( l - k ) ) ) /\ ( Im ` ( ( * ` ( j - i ) ) x. ( l - k ) ) ) =/= 0 ) <-> ( y = ( i + ( t x. ( j - i ) ) ) /\ y = ( c + ( r x. ( l - c ) ) ) /\ ( Im ` ( ( * ` ( j - i ) ) x. ( l - c ) ) ) =/= 0 ) ) )
20 19 2rexbidv 
 |-  ( k = c -> ( E. t e. RR E. r e. RR ( y = ( i + ( t x. ( j - i ) ) ) /\ y = ( k + ( r x. ( l - k ) ) ) /\ ( Im ` ( ( * ` ( j - i ) ) x. ( l - k ) ) ) =/= 0 ) <-> E. t e. RR E. r e. RR ( y = ( i + ( t x. ( j - i ) ) ) /\ y = ( c + ( r x. ( l - c ) ) ) /\ ( Im ` ( ( * ` ( j - i ) ) x. ( l - c ) ) ) =/= 0 ) ) )
21 oveq1 
 |-  ( l = d -> ( l - c ) = ( d - c ) )
22 21 oveq2d 
 |-  ( l = d -> ( r x. ( l - c ) ) = ( r x. ( d - c ) ) )
23 22 oveq2d 
 |-  ( l = d -> ( c + ( r x. ( l - c ) ) ) = ( c + ( r x. ( d - c ) ) ) )
24 23 eqeq2d 
 |-  ( l = d -> ( y = ( c + ( r x. ( l - c ) ) ) <-> y = ( c + ( r x. ( d - c ) ) ) ) )
25 21 oveq2d 
 |-  ( l = d -> ( ( * ` ( j - i ) ) x. ( l - c ) ) = ( ( * ` ( j - i ) ) x. ( d - c ) ) )
26 25 fveq2d 
 |-  ( l = d -> ( Im ` ( ( * ` ( j - i ) ) x. ( l - c ) ) ) = ( Im ` ( ( * ` ( j - i ) ) x. ( d - c ) ) ) )
27 26 neeq1d 
 |-  ( l = d -> ( ( Im ` ( ( * ` ( j - i ) ) x. ( l - c ) ) ) =/= 0 <-> ( Im ` ( ( * ` ( j - i ) ) x. ( d - c ) ) ) =/= 0 ) )
28 24 27 3anbi23d 
 |-  ( l = d -> ( ( y = ( i + ( t x. ( j - i ) ) ) /\ y = ( c + ( r x. ( l - c ) ) ) /\ ( Im ` ( ( * ` ( j - i ) ) x. ( l - c ) ) ) =/= 0 ) <-> ( y = ( i + ( t x. ( j - i ) ) ) /\ y = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( j - i ) ) x. ( d - c ) ) ) =/= 0 ) ) )
29 28 2rexbidv 
 |-  ( l = d -> ( E. t e. RR E. r e. RR ( y = ( i + ( t x. ( j - i ) ) ) /\ y = ( c + ( r x. ( l - c ) ) ) /\ ( Im ` ( ( * ` ( j - i ) ) x. ( l - c ) ) ) =/= 0 ) <-> E. t e. RR E. r e. RR ( y = ( i + ( t x. ( j - i ) ) ) /\ y = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( j - i ) ) x. ( d - c ) ) ) =/= 0 ) ) )
30 20 29 cbvrex2vw 
 |-  ( E. k e. z E. l e. z E. t e. RR E. r e. RR ( y = ( i + ( t x. ( j - i ) ) ) /\ y = ( k + ( r x. ( l - k ) ) ) /\ ( Im ` ( ( * ` ( j - i ) ) x. ( l - k ) ) ) =/= 0 ) <-> E. c e. z E. d e. z E. t e. RR E. r e. RR ( y = ( i + ( t x. ( j - i ) ) ) /\ y = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( j - i ) ) x. ( d - c ) ) ) =/= 0 ) )
31 10 30 bitri 
 |-  ( E. k e. z E. l e. z E. o e. RR E. p e. RR ( y = ( i + ( o x. ( j - i ) ) ) /\ y = ( k + ( p x. ( l - k ) ) ) /\ ( Im ` ( ( * ` ( j - i ) ) x. ( l - k ) ) ) =/= 0 ) <-> E. c e. z E. d e. z E. t e. RR E. r e. RR ( y = ( i + ( t x. ( j - i ) ) ) /\ y = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( j - i ) ) x. ( d - c ) ) ) =/= 0 ) )
32 31 2rexbii 
 |-  ( E. i e. z E. j e. z E. k e. z E. l e. z E. o e. RR E. p e. RR ( y = ( i + ( o x. ( j - i ) ) ) /\ y = ( k + ( p x. ( l - k ) ) ) /\ ( Im ` ( ( * ` ( j - i ) ) x. ( l - k ) ) ) =/= 0 ) <-> E. i e. z E. j e. z E. c e. z E. d e. z E. t e. RR E. r e. RR ( y = ( i + ( t x. ( j - i ) ) ) /\ y = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( j - i ) ) x. ( d - c ) ) ) =/= 0 ) )
33 oveq2 
 |-  ( q = f -> ( m - q ) = ( m - f ) )
34 33 fveq2d 
 |-  ( q = f -> ( abs ` ( m - q ) ) = ( abs ` ( m - f ) ) )
35 34 eqeq2d 
 |-  ( q = f -> ( ( abs ` ( y - k ) ) = ( abs ` ( m - q ) ) <-> ( abs ` ( y - k ) ) = ( abs ` ( m - f ) ) ) )
36 35 anbi2d 
 |-  ( q = f -> ( ( y = ( i + ( o x. ( j - i ) ) ) /\ ( abs ` ( y - k ) ) = ( abs ` ( m - q ) ) ) <-> ( y = ( i + ( o x. ( j - i ) ) ) /\ ( abs ` ( y - k ) ) = ( abs ` ( m - f ) ) ) ) )
37 3 anbi1d 
 |-  ( o = t -> ( ( y = ( i + ( o x. ( j - i ) ) ) /\ ( abs ` ( y - k ) ) = ( abs ` ( m - f ) ) ) <-> ( y = ( i + ( t x. ( j - i ) ) ) /\ ( abs ` ( y - k ) ) = ( abs ` ( m - f ) ) ) ) )
38 36 37 cbvrex2vw 
 |-  ( E. q e. z E. o e. RR ( y = ( i + ( o x. ( j - i ) ) ) /\ ( abs ` ( y - k ) ) = ( abs ` ( m - q ) ) ) <-> E. f e. z E. t e. RR ( y = ( i + ( t x. ( j - i ) ) ) /\ ( abs ` ( y - k ) ) = ( abs ` ( m - f ) ) ) )
39 38 2rexbii 
 |-  ( E. k e. z E. m e. z E. q e. z E. o e. RR ( y = ( i + ( o x. ( j - i ) ) ) /\ ( abs ` ( y - k ) ) = ( abs ` ( m - q ) ) ) <-> E. k e. z E. m e. z E. f e. z E. t e. RR ( y = ( i + ( t x. ( j - i ) ) ) /\ ( abs ` ( y - k ) ) = ( abs ` ( m - f ) ) ) )
40 oveq2 
 |-  ( k = c -> ( y - k ) = ( y - c ) )
41 40 fveq2d 
 |-  ( k = c -> ( abs ` ( y - k ) ) = ( abs ` ( y - c ) ) )
42 41 eqeq1d 
 |-  ( k = c -> ( ( abs ` ( y - k ) ) = ( abs ` ( m - f ) ) <-> ( abs ` ( y - c ) ) = ( abs ` ( m - f ) ) ) )
43 42 anbi2d 
 |-  ( k = c -> ( ( y = ( i + ( t x. ( j - i ) ) ) /\ ( abs ` ( y - k ) ) = ( abs ` ( m - f ) ) ) <-> ( y = ( i + ( t x. ( j - i ) ) ) /\ ( abs ` ( y - c ) ) = ( abs ` ( m - f ) ) ) ) )
44 43 2rexbidv 
 |-  ( k = c -> ( E. f e. z E. t e. RR ( y = ( i + ( t x. ( j - i ) ) ) /\ ( abs ` ( y - k ) ) = ( abs ` ( m - f ) ) ) <-> E. f e. z E. t e. RR ( y = ( i + ( t x. ( j - i ) ) ) /\ ( abs ` ( y - c ) ) = ( abs ` ( m - f ) ) ) ) )
45 oveq1 
 |-  ( m = e -> ( m - f ) = ( e - f ) )
46 45 fveq2d 
 |-  ( m = e -> ( abs ` ( m - f ) ) = ( abs ` ( e - f ) ) )
47 46 eqeq2d 
 |-  ( m = e -> ( ( abs ` ( y - c ) ) = ( abs ` ( m - f ) ) <-> ( abs ` ( y - c ) ) = ( abs ` ( e - f ) ) ) )
48 47 anbi2d 
 |-  ( m = e -> ( ( y = ( i + ( t x. ( j - i ) ) ) /\ ( abs ` ( y - c ) ) = ( abs ` ( m - f ) ) ) <-> ( y = ( i + ( t x. ( j - i ) ) ) /\ ( abs ` ( y - c ) ) = ( abs ` ( e - f ) ) ) ) )
49 48 2rexbidv 
 |-  ( m = e -> ( E. f e. z E. t e. RR ( y = ( i + ( t x. ( j - i ) ) ) /\ ( abs ` ( y - c ) ) = ( abs ` ( m - f ) ) ) <-> E. f e. z E. t e. RR ( y = ( i + ( t x. ( j - i ) ) ) /\ ( abs ` ( y - c ) ) = ( abs ` ( e - f ) ) ) ) )
50 44 49 cbvrex2vw 
 |-  ( E. k e. z E. m e. z E. f e. z E. t e. RR ( y = ( i + ( t x. ( j - i ) ) ) /\ ( abs ` ( y - k ) ) = ( abs ` ( m - f ) ) ) <-> E. c e. z E. e e. z E. f e. z E. t e. RR ( y = ( i + ( t x. ( j - i ) ) ) /\ ( abs ` ( y - c ) ) = ( abs ` ( e - f ) ) ) )
51 39 50 bitri 
 |-  ( E. k e. z E. m e. z E. q e. z E. o e. RR ( y = ( i + ( o x. ( j - i ) ) ) /\ ( abs ` ( y - k ) ) = ( abs ` ( m - q ) ) ) <-> E. c e. z E. e e. z E. f e. z E. t e. RR ( y = ( i + ( t x. ( j - i ) ) ) /\ ( abs ` ( y - c ) ) = ( abs ` ( e - f ) ) ) )
52 51 2rexbii 
 |-  ( E. i e. z E. j e. z E. k e. z E. m e. z E. q e. z E. o e. RR ( y = ( i + ( o x. ( j - i ) ) ) /\ ( abs ` ( y - k ) ) = ( abs ` ( m - q ) ) ) <-> E. i e. z E. j e. z E. c e. z E. e e. z E. f e. z E. t e. RR ( y = ( i + ( t x. ( j - i ) ) ) /\ ( abs ` ( y - c ) ) = ( abs ` ( e - f ) ) ) )
53 oveq1 
 |-  ( m = e -> ( m - q ) = ( e - q ) )
54 53 fveq2d 
 |-  ( m = e -> ( abs ` ( m - q ) ) = ( abs ` ( e - q ) ) )
55 54 eqeq2d 
 |-  ( m = e -> ( ( abs ` ( y - l ) ) = ( abs ` ( m - q ) ) <-> ( abs ` ( y - l ) ) = ( abs ` ( e - q ) ) ) )
56 55 3anbi3d 
 |-  ( m = e -> ( ( i =/= l /\ ( abs ` ( y - i ) ) = ( abs ` ( j - k ) ) /\ ( abs ` ( y - l ) ) = ( abs ` ( m - q ) ) ) <-> ( i =/= l /\ ( abs ` ( y - i ) ) = ( abs ` ( j - k ) ) /\ ( abs ` ( y - l ) ) = ( abs ` ( e - q ) ) ) ) )
57 oveq2 
 |-  ( q = f -> ( e - q ) = ( e - f ) )
58 57 fveq2d 
 |-  ( q = f -> ( abs ` ( e - q ) ) = ( abs ` ( e - f ) ) )
59 58 eqeq2d 
 |-  ( q = f -> ( ( abs ` ( y - l ) ) = ( abs ` ( e - q ) ) <-> ( abs ` ( y - l ) ) = ( abs ` ( e - f ) ) ) )
60 59 3anbi3d 
 |-  ( q = f -> ( ( i =/= l /\ ( abs ` ( y - i ) ) = ( abs ` ( j - k ) ) /\ ( abs ` ( y - l ) ) = ( abs ` ( e - q ) ) ) <-> ( i =/= l /\ ( abs ` ( y - i ) ) = ( abs ` ( j - k ) ) /\ ( abs ` ( y - l ) ) = ( abs ` ( e - f ) ) ) ) )
61 56 60 cbvrex2vw 
 |-  ( E. m e. z E. q e. z ( i =/= l /\ ( abs ` ( y - i ) ) = ( abs ` ( j - k ) ) /\ ( abs ` ( y - l ) ) = ( abs ` ( m - q ) ) ) <-> E. e e. z E. f e. z ( i =/= l /\ ( abs ` ( y - i ) ) = ( abs ` ( j - k ) ) /\ ( abs ` ( y - l ) ) = ( abs ` ( e - f ) ) ) )
62 61 2rexbii 
 |-  ( E. k e. z E. l e. z E. m e. z E. q e. z ( i =/= l /\ ( abs ` ( y - i ) ) = ( abs ` ( j - k ) ) /\ ( abs ` ( y - l ) ) = ( abs ` ( m - q ) ) ) <-> E. k e. z E. l e. z E. e e. z E. f e. z ( i =/= l /\ ( abs ` ( y - i ) ) = ( abs ` ( j - k ) ) /\ ( abs ` ( y - l ) ) = ( abs ` ( e - f ) ) ) )
63 oveq2 
 |-  ( k = c -> ( j - k ) = ( j - c ) )
64 63 fveq2d 
 |-  ( k = c -> ( abs ` ( j - k ) ) = ( abs ` ( j - c ) ) )
65 64 eqeq2d 
 |-  ( k = c -> ( ( abs ` ( y - i ) ) = ( abs ` ( j - k ) ) <-> ( abs ` ( y - i ) ) = ( abs ` ( j - c ) ) ) )
66 65 3anbi2d 
 |-  ( k = c -> ( ( i =/= l /\ ( abs ` ( y - i ) ) = ( abs ` ( j - k ) ) /\ ( abs ` ( y - l ) ) = ( abs ` ( e - f ) ) ) <-> ( i =/= l /\ ( abs ` ( y - i ) ) = ( abs ` ( j - c ) ) /\ ( abs ` ( y - l ) ) = ( abs ` ( e - f ) ) ) ) )
67 66 2rexbidv 
 |-  ( k = c -> ( E. e e. z E. f e. z ( i =/= l /\ ( abs ` ( y - i ) ) = ( abs ` ( j - k ) ) /\ ( abs ` ( y - l ) ) = ( abs ` ( e - f ) ) ) <-> E. e e. z E. f e. z ( i =/= l /\ ( abs ` ( y - i ) ) = ( abs ` ( j - c ) ) /\ ( abs ` ( y - l ) ) = ( abs ` ( e - f ) ) ) ) )
68 neeq2 
 |-  ( l = d -> ( i =/= l <-> i =/= d ) )
69 oveq2 
 |-  ( l = d -> ( y - l ) = ( y - d ) )
70 69 fveq2d 
 |-  ( l = d -> ( abs ` ( y - l ) ) = ( abs ` ( y - d ) ) )
71 70 eqeq1d 
 |-  ( l = d -> ( ( abs ` ( y - l ) ) = ( abs ` ( e - f ) ) <-> ( abs ` ( y - d ) ) = ( abs ` ( e - f ) ) ) )
72 68 71 3anbi13d 
 |-  ( l = d -> ( ( i =/= l /\ ( abs ` ( y - i ) ) = ( abs ` ( j - c ) ) /\ ( abs ` ( y - l ) ) = ( abs ` ( e - f ) ) ) <-> ( i =/= d /\ ( abs ` ( y - i ) ) = ( abs ` ( j - c ) ) /\ ( abs ` ( y - d ) ) = ( abs ` ( e - f ) ) ) ) )
73 72 2rexbidv 
 |-  ( l = d -> ( E. e e. z E. f e. z ( i =/= l /\ ( abs ` ( y - i ) ) = ( abs ` ( j - c ) ) /\ ( abs ` ( y - l ) ) = ( abs ` ( e - f ) ) ) <-> E. e e. z E. f e. z ( i =/= d /\ ( abs ` ( y - i ) ) = ( abs ` ( j - c ) ) /\ ( abs ` ( y - d ) ) = ( abs ` ( e - f ) ) ) ) )
74 67 73 cbvrex2vw 
 |-  ( E. k e. z E. l e. z E. e e. z E. f e. z ( i =/= l /\ ( abs ` ( y - i ) ) = ( abs ` ( j - k ) ) /\ ( abs ` ( y - l ) ) = ( abs ` ( e - f ) ) ) <-> E. c e. z E. d e. z E. e e. z E. f e. z ( i =/= d /\ ( abs ` ( y - i ) ) = ( abs ` ( j - c ) ) /\ ( abs ` ( y - d ) ) = ( abs ` ( e - f ) ) ) )
75 62 74 bitri 
 |-  ( E. k e. z E. l e. z E. m e. z E. q e. z ( i =/= l /\ ( abs ` ( y - i ) ) = ( abs ` ( j - k ) ) /\ ( abs ` ( y - l ) ) = ( abs ` ( m - q ) ) ) <-> E. c e. z E. d e. z E. e e. z E. f e. z ( i =/= d /\ ( abs ` ( y - i ) ) = ( abs ` ( j - c ) ) /\ ( abs ` ( y - d ) ) = ( abs ` ( e - f ) ) ) )
76 75 2rexbii 
 |-  ( E. i e. z E. j e. z E. k e. z E. l e. z E. m e. z E. q e. z ( i =/= l /\ ( abs ` ( y - i ) ) = ( abs ` ( j - k ) ) /\ ( abs ` ( y - l ) ) = ( abs ` ( m - q ) ) ) <-> E. i e. z E. j e. z E. c e. z E. d e. z E. e e. z E. f e. z ( i =/= d /\ ( abs ` ( y - i ) ) = ( abs ` ( j - c ) ) /\ ( abs ` ( y - d ) ) = ( abs ` ( e - f ) ) ) )
77 32 52 76 3orbi123i 
 |-  ( ( E. i e. z E. j e. z E. k e. z E. l e. z E. o e. RR E. p e. RR ( y = ( i + ( o x. ( j - i ) ) ) /\ y = ( k + ( p x. ( l - k ) ) ) /\ ( Im ` ( ( * ` ( j - i ) ) x. ( l - k ) ) ) =/= 0 ) \/ E. i e. z E. j e. z E. k e. z E. m e. z E. q e. z E. o e. RR ( y = ( i + ( o x. ( j - i ) ) ) /\ ( abs ` ( y - k ) ) = ( abs ` ( m - q ) ) ) \/ E. i e. z E. j e. z E. k e. z E. l e. z E. m e. z E. q e. z ( i =/= l /\ ( abs ` ( y - i ) ) = ( abs ` ( j - k ) ) /\ ( abs ` ( y - l ) ) = ( abs ` ( m - q ) ) ) ) <-> ( E. i e. z E. j e. z E. c e. z E. d e. z E. t e. RR E. r e. RR ( y = ( i + ( t x. ( j - i ) ) ) /\ y = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( j - i ) ) x. ( d - c ) ) ) =/= 0 ) \/ E. i e. z E. j e. z E. c e. z E. e e. z E. f e. z E. t e. RR ( y = ( i + ( t x. ( j - i ) ) ) /\ ( abs ` ( y - c ) ) = ( abs ` ( e - f ) ) ) \/ E. i e. z E. j e. z E. c e. z E. d e. z E. e e. z E. f e. z ( i =/= d /\ ( abs ` ( y - i ) ) = ( abs ` ( j - c ) ) /\ ( abs ` ( y - d ) ) = ( abs ` ( e - f ) ) ) ) )
78 id 
 |-  ( i = a -> i = a )
79 oveq2 
 |-  ( i = a -> ( j - i ) = ( j - a ) )
80 79 oveq2d 
 |-  ( i = a -> ( t x. ( j - i ) ) = ( t x. ( j - a ) ) )
81 78 80 oveq12d 
 |-  ( i = a -> ( i + ( t x. ( j - i ) ) ) = ( a + ( t x. ( j - a ) ) ) )
82 81 eqeq2d 
 |-  ( i = a -> ( y = ( i + ( t x. ( j - i ) ) ) <-> y = ( a + ( t x. ( j - a ) ) ) ) )
83 79 fveq2d 
 |-  ( i = a -> ( * ` ( j - i ) ) = ( * ` ( j - a ) ) )
84 83 oveq1d 
 |-  ( i = a -> ( ( * ` ( j - i ) ) x. ( d - c ) ) = ( ( * ` ( j - a ) ) x. ( d - c ) ) )
85 84 fveq2d 
 |-  ( i = a -> ( Im ` ( ( * ` ( j - i ) ) x. ( d - c ) ) ) = ( Im ` ( ( * ` ( j - a ) ) x. ( d - c ) ) ) )
86 85 neeq1d 
 |-  ( i = a -> ( ( Im ` ( ( * ` ( j - i ) ) x. ( d - c ) ) ) =/= 0 <-> ( Im ` ( ( * ` ( j - a ) ) x. ( d - c ) ) ) =/= 0 ) )
87 82 86 3anbi13d 
 |-  ( i = a -> ( ( y = ( i + ( t x. ( j - i ) ) ) /\ y = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( j - i ) ) x. ( d - c ) ) ) =/= 0 ) <-> ( y = ( a + ( t x. ( j - a ) ) ) /\ y = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( j - a ) ) x. ( d - c ) ) ) =/= 0 ) ) )
88 87 2rexbidv 
 |-  ( i = a -> ( E. t e. RR E. r e. RR ( y = ( i + ( t x. ( j - i ) ) ) /\ y = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( j - i ) ) x. ( d - c ) ) ) =/= 0 ) <-> E. t e. RR E. r e. RR ( y = ( a + ( t x. ( j - a ) ) ) /\ y = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( j - a ) ) x. ( d - c ) ) ) =/= 0 ) ) )
89 88 2rexbidv 
 |-  ( i = a -> ( E. c e. z E. d e. z E. t e. RR E. r e. RR ( y = ( i + ( t x. ( j - i ) ) ) /\ y = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( j - i ) ) x. ( d - c ) ) ) =/= 0 ) <-> E. c e. z E. d e. z E. t e. RR E. r e. RR ( y = ( a + ( t x. ( j - a ) ) ) /\ y = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( j - a ) ) x. ( d - c ) ) ) =/= 0 ) ) )
90 oveq1 
 |-  ( j = b -> ( j - a ) = ( b - a ) )
91 90 oveq2d 
 |-  ( j = b -> ( t x. ( j - a ) ) = ( t x. ( b - a ) ) )
92 91 oveq2d 
 |-  ( j = b -> ( a + ( t x. ( j - a ) ) ) = ( a + ( t x. ( b - a ) ) ) )
93 92 eqeq2d 
 |-  ( j = b -> ( y = ( a + ( t x. ( j - a ) ) ) <-> y = ( a + ( t x. ( b - a ) ) ) ) )
94 90 fveq2d 
 |-  ( j = b -> ( * ` ( j - a ) ) = ( * ` ( b - a ) ) )
95 94 oveq1d 
 |-  ( j = b -> ( ( * ` ( j - a ) ) x. ( d - c ) ) = ( ( * ` ( b - a ) ) x. ( d - c ) ) )
96 95 fveq2d 
 |-  ( j = b -> ( Im ` ( ( * ` ( j - a ) ) x. ( d - c ) ) ) = ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) )
97 96 neeq1d 
 |-  ( j = b -> ( ( Im ` ( ( * ` ( j - a ) ) x. ( d - c ) ) ) =/= 0 <-> ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) )
98 93 97 3anbi13d 
 |-  ( j = b -> ( ( y = ( a + ( t x. ( j - a ) ) ) /\ y = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( j - a ) ) x. ( d - c ) ) ) =/= 0 ) <-> ( y = ( a + ( t x. ( b - a ) ) ) /\ y = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) ) )
99 98 2rexbidv 
 |-  ( j = b -> ( E. t e. RR E. r e. RR ( y = ( a + ( t x. ( j - a ) ) ) /\ y = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( j - a ) ) x. ( d - c ) ) ) =/= 0 ) <-> E. t e. RR E. r e. RR ( y = ( a + ( t x. ( b - a ) ) ) /\ y = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) ) )
100 99 2rexbidv 
 |-  ( j = b -> ( E. c e. z E. d e. z E. t e. RR E. r e. RR ( y = ( a + ( t x. ( j - a ) ) ) /\ y = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( j - a ) ) x. ( d - c ) ) ) =/= 0 ) <-> E. c e. z E. d e. z E. t e. RR E. r e. RR ( y = ( a + ( t x. ( b - a ) ) ) /\ y = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) ) )
101 89 100 cbvrex2vw 
 |-  ( E. i e. z E. j e. z E. c e. z E. d e. z E. t e. RR E. r e. RR ( y = ( i + ( t x. ( j - i ) ) ) /\ y = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( j - i ) ) x. ( d - c ) ) ) =/= 0 ) <-> E. a e. z E. b e. z E. c e. z E. d e. z E. t e. RR E. r e. RR ( y = ( a + ( t x. ( b - a ) ) ) /\ y = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) )
102 82 anbi1d 
 |-  ( i = a -> ( ( y = ( i + ( t x. ( j - i ) ) ) /\ ( abs ` ( y - c ) ) = ( abs ` ( e - f ) ) ) <-> ( y = ( a + ( t x. ( j - a ) ) ) /\ ( abs ` ( y - c ) ) = ( abs ` ( e - f ) ) ) ) )
103 102 2rexbidv 
 |-  ( i = a -> ( E. f e. z E. t e. RR ( y = ( i + ( t x. ( j - i ) ) ) /\ ( abs ` ( y - c ) ) = ( abs ` ( e - f ) ) ) <-> E. f e. z E. t e. RR ( y = ( a + ( t x. ( j - a ) ) ) /\ ( abs ` ( y - c ) ) = ( abs ` ( e - f ) ) ) ) )
104 103 2rexbidv 
 |-  ( i = a -> ( E. c e. z E. e e. z E. f e. z E. t e. RR ( y = ( i + ( t x. ( j - i ) ) ) /\ ( abs ` ( y - c ) ) = ( abs ` ( e - f ) ) ) <-> E. c e. z E. e e. z E. f e. z E. t e. RR ( y = ( a + ( t x. ( j - a ) ) ) /\ ( abs ` ( y - c ) ) = ( abs ` ( e - f ) ) ) ) )
105 93 anbi1d 
 |-  ( j = b -> ( ( y = ( a + ( t x. ( j - a ) ) ) /\ ( abs ` ( y - c ) ) = ( abs ` ( e - f ) ) ) <-> ( y = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( y - c ) ) = ( abs ` ( e - f ) ) ) ) )
106 105 2rexbidv 
 |-  ( j = b -> ( E. f e. z E. t e. RR ( y = ( a + ( t x. ( j - a ) ) ) /\ ( abs ` ( y - c ) ) = ( abs ` ( e - f ) ) ) <-> E. f e. z E. t e. RR ( y = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( y - c ) ) = ( abs ` ( e - f ) ) ) ) )
107 106 2rexbidv 
 |-  ( j = b -> ( E. c e. z E. e e. z E. f e. z E. t e. RR ( y = ( a + ( t x. ( j - a ) ) ) /\ ( abs ` ( y - c ) ) = ( abs ` ( e - f ) ) ) <-> E. c e. z E. e e. z E. f e. z E. t e. RR ( y = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( y - c ) ) = ( abs ` ( e - f ) ) ) ) )
108 104 107 cbvrex2vw 
 |-  ( E. i e. z E. j e. z E. c e. z E. e e. z E. f e. z E. t e. RR ( y = ( i + ( t x. ( j - i ) ) ) /\ ( abs ` ( y - c ) ) = ( abs ` ( e - f ) ) ) <-> E. a e. z E. b e. z E. c e. z E. e e. z E. f e. z E. t e. RR ( y = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( y - c ) ) = ( abs ` ( e - f ) ) ) )
109 neeq1 
 |-  ( i = a -> ( i =/= d <-> a =/= d ) )
110 oveq2 
 |-  ( i = a -> ( y - i ) = ( y - a ) )
111 110 fveq2d 
 |-  ( i = a -> ( abs ` ( y - i ) ) = ( abs ` ( y - a ) ) )
112 111 eqeq1d 
 |-  ( i = a -> ( ( abs ` ( y - i ) ) = ( abs ` ( j - c ) ) <-> ( abs ` ( y - a ) ) = ( abs ` ( j - c ) ) ) )
113 109 112 3anbi12d 
 |-  ( i = a -> ( ( i =/= d /\ ( abs ` ( y - i ) ) = ( abs ` ( j - c ) ) /\ ( abs ` ( y - d ) ) = ( abs ` ( e - f ) ) ) <-> ( a =/= d /\ ( abs ` ( y - a ) ) = ( abs ` ( j - c ) ) /\ ( abs ` ( y - d ) ) = ( abs ` ( e - f ) ) ) ) )
114 113 2rexbidv 
 |-  ( i = a -> ( E. e e. z E. f e. z ( i =/= d /\ ( abs ` ( y - i ) ) = ( abs ` ( j - c ) ) /\ ( abs ` ( y - d ) ) = ( abs ` ( e - f ) ) ) <-> E. e e. z E. f e. z ( a =/= d /\ ( abs ` ( y - a ) ) = ( abs ` ( j - c ) ) /\ ( abs ` ( y - d ) ) = ( abs ` ( e - f ) ) ) ) )
115 114 2rexbidv 
 |-  ( i = a -> ( E. c e. z E. d e. z E. e e. z E. f e. z ( i =/= d /\ ( abs ` ( y - i ) ) = ( abs ` ( j - c ) ) /\ ( abs ` ( y - d ) ) = ( abs ` ( e - f ) ) ) <-> E. c e. z E. d e. z E. e e. z E. f e. z ( a =/= d /\ ( abs ` ( y - a ) ) = ( abs ` ( j - c ) ) /\ ( abs ` ( y - d ) ) = ( abs ` ( e - f ) ) ) ) )
116 oveq1 
 |-  ( j = b -> ( j - c ) = ( b - c ) )
117 116 fveq2d 
 |-  ( j = b -> ( abs ` ( j - c ) ) = ( abs ` ( b - c ) ) )
118 117 eqeq2d 
 |-  ( j = b -> ( ( abs ` ( y - a ) ) = ( abs ` ( j - c ) ) <-> ( abs ` ( y - a ) ) = ( abs ` ( b - c ) ) ) )
119 118 3anbi2d 
 |-  ( j = b -> ( ( a =/= d /\ ( abs ` ( y - a ) ) = ( abs ` ( j - c ) ) /\ ( abs ` ( y - d ) ) = ( abs ` ( e - f ) ) ) <-> ( a =/= d /\ ( abs ` ( y - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( y - d ) ) = ( abs ` ( e - f ) ) ) ) )
120 119 2rexbidv 
 |-  ( j = b -> ( E. e e. z E. f e. z ( a =/= d /\ ( abs ` ( y - a ) ) = ( abs ` ( j - c ) ) /\ ( abs ` ( y - d ) ) = ( abs ` ( e - f ) ) ) <-> E. e e. z E. f e. z ( a =/= d /\ ( abs ` ( y - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( y - d ) ) = ( abs ` ( e - f ) ) ) ) )
121 120 2rexbidv 
 |-  ( j = b -> ( E. c e. z E. d e. z E. e e. z E. f e. z ( a =/= d /\ ( abs ` ( y - a ) ) = ( abs ` ( j - c ) ) /\ ( abs ` ( y - d ) ) = ( abs ` ( e - f ) ) ) <-> E. c e. z E. d e. z E. e e. z E. f e. z ( a =/= d /\ ( abs ` ( y - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( y - d ) ) = ( abs ` ( e - f ) ) ) ) )
122 115 121 cbvrex2vw 
 |-  ( E. i e. z E. j e. z E. c e. z E. d e. z E. e e. z E. f e. z ( i =/= d /\ ( abs ` ( y - i ) ) = ( abs ` ( j - c ) ) /\ ( abs ` ( y - d ) ) = ( abs ` ( e - f ) ) ) <-> E. a e. z E. b e. z E. c e. z E. d e. z E. e e. z E. f e. z ( a =/= d /\ ( abs ` ( y - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( y - d ) ) = ( abs ` ( e - f ) ) ) )
123 101 108 122 3orbi123i 
 |-  ( ( E. i e. z E. j e. z E. c e. z E. d e. z E. t e. RR E. r e. RR ( y = ( i + ( t x. ( j - i ) ) ) /\ y = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( j - i ) ) x. ( d - c ) ) ) =/= 0 ) \/ E. i e. z E. j e. z E. c e. z E. e e. z E. f e. z E. t e. RR ( y = ( i + ( t x. ( j - i ) ) ) /\ ( abs ` ( y - c ) ) = ( abs ` ( e - f ) ) ) \/ E. i e. z E. j e. z E. c e. z E. d e. z E. e e. z E. f e. z ( i =/= d /\ ( abs ` ( y - i ) ) = ( abs ` ( j - c ) ) /\ ( abs ` ( y - d ) ) = ( abs ` ( e - f ) ) ) ) <-> ( E. a e. z E. b e. z E. c e. z E. d e. z E. t e. RR E. r e. RR ( y = ( a + ( t x. ( b - a ) ) ) /\ y = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) \/ E. a e. z E. b e. z E. c e. z E. e e. z E. f e. z E. t e. RR ( y = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( y - c ) ) = ( abs ` ( e - f ) ) ) \/ E. a e. z E. b e. z E. c e. z E. d e. z E. e e. z E. f e. z ( a =/= d /\ ( abs ` ( y - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( y - d ) ) = ( abs ` ( e - f ) ) ) ) )
124 77 123 bitri 
 |-  ( ( E. i e. z E. j e. z E. k e. z E. l e. z E. o e. RR E. p e. RR ( y = ( i + ( o x. ( j - i ) ) ) /\ y = ( k + ( p x. ( l - k ) ) ) /\ ( Im ` ( ( * ` ( j - i ) ) x. ( l - k ) ) ) =/= 0 ) \/ E. i e. z E. j e. z E. k e. z E. m e. z E. q e. z E. o e. RR ( y = ( i + ( o x. ( j - i ) ) ) /\ ( abs ` ( y - k ) ) = ( abs ` ( m - q ) ) ) \/ E. i e. z E. j e. z E. k e. z E. l e. z E. m e. z E. q e. z ( i =/= l /\ ( abs ` ( y - i ) ) = ( abs ` ( j - k ) ) /\ ( abs ` ( y - l ) ) = ( abs ` ( m - q ) ) ) ) <-> ( E. a e. z E. b e. z E. c e. z E. d e. z E. t e. RR E. r e. RR ( y = ( a + ( t x. ( b - a ) ) ) /\ y = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) \/ E. a e. z E. b e. z E. c e. z E. e e. z E. f e. z E. t e. RR ( y = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( y - c ) ) = ( abs ` ( e - f ) ) ) \/ E. a e. z E. b e. z E. c e. z E. d e. z E. e e. z E. f e. z ( a =/= d /\ ( abs ` ( y - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( y - d ) ) = ( abs ` ( e - f ) ) ) ) )
125 124 rabbii 
 |-  { y e. CC | ( E. i e. z E. j e. z E. k e. z E. l e. z E. o e. RR E. p e. RR ( y = ( i + ( o x. ( j - i ) ) ) /\ y = ( k + ( p x. ( l - k ) ) ) /\ ( Im ` ( ( * ` ( j - i ) ) x. ( l - k ) ) ) =/= 0 ) \/ E. i e. z E. j e. z E. k e. z E. m e. z E. q e. z E. o e. RR ( y = ( i + ( o x. ( j - i ) ) ) /\ ( abs ` ( y - k ) ) = ( abs ` ( m - q ) ) ) \/ E. i e. z E. j e. z E. k e. z E. l e. z E. m e. z E. q e. z ( i =/= l /\ ( abs ` ( y - i ) ) = ( abs ` ( j - k ) ) /\ ( abs ` ( y - l ) ) = ( abs ` ( m - q ) ) ) ) } = { y e. CC | ( E. a e. z E. b e. z E. c e. z E. d e. z E. t e. RR E. r e. RR ( y = ( a + ( t x. ( b - a ) ) ) /\ y = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) \/ E. a e. z E. b e. z E. c e. z E. e e. z E. f e. z E. t e. RR ( y = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( y - c ) ) = ( abs ` ( e - f ) ) ) \/ E. a e. z E. b e. z E. c e. z E. d e. z E. e e. z E. f e. z ( a =/= d /\ ( abs ` ( y - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( y - d ) ) = ( abs ` ( e - f ) ) ) ) }
126 eqeq1 
 |-  ( y = x -> ( y = ( a + ( t x. ( b - a ) ) ) <-> x = ( a + ( t x. ( b - a ) ) ) ) )
127 eqeq1 
 |-  ( y = x -> ( y = ( c + ( r x. ( d - c ) ) ) <-> x = ( c + ( r x. ( d - c ) ) ) ) )
128 biidd 
 |-  ( y = x -> ( ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 <-> ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) )
129 126 127 128 3anbi123d 
 |-  ( y = x -> ( ( y = ( a + ( t x. ( b - a ) ) ) /\ y = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) <-> ( x = ( a + ( t x. ( b - a ) ) ) /\ x = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) ) )
130 129 2rexbidv 
 |-  ( y = x -> ( E. t e. RR E. r e. RR ( y = ( a + ( t x. ( b - a ) ) ) /\ y = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) <-> E. t e. RR E. r e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ x = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) ) )
131 130 2rexbidv 
 |-  ( y = x -> ( E. c e. z E. d e. z E. t e. RR E. r e. RR ( y = ( a + ( t x. ( b - a ) ) ) /\ y = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) <-> E. c e. z E. d e. z E. t e. RR E. r e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ x = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) ) )
132 131 2rexbidv 
 |-  ( y = x -> ( E. a e. z E. b e. z E. c e. z E. d e. z E. t e. RR E. r e. RR ( y = ( a + ( t x. ( b - a ) ) ) /\ y = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) <-> E. a e. z E. b e. z E. c e. z E. d e. z E. t e. RR E. r e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ x = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) ) )
133 oveq1 
 |-  ( y = x -> ( y - c ) = ( x - c ) )
134 133 fveq2d 
 |-  ( y = x -> ( abs ` ( y - c ) ) = ( abs ` ( x - c ) ) )
135 134 eqeq1d 
 |-  ( y = x -> ( ( abs ` ( y - c ) ) = ( abs ` ( e - f ) ) <-> ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) )
136 126 135 anbi12d 
 |-  ( y = x -> ( ( y = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( y - c ) ) = ( abs ` ( e - f ) ) ) <-> ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) ) )
137 136 2rexbidv 
 |-  ( y = x -> ( E. f e. z E. t e. RR ( y = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( y - c ) ) = ( abs ` ( e - f ) ) ) <-> E. f e. z E. t e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) ) )
138 137 2rexbidv 
 |-  ( y = x -> ( E. c e. z E. e e. z E. f e. z E. t e. RR ( y = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( y - c ) ) = ( abs ` ( e - f ) ) ) <-> E. c e. z E. e e. z E. f e. z E. t e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) ) )
139 138 2rexbidv 
 |-  ( y = x -> ( E. a e. z E. b e. z E. c e. z E. e e. z E. f e. z E. t e. RR ( y = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( y - c ) ) = ( abs ` ( e - f ) ) ) <-> E. a e. z E. b e. z E. c e. z E. e e. z E. f e. z E. t e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) ) )
140 biidd 
 |-  ( y = x -> ( a =/= d <-> a =/= d ) )
141 oveq1 
 |-  ( y = x -> ( y - a ) = ( x - a ) )
142 141 fveq2d 
 |-  ( y = x -> ( abs ` ( y - a ) ) = ( abs ` ( x - a ) ) )
143 142 eqeq1d 
 |-  ( y = x -> ( ( abs ` ( y - a ) ) = ( abs ` ( b - c ) ) <-> ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) ) )
144 oveq1 
 |-  ( y = x -> ( y - d ) = ( x - d ) )
145 144 fveq2d 
 |-  ( y = x -> ( abs ` ( y - d ) ) = ( abs ` ( x - d ) ) )
146 145 eqeq1d 
 |-  ( y = x -> ( ( abs ` ( y - d ) ) = ( abs ` ( e - f ) ) <-> ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) )
147 140 143 146 3anbi123d 
 |-  ( y = x -> ( ( a =/= d /\ ( abs ` ( y - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( y - d ) ) = ( abs ` ( e - f ) ) ) <-> ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) )
148 147 2rexbidv 
 |-  ( y = x -> ( E. e e. z E. f e. z ( a =/= d /\ ( abs ` ( y - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( y - d ) ) = ( abs ` ( e - f ) ) ) <-> E. e e. z E. f e. z ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) )
149 148 2rexbidv 
 |-  ( y = x -> ( E. c e. z E. d e. z E. e e. z E. f e. z ( a =/= d /\ ( abs ` ( y - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( y - d ) ) = ( abs ` ( e - f ) ) ) <-> E. c e. z E. d e. z E. e e. z E. f e. z ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) )
150 149 2rexbidv 
 |-  ( y = x -> ( E. a e. z E. b e. z E. c e. z E. d e. z E. e e. z E. f e. z ( a =/= d /\ ( abs ` ( y - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( y - d ) ) = ( abs ` ( e - f ) ) ) <-> E. a e. z E. b e. z E. c e. z E. d e. z E. e e. z E. f e. z ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) )
151 132 139 150 3orbi123d 
 |-  ( y = x -> ( ( E. a e. z E. b e. z E. c e. z E. d e. z E. t e. RR E. r e. RR ( y = ( a + ( t x. ( b - a ) ) ) /\ y = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) \/ E. a e. z E. b e. z E. c e. z E. e e. z E. f e. z E. t e. RR ( y = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( y - c ) ) = ( abs ` ( e - f ) ) ) \/ E. a e. z E. b e. z E. c e. z E. d e. z E. e e. z E. f e. z ( a =/= d /\ ( abs ` ( y - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( y - d ) ) = ( abs ` ( e - f ) ) ) ) <-> ( E. a e. z E. b e. z E. c e. z E. d e. z E. t e. RR E. r e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ x = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) \/ E. a e. z E. b e. z E. c e. z E. e e. z E. f e. z E. t e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) \/ E. a e. z E. b e. z E. c e. z E. d e. z E. e e. z E. f e. z ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) ) )
152 151 cbvrabv 
 |-  { y e. CC | ( E. a e. z E. b e. z E. c e. z E. d e. z E. t e. RR E. r e. RR ( y = ( a + ( t x. ( b - a ) ) ) /\ y = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) \/ E. a e. z E. b e. z E. c e. z E. e e. z E. f e. z E. t e. RR ( y = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( y - c ) ) = ( abs ` ( e - f ) ) ) \/ E. a e. z E. b e. z E. c e. z E. d e. z E. e e. z E. f e. z ( a =/= d /\ ( abs ` ( y - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( y - d ) ) = ( abs ` ( e - f ) ) ) ) } = { x e. CC | ( E. a e. z E. b e. z E. c e. z E. d e. z E. t e. RR E. r e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ x = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) \/ E. a e. z E. b e. z E. c e. z E. e e. z E. f e. z E. t e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) \/ E. a e. z E. b e. z E. c e. z E. d e. z E. e e. z E. f e. z ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) }
153 125 152 eqtri 
 |-  { y e. CC | ( E. i e. z E. j e. z E. k e. z E. l e. z E. o e. RR E. p e. RR ( y = ( i + ( o x. ( j - i ) ) ) /\ y = ( k + ( p x. ( l - k ) ) ) /\ ( Im ` ( ( * ` ( j - i ) ) x. ( l - k ) ) ) =/= 0 ) \/ E. i e. z E. j e. z E. k e. z E. m e. z E. q e. z E. o e. RR ( y = ( i + ( o x. ( j - i ) ) ) /\ ( abs ` ( y - k ) ) = ( abs ` ( m - q ) ) ) \/ E. i e. z E. j e. z E. k e. z E. l e. z E. m e. z E. q e. z ( i =/= l /\ ( abs ` ( y - i ) ) = ( abs ` ( j - k ) ) /\ ( abs ` ( y - l ) ) = ( abs ` ( m - q ) ) ) ) } = { x e. CC | ( E. a e. z E. b e. z E. c e. z E. d e. z E. t e. RR E. r e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ x = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) \/ E. a e. z E. b e. z E. c e. z E. e e. z E. f e. z E. t e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) \/ E. a e. z E. b e. z E. c e. z E. d e. z E. e e. z E. f e. z ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) }
154 153 mpteq2i 
 |-  ( z e. _V |-> { y e. CC | ( E. i e. z E. j e. z E. k e. z E. l e. z E. o e. RR E. p e. RR ( y = ( i + ( o x. ( j - i ) ) ) /\ y = ( k + ( p x. ( l - k ) ) ) /\ ( Im ` ( ( * ` ( j - i ) ) x. ( l - k ) ) ) =/= 0 ) \/ E. i e. z E. j e. z E. k e. z E. m e. z E. q e. z E. o e. RR ( y = ( i + ( o x. ( j - i ) ) ) /\ ( abs ` ( y - k ) ) = ( abs ` ( m - q ) ) ) \/ E. i e. z E. j e. z E. k e. z E. l e. z E. m e. z E. q e. z ( i =/= l /\ ( abs ` ( y - i ) ) = ( abs ` ( j - k ) ) /\ ( abs ` ( y - l ) ) = ( abs ` ( m - q ) ) ) ) } ) = ( z e. _V |-> { x e. CC | ( E. a e. z E. b e. z E. c e. z E. d e. z E. t e. RR E. r e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ x = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) \/ E. a e. z E. b e. z E. c e. z E. e e. z E. f e. z E. t e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) \/ E. a e. z E. b e. z E. c e. z E. d e. z E. e e. z E. f e. z ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) } )
155 elequ2 
 |-  ( z = s -> ( a e. z <-> a e. s ) )
156 elequ2 
 |-  ( z = s -> ( b e. z <-> b e. s ) )
157 elequ2 
 |-  ( z = s -> ( c e. z <-> c e. s ) )
158 rexeq 
 |-  ( z = s -> ( E. d e. z E. t e. RR E. r e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ x = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) <-> E. d e. s E. t e. RR E. r e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ x = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) ) )
159 157 158 anbi12d 
 |-  ( z = s -> ( ( c e. z /\ E. d e. z E. t e. RR E. r e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ x = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) ) <-> ( c e. s /\ E. d e. s E. t e. RR E. r e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ x = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) ) ) )
160 159 rexbidv2 
 |-  ( z = s -> ( E. c e. z E. d e. z E. t e. RR E. r e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ x = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) <-> E. c e. s E. d e. s E. t e. RR E. r e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ x = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) ) )
161 156 160 anbi12d 
 |-  ( z = s -> ( ( b e. z /\ E. c e. z E. d e. z E. t e. RR E. r e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ x = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) ) <-> ( b e. s /\ E. c e. s E. d e. s E. t e. RR E. r e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ x = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) ) ) )
162 161 rexbidv2 
 |-  ( z = s -> ( E. b e. z E. c e. z E. d e. z E. t e. RR E. r e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ x = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) <-> E. b e. s E. c e. s E. d e. s E. t e. RR E. r e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ x = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) ) )
163 155 162 anbi12d 
 |-  ( z = s -> ( ( a e. z /\ E. b e. z E. c e. z E. d e. z E. t e. RR E. r e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ x = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) ) <-> ( a e. s /\ E. b e. s E. c e. s E. d e. s E. t e. RR E. r e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ x = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) ) ) )
164 163 rexbidv2 
 |-  ( z = s -> ( E. a e. z E. b e. z E. c e. z E. d e. z E. t e. RR E. r e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ x = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) <-> E. a e. s E. b e. s E. c e. s E. d e. s E. t e. RR E. r e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ x = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) ) )
165 elequ2 
 |-  ( z = s -> ( e e. z <-> e e. s ) )
166 rexeq 
 |-  ( z = s -> ( E. f e. z E. t e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) <-> E. f e. s E. t e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) ) )
167 165 166 anbi12d 
 |-  ( z = s -> ( ( e e. z /\ E. f e. z E. t e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) ) <-> ( e e. s /\ E. f e. s E. t e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) ) ) )
168 167 rexbidv2 
 |-  ( z = s -> ( E. e e. z E. f e. z E. t e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) <-> E. e e. s E. f e. s E. t e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) ) )
169 157 168 anbi12d 
 |-  ( z = s -> ( ( c e. z /\ E. e e. z E. f e. z E. t e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) ) <-> ( c e. s /\ E. e e. s E. f e. s E. t e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) ) ) )
170 169 rexbidv2 
 |-  ( z = s -> ( E. c e. z E. e e. z E. f e. z E. t e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) <-> E. c e. s E. e e. s E. f e. s E. t e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) ) )
171 156 170 anbi12d 
 |-  ( z = s -> ( ( b e. z /\ E. c e. z E. e e. z E. f e. z E. t e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) ) <-> ( b e. s /\ E. c e. s E. e e. s E. f e. s E. t e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) ) ) )
172 171 rexbidv2 
 |-  ( z = s -> ( E. b e. z E. c e. z E. e e. z E. f e. z E. t e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) <-> E. b e. s E. c e. s E. e e. s E. f e. s E. t e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) ) )
173 155 172 anbi12d 
 |-  ( z = s -> ( ( a e. z /\ E. b e. z E. c e. z E. e e. z E. f e. z E. t e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) ) <-> ( a e. s /\ E. b e. s E. c e. s E. e e. s E. f e. s E. t e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) ) ) )
174 173 rexbidv2 
 |-  ( z = s -> ( E. a e. z E. b e. z E. c e. z E. e e. z E. f e. z E. t e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) <-> E. a e. s E. b e. s E. c e. s E. e e. s E. f e. s E. t e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) ) )
175 elequ2 
 |-  ( z = s -> ( d e. z <-> d e. s ) )
176 rexeq 
 |-  ( z = s -> ( E. f e. z ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) <-> E. f e. s ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) )
177 165 176 anbi12d 
 |-  ( z = s -> ( ( e e. z /\ E. f e. z ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) <-> ( e e. s /\ E. f e. s ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) ) )
178 177 rexbidv2 
 |-  ( z = s -> ( E. e e. z E. f e. z ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) <-> E. e e. s E. f e. s ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) )
179 175 178 anbi12d 
 |-  ( z = s -> ( ( d e. z /\ E. e e. z E. f e. z ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) <-> ( d e. s /\ E. e e. s E. f e. s ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) ) )
180 179 rexbidv2 
 |-  ( z = s -> ( E. d e. z E. e e. z E. f e. z ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) <-> E. d e. s E. e e. s E. f e. s ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) )
181 157 180 anbi12d 
 |-  ( z = s -> ( ( c e. z /\ E. d e. z E. e e. z E. f e. z ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) <-> ( c e. s /\ E. d e. s E. e e. s E. f e. s ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) ) )
182 181 rexbidv2 
 |-  ( z = s -> ( E. c e. z E. d e. z E. e e. z E. f e. z ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) <-> E. c e. s E. d e. s E. e e. s E. f e. s ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) )
183 156 182 anbi12d 
 |-  ( z = s -> ( ( b e. z /\ E. c e. z E. d e. z E. e e. z E. f e. z ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) <-> ( b e. s /\ E. c e. s E. d e. s E. e e. s E. f e. s ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) ) )
184 183 rexbidv2 
 |-  ( z = s -> ( E. b e. z E. c e. z E. d e. z E. e e. z E. f e. z ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) <-> E. b e. s E. c e. s E. d e. s E. e e. s E. f e. s ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) )
185 155 184 anbi12d 
 |-  ( z = s -> ( ( a e. z /\ E. b e. z E. c e. z E. d e. z E. e e. z E. f e. z ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) <-> ( a e. s /\ E. b e. s E. c e. s E. d e. s E. e e. s E. f e. s ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) ) )
186 185 rexbidv2 
 |-  ( z = s -> ( E. a e. z E. b e. z E. c e. z E. d e. z E. e e. z E. f e. z ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) <-> E. a e. s E. b e. s E. c e. s E. d e. s E. e e. s E. f e. s ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) )
187 164 174 186 3orbi123d 
 |-  ( z = s -> ( ( E. a e. z E. b e. z E. c e. z E. d e. z E. t e. RR E. r e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ x = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) \/ E. a e. z E. b e. z E. c e. z E. e e. z E. f e. z E. t e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) \/ E. a e. z E. b e. z E. c e. z E. d e. z E. e e. z E. f e. z ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) <-> ( E. a e. s E. b e. s E. c e. s E. d e. s E. t e. RR E. r e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ x = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) \/ E. a e. s E. b e. s E. c e. s E. e e. s E. f e. s E. t e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) \/ E. a e. s E. b e. s E. c e. s E. d e. s E. e e. s E. f e. s ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) ) )
188 187 rabbidv 
 |-  ( z = s -> { x e. CC | ( E. a e. z E. b e. z E. c e. z E. d e. z E. t e. RR E. r e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ x = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) \/ E. a e. z E. b e. z E. c e. z E. e e. z E. f e. z E. t e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) \/ E. a e. z E. b e. z E. c e. z E. d e. z E. e e. z E. f e. z ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) } = { x e. CC | ( E. a e. s E. b e. s E. c e. s E. d e. s E. t e. RR E. r e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ x = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) \/ E. a e. s E. b e. s E. c e. s E. e e. s E. f e. s E. t e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) \/ E. a e. s E. b e. s E. c e. s E. d e. s E. e e. s E. f e. s ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) } )
189 188 cbvmptv 
 |-  ( z e. _V |-> { x e. CC | ( E. a e. z E. b e. z E. c e. z E. d e. z E. t e. RR E. r e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ x = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) \/ E. a e. z E. b e. z E. c e. z E. e e. z E. f e. z E. t e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) \/ E. a e. z E. b e. z E. c e. z E. d e. z E. e e. z E. f e. z ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) } ) = ( s e. _V |-> { x e. CC | ( E. a e. s E. b e. s E. c e. s E. d e. s E. t e. RR E. r e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ x = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) \/ E. a e. s E. b e. s E. c e. s E. e e. s E. f e. s E. t e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) \/ E. a e. s E. b e. s E. c e. s E. d e. s E. e e. s E. f e. s ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) } )
190 154 189 eqtri 
 |-  ( z e. _V |-> { y e. CC | ( E. i e. z E. j e. z E. k e. z E. l e. z E. o e. RR E. p e. RR ( y = ( i + ( o x. ( j - i ) ) ) /\ y = ( k + ( p x. ( l - k ) ) ) /\ ( Im ` ( ( * ` ( j - i ) ) x. ( l - k ) ) ) =/= 0 ) \/ E. i e. z E. j e. z E. k e. z E. m e. z E. q e. z E. o e. RR ( y = ( i + ( o x. ( j - i ) ) ) /\ ( abs ` ( y - k ) ) = ( abs ` ( m - q ) ) ) \/ E. i e. z E. j e. z E. k e. z E. l e. z E. m e. z E. q e. z ( i =/= l /\ ( abs ` ( y - i ) ) = ( abs ` ( j - k ) ) /\ ( abs ` ( y - l ) ) = ( abs ` ( m - q ) ) ) ) } ) = ( s e. _V |-> { x e. CC | ( E. a e. s E. b e. s E. c e. s E. d e. s E. t e. RR E. r e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ x = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) \/ E. a e. s E. b e. s E. c e. s E. e e. s E. f e. s E. t e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) \/ E. a e. s E. b e. s E. c e. s E. d e. s E. e e. s E. f e. s ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) } )
191 rdgeq1 
 |-  ( ( z e. _V |-> { y e. CC | ( E. i e. z E. j e. z E. k e. z E. l e. z E. o e. RR E. p e. RR ( y = ( i + ( o x. ( j - i ) ) ) /\ y = ( k + ( p x. ( l - k ) ) ) /\ ( Im ` ( ( * ` ( j - i ) ) x. ( l - k ) ) ) =/= 0 ) \/ E. i e. z E. j e. z E. k e. z E. m e. z E. q e. z E. o e. RR ( y = ( i + ( o x. ( j - i ) ) ) /\ ( abs ` ( y - k ) ) = ( abs ` ( m - q ) ) ) \/ E. i e. z E. j e. z E. k e. z E. l e. z E. m e. z E. q e. z ( i =/= l /\ ( abs ` ( y - i ) ) = ( abs ` ( j - k ) ) /\ ( abs ` ( y - l ) ) = ( abs ` ( m - q ) ) ) ) } ) = ( s e. _V |-> { x e. CC | ( E. a e. s E. b e. s E. c e. s E. d e. s E. t e. RR E. r e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ x = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) \/ E. a e. s E. b e. s E. c e. s E. e e. s E. f e. s E. t e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) \/ E. a e. s E. b e. s E. c e. s E. d e. s E. e e. s E. f e. s ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) } ) -> rec ( ( z e. _V |-> { y e. CC | ( E. i e. z E. j e. z E. k e. z E. l e. z E. o e. RR E. p e. RR ( y = ( i + ( o x. ( j - i ) ) ) /\ y = ( k + ( p x. ( l - k ) ) ) /\ ( Im ` ( ( * ` ( j - i ) ) x. ( l - k ) ) ) =/= 0 ) \/ E. i e. z E. j e. z E. k e. z E. m e. z E. q e. z E. o e. RR ( y = ( i + ( o x. ( j - i ) ) ) /\ ( abs ` ( y - k ) ) = ( abs ` ( m - q ) ) ) \/ E. i e. z E. j e. z E. k e. z E. l e. z E. m e. z E. q e. z ( i =/= l /\ ( abs ` ( y - i ) ) = ( abs ` ( j - k ) ) /\ ( abs ` ( y - l ) ) = ( abs ` ( m - q ) ) ) ) } ) , { 0 , 1 } ) = rec ( ( s e. _V |-> { x e. CC | ( E. a e. s E. b e. s E. c e. s E. d e. s E. t e. RR E. r e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ x = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) \/ E. a e. s E. b e. s E. c e. s E. e e. s E. f e. s E. t e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) \/ E. a e. s E. b e. s E. c e. s E. d e. s E. e e. s E. f e. s ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) } ) , { 0 , 1 } ) )
192 190 191 ax-mp 
 |-  rec ( ( z e. _V |-> { y e. CC | ( E. i e. z E. j e. z E. k e. z E. l e. z E. o e. RR E. p e. RR ( y = ( i + ( o x. ( j - i ) ) ) /\ y = ( k + ( p x. ( l - k ) ) ) /\ ( Im ` ( ( * ` ( j - i ) ) x. ( l - k ) ) ) =/= 0 ) \/ E. i e. z E. j e. z E. k e. z E. m e. z E. q e. z E. o e. RR ( y = ( i + ( o x. ( j - i ) ) ) /\ ( abs ` ( y - k ) ) = ( abs ` ( m - q ) ) ) \/ E. i e. z E. j e. z E. k e. z E. l e. z E. m e. z E. q e. z ( i =/= l /\ ( abs ` ( y - i ) ) = ( abs ` ( j - k ) ) /\ ( abs ` ( y - l ) ) = ( abs ` ( m - q ) ) ) ) } ) , { 0 , 1 } ) = rec ( ( s e. _V |-> { x e. CC | ( E. a e. s E. b e. s E. c e. s E. d e. s E. t e. RR E. r e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ x = ( c + ( r x. ( d - c ) ) ) /\ ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) =/= 0 ) \/ E. a e. s E. b e. s E. c e. s E. e e. s E. f e. s E. t e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) \/ E. a e. s E. b e. s E. c e. s E. d e. s E. e e. s E. f e. s ( a =/= d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) } ) , { 0 , 1 } )