:: JORDAN24 semantic presentation begin definition let n be Element of NAT ; let A be Subset of (TOP-REAL n); let a, b be Point of (TOP-REAL n); preda,b realize-max-dist-in A means :Def1: :: JORDAN24:def 1 ( a in A & b in A & ( for x, y being Point of (TOP-REAL n) st x in A & y in A holds dist (a,b) >= dist (x,y) ) ); end; :: deftheorem Def1 defines realize-max-dist-in JORDAN24:def_1_:_ for n being Element of NAT for A being Subset of (TOP-REAL n) for a, b being Point of (TOP-REAL n) holds ( a,b realize-max-dist-in A iff ( a in A & b in A & ( for x, y being Point of (TOP-REAL n) st x in A & y in A holds dist (a,b) >= dist (x,y) ) ) ); set rl = - 1; set rp = 1; set a = |[(- 1),0]|; set b = |[1,0]|; Lm1: TopStruct(# the carrier of (TOP-REAL 2), the topology of (TOP-REAL 2) #) = TopSpaceMetr (Euclid 2) by EUCLID:def_8; theorem Th1: :: JORDAN24:1 for C being non empty compact Subset of (TOP-REAL 2) ex p1, p2 being Point of (TOP-REAL 2) st p1,p2 realize-max-dist-in C proof let C be non empty compact Subset of (TOP-REAL 2); ::_thesis: ex p1, p2 being Point of (TOP-REAL 2) st p1,p2 realize-max-dist-in C reconsider D = C as Subset of (TopSpaceMetr (Euclid 2)) by Lm1; A1: D is compact by Lm1, COMPTS_1:23; then consider x1, x2 being Point of (Euclid 2) such that A2: ( x1 in D & x2 in D ) and A3: dist (x1,x2) = max_dist_max (D,D) by WEIERSTR:33; reconsider a = x1, b = x2 as Point of (TOP-REAL 2) by EUCLID:67; take a ; ::_thesis: ex p2 being Point of (TOP-REAL 2) st a,p2 realize-max-dist-in C take b ; ::_thesis: a,b realize-max-dist-in C thus ( a in C & b in C ) by A2; :: according to JORDAN24:def_1 ::_thesis: for x, y being Point of (TOP-REAL 2) st x in C & y in C holds dist (a,b) >= dist (x,y) let x, y be Point of (TOP-REAL 2); ::_thesis: ( x in C & y in C implies dist (a,b) >= dist (x,y) ) assume A4: ( x in C & y in C ) ; ::_thesis: dist (a,b) >= dist (x,y) reconsider x9 = x, y9 = y as Point of (Euclid 2) by EUCLID:67; dist (x9,y9) <= max_dist_max (D,D) by A1, A4, WEIERSTR:34; then dist (x,y) <= max_dist_max (D,D) by TOPREAL6:def_1; hence dist (a,b) >= dist (x,y) by A3, TOPREAL6:def_1; ::_thesis: verum end; definition let M be non empty MetrStruct ; let f be Function of (TopSpaceMetr M),(TopSpaceMetr M); attrf is isometric means :Def2: :: JORDAN24:def 2 ex g being isometric Function of M,M st g = f; end; :: deftheorem Def2 defines isometric JORDAN24:def_2_:_ for M being non empty MetrStruct for f being Function of (TopSpaceMetr M),(TopSpaceMetr M) holds ( f is isometric iff ex g being isometric Function of M,M st g = f ); registration let M be non empty MetrStruct ; cluster non empty V16() V19( the carrier of (TopSpaceMetr M)) V20( the carrier of (TopSpaceMetr M)) Function-like V26( the carrier of (TopSpaceMetr M)) quasi_total onto isometric for Element of K6(K7( the carrier of (TopSpaceMetr M), the carrier of (TopSpaceMetr M))); existence ex b1 being Function of (TopSpaceMetr M),(TopSpaceMetr M) st ( b1 is onto & b1 is isometric ) proof set f = the onto isometric Function of M,M; reconsider f = the onto isometric Function of M,M as Function of (TopSpaceMetr M),(TopSpaceMetr M) ; take f ; ::_thesis: ( f is onto & f is isometric ) thus ( f is onto & f is isometric ) by Def2; ::_thesis: verum end; end; registration let M be non empty MetrSpace; cluster Function-like quasi_total isometric -> continuous for Element of K6(K7( the carrier of (TopSpaceMetr M), the carrier of (TopSpaceMetr M))); coherence for b1 being Function of (TopSpaceMetr M),(TopSpaceMetr M) st b1 is isometric holds b1 is continuous proof let f be Function of (TopSpaceMetr M),(TopSpaceMetr M); ::_thesis: ( f is isometric implies f is continuous ) assume f is isometric ; ::_thesis: f is continuous then consider g being isometric Function of M,M such that A1: g = f by Def2; let W be Point of (TopSpaceMetr M); :: according to BORSUK_1:def_1 ::_thesis: for b1 being a_neighborhood of f . W ex b2 being a_neighborhood of W st f .: b2 c= b1 let G be a_neighborhood of f . W; ::_thesis: ex b1 being a_neighborhood of W st f .: b1 c= G reconsider fw = f . W, w = W as Point of M ; f . W in Int G by CONNSP_2:def_1; then consider r being real number such that A2: r > 0 and A3: Ball (fw,r) c= G by GOBOARD6:4; reconsider H = Ball (w,r) as a_neighborhood of W by A2, GOBOARD6:91; take H ; ::_thesis: f .: H c= G thus f .: H c= G ::_thesis: verum proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in f .: H or a in G ) assume a in f .: H ; ::_thesis: a in G then consider b being set such that A4: b in dom f and A5: b in H and A6: f . b = a by FUNCT_1:def_6; reconsider b = b as Point of (TopSpaceMetr M) by A4; reconsider b9 = b as Point of M ; dist (b9,w) < r by A5, METRIC_1:11; then dist ((g . b9),fw) < r by A1, VECTMETR:def_3; then a in Ball (fw,r) by A1, A6, METRIC_1:11; hence a in G by A3; ::_thesis: verum end; end; end; registration let M be non empty MetrSpace; cluster Function-like quasi_total onto isometric -> being_homeomorphism for Element of K6(K7( the carrier of (TopSpaceMetr M), the carrier of (TopSpaceMetr M))); coherence for b1 being Function of (TopSpaceMetr M),(TopSpaceMetr M) st b1 is onto & b1 is isometric holds b1 is being_homeomorphism proof let f be Function of (TopSpaceMetr M),(TopSpaceMetr M); ::_thesis: ( f is onto & f is isometric implies f is being_homeomorphism ) assume A1: ( f is onto & f is isometric ) ; ::_thesis: f is being_homeomorphism then reconsider f1 = f as onto isometric Function of (TopSpaceMetr M),(TopSpaceMetr M) ; thus dom f = [#] (TopSpaceMetr M) by FUNCT_2:def_1; :: according to TOPS_2:def_5 ::_thesis: ( rng f = [#] (TopSpaceMetr M) & f is one-to-one & f is continuous & f " is continuous ) consider g being isometric Function of M,M such that A2: g = f by A1, Def2; g is onto by A1, A2; hence rng f = [#] (TopSpaceMetr M) by A2, FUNCT_2:def_3; ::_thesis: ( f is one-to-one & f is continuous & f " is continuous ) thus f is one-to-one by A2; ::_thesis: ( f is continuous & f " is continuous ) f1 is continuous ; hence f is continuous ; ::_thesis: f " is continuous f " is isometric Function of (TopSpaceMetr M),(TopSpaceMetr M) by A1, A2, Def2; hence f " is continuous ; ::_thesis: verum end; end; definition let a be Real; func Rotate a -> Function of (TOP-REAL 2),(TOP-REAL 2) means :Def3: :: JORDAN24:def 3 for p being Point of (TOP-REAL 2) holds it . p = |[(Re (Rotate (((p `1) + ((p `2) * )),a))),(Im (Rotate (((p `1) + ((p `2) * )),a)))]|; existence ex b1 being Function of (TOP-REAL 2),(TOP-REAL 2) st for p being Point of (TOP-REAL 2) holds b1 . p = |[(Re (Rotate (((p `1) + ((p `2) * )),a))),(Im (Rotate (((p `1) + ((p `2) * )),a)))]| proof deffunc H1( Point of (TOP-REAL 2)) -> Element of the carrier of (TOP-REAL 2) = |[(Re (Rotate (((\$1 `1) + ((\$1 `2) * )),a))),(Im (Rotate (((\$1 `1) + ((\$1 `2) * )),a)))]|; consider f being Function of (TOP-REAL 2),(TOP-REAL 2) such that A1: for p being Point of (TOP-REAL 2) holds f . p = H1(p) from FUNCT_2:sch_4(); take f ; ::_thesis: for p being Point of (TOP-REAL 2) holds f . p = |[(Re (Rotate (((p `1) + ((p `2) * )),a))),(Im (Rotate (((p `1) + ((p `2) * )),a)))]| thus for p being Point of (TOP-REAL 2) holds f . p = |[(Re (Rotate (((p `1) + ((p `2) * )),a))),(Im (Rotate (((p `1) + ((p `2) * )),a)))]| by A1; ::_thesis: verum end; uniqueness for b1, b2 being Function of (TOP-REAL 2),(TOP-REAL 2) st ( for p being Point of (TOP-REAL 2) holds b1 . p = |[(Re (Rotate (((p `1) + ((p `2) * )),a))),(Im (Rotate (((p `1) + ((p `2) * )),a)))]| ) & ( for p being Point of (TOP-REAL 2) holds b2 . p = |[(Re (Rotate (((p `1) + ((p `2) * )),a))),(Im (Rotate (((p `1) + ((p `2) * )),a)))]| ) holds b1 = b2 proof let f, g be Function of (TOP-REAL 2),(TOP-REAL 2); ::_thesis: ( ( for p being Point of (TOP-REAL 2) holds f . p = |[(Re (Rotate (((p `1) + ((p `2) * )),a))),(Im (Rotate (((p `1) + ((p `2) * )),a)))]| ) & ( for p being Point of (TOP-REAL 2) holds g . p = |[(Re (Rotate (((p `1) + ((p `2) * )),a))),(Im (Rotate (((p `1) + ((p `2) * )),a)))]| ) implies f = g ) assume that A2: for p being Point of (TOP-REAL 2) holds f . p = |[(Re (Rotate (((p `1) + ((p `2) * )),a))),(Im (Rotate (((p `1) + ((p `2) * )),a)))]| and A3: for p being Point of (TOP-REAL 2) holds g . p = |[(Re (Rotate (((p `1) + ((p `2) * )),a))),(Im (Rotate (((p `1) + ((p `2) * )),a)))]| ; ::_thesis: f = g now__::_thesis:_for_p_being_Point_of_(TOP-REAL_2)_holds_f_._p_=_g_._p let p be Point of (TOP-REAL 2); ::_thesis: f . p = g . p thus f . p = |[(Re (Rotate (((p `1) + ((p `2) * )),a))),(Im (Rotate (((p `1) + ((p `2) * )),a)))]| by A2 .= g . p by A3 ; ::_thesis: verum end; hence f = g by FUNCT_2:63; ::_thesis: verum end; end; :: deftheorem Def3 defines Rotate JORDAN24:def_3_:_ for a being Real for b2 being Function of (TOP-REAL 2),(TOP-REAL 2) holds ( b2 = Rotate a iff for p being Point of (TOP-REAL 2) holds b2 . p = |[(Re (Rotate (((p `1) + ((p `2) * )),a))),(Im (Rotate (((p `1) + ((p `2) * )),a)))]| ); Lm2: now__::_thesis:_for_a_being_Real for_c_being_complex_number_ for_i_being_integer_number_holds_Rotate_(c,a)_=_Rotate_(c,(a_+_((2_*_PI)_*_i))) let a be Real; ::_thesis: for c being complex number for i being integer number holds Rotate (c,a) = Rotate (c,(a + ((2 * PI) * i))) let c be complex number ; ::_thesis: for i being integer number holds Rotate (c,a) = Rotate (c,(a + ((2 * PI) * i))) let i be integer number ; ::_thesis: Rotate (c,a) = Rotate (c,(a + ((2 * PI) * i))) cos (a + (Arg c)) = cos ((a + (Arg c)) + ((2 * PI) * i)) by COMPLEX2:9; hence Rotate (c,a) = Rotate (c,(a + ((2 * PI) * i))) by COMPLEX2:8; ::_thesis: verum end; Lm3: now__::_thesis:_for_a_being_Real for_i_being_integer_number_holds_Rotate_a_=_Rotate_(a_+_((2_*_PI)_*_i)) let a be Real; ::_thesis: for i being integer number holds Rotate a = Rotate (a + ((2 * PI) * i)) let i be integer number ; ::_thesis: Rotate a = Rotate (a + ((2 * PI) * i)) thus Rotate a = Rotate (a + ((2 * PI) * i)) ::_thesis: verum proof let p be Point of (TOP-REAL 2); :: according to FUNCT_2:def_8 ::_thesis: (Rotate a) . p = (Rotate (a + ((2 * PI) * i))) . p set q = (p `1) + ((p `2) * ); A1: Rotate (((p `1) + ((p `2) * )),a) = Rotate (((p `1) + ((p `2) * )),(a + ((2 * PI) * i))) by Lm2; thus (Rotate a) . p = |[(Re (Rotate (((p `1) + ((p `2) * )),a))),(Im (Rotate (((p `1) + ((p `2) * )),a)))]| by Def3 .= (Rotate (a + ((2 * PI) * i))) . p by A1, Def3 ; ::_thesis: verum end; end; theorem Th2: :: JORDAN24:2 for a being Real for f being Function of (TopSpaceMetr (Euclid 2)),(TopSpaceMetr (Euclid 2)) st f = Rotate a holds ( f is onto & f is isometric ) proof let a be Real; ::_thesis: for f being Function of (TopSpaceMetr (Euclid 2)),(TopSpaceMetr (Euclid 2)) st f = Rotate a holds ( f is onto & f is isometric ) consider A being real number such that A1: A = ((2 * PI) * (- [\(a / (2 * PI))/])) + a and A2: 0 <= A and A3: A < 2 * PI by COMPLEX2:1; reconsider A = A as Real by XREAL_0:def_1; let f be Function of (TopSpaceMetr (Euclid 2)),(TopSpaceMetr (Euclid 2)); ::_thesis: ( f = Rotate a implies ( f is onto & f is isometric ) ) assume A4: f = Rotate a ; ::_thesis: ( f is onto & f is isometric ) reconsider g = f as Function of (Euclid 2),(Euclid 2) ; A5: Rotate A = Rotate a by A1, Lm3; ( g is onto & g is isometric ) proof thus rng g = the carrier of (Euclid 2) :: according to FUNCT_2:def_3 ::_thesis: g is isometric proof thus rng g c= the carrier of (Euclid 2) ; :: according to XBOOLE_0:def_10 ::_thesis: the carrier of (Euclid 2) c= rng g let o be set ; :: according to TARSKI:def_3 ::_thesis: ( not o in the carrier of (Euclid 2) or o in rng g ) assume o in the carrier of (Euclid 2) ; ::_thesis: o in rng g then reconsider p = o as Point of (TOP-REAL 2) by EUCLID:67; set pz = (p `1) + ((p `2) * ); reconsider pz = (p `1) + ((p `2) * ) as Element of COMPLEX by XCMPLX_0:def_2; set arg = Arg pz; percases ( pz <> 0 or pz = 0 ) ; supposeA6: pz <> 0 ; ::_thesis: o in rng g percases ( A <= Arg pz or A > Arg pz ) ; suppose A <= Arg pz ; ::_thesis: o in rng g then A7: 0 <= (Arg pz) - A by XREAL_1:48; set qz = Rotate (pz,(- A)); A8: |.(Rotate (pz,(- A))).| = |.pz.| by COMPLEX2:53; ( (Arg pz) - A <= Arg pz & Arg pz < 2 * PI ) by A2, COMPTRIG:34, XREAL_1:43; then A9: (- A) + (Arg pz) < 2 * PI by XXREAL_0:2; Rotate (pz,(- A)) <> 0 by A6, COMPLEX2:52; then Arg (Rotate (pz,(- A))) = (- A) + (Arg pz) by A7, A9, A8, COMPTRIG:def_1; then A10: Rotate ((Rotate (pz,(- A))),A) = pz by A8, COMPLEX2:12; set q = |[(Re (Rotate (pz,(- A)))),(Im (Rotate (pz,(- A))))]|; A11: dom g = the carrier of (Euclid 2) by FUNCT_2:def_1; g . |[(Re (Rotate (pz,(- A)))),(Im (Rotate (pz,(- A))))]| = |[(Re (Rotate (((|[(Re (Rotate (pz,(- A)))),(Im (Rotate (pz,(- A))))]| `1) + ((|[(Re (Rotate (pz,(- A)))),(Im (Rotate (pz,(- A))))]| `2) * )),A))),(Im (Rotate (((|[(Re (Rotate (pz,(- A)))),(Im (Rotate (pz,(- A))))]| `1) + ((|[(Re (Rotate (pz,(- A)))),(Im (Rotate (pz,(- A))))]| `2) * )),A)))]| by A4, A5, Def3 .= |[(Re (Rotate (((Re (Rotate (pz,(- A)))) + ((|[(Re (Rotate (pz,(- A)))),(Im (Rotate (pz,(- A))))]| `2) * )),A))),(Im (Rotate (((|[(Re (Rotate (pz,(- A)))),(Im (Rotate (pz,(- A))))]| `1) + ((|[(Re (Rotate (pz,(- A)))),(Im (Rotate (pz,(- A))))]| `2) * )),A)))]| by EUCLID:52 .= |[(Re (Rotate (((Re (Rotate (pz,(- A)))) + ((Im (Rotate (pz,(- A)))) * )),A))),(Im (Rotate (((|[(Re (Rotate (pz,(- A)))),(Im (Rotate (pz,(- A))))]| `1) + ((|[(Re (Rotate (pz,(- A)))),(Im (Rotate (pz,(- A))))]| `2) * )),A)))]| by EUCLID:52 .= |[(Re (Rotate (((Re (Rotate (pz,(- A)))) + ((Im (Rotate (pz,(- A)))) * )),A))),(Im (Rotate (((Re (Rotate (pz,(- A)))) + ((|[(Re (Rotate (pz,(- A)))),(Im (Rotate (pz,(- A))))]| `2) * )),A)))]| by EUCLID:52 .= |[(Re (Rotate (((Re (Rotate (pz,(- A)))) + ((Im (Rotate (pz,(- A)))) * )),A))),(Im (Rotate (((Re (Rotate (pz,(- A)))) + ((Im (Rotate (pz,(- A)))) * )),A)))]| by EUCLID:52 .= |[(Re (Rotate ((Rotate (pz,(- A))),A))),(Im (Rotate (((Re (Rotate (pz,(- A)))) + ((Im (Rotate (pz,(- A)))) * )),A)))]| by COMPLEX1:13 .= |[(Re pz),(Im pz)]| by A10, COMPLEX1:13 .= |[(p `1),(Im pz)]| by COMPLEX1:12 .= |[(p `1),(p `2)]| by COMPLEX1:12 .= p by EUCLID:53 ; hence o in rng g by A11, Lm1, FUNCT_1:def_3; ::_thesis: verum end; suppose A > Arg pz ; ::_thesis: o in rng g then (Arg pz) - A < 0 by XREAL_1:49; then A12: (2 * PI) + ((Arg pz) - A) < 2 * PI by XREAL_1:30; set qz = Rotate (pz,(- A)); set q = |[(Re (Rotate (pz,(- A)))),(Im (Rotate (pz,(- A))))]|; A13: dom g = the carrier of (Euclid 2) by FUNCT_2:def_1; A14: |.(Rotate (pz,(- A))).| = |.pz.| by COMPLEX2:53; then Rotate (pz,(- A)) = (|.(Rotate (pz,(- A))).| * (cos (((2 * PI) * 1) + ((- A) + (Arg pz))))) + ((|.(Rotate (pz,(- A))).| * (sin ((- A) + (Arg pz)))) * ) by COMPLEX2:9; then A15: Rotate (pz,(- A)) = (|.(Rotate (pz,(- A))).| * (cos ((2 * PI) + ((Arg pz) - A)))) + ((|.(Rotate (pz,(- A))).| * (sin (((2 * PI) * 1) + ((- A) + (Arg pz))))) * ) by COMPLEX2:8; ( 0 <= (2 * PI) - A & Arg pz >= 0 ) by A3, COMPTRIG:34, XREAL_1:48; then A16: 0 <= ((2 * PI) - A) + (Arg pz) ; Rotate (pz,(- A)) <> 0 by A6, COMPLEX2:52; then Arg (Rotate (pz,(- A))) = (2 * PI) + ((Arg pz) - A) by A16, A12, A15, COMPTRIG:def_1; then Rotate ((Rotate (pz,(- A))),A) = (|.(Rotate (pz,(- A))).| * (cos (Arg pz))) + ((|.(Rotate (pz,(- A))).| * (sin (((2 * PI) * 1) + (Arg pz)))) * ) by COMPLEX2:9; then Rotate ((Rotate (pz,(- A))),A) = (|.(Rotate (pz,(- A))).| * (cos (Arg pz))) + ((|.(Rotate (pz,(- A))).| * (sin (Arg pz))) * ) by COMPLEX2:8; then A17: Rotate ((Rotate (pz,(- A))),A) = pz by A14, COMPLEX2:12; g . |[(Re (Rotate (pz,(- A)))),(Im (Rotate (pz,(- A))))]| = |[(Re (Rotate (((|[(Re (Rotate (pz,(- A)))),(Im (Rotate (pz,(- A))))]| `1) + ((|[(Re (Rotate (pz,(- A)))),(Im (Rotate (pz,(- A))))]| `2) * )),A))),(Im (Rotate (((|[(Re (Rotate (pz,(- A)))),(Im (Rotate (pz,(- A))))]| `1) + ((|[(Re (Rotate (pz,(- A)))),(Im (Rotate (pz,(- A))))]| `2) * )),A)))]| by A4, A5, Def3 .= |[(Re (Rotate (((Re (Rotate (pz,(- A)))) + ((|[(Re (Rotate (pz,(- A)))),(Im (Rotate (pz,(- A))))]| `2) * )),A))),(Im (Rotate (((|[(Re (Rotate (pz,(- A)))),(Im (Rotate (pz,(- A))))]| `1) + ((|[(Re (Rotate (pz,(- A)))),(Im (Rotate (pz,(- A))))]| `2) * )),A)))]| by EUCLID:52 .= |[(Re (Rotate (((Re (Rotate (pz,(- A)))) + ((Im (Rotate (pz,(- A)))) * )),A))),(Im (Rotate (((|[(Re (Rotate (pz,(- A)))),(Im (Rotate (pz,(- A))))]| `1) + ((|[(Re (Rotate (pz,(- A)))),(Im (Rotate (pz,(- A))))]| `2) * )),A)))]| by EUCLID:52 .= |[(Re (Rotate (((Re (Rotate (pz,(- A)))) + ((Im (Rotate (pz,(- A)))) * )),A))),(Im (Rotate (((Re (Rotate (pz,(- A)))) + ((|[(Re (Rotate (pz,(- A)))),(Im (Rotate (pz,(- A))))]| `2) * )),A)))]| by EUCLID:52 .= |[(Re (Rotate (((Re (Rotate (pz,(- A)))) + ((Im (Rotate (pz,(- A)))) * )),A))),(Im (Rotate (((Re (Rotate (pz,(- A)))) + ((Im (Rotate (pz,(- A)))) * )),A)))]| by EUCLID:52 .= |[(Re (Rotate ((Rotate (pz,(- A))),A))),(Im (Rotate (((Re (Rotate (pz,(- A)))) + ((Im (Rotate (pz,(- A)))) * )),A)))]| by COMPLEX1:13 .= |[(Re pz),(Im pz)]| by A17, COMPLEX1:13 .= |[(p `1),(Im pz)]| by COMPLEX1:12 .= |[(p `1),(p `2)]| by COMPLEX1:12 .= p by EUCLID:53 ; hence o in rng g by A13, Lm1, FUNCT_1:def_3; ::_thesis: verum end; end; end; supposeA18: pz = 0 ; ::_thesis: o in rng g reconsider z = 0 as Element of COMPLEX by XCMPLX_0:def_2; set q = |[0,0]|; A19: dom g = the carrier of (Euclid 2) by FUNCT_2:def_1; A20: p `1 = 0 by A18, COMPLEX1:4, COMPLEX1:12; g . |[0,0]| = |[(Re (Rotate (((|[0,0]| `1) + ((|[0,0]| `2) * )),a))),(Im (Rotate (((|[0,0]| `1) + ((|[0,0]| `2) * )),a)))]| by A4, Def3 .= |[(Re (Rotate ((z + ((|[0,0]| `2) * )),a))),(Im (Rotate (((|[0,0]| `1) + ((|[0,0]| `2) * )),a)))]| by EUCLID:52 .= |[(Re (Rotate ((z + (z * )),a))),(Im (Rotate (((|[0,0]| `1) + ((|[0,0]| `2) * )),a)))]| by EUCLID:52 .= |[(Re (Rotate ((z + (z * )),a))),(Im (Rotate ((z + ((|[0,0]| `2) * )),a)))]| by EUCLID:52 .= |[(Re (Rotate (z,a))),(Im (Rotate (z,a)))]| by EUCLID:52 .= |[(Re z),(Im (Rotate (z,a)))]| by COMPLEX2:52 .= |[(Re z),(Im z)]| by COMPLEX2:52 .= p by A18, A20, COMPLEX1:4, EUCLID:53 ; hence o in rng g by A19, Lm1, FUNCT_1:def_3; ::_thesis: verum end; end; end; let X, Y be Point of (Euclid 2); :: according to VECTMETR:def_3 ::_thesis: dist (X,Y) = dist ((g . X),(g . Y)) reconsider x = X, y = Y, gx = g . X, gy = g . Y as Point of (TOP-REAL 2) by EUCLID:67; A21: ( |[(Re (Rotate (((x `1) + ((x `2) * )),a))),(Im (Rotate (((x `1) + ((x `2) * )),a)))]| `1 = Re (Rotate (((x `1) + ((x `2) * )),a)) & |[(Re (Rotate (((x `1) + ((x `2) * )),a))),(Im (Rotate (((x `1) + ((x `2) * )),a)))]| `2 = Im (Rotate (((x `1) + ((x `2) * )),a)) ) by EUCLID:52; reconsider xx = (x `1) + ((x `2) * ), yy = (y `1) + ((y `2) * ) as Element of COMPLEX by XCMPLX_0:def_2; A22: ( |[(Re (Rotate (((y `1) + ((y `2) * )),a))),(Im (Rotate (((y `1) + ((y `2) * )),a)))]| `1 = Re (Rotate (((y `1) + ((y `2) * )),a)) & |[(Re (Rotate (((y `1) + ((y `2) * )),a))),(Im (Rotate (((y `1) + ((y `2) * )),a)))]| `2 = Im (Rotate (((y `1) + ((y `2) * )),a)) ) by EUCLID:52; A23: ( Re ((y `1) + ((y `2) * )) = y `1 & Im ((y `1) + ((y `2) * )) = y `2 ) by COMPLEX1:12; A24: ((sin a) ^2) + ((cos a) ^2) = 1 by SIN_COS:29; A25: ( Re ((x `1) + ((x `2) * )) = x `1 & Im ((x `1) + ((x `2) * )) = x `2 ) by COMPLEX1:12; ( x = |[(x `1),(x `2)]| & y = |[(y `1),(y `2)]| ) by EUCLID:53; hence dist (X,Y) = sqrt ((((x `1) - (y `1)) ^2) + (((x `2) - (y `2)) ^2)) by GOBOARD6:6 .= sqrt ((((((x `1) * (x `1)) - ((2 * (x `1)) * (y `1))) + ((y `1) * (y `1))) * (((sin a) * (sin a)) + ((cos a) * (cos a)))) + (((((x `2) * (x `2)) - ((2 * (x `2)) * (y `2))) + ((y `2) * (y `2))) * (((sin a) ^2) + ((cos a) ^2)))) by A24 .= sqrt ((((((x `1) * (cos a)) - ((x `2) * (sin a))) - (((y `1) * (cos a)) - ((y `2) * (sin a)))) ^2) + ((((((x `1) * (sin a)) + ((x `2) * (cos a))) ^2) - ((2 * (((x `1) * (sin a)) + ((x `2) * (cos a)))) * (((y `1) * (sin a)) + ((y `2) * (cos a))))) + ((((y `1) * (sin a)) + ((y `2) * (cos a))) ^2))) .= sqrt ((((Re (Rotate (xx,a))) - (((y `1) * (cos a)) - ((y `2) * (sin a)))) ^2) + (((((x `1) * (sin a)) + ((x `2) * (cos a))) - (((y `1) * (sin a)) + ((y `2) * (cos a)))) ^2)) by A25, COMPLEX2:56 .= sqrt ((((Re (Rotate (xx,a))) - (((y `1) * (cos a)) - ((y `2) * (sin a)))) ^2) + (((Im (Rotate (xx,a))) - (((y `1) * (sin a)) + ((y `2) * (cos a)))) ^2)) by A25, COMPLEX2:56 .= sqrt ((((Re (Rotate (xx,a))) - (Re (Rotate (yy,a)))) ^2) + (((Im (Rotate (xx,a))) - (((y `1) * (sin a)) + ((y `2) * (cos a)))) ^2)) by A23, COMPLEX2:56 .= sqrt ((((Re (Rotate (xx,a))) - (Re (Rotate (yy,a)))) ^2) + (((Im (Rotate (xx,a))) - (Im (Rotate (yy,a)))) ^2)) by A23, COMPLEX2:56 .= dist (|[(Re (Rotate (((x `1) + ((x `2) * )),a))),(Im (Rotate (((x `1) + ((x `2) * )),a)))]|,|[(Re (Rotate (((y `1) + ((y `2) * )),a))),(Im (Rotate (((y `1) + ((y `2) * )),a)))]|) by A21, A22, TOPREAL6:92 .= dist (|[(Re (Rotate (((x `1) + ((x `2) * )),a))),(Im (Rotate (((x `1) + ((x `2) * )),a)))]|,gy) by A4, Def3 .= dist (gx,gy) by A4, Def3 .= dist ((g . X),(g . Y)) by TOPREAL6:def_1 ; ::_thesis: verum end; hence ( f is onto & f is isometric ) by Def2; ::_thesis: verum end; theorem Th3: :: JORDAN24:3 for p1, p2 being Point of (TOP-REAL 2) for P being Subset of (TOP-REAL 2) for A, B, D being real number st p1,p2 realize-max-dist-in P holds (AffineMap (A,B,A,D)) . p1,(AffineMap (A,B,A,D)) . p2 realize-max-dist-in (AffineMap (A,B,A,D)) .: P proof let p1, p2 be Point of (TOP-REAL 2); ::_thesis: for P being Subset of (TOP-REAL 2) for A, B, D being real number st p1,p2 realize-max-dist-in P holds (AffineMap (A,B,A,D)) . p1,(AffineMap (A,B,A,D)) . p2 realize-max-dist-in (AffineMap (A,B,A,D)) .: P let P be Subset of (TOP-REAL 2); ::_thesis: for A, B, D being real number st p1,p2 realize-max-dist-in P holds (AffineMap (A,B,A,D)) . p1,(AffineMap (A,B,A,D)) . p2 realize-max-dist-in (AffineMap (A,B,A,D)) .: P let A, B, D be real number ; ::_thesis: ( p1,p2 realize-max-dist-in P implies (AffineMap (A,B,A,D)) . p1,(AffineMap (A,B,A,D)) . p2 realize-max-dist-in (AffineMap (A,B,A,D)) .: P ) set a = p1; set b = p2; set C = P; A1: dom (AffineMap (A,B,A,D)) = the carrier of (TOP-REAL 2) by FUNCT_2:def_1; assume A2: p1,p2 realize-max-dist-in P ; ::_thesis: (AffineMap (A,B,A,D)) . p1,(AffineMap (A,B,A,D)) . p2 realize-max-dist-in (AffineMap (A,B,A,D)) .: P then p1 in P by Def1; hence (AffineMap (A,B,A,D)) . p1 in (AffineMap (A,B,A,D)) .: P by A1, FUNCT_1:def_6; :: according to JORDAN24:def_1 ::_thesis: ( (AffineMap (A,B,A,D)) . p2 in (AffineMap (A,B,A,D)) .: P & ( for x, y being Point of (TOP-REAL 2) st x in (AffineMap (A,B,A,D)) .: P & y in (AffineMap (A,B,A,D)) .: P holds dist (((AffineMap (A,B,A,D)) . p1),((AffineMap (A,B,A,D)) . p2)) >= dist (x,y) ) ) p2 in P by A2, Def1; hence (AffineMap (A,B,A,D)) . p2 in (AffineMap (A,B,A,D)) .: P by A1, FUNCT_1:def_6; ::_thesis: for x, y being Point of (TOP-REAL 2) st x in (AffineMap (A,B,A,D)) .: P & y in (AffineMap (A,B,A,D)) .: P holds dist (((AffineMap (A,B,A,D)) . p1),((AffineMap (A,B,A,D)) . p2)) >= dist (x,y) let x, y be Point of (TOP-REAL 2); ::_thesis: ( x in (AffineMap (A,B,A,D)) .: P & y in (AffineMap (A,B,A,D)) .: P implies dist (((AffineMap (A,B,A,D)) . p1),((AffineMap (A,B,A,D)) . p2)) >= dist (x,y) ) assume x in (AffineMap (A,B,A,D)) .: P ; ::_thesis: ( not y in (AffineMap (A,B,A,D)) .: P or dist (((AffineMap (A,B,A,D)) . p1),((AffineMap (A,B,A,D)) . p2)) >= dist (x,y) ) then consider X being set such that A3: X in dom (AffineMap (A,B,A,D)) and A4: X in P and A5: (AffineMap (A,B,A,D)) . X = x by FUNCT_1:def_6; reconsider X = X as Point of (TOP-REAL 2) by A3; assume y in (AffineMap (A,B,A,D)) .: P ; ::_thesis: dist (((AffineMap (A,B,A,D)) . p1),((AffineMap (A,B,A,D)) . p2)) >= dist (x,y) then consider Y being set such that A6: Y in dom (AffineMap (A,B,A,D)) and A7: Y in P and A8: (AffineMap (A,B,A,D)) . Y = y by FUNCT_1:def_6; reconsider Y = Y as Point of (TOP-REAL 2) by A6; A9: ( ((X `1) - (Y `1)) ^2 >= 0 & ((X `2) - (Y `2)) ^2 >= 0 ) by XREAL_1:63; A10: ( ((p1 `1) - (p2 `1)) ^2 >= 0 & ((p1 `2) - (p2 `2)) ^2 >= 0 ) by XREAL_1:63; A11: A ^2 >= 0 by XREAL_1:63; then A12: sqrt (A ^2) >= 0 by SQUARE_1:def_2; A13: dist (((AffineMap (A,B,A,D)) . p1),((AffineMap (A,B,A,D)) . p2)) = dist (|[((A * (p1 `1)) + B),((A * (p1 `2)) + D)]|,((AffineMap (A,B,A,D)) . p2)) by JGRAPH_2:def_2 .= dist (|[((A * (p1 `1)) + B),((A * (p1 `2)) + D)]|,|[((A * (p2 `1)) + B),((A * (p2 `2)) + D)]|) by JGRAPH_2:def_2 .= sqrt ((((|[((A * (p1 `1)) + B),((A * (p1 `2)) + D)]| `1) - (|[((A * (p2 `1)) + B),((A * (p2 `2)) + D)]| `1)) ^2) + (((|[((A * (p1 `1)) + B),((A * (p1 `2)) + D)]| `2) - (|[((A * (p2 `1)) + B),((A * (p2 `2)) + D)]| `2)) ^2)) by TOPREAL6:92 .= sqrt (((((A * (p1 `1)) + B) - (|[((A * (p2 `1)) + B),((A * (p2 `2)) + D)]| `1)) ^2) + (((|[((A * (p1 `1)) + B),((A * (p1 `2)) + D)]| `2) - (|[((A * (p2 `1)) + B),((A * (p2 `2)) + D)]| `2)) ^2)) by EUCLID:52 .= sqrt (((((A * (p1 `1)) + B) - ((A * (p2 `1)) + B)) ^2) + (((|[((A * (p1 `1)) + B),((A * (p1 `2)) + D)]| `2) - (|[((A * (p2 `1)) + B),((A * (p2 `2)) + D)]| `2)) ^2)) by EUCLID:52 .= sqrt (((((A * (p1 `1)) + B) - ((A * (p2 `1)) + B)) ^2) + ((((A * (p1 `2)) + D) - (|[((A * (p2 `1)) + B),((A * (p2 `2)) + D)]| `2)) ^2)) by EUCLID:52 .= sqrt (((((A * (p1 `1)) + B) - ((A * (p2 `1)) + B)) ^2) + ((((A * (p1 `2)) + D) - ((A * (p2 `2)) + D)) ^2)) by EUCLID:52 .= sqrt ((A ^2) * ((((p1 `1) - (p2 `1)) ^2) + (((p1 `2) - (p2 `2)) ^2))) .= (sqrt (A ^2)) * (sqrt ((((p1 `1) - (p2 `1)) ^2) + (((p1 `2) - (p2 `2)) ^2))) by A11, A10, SQUARE_1:29 .= (sqrt (A ^2)) * (dist (p1,p2)) by TOPREAL6:92 ; A14: dist (x,y) = dist (|[((A * (X `1)) + B),((A * (X `2)) + D)]|,((AffineMap (A,B,A,D)) . Y)) by A5, A8, JGRAPH_2:def_2 .= dist (|[((A * (X `1)) + B),((A * (X `2)) + D)]|,|[((A * (Y `1)) + B),((A * (Y `2)) + D)]|) by JGRAPH_2:def_2 .= sqrt ((((|[((A * (X `1)) + B),((A * (X `2)) + D)]| `1) - (|[((A * (Y `1)) + B),((A * (Y `2)) + D)]| `1)) ^2) + (((|[((A * (X `1)) + B),((A * (X `2)) + D)]| `2) - (|[((A * (Y `1)) + B),((A * (Y `2)) + D)]| `2)) ^2)) by TOPREAL6:92 .= sqrt (((((A * (X `1)) + B) - (|[((A * (Y `1)) + B),((A * (Y `2)) + D)]| `1)) ^2) + (((|[((A * (X `1)) + B),((A * (X `2)) + D)]| `2) - (|[((A * (Y `1)) + B),((A * (Y `2)) + D)]| `2)) ^2)) by EUCLID:52 .= sqrt (((((A * (X `1)) + B) - ((A * (Y `1)) + B)) ^2) + (((|[((A * (X `1)) + B),((A * (X `2)) + D)]| `2) - (|[((A * (Y `1)) + B),((A * (Y `2)) + D)]| `2)) ^2)) by EUCLID:52 .= sqrt (((((A * (X `1)) + B) - ((A * (Y `1)) + B)) ^2) + ((((A * (X `2)) + D) - (|[((A * (Y `1)) + B),((A * (Y `2)) + D)]| `2)) ^2)) by EUCLID:52 .= sqrt (((((A * (X `1)) + B) - ((A * (Y `1)) + B)) ^2) + ((((A * (X `2)) + D) - ((A * (Y `2)) + D)) ^2)) by EUCLID:52 .= sqrt ((A ^2) * ((((X `1) - (Y `1)) ^2) + (((X `2) - (Y `2)) ^2))) .= (sqrt (A ^2)) * (sqrt ((((X `1) - (Y `1)) ^2) + (((X `2) - (Y `2)) ^2))) by A11, A9, SQUARE_1:29 .= (sqrt (A ^2)) * (dist (X,Y)) by TOPREAL6:92 ; dist (p1,p2) >= dist (X,Y) by A2, A4, A7, Def1; hence dist (((AffineMap (A,B,A,D)) . p1),((AffineMap (A,B,A,D)) . p2)) >= dist (x,y) by A13, A14, A12, XREAL_1:64; ::_thesis: verum end; theorem Th4: :: JORDAN24:4 for p1, p2 being Point of (TOP-REAL 2) for P being Subset of (TOP-REAL 2) for A being Real st p1,p2 realize-max-dist-in P holds (Rotate A) . p1,(Rotate A) . p2 realize-max-dist-in (Rotate A) .: P proof let p1, p2 be Point of (TOP-REAL 2); ::_thesis: for P being Subset of (TOP-REAL 2) for A being Real st p1,p2 realize-max-dist-in P holds (Rotate A) . p1,(Rotate A) . p2 realize-max-dist-in (Rotate A) .: P let P be Subset of (TOP-REAL 2); ::_thesis: for A being Real st p1,p2 realize-max-dist-in P holds (Rotate A) . p1,(Rotate A) . p2 realize-max-dist-in (Rotate A) .: P let A be Real; ::_thesis: ( p1,p2 realize-max-dist-in P implies (Rotate A) . p1,(Rotate A) . p2 realize-max-dist-in (Rotate A) .: P ) reconsider f = Rotate A as Function of (TopSpaceMetr (Euclid 2)),(TopSpaceMetr (Euclid 2)) by Lm1; set C = P; A1: dom (Rotate A) = the carrier of (TOP-REAL 2) by FUNCT_2:def_1; assume A2: p1,p2 realize-max-dist-in P ; ::_thesis: (Rotate A) . p1,(Rotate A) . p2 realize-max-dist-in (Rotate A) .: P then ( p1 in P & p2 in P ) by Def1; hence ( (Rotate A) . p1 in (Rotate A) .: P & (Rotate A) . p2 in (Rotate A) .: P ) by A1, FUNCT_1:def_6; :: according to JORDAN24:def_1 ::_thesis: for x, y being Point of (TOP-REAL 2) st x in (Rotate A) .: P & y in (Rotate A) .: P holds dist (((Rotate A) . p1),((Rotate A) . p2)) >= dist (x,y) let x, y be Point of (TOP-REAL 2); ::_thesis: ( x in (Rotate A) .: P & y in (Rotate A) .: P implies dist (((Rotate A) . p1),((Rotate A) . p2)) >= dist (x,y) ) assume that A3: x in (Rotate A) .: P and A4: y in (Rotate A) .: P ; ::_thesis: dist (((Rotate A) . p1),((Rotate A) . p2)) >= dist (x,y) f is isometric by Th2; then consider g being isometric Function of (Euclid 2),(Euclid 2) such that A5: f = g by Def2; consider yy being set such that A6: yy in dom (Rotate A) and A7: yy in P and A8: (Rotate A) . yy = y by A4, FUNCT_1:def_6; reconsider yy = yy as Point of (TOP-REAL 2) by A6; consider xx being set such that A9: xx in dom (Rotate A) and A10: xx in P and A11: (Rotate A) . xx = x by A3, FUNCT_1:def_6; reconsider xx = xx as Point of (TOP-REAL 2) by A9; reconsider p19 = p1, p29 = p2, xx9 = xx, yy9 = yy as Point of (Euclid 2) by EUCLID:67; dist (p1,p2) >= dist (xx,yy) by A2, A10, A7, Def1; then dist (p19,p29) >= dist (xx,yy) by TOPREAL6:def_1; then dist (p19,p29) >= dist (xx9,yy9) by TOPREAL6:def_1; then dist ((g . p19),(g . p29)) >= dist (xx9,yy9) by VECTMETR:def_3; then dist ((g . p19),(g . p29)) >= dist ((g . xx9),(g . yy9)) by VECTMETR:def_3; then dist (((Rotate A) . p1),((Rotate A) . p2)) >= dist ((g . xx9),(g . yy9)) by A5, TOPREAL6:def_1; hence dist (((Rotate A) . p1),((Rotate A) . p2)) >= dist (x,y) by A11, A8, A5, TOPREAL6:def_1; ::_thesis: verum end; theorem Th5: :: JORDAN24:5 for z being complex number for r being Real holds Rotate (z,(- r)) = Rotate (z,((2 * PI) - r)) proof let z be complex number ; ::_thesis: for r being Real holds Rotate (z,(- r)) = Rotate (z,((2 * PI) - r)) let r be Real; ::_thesis: Rotate (z,(- r)) = Rotate (z,((2 * PI) - r)) thus Rotate (z,(- r)) = (|.z.| * (cos (((2 * PI) * 1) + ((- r) + (Arg z))))) + ((|.z.| * (sin ((- r) + (Arg z)))) * ) by COMPLEX2:9 .= Rotate (z,((2 * PI) - r)) by COMPLEX2:8 ; ::_thesis: verum end; theorem Th6: :: JORDAN24:6 for r being Real holds Rotate (- r) = Rotate ((2 * PI) - r) proof let r be Real; ::_thesis: Rotate (- r) = Rotate ((2 * PI) - r) now__::_thesis:_for_p_being_Point_of_(TOP-REAL_2)_holds_(Rotate_((2_*_PI)_-_r))_._p_=_|[(Re_(Rotate_(((p_`1)_+_((p_`2)_*_)),(-_r)))),(Im_(Rotate_(((p_`1)_+_((p_`2)_*_)),(-_r))))]| let p be Point of (TOP-REAL 2); ::_thesis: (Rotate ((2 * PI) - r)) . p = |[(Re (Rotate (((p `1) + ((p `2) * )),(- r)))),(Im (Rotate (((p `1) + ((p `2) * )),(- r))))]| thus (Rotate ((2 * PI) - r)) . p = |[(Re (Rotate (((p `1) + ((p `2) * )),((2 * PI) - r)))),(Im (Rotate (((p `1) + ((p `2) * )),((2 * PI) - r))))]| by Def3 .= |[(Re (Rotate (((p `1) + ((p `2) * )),(- r)))),(Im (Rotate (((p `1) + ((p `2) * )),((2 * PI) - r))))]| by Th5 .= |[(Re (Rotate (((p `1) + ((p `2) * )),(- r)))),(Im (Rotate (((p `1) + ((p `2) * )),(- r))))]| by Th5 ; ::_thesis: verum end; hence Rotate (- r) = Rotate ((2 * PI) - r) by Def3; ::_thesis: verum end; Lm4: for T1, T2 being TopSpace for f being Function of T1,T2 for g being Function of TopStruct(# the carrier of T1, the topology of T1 #),TopStruct(# the carrier of T2, the topology of T2 #) st g = f & g is being_homeomorphism holds f is being_homeomorphism proof let T1, T2 be TopSpace; ::_thesis: for f being Function of T1,T2 for g being Function of TopStruct(# the carrier of T1, the topology of T1 #),TopStruct(# the carrier of T2, the topology of T2 #) st g = f & g is being_homeomorphism holds f is being_homeomorphism let f be Function of T1,T2; ::_thesis: for g being Function of TopStruct(# the carrier of T1, the topology of T1 #),TopStruct(# the carrier of T2, the topology of T2 #) st g = f & g is being_homeomorphism holds f is being_homeomorphism let g be Function of TopStruct(# the carrier of T1, the topology of T1 #),TopStruct(# the carrier of T2, the topology of T2 #); ::_thesis: ( g = f & g is being_homeomorphism implies f is being_homeomorphism ) assume that A1: g = f and A2: g is being_homeomorphism ; ::_thesis: f is being_homeomorphism ( dom f = [#] TopStruct(# the carrier of T1, the topology of T1 #) & rng f = [#] TopStruct(# the carrier of T2, the topology of T2 #) ) by A1, A2, TOPS_2:def_5; hence ( dom f = [#] T1 & rng f = [#] T2 ) ; :: according to TOPS_2:def_5 ::_thesis: ( f is one-to-one & f is continuous & f " is continuous ) thus f is one-to-one by A1, A2; ::_thesis: ( f is continuous & f " is continuous ) thus f is continuous by A1, A2, PRE_TOPC:34; ::_thesis: f " is continuous g " is continuous by A2, TOPS_2:def_5; hence f " is continuous by A1, PRE_TOPC:34; ::_thesis: verum end; theorem :: JORDAN24:7 for C being Simple_closed_curve ex f being Homeomorphism of TOP-REAL 2 st |[(- 1),0]|,|[1,0]| realize-max-dist-in f .: C proof 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) * )); reconsider qq = ((g . p2) `1) + (((g . p2) `2) * ) as Element of COMPLEX by XCMPLX_0:def_2; set h = Rotate (- (Arg (((g . p2) `1) + (((g . p2) `2) * )))); A5: Rotate (- (Arg (((g . p2) `1) + (((g . p2) `2) * )))) = Rotate ((2 * PI) - (Arg (((g . p2) `1) + (((g . p2) `2) * )))) 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) * ))))) . (g . p1),(Rotate ((2 * PI) - (Arg (((g . p2) `1) + (((g . p2) `2) * ))))) . (g . p2) realize-max-dist-in (Rotate ((2 * PI) - (Arg (((g . p2) `1) + (((g . p2) `2) * ))))) .: (g .: C) by Th4; reconsider h0 = Rotate (- (Arg (((g . p2) `1) + (((g . p2) `2) * )))) as onto isometric Function of (TopSpaceMetr (Euclid 2)),(TopSpaceMetr (Euclid 2)) by Lm1, Th2; A7: Rotate (z,(- (Arg (((g . p2) `1) + (((g . p2) `2) * ))))) = 0 by COMPLEX2:52; h0 is being_homeomorphism ; then reconsider h = Rotate (- (Arg (((g . p2) `1) + (((g . p2) `2) * )))) 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) * )),(- (Arg (((g . p2) `1) + (((g . p2) `2) * ))))))),(Im (Rotate (((|[0,0]| `1) + ((|[0,0]| `2) * )),(- (Arg (((g . p2) `1) + (((g . p2) `2) * )))))))]| by Def3 .= |[(Re (Rotate ((0 + ((|[0,0]| `2) * )),(- (Arg (((g . p2) `1) + (((g . p2) `2) * ))))))),(Im (Rotate (((|[0,0]| `1) + ((|[0,0]| `2) * )),(- (Arg (((g . p2) `1) + (((g . p2) `2) * )))))))]| by EUCLID:52 .= |[(Re (Rotate ((0 + (0 * )),(- (Arg (((g . p2) `1) + (((g . p2) `2) * ))))))),(Im (Rotate (((|[0,0]| `1) + ((|[0,0]| `2) * )),(- (Arg (((g . p2) `1) + (((g . p2) `2) * )))))))]| by EUCLID:52 .= |[(Re (Rotate ((0 + (0 * )),(- (Arg (((g . p2) `1) + (((g . p2) `2) * ))))))),(Im (Rotate ((0 + ((|[0,0]| `2) * )),(- (Arg (((g . p2) `1) + (((g . p2) `2) * )))))))]| by EUCLID:52 .= |[0,0]| by A7, COMPLEX1:4, EUCLID:52 ; Rotate (qq,(- (Arg (((g . p2) `1) + (((g . p2) `2) * ))))) = |.(((g . p2) `1) + (((g . p2) `2) * )).| + (0 * ) by COMPLEX2:55; then A9: h . (g . p2) = |[(Re (|.(((g . p2) `1) + (((g . p2) `2) * )).| + (0 * ))),(Im (|.(((g . p2) `1) + (((g . p2) `2) * )).| + (0 * )))]| by Def3 .= |[|.(((g . p2) `1) + (((g . p2) `2) * )).|,(Im (|.(((g . p2) `1) + (((g . p2) `2) * )).| + (0 * )))]| by COMPLEX1:12 .= |[|.(((g . p2) `1) + (((g . p2) `2) * )).|,0]| by COMPLEX1:12 ; then A10: (h . (g . p2)) `2 = 0 by EUCLID:52; dist (p1,p2) >= dist (x,y) by A4, A2, Def1; 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) * )).| 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 end; definition let T1, T2 be TopStruct ; let f be Function of T1,T2; attrf is closed means :: JORDAN24:def 4 for A being Subset of T1 st A is closed holds f .: A is closed ; end; :: deftheorem defines closed JORDAN24:def_4_:_ for T1, T2 being TopStruct for f being Function of T1,T2 holds ( f is closed iff for A being Subset of T1 st A is closed holds f .: A is closed ); theorem :: JORDAN24:8 for X, Y being non empty TopSpace for f being continuous Function of X,Y st f is one-to-one & f is onto holds ( f is being_homeomorphism iff f is closed ) proof let X, Y be non empty TopSpace; ::_thesis: for f being continuous Function of X,Y st f is one-to-one & f is onto holds ( f is being_homeomorphism iff f is closed ) let f be continuous Function of X,Y; ::_thesis: ( f is one-to-one & f is onto implies ( f is being_homeomorphism iff f is closed ) ) assume A1: ( f is one-to-one & f is onto ) ; ::_thesis: ( f is being_homeomorphism iff f is closed ) hereby ::_thesis: ( f is closed implies f is being_homeomorphism ) assume A2: f is being_homeomorphism ; ::_thesis: f is closed thus f is closed ::_thesis: verum proof let A be Subset of X; :: according to JORDAN24:def_4 ::_thesis: ( A is closed implies f .: A is closed ) thus ( A is closed implies f .: A is closed ) by A2, TOPS_2:58; ::_thesis: verum end; end; assume A3: for A being Subset of X st A is closed holds f .: A is closed ; :: according to JORDAN24:def_4 ::_thesis: f is being_homeomorphism A4: ( [#] X = the carrier of X & [#] Y = the carrier of Y ) ; A5: dom f = the carrier of X by FUNCT_2:def_1; A6: now__::_thesis:_for_A_being_Subset_of_X_st_f_.:_A_is_closed_holds_ A_is_closed let A be Subset of X; ::_thesis: ( f .: A is closed implies A is closed ) assume f .: A is closed ; ::_thesis: A is closed then f " (f .: A) is closed by PRE_TOPC:def_6; hence A is closed by A1, A5, FUNCT_1:94; ::_thesis: verum end; rng f = the carrier of Y by A1, FUNCT_2:def_3; hence f is being_homeomorphism by A1, A3, A5, A4, A6, TOPS_2:58; ::_thesis: verum end; theorem Th9: :: JORDAN24:9 for X being set for A being Subset of X holds ( A ` = {} iff A = X ) proof let X be set ; ::_thesis: for A being Subset of X holds ( A ` = {} iff A = X ) let A be Subset of X; ::_thesis: ( A ` = {} iff A = X ) (A `) ` = A ; hence ( A ` = {} iff A = X ) by XBOOLE_1:37; ::_thesis: verum end; theorem :: JORDAN24:10 for T1, T2 being non empty TopSpace for f being Function of T1,T2 st f is being_homeomorphism holds for A being Subset of T1 st A is connected holds f .: A is connected by TOPS_2:61; theorem Th11: :: JORDAN24:11 for T1, T2 being non empty TopSpace for f being Function of T1,T2 st f is being_homeomorphism holds for A being Subset of T1 st A is a_component holds f .: A is a_component proof let T1, T2 be non empty TopSpace; ::_thesis: for f being Function of T1,T2 st f is being_homeomorphism holds for A being Subset of T1 st A is a_component holds f .: A is a_component let f be Function of T1,T2; ::_thesis: ( f is being_homeomorphism implies for A being Subset of T1 st A is a_component holds f .: A is a_component ) assume A1: f is being_homeomorphism ; ::_thesis: for A being Subset of T1 st A is a_component holds f .: A is a_component let A be Subset of T1; ::_thesis: ( A is a_component implies f .: A is a_component ) assume that A2: A is connected and A3: for B being Subset of T1 st B is connected & A c= B holds A = B ; :: according to CONNSP_1:def_5 ::_thesis: f .: A is a_component thus f .: A is connected by A1, A2, TOPS_2:61; :: according to CONNSP_1:def_5 ::_thesis: for b1 being Element of K6( the carrier of T2) holds ( not b1 is connected or not f .: A c= b1 or f .: A = b1 ) let B be Subset of T2; ::_thesis: ( not B is connected or not f .: A c= B or f .: A = B ) [#] T2 = the carrier of T2 ; then rng f = the carrier of T2 by A1, TOPS_2:def_5; then A4: f .: (f " B) = B by FUNCT_1:77; dom f = the carrier of T1 by FUNCT_2:def_1; then A5: f " (f .: A) = A by A1, FUNCT_1:94; assume that A6: B is connected and A7: f .: A c= B ; ::_thesis: f .: A = B f " B is connected by A1, A6, TOPS_2:62; hence f .: A = B by A3, A4, A5, A7, RELAT_1:143; ::_thesis: verum end; theorem Th12: :: JORDAN24:12 for T1, T2 being non empty TopSpace for f being Function of T1,T2 for A being Subset of T1 holds f | A is Function of (T1 | A),(T2 | (f .: A)) proof let T1, T2 be non empty TopSpace; ::_thesis: for f being Function of T1,T2 for A being Subset of T1 holds f | A is Function of (T1 | A),(T2 | (f .: A)) let f be Function of T1,T2; ::_thesis: for A being Subset of T1 holds f | A is Function of (T1 | A),(T2 | (f .: A)) let A be Subset of T1; ::_thesis: f | A is Function of (T1 | A),(T2 | (f .: A)) A1: rng (f | A) = f .: A by RELAT_1:115; dom f = the carrier of T1 by FUNCT_2:def_1; then A2: dom (f | A) = A by RELAT_1:62; ( [#] (T1 | A) = A & [#] (T2 | (f .: A)) = f .: A ) by PRE_TOPC:def_5; hence f | A is Function of (T1 | A),(T2 | (f .: A)) by A2, A1, FUNCT_2:2; ::_thesis: verum end; theorem Th13: :: JORDAN24:13 for T1, T2 being non empty TopSpace for f being Function of T1,T2 st f is continuous holds for A being Subset of T1 for g being Function of (T1 | A),(T2 | (f .: A)) st g = f | A holds g is continuous proof let T1, T2 be non empty TopSpace; ::_thesis: for f being Function of T1,T2 st f is continuous holds for A being Subset of T1 for g being Function of (T1 | A),(T2 | (f .: A)) st g = f | A holds g is continuous let f be Function of T1,T2; ::_thesis: ( f is continuous implies for A being Subset of T1 for g being Function of (T1 | A),(T2 | (f .: A)) st g = f | A holds g is continuous ) assume A1: f is continuous ; ::_thesis: for A being Subset of T1 for g being Function of (T1 | A),(T2 | (f .: A)) st g = f | A holds g is continuous let A be Subset of T1; ::_thesis: for g being Function of (T1 | A),(T2 | (f .: A)) st g = f | A holds g is continuous let g be Function of (T1 | A),(T2 | (f .: A)); ::_thesis: ( g = f | A implies g is continuous ) assume A2: g = f | A ; ::_thesis: g is continuous A3: dom f = the carrier of T1 by FUNCT_2:def_1; A4: [#] (T1 | A) = A by PRE_TOPC:def_5; percases ( A is empty or not A is empty ) ; suppose A is empty ; ::_thesis: g is continuous hence g is continuous by TIETZE:4; ::_thesis: verum end; suppose not A is empty ; ::_thesis: g is continuous then reconsider S1 = T1 | A, S2 = T2 | (f .: A) as non empty TopSpace by A3; f | A = f | (T1 | A) by A4, TMAP_1:def_3; then A5: g is continuous Function of S1,T2 by A1, A2; g is Function of S1,S2 ; hence g is continuous by A5, JORDAN16:8; ::_thesis: verum end; end; end; theorem Th14: :: JORDAN24:14 for T1, T2 being non empty TopSpace for f being Function of T1,T2 st f is being_homeomorphism holds for A being Subset of T1 for g being Function of (T1 | A),(T2 | (f .: A)) st g = f | A holds g is being_homeomorphism proof let T1, T2 be non empty TopSpace; ::_thesis: for f being Function of T1,T2 st f is being_homeomorphism holds for A being Subset of T1 for g being Function of (T1 | A),(T2 | (f .: A)) st g = f | A holds g is being_homeomorphism let f be Function of T1,T2; ::_thesis: ( f is being_homeomorphism implies for A being Subset of T1 for g being Function of (T1 | A),(T2 | (f .: A)) st g = f | A holds g is being_homeomorphism ) assume that A1: dom f = [#] T1 and A2: rng f = [#] T2 and A3: f is one-to-one and A4: f is continuous and A5: f " is continuous ; :: according to TOPS_2:def_5 ::_thesis: for A being Subset of T1 for g being Function of (T1 | A),(T2 | (f .: A)) st g = f | A holds g is being_homeomorphism let A be Subset of T1; ::_thesis: for g being Function of (T1 | A),(T2 | (f .: A)) st g = f | A holds g is being_homeomorphism f is onto by A2, FUNCT_2:def_3; then A6: f " = f " by A3, TOPS_2:def_4; then A7: (f ") .: (f .: A) = f " (f .: A) by A3, FUNCT_1:85 .= A by A1, A3, FUNCT_1:94 ; A8: dom f = the carrier of T1 by FUNCT_2:def_1; let g be Function of (T1 | A),(T2 | (f .: A)); ::_thesis: ( g = f | A implies g is being_homeomorphism ) assume A9: g = f | A ; ::_thesis: g is being_homeomorphism ( [#] (T1 | A) = A & [#] (T2 | (f .: A)) = f .: A ) by PRE_TOPC:def_5; hence A10: ( dom g = [#] (T1 | A) & rng g = [#] (T2 | (f .: A)) ) by A9, A8, RELAT_1:62, RELAT_1:115; :: according to TOPS_2:def_5 ::_thesis: ( g is one-to-one & g is continuous & g " is continuous ) A11: g is onto by A10, FUNCT_2:def_3; thus g is one-to-one by A3, A9, FUNCT_1:52; ::_thesis: ( g is continuous & g " is continuous ) then A12: g " = g " by A11, TOPS_2:def_4; thus g is continuous by A4, A9, Th13; ::_thesis: g " is continuous g " = (f ") | (f .: A) by A3, A9, A6, A12, RFUNCT_2:17; hence g " is continuous by A5, A7, Th13; ::_thesis: verum end; theorem Th15: :: JORDAN24:15 for T1, T2 being non empty TopSpace for f being Function of T1,T2 st f is being_homeomorphism holds for A, B being Subset of T1 st A is_a_component_of B holds f .: A is_a_component_of f .: B proof let T1, T2 be non empty TopSpace; ::_thesis: for f being Function of T1,T2 st f is being_homeomorphism holds for A, B being Subset of T1 st A is_a_component_of B holds f .: A is_a_component_of f .: B let f be Function of T1,T2; ::_thesis: ( f is being_homeomorphism implies for A, B being Subset of T1 st A is_a_component_of B holds f .: A is_a_component_of f .: B ) assume A1: f is being_homeomorphism ; ::_thesis: for A, B being Subset of T1 st A is_a_component_of B holds f .: A is_a_component_of f .: B let A, B be Subset of T1; ::_thesis: ( A is_a_component_of B implies f .: A is_a_component_of f .: B ) given A1 being Subset of (T1 | B) such that A2: A1 = A and A3: A1 is a_component ; :: according to CONNSP_1:def_6 ::_thesis: f .: A is_a_component_of f .: B A4: [#] (T2 | (f .: B)) = f .: B by PRE_TOPC:def_5; A5: dom f = the carrier of T1 by FUNCT_2:def_1; A6: [#] (T1 | B) = B by PRE_TOPC:def_5; then reconsider A2 = f .: A as Subset of (T2 | (f .: B)) by A2, A4, RELAT_1:123; percases ( B is empty or not B is empty ) ; supposeA7: B is empty ; ::_thesis: f .: A is_a_component_of f .: B then f .: B = {} ; then A8: A2 = {} by A4, XBOOLE_1:3; {} T2 = f .: B by A7; hence f .: A is_a_component_of f .: B by A8, JORDAN1K:6; ::_thesis: verum end; suppose not B is empty ; ::_thesis: f .: A is_a_component_of f .: B then reconsider S1 = T1 | B, S2 = T2 | (f .: B) as non empty TopSpace by A5; take A2 ; :: according to CONNSP_1:def_6 ::_thesis: ( A2 = f .: A & A2 is a_component ) thus A2 = f .: A ; ::_thesis: A2 is a_component reconsider fB = f | B as Function of S1,S2 by Th12; fB .: A = A2 by A2, A6, RELAT_1:129; hence A2 is a_component by A1, A2, A3, Th11, Th14; ::_thesis: verum end; end; end; theorem :: JORDAN24:16 for S being Subset of (TOP-REAL 2) for f being Homeomorphism of TOP-REAL 2 st S is Jordan holds f .: S is Jordan proof let S be Subset of (TOP-REAL 2); ::_thesis: for f being Homeomorphism of TOP-REAL 2 st S is Jordan holds f .: S is Jordan let f be Homeomorphism of TOP-REAL 2; ::_thesis: ( S is Jordan implies f .: S is Jordan ) set s = the Element of S ` ; assume A1: S ` <> {} ; :: according to SPRECT_1:def_3 ::_thesis: ( for b1, b2 being Element of K6( the carrier of (TOP-REAL 2)) holds ( not S ` = b1 \/ b2 or not b1 misses b2 or not (Cl b1) \ b1 = (Cl b2) \ b2 or not b1 is_a_component_of S ` or not b2 is_a_component_of S ` ) or f .: S is Jordan ) then the Element of S ` in S ` ; then reconsider s = the Element of S ` as Element of (TOP-REAL 2) ; given A1, A2 being Subset of (TOP-REAL 2) such that A2: S ` = A1 \/ A2 and A3: A1 misses A2 and A4: (Cl A1) \ A1 = (Cl A2) \ A2 and A5: ( A1 is_a_component_of S ` & A2 is_a_component_of S ` ) ; ::_thesis: f .: S is Jordan A6: not s in S by A1, XBOOLE_0:def_5; hereby :: according to SPRECT_1:def_3 ::_thesis: ex b1, b2 being Element of K6( the carrier of (TOP-REAL 2)) st ( (f .: S) ` = b1 \/ b2 & b1 misses b2 & (Cl b1) \ b1 = (Cl b2) \ b2 & b1 is_a_component_of (f .: S) ` & b2 is_a_component_of (f .: S) ` ) assume (f .: S) ` = {} ; ::_thesis: contradiction then f .: S = the carrier of (TOP-REAL 2) by Th9; then ex s9 being Element of (TOP-REAL 2) st ( s9 in S & f . s = f . s9 ) by FUNCT_2:65; hence contradiction by A6, FUNCT_2:56; ::_thesis: verum end; take B1 = f .: A1; ::_thesis: ex b1 being Element of K6( the carrier of (TOP-REAL 2)) st ( (f .: S) ` = B1 \/ b1 & B1 misses b1 & (Cl B1) \ B1 = (Cl b1) \ b1 & B1 is_a_component_of (f .: S) ` & b1 is_a_component_of (f .: S) ` ) take B2 = f .: A2; ::_thesis: ( (f .: S) ` = B1 \/ B2 & B1 misses B2 & (Cl B1) \ B1 = (Cl B2) \ B2 & B1 is_a_component_of (f .: S) ` & B2 is_a_component_of (f .: S) ` ) f .: (A1 \/ A2) = B1 \/ B2 by RELAT_1:120; hence (f .: S) ` = B1 \/ B2 by A2, JORDAN1K:5; ::_thesis: ( B1 misses B2 & (Cl B1) \ B1 = (Cl B2) \ B2 & B1 is_a_component_of (f .: S) ` & B2 is_a_component_of (f .: S) ` ) thus B1 misses B2 by A3, FUNCT_1:66; ::_thesis: ( (Cl B1) \ B1 = (Cl B2) \ B2 & B1 is_a_component_of (f .: S) ` & B2 is_a_component_of (f .: S) ` ) thus (Cl B1) \ B1 = (f .: (Cl A1)) \ B1 by TOPS_2:60 .= f .: ((Cl A2) \ A2) by A4, FUNCT_1:64 .= (f .: (Cl A2)) \ B2 by FUNCT_1:64 .= (Cl B2) \ B2 by TOPS_2:60 ; ::_thesis: ( B1 is_a_component_of (f .: S) ` & B2 is_a_component_of (f .: S) ` ) f .: (S `) = (f .: S) ` by JORDAN1K:5; hence ( B1 is_a_component_of (f .: S) ` & B2 is_a_component_of (f .: S) ` ) by A5, Th15; ::_thesis: verum end;