let a, b, r be Real; 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 ;
A2:
(AffineMap (r,a,r,b)) .: Kb c= Cb
proof
let y be
object ;
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
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;
verum
end;
Cb c= (AffineMap (r,a,r,b)) .: Kb
proof
let y be
object ;
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 ( ( r > 0 & y in (AffineMap (r,a,r,b)) .: Kb ) or ( r = 0 & y in (AffineMap (r,a,r,b)) .: Kb ) )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]|)).| =
|.(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;
verum end; case A19:
r = 0
;
y in (AffineMap (r,a,r,b)) .: Kbset 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
;
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;
verum end;
hence
y in (AffineMap (r,a,r,b)) .: Kb
;
verum
end;
hence
(AffineMap (r,a,r,b)) .: Kb = Cb
by A2; verum