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

(AffineMap (r,a,r,b)) .: Kb = Cb

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

assume A1: ( r >= 0 & Kb = { q where q is Point of (TOP-REAL 2) : |.q.| = 1 } & Cb = { p2 where p2 is Point of (TOP-REAL 2) : |.(p2 - |[a,b]|).| = r } ) ; :: thesis: (AffineMap (r,a,r,b)) .: Kb = Cb

reconsider rr = r as Real ;

A2: (AffineMap (r,a,r,b)) .: Kb c= Cb

(AffineMap (r,a,r,b)) .: Kb = Cb

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

assume A1: ( r >= 0 & Kb = { q where q is Point of (TOP-REAL 2) : |.q.| = 1 } & Cb = { p2 where p2 is Point of (TOP-REAL 2) : |.(p2 - |[a,b]|).| = r } ) ; :: thesis: (AffineMap (r,a,r,b)) .: Kb = Cb

reconsider rr = r as Real ;

A2: (AffineMap (r,a,r,b)) .: Kb c= Cb

proof

Cb c= (AffineMap (r,a,r,b)) .: Kb
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in (AffineMap (r,a,r,b)) .: Kb or y in Cb )

assume y in (AffineMap (r,a,r,b)) .: Kb ; :: thesis: y in Cb

then consider x being object such that

x in dom (AffineMap (r,a,r,b)) and

A3: x in Kb and

A4: y = (AffineMap (r,a,r,b)) . x by FUNCT_1:def 6;

consider p being Point of (TOP-REAL 2) such that

A5: x = p and

A6: |.p.| = 1 by A1, A3;

A7: (AffineMap (r,a,r,b)) . p = |[((r * (p `1)) + a),((r * (p `2)) + b)]| by JGRAPH_2:def 2;

then reconsider q = y as Point of (TOP-REAL 2) by A4, A5;

A8: q - |[a,b]| = |[(((r * (p `1)) + a) - a),(((r * (p `2)) + b) - b)]| by A4, A5, A7, EUCLID:62

.= r * |[(p `1),(p `2)]| by EUCLID:58

.= r * p by EUCLID:53 ;

|.(r * p).| = |.rr.| * |.p.| by TOPRNS_1:7

.= r by A1, A6, ABSVALUE:def 1 ;

hence y in Cb by A1, A8; :: thesis: verum

end;assume y in (AffineMap (r,a,r,b)) .: Kb ; :: thesis: y in Cb

then consider x being object such that

x in dom (AffineMap (r,a,r,b)) and

A3: x in Kb and

A4: y = (AffineMap (r,a,r,b)) . x by FUNCT_1:def 6;

consider p being Point of (TOP-REAL 2) such that

A5: x = p and

A6: |.p.| = 1 by A1, A3;

A7: (AffineMap (r,a,r,b)) . p = |[((r * (p `1)) + a),((r * (p `2)) + b)]| by JGRAPH_2:def 2;

then reconsider q = y as Point of (TOP-REAL 2) by A4, A5;

A8: q - |[a,b]| = |[(((r * (p `1)) + a) - a),(((r * (p `2)) + b) - b)]| by A4, A5, A7, EUCLID:62

.= r * |[(p `1),(p `2)]| by EUCLID:58

.= r * p by EUCLID:53 ;

|.(r * p).| = |.rr.| * |.p.| by TOPRNS_1:7

.= r by A1, A6, ABSVALUE:def 1 ;

hence y in Cb by A1, A8; :: thesis: verum

proof

hence
(AffineMap (r,a,r,b)) .: Kb = Cb
by A2; :: thesis: verum
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in Cb or y in (AffineMap (r,a,r,b)) .: Kb )

assume y in Cb ; :: thesis: y in (AffineMap (r,a,r,b)) .: Kb

then consider p2 being Point of (TOP-REAL 2) such that

A9: y = p2 and

A10: |.(p2 - |[a,b]|).| = r by A1;

end;assume y in Cb ; :: thesis: y in (AffineMap (r,a,r,b)) .: Kb

then consider p2 being Point of (TOP-REAL 2) such that

A9: y = p2 and

A10: |.(p2 - |[a,b]|).| = r by A1;

now :: thesis: ( ( r > 0 & y in (AffineMap (r,a,r,b)) .: Kb ) or ( r = 0 & y in (AffineMap (r,a,r,b)) .: Kb ) )end;

hence
y in (AffineMap (r,a,r,b)) .: Kb
; :: thesis: verumper cases
( r > 0 or r = 0 )
by A1;

end;

case A11:
r > 0
; :: thesis: y in (AffineMap (r,a,r,b)) .: Kb

set p1 = (1 / r) * (p2 - |[a,b]|);

|.((1 / r) * (p2 - |[a,b]|)).| = |.(1 / rr).| * |.(p2 - |[a,b]|).| by TOPRNS_1:7

.= (1 / r) * r by A10, ABSVALUE:def 1

.= 1 by A11, XCMPLX_1:87 ;

then A12: (1 / r) * (p2 - |[a,b]|) in Kb by A1;

A13: (1 / r) * (p2 - |[a,b]|) = |[((1 / r) * ((p2 - |[a,b]|) `1)),((1 / r) * ((p2 - |[a,b]|) `2))]| by EUCLID:57;

then A14: ((1 / r) * (p2 - |[a,b]|)) `1 = (1 / r) * ((p2 - |[a,b]|) `1) by EUCLID:52;

A15: ((1 / r) * (p2 - |[a,b]|)) `2 = (1 / r) * ((p2 - |[a,b]|) `2) by A13, EUCLID:52;

A16: r * (((1 / r) * (p2 - |[a,b]|)) `1) = (r * (1 / r)) * ((p2 - |[a,b]|) `1) by A14

.= 1 * ((p2 - |[a,b]|) `1) by A11, XCMPLX_1:87

.= (p2 `1) - (|[a,b]| `1) by TOPREAL3:3

.= (p2 `1) - a by EUCLID:52 ;

A17: r * (((1 / r) * (p2 - |[a,b]|)) `2) = (r * (1 / r)) * ((p2 - |[a,b]|) `2) by A15

.= 1 * ((p2 - |[a,b]|) `2) by A11, XCMPLX_1:87

.= (p2 `2) - (|[a,b]| `2) by TOPREAL3:3

.= (p2 `2) - b by EUCLID:52 ;

A18: (AffineMap (r,a,r,b)) . ((1 / r) * (p2 - |[a,b]|)) = |[((r * (((1 / r) * (p2 - |[a,b]|)) `1)) + a),((r * (((1 / r) * (p2 - |[a,b]|)) `2)) + b)]| by JGRAPH_2:def 2

.= p2 by A16, A17, EUCLID:53 ;

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

hence y in (AffineMap (r,a,r,b)) .: Kb by A9, A12, A18, FUNCT_1:def 6; :: thesis: verum

end;|.((1 / r) * (p2 - |[a,b]|)).| = |.(1 / rr).| * |.(p2 - |[a,b]|).| by TOPRNS_1:7

.= (1 / r) * r by A10, ABSVALUE:def 1

.= 1 by A11, XCMPLX_1:87 ;

then A12: (1 / r) * (p2 - |[a,b]|) in Kb by A1;

A13: (1 / r) * (p2 - |[a,b]|) = |[((1 / r) * ((p2 - |[a,b]|) `1)),((1 / r) * ((p2 - |[a,b]|) `2))]| by EUCLID:57;

then A14: ((1 / r) * (p2 - |[a,b]|)) `1 = (1 / r) * ((p2 - |[a,b]|) `1) by EUCLID:52;

A15: ((1 / r) * (p2 - |[a,b]|)) `2 = (1 / r) * ((p2 - |[a,b]|) `2) by A13, EUCLID:52;

A16: r * (((1 / r) * (p2 - |[a,b]|)) `1) = (r * (1 / r)) * ((p2 - |[a,b]|) `1) by A14

.= 1 * ((p2 - |[a,b]|) `1) by A11, XCMPLX_1:87

.= (p2 `1) - (|[a,b]| `1) by TOPREAL3:3

.= (p2 `1) - a by EUCLID:52 ;

A17: r * (((1 / r) * (p2 - |[a,b]|)) `2) = (r * (1 / r)) * ((p2 - |[a,b]|) `2) by A15

.= 1 * ((p2 - |[a,b]|) `2) by A11, XCMPLX_1:87

.= (p2 `2) - (|[a,b]| `2) by TOPREAL3:3

.= (p2 `2) - b by EUCLID:52 ;

A18: (AffineMap (r,a,r,b)) . ((1 / r) * (p2 - |[a,b]|)) = |[((r * (((1 / r) * (p2 - |[a,b]|)) `1)) + a),((r * (((1 / r) * (p2 - |[a,b]|)) `2)) + b)]| by JGRAPH_2:def 2

.= p2 by A16, A17, EUCLID:53 ;

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

hence y in (AffineMap (r,a,r,b)) .: Kb by A9, A12, A18, FUNCT_1:def 6; :: thesis: verum

case A19:
r = 0
; :: thesis: y in (AffineMap (r,a,r,b)) .: Kb

set p1 = |[1,0]|;

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

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

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

.= 1 by SQUARE_1:22 ;

then A21: |[1,0]| in Kb by A1;

A22: (AffineMap (r,a,r,b)) . |[1,0]| = |[((0 * (|[1,0]| `1)) + a),((0 * (|[1,0]| `2)) + b)]| by A19, JGRAPH_2:def 2

.= p2 by A10, A19, TOPRNS_1:28 ;

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

hence y in (AffineMap (r,a,r,b)) .: Kb by A9, A21, A22, FUNCT_1:def 6; :: thesis: verum

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

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

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

.= 1 by SQUARE_1:22 ;

then A21: |[1,0]| in Kb by A1;

A22: (AffineMap (r,a,r,b)) . |[1,0]| = |[((0 * (|[1,0]| `1)) + a),((0 * (|[1,0]| `2)) + b)]| by A19, JGRAPH_2:def 2

.= p2 by A10, A19, TOPRNS_1:28 ;

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

hence y in (AffineMap (r,a,r,b)) .: Kb by A9, A21, A22, FUNCT_1:def 6; :: thesis: verum