let a, b, r be real number ; 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); ( 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 } )
; (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 ;
TARSKI:def 3 ( not y in (AffineMap r,a,r,b) .: Kb or y in Cb )
assume
y in (AffineMap r,a,r,b) .: Kb
;
y in Cb
then consider x being
set 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 12;
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: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, A6, ABSVALUE:def 1
;
hence
y in Cb
by A1, A8;
verum
end;
Cb c= (AffineMap r,a,r,b) .: Kb
proof
let y be
set ;
TARSKI:def 3 ( not y in Cb or y in (AffineMap r,a,r,b) .: Kb )
assume
y in Cb
;
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 per cases
( r > 0 or r = 0 )
by A1;
case A11:
r > 0
;
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 A10, ABSVALUE:def 1
.=
1
by A11, XCMPLX_1:88
;
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:61;
then A14:
((1 / r) * (p2 - |[a,b]|)) `1 = (1 / r) * ((p2 - |[a,b]|) `1 )
by EUCLID:56;
A15:
((1 / r) * (p2 - |[a,b]|)) `2 = (1 / r) * ((p2 - |[a,b]|) `2 )
by A13, EUCLID:56;
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:88
.=
(p2 `1 ) - (|[a,b]| `1 )
by TOPREAL3:8
.=
(p2 `1 ) - a
by EUCLID:56
;
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:88
.=
(p2 `2 ) - (|[a,b]| `2 )
by TOPREAL3:8
.=
(p2 `2 ) - b
by EUCLID:56
;
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: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 A9, A12, A18, FUNCT_1:def 12;
verum end; case A19:
r = 0
;
y in (AffineMap r,a,r,b) .: Kbset p1 =
|[1,0 ]|;
A20:
|[1,0 ]| `1 = 1
by EUCLID:56;
|[1,0 ]| `2 = 0
by EUCLID:56;
then |.|[1,0 ]|.| =
sqrt ((1 ^2 ) + (0 ^2 ))
by A20, JGRAPH_3:10
.=
1
by SQUARE_1:89
;
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: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 A9, A21, A22, FUNCT_1:def 12;
verum end;
hence
y in (AffineMap r,a,r,b) .: Kb
;
verum
end;
hence
(AffineMap r,a,r,b) .: Kb = Cb
by A2, XBOOLE_0:def 10; verum