let C be Simple_closed_curve; :: thesis: ex f being Homeomorphism of TOP-REAL 2 st |[(- 1),0]|,|[1,0]| realize-max-dist-in f .: C
reconsider z = 0 as Element of COMPLEX by XCMPLX_0:def 2;
consider x, y being Point of (TOP-REAL 2) such that
A1: x <> y and
A2: ( x in C & y in C ) by TOPREAL2:4;
A3: dist (x,y) > 0 by A1, JORDAN1K:22;
consider p1, p2 being Point of (TOP-REAL 2) such that
A4: p1,p2 realize-max-dist-in C by Th1;
reconsider g = AffineMap (1,(- (p1 `1)),1,(- (p1 `2))) as being_homeomorphism Function of (TOP-REAL 2),(TOP-REAL 2) by JGRAPH_7:50;
set D = g .: C;
set q1 = g . p1;
set q2 = g . p2;
set arg = Arg (((g . p2) `1) + (((g . p2) `2) * <i>));
reconsider qq = ((g . p2) `1) + (((g . p2) `2) * <i>) as Element of COMPLEX by XCMPLX_0:def 2;
set h = Rotate (- (Arg (((g . p2) `1) + (((g . p2) `2) * <i>))));
A5: Rotate (- (Arg (((g . p2) `1) + (((g . p2) `2) * <i>)))) = Rotate ((2 * PI) - (Arg (((g . p2) `1) + (((g . p2) `2) * <i>)))) by Th6;
g . p1,g . p2 realize-max-dist-in g .: C by A4, Th3;
then A6: (Rotate ((2 * PI) - (Arg (((g . p2) `1) + (((g . p2) `2) * <i>))))) . (g . p1),(Rotate ((2 * PI) - (Arg (((g . p2) `1) + (((g . p2) `2) * <i>))))) . (g . p2) realize-max-dist-in (Rotate ((2 * PI) - (Arg (((g . p2) `1) + (((g . p2) `2) * <i>))))) .: (g .: C) by Th4;
reconsider h0 = Rotate (- (Arg (((g . p2) `1) + (((g . p2) `2) * <i>)))) as onto isometric Function of (TopSpaceMetr (Euclid 2)),(TopSpaceMetr (Euclid 2)) by Lm1, Th2;
A7: Rotate (z,(- (Arg (((g . p2) `1) + (((g . p2) `2) * <i>))))) = 0 by COMPLEX2:52;
h0 is being_homeomorphism ;
then reconsider h = Rotate (- (Arg (((g . p2) `1) + (((g . p2) `2) * <i>)))) as being_homeomorphism Function of (TOP-REAL 2),(TOP-REAL 2) by Lm1, Lm4;
set F = h .: (g .: C);
set s1 = h . (g . p1);
set s2 = h . (g . p2);
g . p1 = |[((1 * (p1 `1)) + (- (p1 `1))),((1 * (p1 `2)) + (- (p1 `2)))]| by JGRAPH_2:def 2
.= |[0,0]| ;
then A8: h . (g . p1) = |[(Re (Rotate (((|[0,0]| `1) + ((|[0,0]| `2) * <i>)),(- (Arg (((g . p2) `1) + (((g . p2) `2) * <i>))))))),(Im (Rotate (((|[0,0]| `1) + ((|[0,0]| `2) * <i>)),(- (Arg (((g . p2) `1) + (((g . p2) `2) * <i>)))))))]| by Def3
.= |[(Re (Rotate ((0 + ((|[0,0]| `2) * <i>)),(- (Arg (((g . p2) `1) + (((g . p2) `2) * <i>))))))),(Im (Rotate (((|[0,0]| `1) + ((|[0,0]| `2) * <i>)),(- (Arg (((g . p2) `1) + (((g . p2) `2) * <i>)))))))]| by EUCLID:52
.= |[(Re (Rotate ((0 + (0 * <i>)),(- (Arg (((g . p2) `1) + (((g . p2) `2) * <i>))))))),(Im (Rotate (((|[0,0]| `1) + ((|[0,0]| `2) * <i>)),(- (Arg (((g . p2) `1) + (((g . p2) `2) * <i>)))))))]| by EUCLID:52
.= |[(Re (Rotate ((0 + (0 * <i>)),(- (Arg (((g . p2) `1) + (((g . p2) `2) * <i>))))))),(Im (Rotate ((0 + ((|[0,0]| `2) * <i>)),(- (Arg (((g . p2) `1) + (((g . p2) `2) * <i>)))))))]| by EUCLID:52
.= |[0,0]| by A7, COMPLEX1:4, EUCLID:52 ;
Rotate (qq,(- (Arg (((g . p2) `1) + (((g . p2) `2) * <i>))))) = |.(((g . p2) `1) + (((g . p2) `2) * <i>)).| + (0 * <i>) by COMPLEX2:55;
then A9: h . (g . p2) = |[(Re (|.(((g . p2) `1) + (((g . p2) `2) * <i>)).| + (0 * <i>))),(Im (|.(((g . p2) `1) + (((g . p2) `2) * <i>)).| + (0 * <i>)))]| by Def3
.= |[|.(((g . p2) `1) + (((g . p2) `2) * <i>)).|,(Im (|.(((g . p2) `1) + (((g . p2) `2) * <i>)).| + (0 * <i>)))]| by COMPLEX1:12
.= |[|.(((g . p2) `1) + (((g . p2) `2) * <i>)).|,0]| by COMPLEX1:12 ;
then A10: (h . (g . p2)) `2 = 0 by EUCLID:52;
dist (p1,p2) >= dist (x,y) by A4, A2;
then A11: p1 <> p2 by A3, TOPREAL6:93;
A12: now :: thesis: not (h . (g . p2)) `1 = 0
dom g = the carrier of (TOP-REAL 2) by FUNCT_2:def 1;
then A13: g . p1 <> g . p2 by A11, FUNCT_1:def 4;
assume A14: (h . (g . p2)) `1 = 0 ; :: thesis: contradiction
dom h = the carrier of (TOP-REAL 2) by FUNCT_2:def 1;
then h . (g . p1) <> h . (g . p2) by A13, FUNCT_1:def 4;
hence contradiction by A8, A9, A14, EUCLID:52; :: thesis: verum
end;
(h . (g . p2)) `1 = |.(((g . p2) `1) + (((g . p2) `2) * <i>)).| by A9, EUCLID:52;
then (h . (g . p2)) `1 >= 0 by COMPLEX1:46;
then reconsider j = AffineMap ((2 / ((h . (g . p2)) `1)),(- 1),(2 / ((h . (g . p2)) `1)),0) as being_homeomorphism Function of (TOP-REAL 2),(TOP-REAL 2) by A12, JGRAPH_7:50;
set E = j .: (h .: (g .: C));
set r1 = j . (h . (g . p1));
set r2 = j . (h . (g . p2));
A15: j . (h . (g . p2)) = |[(((2 / ((h . (g . p2)) `1)) * ((h . (g . p2)) `1)) + (- 1)),(((2 / ((h . (g . p2)) `1)) * ((h . (g . p2)) `2)) + 0)]| by JGRAPH_2:def 2
.= |[(2 + (- 1)),(((2 / ((h . (g . p2)) `1)) * ((h . (g . p2)) `2)) + 0)]| by A12, XCMPLX_1:87
.= |[1,0]| by A10 ;
set f = j * (h * g);
h * g is being_homeomorphism by TOPS_2:57;
then j * (h * g) is being_homeomorphism by TOPS_2:57;
then reconsider f = j * (h * g) as Homeomorphism of TOP-REAL 2 by TOPGRP_1:def 4;
take f ; :: thesis: |[(- 1),0]|,|[1,0]| realize-max-dist-in f .: C
(h * g) .: C = h .: (g .: C) by RELAT_1:126;
then A16: f .: C = j .: (h .: (g .: C)) by RELAT_1:126;
j . (h . (g . p1)) = |[(((2 / ((h . (g . p2)) `1)) * ((h . (g . p1)) `1)) + (- 1)),(((2 / ((h . (g . p2)) `1)) * ((h . (g . p1)) `2)) + 0)]| by JGRAPH_2:def 2
.= |[(((2 / ((h . (g . p2)) `1)) * 0) + (- 1)),(((2 / ((h . (g . p2)) `1)) * ((h . (g . p1)) `2)) + 0)]| by A8, EUCLID:52
.= |[(- 1),0]| by A8, EUCLID:52 ;
hence |[(- 1),0]|,|[1,0]| realize-max-dist-in f .: C by A5, A15, A16, A6, Th3; :: thesis: verum