let p1, p2, p3, p4 be Point of (TOP-REAL 2); :: thesis: for P being non empty compact Subset of (TOP-REAL 2) st P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } & LE p1,p2,P & LE p2,p3,P & LE p3,p4,P holds
ex f being Function of (TOP-REAL 2),(TOP-REAL 2) ex q1, q2, q3, q4 being Point of (TOP-REAL 2) st
( f is being_homeomorphism & ( for q being Point of (TOP-REAL 2) holds |.(f . q).| = |.q.| ) & q1 = f . p1 & q2 = f . p2 & q3 = f . p3 & q4 = f . p4 & q1 `1 < 0 & q1 `2 < 0 & q2 `1 < 0 & q2 `2 < 0 & q3 `1 < 0 & q3 `2 < 0 & q4 `1 < 0 & q4 `2 < 0 & LE q1,q2,P & LE q2,q3,P & LE q3,q4,P )
let P be non empty compact Subset of (TOP-REAL 2); :: thesis: ( P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } & LE p1,p2,P & LE p2,p3,P & LE p3,p4,P implies ex f being Function of (TOP-REAL 2),(TOP-REAL 2) ex q1, q2, q3, q4 being Point of (TOP-REAL 2) st
( f is being_homeomorphism & ( for q being Point of (TOP-REAL 2) holds |.(f . q).| = |.q.| ) & q1 = f . p1 & q2 = f . p2 & q3 = f . p3 & q4 = f . p4 & q1 `1 < 0 & q1 `2 < 0 & q2 `1 < 0 & q2 `2 < 0 & q3 `1 < 0 & q3 `2 < 0 & q4 `1 < 0 & q4 `2 < 0 & LE q1,q2,P & LE q2,q3,P & LE q3,q4,P ) )
assume that
A1: P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } and
A2: LE p1,p2,P and
A3: LE p2,p3,P and
A4: LE p3,p4,P ; :: thesis: ex f being Function of (TOP-REAL 2),(TOP-REAL 2) ex q1, q2, q3, q4 being Point of (TOP-REAL 2) st
( f is being_homeomorphism & ( for q being Point of (TOP-REAL 2) holds |.(f . q).| = |.q.| ) & q1 = f . p1 & q2 = f . p2 & q3 = f . p3 & q4 = f . p4 & q1 `1 < 0 & q1 `2 < 0 & q2 `1 < 0 & q2 `2 < 0 & q3 `1 < 0 & q3 `2 < 0 & q4 `1 < 0 & q4 `2 < 0 & LE q1,q2,P & LE q2,q3,P & LE q3,q4,P )
A5: Lower_Arc P = { p7 where p7 is Point of (TOP-REAL 2) : ( p7 in P & p7 `2 <= 0 ) } by A1, Th35;
A6: W-min P = |[(- 1),0]| by A1, Th29;
then A7: (W-min P) `2 = 0 by EUCLID:52;
A8: P is being_simple_closed_curve by A1, JGRAPH_3:26;
then A9: p1 in P by A2, JORDAN7:5;
A10: Upper_Arc P is_an_arc_of W-min P, E-max P by A8, JORDAN6:def 8;
A11: Upper_Arc P = { p7 where p7 is Point of (TOP-REAL 2) : ( p7 in P & p7 `2 >= 0 ) } by A1, Th34;
A12: p4 in P by A4, A8, JORDAN7:5;
then A13: ex p44 being Point of (TOP-REAL 2) st
( p44 = p4 & |.p44.| = 1 ) by A1;
then A14: p4 `1 <= 1 by Th1;
A15: - 1 <= p4 `1 by A13, Th1;
now :: thesis: ( ( p4 `1 = - 1 & ex f being Function of (TOP-REAL 2),(TOP-REAL 2) ex q1, q2, q3, q4 being Point of (TOP-REAL 2) st
( f is being_homeomorphism & ( for q being Point of (TOP-REAL 2) holds |.(f . q).| = |.q.| ) & q1 = f . p1 & q2 = f . p2 & q3 = f . p3 & q4 = f . p4 & q1 `1 < 0 & q1 `2 < 0 & q2 `1 < 0 & q2 `2 < 0 & q3 `1 < 0 & q3 `2 < 0 & q4 `1 < 0 & q4 `2 < 0 & LE q1,q2,P & LE q2,q3,P & LE q3,q4,P ) ) or ( p4 `1 <> - 1 & ex f being Function of (TOP-REAL 2),(TOP-REAL 2) ex q1, q2, q3, q4 being Point of (TOP-REAL 2) st
( f is being_homeomorphism & ( for q being Point of (TOP-REAL 2) holds |.(f . q).| = |.q.| ) & q1 = f . p1 & q2 = f . p2 & q3 = f . p3 & q4 = f . p4 & q1 `1 < 0 & q1 `2 < 0 & q2 `1 < 0 & q2 `2 < 0 & q3 `1 < 0 & q3 `2 < 0 & q4 `1 < 0 & q4 `2 < 0 & LE q1,q2,P & LE q2,q3,P & LE q3,q4,P ) ) )
per cases ( p4 `1 = - 1 or p4 `1 <> - 1 ) ;
case A16: p4 `1 = - 1 ; :: thesis: ex f being Function of (TOP-REAL 2),(TOP-REAL 2) ex q1, q2, q3, q4 being Point of (TOP-REAL 2) st
( f is being_homeomorphism & ( for q being Point of (TOP-REAL 2) holds |.(f . q).| = |.q.| ) & q1 = f . p1 & q2 = f . p2 & q3 = f . p3 & q4 = f . p4 & q1 `1 < 0 & q1 `2 < 0 & q2 `1 < 0 & q2 `2 < 0 & q3 `1 < 0 & q3 `2 < 0 & q4 `1 < 0 & q4 `2 < 0 & LE q1,q2,P & LE q2,q3,P & LE q3,q4,P )
1 ^2 = ((p4 `1) ^2) + ((p4 `2) ^2) by A13, JGRAPH_3:1
.= ((p4 `2) ^2) + 1 by A16 ;
then A17: p4 `2 = 0 by XCMPLX_1:6;
then A18: p4 in Upper_Arc P by A12, A11;
A19: p4 = W-min P by A6, A16, A17, EUCLID:53;
A20: now :: thesis: ( ( p1 in Upper_Arc P & LE p4,p1,P ) or ( not p1 in Upper_Arc P & LE p4,p1,P ) )
end;
then A23: LE p4,p2,P by A1, A2, JGRAPH_3:26, JORDAN6:58;
then LE p4,p3,P by A1, A3, JGRAPH_3:26, JORDAN6:58;
then A24: p3 = p4 by A1, A4, JGRAPH_3:26, JORDAN6:57;
LE p2,p4,P by A1, A3, A4, JGRAPH_3:26, JORDAN6:58;
then A25: p2 = p4 by A1, A23, JGRAPH_3:26, JORDAN6:57;
LE p1,p3,P by A1, A2, A3, JGRAPH_3:26, JORDAN6:58;
then LE p1,p4,P by A1, A4, JGRAPH_3:26, JORDAN6:58;
then p4 = p1 by A1, A20, JGRAPH_3:26, JORDAN6:57;
hence ex f being Function of (TOP-REAL 2),(TOP-REAL 2) ex q1, q2, q3, q4 being Point of (TOP-REAL 2) st
( f is being_homeomorphism & ( for q being Point of (TOP-REAL 2) holds |.(f . q).| = |.q.| ) & q1 = f . p1 & q2 = f . p2 & q3 = f . p3 & q4 = f . p4 & q1 `1 < 0 & q1 `2 < 0 & q2 `1 < 0 & q2 `2 < 0 & q3 `1 < 0 & q3 `2 < 0 & q4 `1 < 0 & q4 `2 < 0 & LE q1,q2,P & LE q2,q3,P & LE q3,q4,P ) by A1, A2, A16, A17, A25, A24, Th59; :: thesis: verum
end;
case A26: p4 `1 <> - 1 ; :: thesis: ex f being Function of (TOP-REAL 2),(TOP-REAL 2) ex q1, q2, q3, q4 being Point of (TOP-REAL 2) st
( f is being_homeomorphism & ( for q being Point of (TOP-REAL 2) holds |.(f . q).| = |.q.| ) & q1 = f . p1 & q2 = f . p2 & q3 = f . p3 & q4 = f . p4 & q1 `1 < 0 & q1 `2 < 0 & q2 `1 < 0 & q2 `2 < 0 & q3 `1 < 0 & q3 `2 < 0 & q4 `1 < 0 & q4 `2 < 0 & LE q1,q2,P & LE q2,q3,P & LE q3,q4,P )
then p4 `1 > - 1 by A15, XXREAL_0:1;
then consider r being Real such that
A27: - 1 < r and
A28: r < p4 `1 by XREAL_1:5;
reconsider r1 = r as Real ;
A29: r1 < 1 by A14, A28, XXREAL_0:2;
then consider f1 being Function of (TOP-REAL 2),(TOP-REAL 2) such that
A30: f1 = r1 -FanMorphS and
A31: f1 is being_homeomorphism by A27, JGRAPH_4:136;
set q11 = f1 . p1;
set q22 = f1 . p2;
set q33 = f1 . p3;
set q44 = f1 . p4;
now :: thesis: ( ( ( p4 `1 > 0 or p4 `2 >= 0 ) & ex f being Function of (TOP-REAL 2),(TOP-REAL 2) ex q1, q2, q3, q4 being Point of (TOP-REAL 2) st
( f is being_homeomorphism & ( for q being Point of (TOP-REAL 2) holds |.(f . q).| = |.q.| ) & q1 = f . p1 & q2 = f . p2 & q3 = f . p3 & q4 = f . p4 & q1 `1 < 0 & q1 `2 < 0 & q2 `1 < 0 & q2 `2 < 0 & q3 `1 < 0 & q3 `2 < 0 & q4 `1 < 0 & q4 `2 < 0 & LE q1,q2,P & LE q2,q3,P & LE q3,q4,P ) ) or ( p4 `1 <= 0 & p4 `2 < 0 & ex f being Function of (TOP-REAL 2),(TOP-REAL 2) ex q1, q2, q3, q4 being Point of (TOP-REAL 2) st
( f is being_homeomorphism & ( for q being Point of (TOP-REAL 2) holds |.(f . q).| = |.q.| ) & q1 = f . p1 & q2 = f . p2 & q3 = f . p3 & q4 = f . p4 & q1 `1 < 0 & q1 `2 < 0 & q2 `1 < 0 & q2 `2 < 0 & q3 `1 < 0 & q3 `2 < 0 & q4 `1 < 0 & q4 `2 < 0 & LE q1,q2,P & LE q2,q3,P & LE q3,q4,P ) ) )
per cases ( p4 `1 > 0 or p4 `2 >= 0 or ( p4 `1 <= 0 & p4 `2 < 0 ) ) ;
case A32: ( p4 `1 > 0 or p4 `2 >= 0 ) ; :: thesis: ex f being Function of (TOP-REAL 2),(TOP-REAL 2) ex q1, q2, q3, q4 being Point of (TOP-REAL 2) st
( f is being_homeomorphism & ( for q being Point of (TOP-REAL 2) holds |.(f . q).| = |.q.| ) & q1 = f . p1 & q2 = f . p2 & q3 = f . p3 & q4 = f . p4 & q1 `1 < 0 & q1 `2 < 0 & q2 `1 < 0 & q2 `2 < 0 & q3 `1 < 0 & q3 `2 < 0 & q4 `1 < 0 & q4 `2 < 0 & LE q1,q2,P & LE q2,q3,P & LE q3,q4,P )
A33: now :: thesis: ( p4 `2 = 0 implies not p4 `1 <= 0 )
assume that
A34: p4 `2 = 0 and
A35: p4 `1 <= 0 ; :: thesis: contradiction
1 ^2 = ((p4 `1) ^2) + ((p4 `2) ^2) by A13, JGRAPH_3:1
.= (p4 `1) ^2 by A34 ;
hence contradiction by A26, A35, SQUARE_1:40; :: thesis: verum
end;
A36: ( p3 `1 >= 0 or p3 `2 >= 0 ) by A1, A4, A32, Th49;
then A37: ( p2 `1 >= 0 or p2 `2 >= 0 ) by A1, A3, Th49;
then ( p1 `1 >= 0 or p1 `2 >= 0 ) by A1, A2, Th49;
hence ex f being Function of (TOP-REAL 2),(TOP-REAL 2) ex q1, q2, q3, q4 being Point of (TOP-REAL 2) st
( f is being_homeomorphism & ( for q being Point of (TOP-REAL 2) holds |.(f . q).| = |.q.| ) & q1 = f . p1 & q2 = f . p2 & q3 = f . p3 & q4 = f . p4 & q1 `1 < 0 & q1 `2 < 0 & q2 `1 < 0 & q2 `2 < 0 & q3 `1 < 0 & q3 `2 < 0 & q4 `1 < 0 & q4 `2 < 0 & LE q1,q2,P & LE q2,q3,P & LE q3,q4,P ) by A1, A2, A3, A4, A32, A36, A37, A33, Th63; :: thesis: verum
end;
case A38: ( p4 `1 <= 0 & p4 `2 < 0 ) ; :: thesis: ex f being Function of (TOP-REAL 2),(TOP-REAL 2) ex q1, q2, q3, q4 being Point of (TOP-REAL 2) st
( f is being_homeomorphism & ( for q being Point of (TOP-REAL 2) holds |.(f . q).| = |.q.| ) & q1 = f . p1 & q2 = f . p2 & q3 = f . p3 & q4 = f . p4 & q1 `1 < 0 & q1 `2 < 0 & q2 `1 < 0 & q2 `2 < 0 & q3 `1 < 0 & q3 `2 < 0 & q4 `1 < 0 & q4 `2 < 0 & LE q1,q2,P & LE q2,q3,P & LE q3,q4,P )
(p4 `1) / |.p4.| > r1 by A13, A28;
then A39: (f1 . p4) `1 > 0 by A27, A28, A30, A38, Th26;
A40: LE f1 . p3,f1 . p4,P by A1, A4, A27, A29, A30, Th58;
W-min P = |[(- 1),0]| by A1, Th29;
then A41: (W-min P) `2 = 0 by EUCLID:52;
A42: now :: thesis: ( ( (f1 . p3) `2 >= 0 & ( (f1 . p3) `2 >= 0 or (f1 . p3) `1 >= 0 ) ) or ( (f1 . p3) `2 < 0 & ( (f1 . p3) `2 >= 0 or (f1 . p3) `1 >= 0 ) ) )
per cases ( (f1 . p3) `2 >= 0 or (f1 . p3) `2 < 0 ) ;
case (f1 . p3) `2 >= 0 ; :: thesis: ( (f1 . p3) `2 >= 0 or (f1 . p3) `1 >= 0 )
hence ( (f1 . p3) `2 >= 0 or (f1 . p3) `1 >= 0 ) ; :: thesis: verum
end;
case (f1 . p3) `2 < 0 ; :: thesis: ( (f1 . p3) `2 >= 0 or (f1 . p3) `1 >= 0 )
thus ( (f1 . p3) `2 >= 0 or (f1 . p3) `1 >= 0 ) by A1, A39, A40, A41, Th48; :: thesis: verum
end;
end;
end;
A43: LE f1 . p2,f1 . p3,P by A1, A3, A27, A29, A30, Th58;
A44: now :: thesis: ( ( (f1 . p2) `2 >= 0 & ( (f1 . p2) `2 >= 0 or (f1 . p2) `1 >= 0 ) ) or ( (f1 . p2) `2 < 0 & ( (f1 . p2) `2 >= 0 or (f1 . p2) `1 >= 0 ) ) )
per cases ( (f1 . p2) `2 >= 0 or (f1 . p2) `2 < 0 ) ;
case (f1 . p2) `2 >= 0 ; :: thesis: ( (f1 . p2) `2 >= 0 or (f1 . p2) `1 >= 0 )
hence ( (f1 . p2) `2 >= 0 or (f1 . p2) `1 >= 0 ) ; :: thesis: verum
end;
case (f1 . p2) `2 < 0 ; :: thesis: ( (f1 . p2) `2 >= 0 or (f1 . p2) `1 >= 0 )
thus ( (f1 . p2) `2 >= 0 or (f1 . p2) `1 >= 0 ) by A1, A8, A39, A40, A43, A41, Th48, JORDAN6:58; :: thesis: verum
end;
end;
end;
A45: LE f1 . p1,f1 . p2,P by A1, A2, A27, A29, A30, Th58;
A46: LE f1 . p2,f1 . p4,P by A1, A40, A43, JGRAPH_3:26, JORDAN6:58;
now :: thesis: ( ( (f1 . p1) `2 >= 0 & ( (f1 . p1) `2 >= 0 or (f1 . p1) `1 >= 0 ) ) or ( (f1 . p1) `2 < 0 & ( (f1 . p1) `2 >= 0 or (f1 . p1) `1 >= 0 ) ) )
per cases ( (f1 . p1) `2 >= 0 or (f1 . p1) `2 < 0 ) ;
case (f1 . p1) `2 >= 0 ; :: thesis: ( (f1 . p1) `2 >= 0 or (f1 . p1) `1 >= 0 )
hence ( (f1 . p1) `2 >= 0 or (f1 . p1) `1 >= 0 ) ; :: thesis: verum
end;
case (f1 . p1) `2 < 0 ; :: thesis: ( (f1 . p1) `2 >= 0 or (f1 . p1) `1 >= 0 )
thus ( (f1 . p1) `2 >= 0 or (f1 . p1) `1 >= 0 ) by A1, A8, A39, A46, A45, A41, Th48, JORDAN6:58; :: thesis: verum
end;
end;
end;
then consider f2 being Function of (TOP-REAL 2),(TOP-REAL 2), q81, q82, q83, q84 being Point of (TOP-REAL 2) such that
A47: f2 is being_homeomorphism and
A48: for q being Point of (TOP-REAL 2) holds |.(f2 . q).| = |.q.| and
A49: ( q81 = f2 . (f1 . p1) & q82 = f2 . (f1 . p2) ) and
A50: ( q83 = f2 . (f1 . p3) & q84 = f2 . (f1 . p4) ) and
A51: ( q81 `1 < 0 & q81 `2 < 0 & q82 `1 < 0 & q82 `2 < 0 & q83 `1 < 0 & q83 `2 < 0 & q84 `1 < 0 & q84 `2 < 0 & LE q81,q82,P & LE q82,q83,P & LE q83,q84,P ) by A1, A39, A40, A43, A45, A42, A44, Th63;
reconsider f3 = f2 * f1 as Function of (TOP-REAL 2),(TOP-REAL 2) ;
A52: dom f1 = the carrier of (TOP-REAL 2) by FUNCT_2:def 1;
then A53: ( f3 . p1 = q81 & f3 . p2 = q82 ) by A49, FUNCT_1:13;
A54: for q being Point of (TOP-REAL 2) holds |.(f3 . q).| = |.q.|
proof
let q be Point of (TOP-REAL 2); :: thesis: |.(f3 . q).| = |.q.|
dom f1 = the carrier of (TOP-REAL 2) by FUNCT_2:def 1;
then f3 . q = f2 . (f1 . q) by FUNCT_1:13;
hence |.(f3 . q).| = |.(f1 . q).| by A48
.= |.q.| by A30, JGRAPH_4:128 ;
:: thesis: verum
end;
A55: ( f3 . p3 = q83 & f3 . p4 = q84 ) by A50, A52, FUNCT_1:13;
f3 is being_homeomorphism by A31, A47, TOPS_2:57;
hence ex f being Function of (TOP-REAL 2),(TOP-REAL 2) ex q1, q2, q3, q4 being Point of (TOP-REAL 2) st
( f is being_homeomorphism & ( for q being Point of (TOP-REAL 2) holds |.(f . q).| = |.q.| ) & q1 = f . p1 & q2 = f . p2 & q3 = f . p3 & q4 = f . p4 & q1 `1 < 0 & q1 `2 < 0 & q2 `1 < 0 & q2 `2 < 0 & q3 `1 < 0 & q3 `2 < 0 & q4 `1 < 0 & q4 `2 < 0 & LE q1,q2,P & LE q2,q3,P & LE q3,q4,P ) by A51, A54, A53, A55; :: thesis: verum
end;
end;
end;
hence ex f being Function of (TOP-REAL 2),(TOP-REAL 2) ex q1, q2, q3, q4 being Point of (TOP-REAL 2) st
( f is being_homeomorphism & ( for q being Point of (TOP-REAL 2) holds |.(f . q).| = |.q.| ) & q1 = f . p1 & q2 = f . p2 & q3 = f . p3 & q4 = f . p4 & q1 `1 < 0 & q1 `2 < 0 & q2 `1 < 0 & q2 `2 < 0 & q3 `1 < 0 & q3 `2 < 0 & q4 `1 < 0 & q4 `2 < 0 & LE q1,q2,P & LE q2,q3,P & LE q3,q4,P ) ; :: thesis: verum
end;
end;
end;
hence ex f being Function of (TOP-REAL 2),(TOP-REAL 2) ex q1, q2, q3, q4 being Point of (TOP-REAL 2) st
( f is being_homeomorphism & ( for q being Point of (TOP-REAL 2) holds |.(f . q).| = |.q.| ) & q1 = f . p1 & q2 = f . p2 & q3 = f . p3 & q4 = f . p4 & q1 `1 < 0 & q1 `2 < 0 & q2 `1 < 0 & q2 `2 < 0 & q3 `1 < 0 & q3 `2 < 0 & q4 `1 < 0 & q4 `2 < 0 & LE q1,q2,P & LE q2,q3,P & LE q3,q4,P ) ; :: thesis: verum