let a, b, r be real number ; :: 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 by XREAL_0:def 1;
A2:
(AffineMap r,a,r,b) .: Kb c= Cb
proof
let y be
set ;
:: 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
set such that A3:
(
x in dom (AffineMap r,a,r,b) &
x in Kb &
y = (AffineMap r,a,r,b) . x )
by FUNCT_1:def 12;
consider p being
Point of
(TOP-REAL 2) such that A4:
(
x = p &
|.p.| = 1 )
by A1, A3;
A5:
(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 A3, A4;
A6:
q - |[a,b]| =
|[(((r * (p `1 )) + a) - a),(((r * (p `2 )) + b) - b)]|
by A3, A4, A5, EUCLID:66
.=
r * |[(p `1 ),(p `2 )]|
by EUCLID:62
.=
r * p
by EUCLID:57
;
|.(r * p).| =
(abs rr) * |.p.|
by TOPRNS_1:8
.=
r
by A1, A4, ABSVALUE:def 1
;
hence
y in Cb
by A1, A6;
:: thesis: verum
end;
Cb c= (AffineMap r,a,r,b) .: Kb
proof
let y be
set ;
:: 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 A7:
(
y = p2 &
|.(p2 - |[a,b]|).| = r )
by A1;
now per cases
( r > 0 or r = 0 )
by A1;
case A8:
r > 0
;
:: thesis: y in (AffineMap r,a,r,b) .: Kbset p1 =
(1 / r) * (p2 - |[a,b]|);
|.((1 / r) * (p2 - |[a,b]|)).| =
(abs (1 / rr)) * |.(p2 - |[a,b]|).|
by TOPRNS_1:8
.=
(1 / r) * r
by A7, ABSVALUE:def 1
.=
1
by A8, XCMPLX_1:88
;
then A10:
(1 / r) * (p2 - |[a,b]|) in Kb
by A1;
(1 / r) * (p2 - |[a,b]|) = |[((1 / r) * ((p2 - |[a,b]|) `1 )),((1 / r) * ((p2 - |[a,b]|) `2 ))]|
by EUCLID:61;
then A11:
(
((1 / r) * (p2 - |[a,b]|)) `1 = (1 / r) * ((p2 - |[a,b]|) `1 ) &
((1 / r) * (p2 - |[a,b]|)) `2 = (1 / r) * ((p2 - |[a,b]|) `2 ) )
by EUCLID:56;
then A12:
r * (((1 / r) * (p2 - |[a,b]|)) `1 ) =
(r * (1 / r)) * ((p2 - |[a,b]|) `1 )
.=
1
* ((p2 - |[a,b]|) `1 )
by A8, XCMPLX_1:88
.=
(p2 `1 ) - (|[a,b]| `1 )
by TOPREAL3:8
.=
(p2 `1 ) - a
by EUCLID:56
;
A13:
r * (((1 / r) * (p2 - |[a,b]|)) `2 ) =
(r * (1 / r)) * ((p2 - |[a,b]|) `2 )
by A11
.=
1
* ((p2 - |[a,b]|) `2 )
by A8, XCMPLX_1:88
.=
(p2 `2 ) - (|[a,b]| `2 )
by TOPREAL3:8
.=
(p2 `2 ) - b
by EUCLID:56
;
A14:
(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 A12, A13, EUCLID:57
;
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 A7, A10, A14, FUNCT_1:def 12;
:: thesis: verum end; case A15:
r = 0
;
:: thesis: y in (AffineMap r,a,r,b) .: Kbset p1 =
|[1,0 ]|;
(
|[1,0 ]| `1 = 1 &
|[1,0 ]| `2 = 0 )
by EUCLID:56;
then |.|[1,0 ]|.| =
sqrt ((1 ^2 ) + (0 ^2 ))
by JGRAPH_3:10
.=
1
by SQUARE_1:89
;
then A16:
|[1,0 ]| in Kb
by A1;
A17:
(AffineMap r,a,r,b) . |[1,0 ]| =
|[((0 * (|[1,0 ]| `1 )) + a),((0 * (|[1,0 ]| `2 )) + b)]|
by A15, JGRAPH_2:def 2
.=
p2
by A7, A15, TOPRNS_1:29
;
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 A7, A16, A17, FUNCT_1:def 12;
:: thesis: verum end;
hence
y in (AffineMap r,a,r,b) .: Kb
;
:: thesis: verum
end;
hence
(AffineMap r,a,r,b) .: Kb = Cb
by A2, XBOOLE_0:def 10; :: thesis: verum