let C be Simple_closed_curve; 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;
(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
; |[(- 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; verum