let a, b, r be Real; :: thesis: for Cb being Subset of (TOP-REAL 2) st r > 0 & Cb = { p where p is Point of (TOP-REAL 2) : |.(p - |[a,b]|).| = r } holds

Cb is being_simple_closed_curve

let Cb be Subset of (TOP-REAL 2); :: thesis: ( r > 0 & Cb = { p where p is Point of (TOP-REAL 2) : |.(p - |[a,b]|).| = r } implies Cb is being_simple_closed_curve )

assume that

A1: r > 0 and

A2: Cb = { p where p is Point of (TOP-REAL 2) : |.(p - |[a,b]|).| = r } ; :: thesis: Cb is being_simple_closed_curve

A3: |[r,0]| `1 = r by EUCLID:52;

A4: |[r,0]| `2 = 0 by EUCLID:52;

|.(|[(r + a),b]| - |[a,b]|).| = |.(|[(r + a),(0 + b)]| - |[a,b]|).|

.= |.((|[r,0]| + |[a,b]|) - |[a,b]|).| by EUCLID:56

.= |.(|[r,0]| + (|[a,b]| - |[a,b]|)).| by RLVECT_1:def 3

.= |.(|[r,0]| + (0. (TOP-REAL 2))).| by RLVECT_1:5

.= |.|[r,0]|.| by RLVECT_1:4

.= sqrt ((r ^2) + (0 ^2)) by A3, A4, JGRAPH_3:1

.= r by A1, SQUARE_1:22 ;

then |[(r + a),b]| in Cb by A2;

then reconsider Cbb = Cb as non empty Subset of (TOP-REAL 2) ;

set v = |[1,0]|;

A5: |[1,0]| `1 = 1 by EUCLID:52;

|[1,0]| `2 = 0 by EUCLID:52;

then |.|[1,0]|.| = sqrt ((1 ^2) + (0 ^2)) by A5, JGRAPH_3:1

.= 1 by SQUARE_1:22 ;

then A6: |[1,0]| in { q where q is Point of (TOP-REAL 2) : |.q.| = 1 } ;

defpred S_{1}[ Point of (TOP-REAL 2)] means |.$1.| = 1;

{ q where q is Element of (TOP-REAL 2) : S_{1}[q] } is Subset of (TOP-REAL 2)
from DOMAIN_1:sch 7();

then reconsider Kb = { q where q is Point of (TOP-REAL 2) : |.q.| = 1 } as non empty Subset of (TOP-REAL 2) by A6;

A7: the carrier of ((TOP-REAL 2) | Kb) = Kb by PRE_TOPC:8;

set SC = AffineMap (r,a,r,b);

A8: AffineMap (r,a,r,b) is one-to-one by A1, JGRAPH_2:44;

A9: dom (AffineMap (r,a,r,b)) = the carrier of (TOP-REAL 2) by FUNCT_2:def 1;

A10: dom ((AffineMap (r,a,r,b)) | Kb) = (dom (AffineMap (r,a,r,b))) /\ Kb by RELAT_1:61

.= the carrier of ((TOP-REAL 2) | Kb) by A7, A9, XBOOLE_1:28 ;

A11: rng ((AffineMap (r,a,r,b)) | Kb) c= ((AffineMap (r,a,r,b)) | Kb) .: the carrier of ((TOP-REAL 2) | Kb)

.= Cb by A1, A2, Th20

.= the carrier of ((TOP-REAL 2) | Cbb) by PRE_TOPC:8 ;

then reconsider f0 = (AffineMap (r,a,r,b)) | Kb as Function of ((TOP-REAL 2) | Kb),((TOP-REAL 2) | Cbb) by A10, A11, FUNCT_2:2;

rng ((AffineMap (r,a,r,b)) | Kb) c= the carrier of (TOP-REAL 2) ;

then reconsider f00 = f0 as Function of ((TOP-REAL 2) | Kb),(TOP-REAL 2) by A10, FUNCT_2:2;

A12: rng f0 = ((AffineMap (r,a,r,b)) | Kb) .: the carrier of ((TOP-REAL 2) | Kb) by RELSET_1:22

.= (AffineMap (r,a,r,b)) .: Kb by A7, RELAT_1:129

.= Cb by A1, A2, Th20 ;

A13: f0 is one-to-one by A8, FUNCT_1:52;

Kb is compact by Th22, JGRAPH_3:26;

then ex f1 being Function of ((TOP-REAL 2) | Kb),((TOP-REAL 2) | Cbb) st

( f00 = f1 & f1 is being_homeomorphism ) by A12, A13, JGRAPH_1:46, TOPMETR:7;

hence Cb is being_simple_closed_curve by Th21, JGRAPH_3:26; :: thesis: verum

Cb is being_simple_closed_curve

let Cb be Subset of (TOP-REAL 2); :: thesis: ( r > 0 & Cb = { p where p is Point of (TOP-REAL 2) : |.(p - |[a,b]|).| = r } implies Cb is being_simple_closed_curve )

assume that

A1: r > 0 and

A2: Cb = { p where p is Point of (TOP-REAL 2) : |.(p - |[a,b]|).| = r } ; :: thesis: Cb is being_simple_closed_curve

A3: |[r,0]| `1 = r by EUCLID:52;

A4: |[r,0]| `2 = 0 by EUCLID:52;

|.(|[(r + a),b]| - |[a,b]|).| = |.(|[(r + a),(0 + b)]| - |[a,b]|).|

.= |.((|[r,0]| + |[a,b]|) - |[a,b]|).| by EUCLID:56

.= |.(|[r,0]| + (|[a,b]| - |[a,b]|)).| by RLVECT_1:def 3

.= |.(|[r,0]| + (0. (TOP-REAL 2))).| by RLVECT_1:5

.= |.|[r,0]|.| by RLVECT_1:4

.= sqrt ((r ^2) + (0 ^2)) by A3, A4, JGRAPH_3:1

.= r by A1, SQUARE_1:22 ;

then |[(r + a),b]| in Cb by A2;

then reconsider Cbb = Cb as non empty Subset of (TOP-REAL 2) ;

set v = |[1,0]|;

A5: |[1,0]| `1 = 1 by EUCLID:52;

|[1,0]| `2 = 0 by EUCLID:52;

then |.|[1,0]|.| = sqrt ((1 ^2) + (0 ^2)) by A5, JGRAPH_3:1

.= 1 by SQUARE_1:22 ;

then A6: |[1,0]| in { q where q is Point of (TOP-REAL 2) : |.q.| = 1 } ;

defpred S

{ q where q is Element of (TOP-REAL 2) : S

then reconsider Kb = { q where q is Point of (TOP-REAL 2) : |.q.| = 1 } as non empty Subset of (TOP-REAL 2) by A6;

A7: the carrier of ((TOP-REAL 2) | Kb) = Kb by PRE_TOPC:8;

set SC = AffineMap (r,a,r,b);

A8: AffineMap (r,a,r,b) is one-to-one by A1, JGRAPH_2:44;

A9: dom (AffineMap (r,a,r,b)) = the carrier of (TOP-REAL 2) by FUNCT_2:def 1;

A10: dom ((AffineMap (r,a,r,b)) | Kb) = (dom (AffineMap (r,a,r,b))) /\ Kb by RELAT_1:61

.= the carrier of ((TOP-REAL 2) | Kb) by A7, A9, XBOOLE_1:28 ;

A11: rng ((AffineMap (r,a,r,b)) | Kb) c= ((AffineMap (r,a,r,b)) | Kb) .: the carrier of ((TOP-REAL 2) | Kb)

proof

((AffineMap (r,a,r,b)) | Kb) .: the carrier of ((TOP-REAL 2) | Kb) =
(AffineMap (r,a,r,b)) .: Kb
by A7, RELAT_1:129
let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in rng ((AffineMap (r,a,r,b)) | Kb) or u in ((AffineMap (r,a,r,b)) | Kb) .: the carrier of ((TOP-REAL 2) | Kb) )

assume u in rng ((AffineMap (r,a,r,b)) | Kb) ; :: thesis: u in ((AffineMap (r,a,r,b)) | Kb) .: the carrier of ((TOP-REAL 2) | Kb)

then ex z being object st

( z in dom ((AffineMap (r,a,r,b)) | Kb) & u = ((AffineMap (r,a,r,b)) | Kb) . z ) by FUNCT_1:def 3;

hence u in ((AffineMap (r,a,r,b)) | Kb) .: the carrier of ((TOP-REAL 2) | Kb) by A10, FUNCT_1:def 6; :: thesis: verum

end;assume u in rng ((AffineMap (r,a,r,b)) | Kb) ; :: thesis: u in ((AffineMap (r,a,r,b)) | Kb) .: the carrier of ((TOP-REAL 2) | Kb)

then ex z being object st

( z in dom ((AffineMap (r,a,r,b)) | Kb) & u = ((AffineMap (r,a,r,b)) | Kb) . z ) by FUNCT_1:def 3;

hence u in ((AffineMap (r,a,r,b)) | Kb) .: the carrier of ((TOP-REAL 2) | Kb) by A10, FUNCT_1:def 6; :: thesis: verum

.= Cb by A1, A2, Th20

.= the carrier of ((TOP-REAL 2) | Cbb) by PRE_TOPC:8 ;

then reconsider f0 = (AffineMap (r,a,r,b)) | Kb as Function of ((TOP-REAL 2) | Kb),((TOP-REAL 2) | Cbb) by A10, A11, FUNCT_2:2;

rng ((AffineMap (r,a,r,b)) | Kb) c= the carrier of (TOP-REAL 2) ;

then reconsider f00 = f0 as Function of ((TOP-REAL 2) | Kb),(TOP-REAL 2) by A10, FUNCT_2:2;

A12: rng f0 = ((AffineMap (r,a,r,b)) | Kb) .: the carrier of ((TOP-REAL 2) | Kb) by RELSET_1:22

.= (AffineMap (r,a,r,b)) .: Kb by A7, RELAT_1:129

.= Cb by A1, A2, Th20 ;

A13: f0 is one-to-one by A8, FUNCT_1:52;

Kb is compact by Th22, JGRAPH_3:26;

then ex f1 being Function of ((TOP-REAL 2) | Kb),((TOP-REAL 2) | Cbb) st

( f00 = f1 & f1 is being_homeomorphism ) by A12, A13, JGRAPH_1:46, TOPMETR:7;

hence Cb is being_simple_closed_curve by Th21, JGRAPH_3:26; :: thesis: verum