let q be Point of (TOP-REAL 2); for r being Real
for x, y being Point of (Euclid 2) st y = |[0,0]| & x = q & r > 0 holds
(AffineMap (r,(q `1),r,(q `2))) .: (Ball (y,1)) = Ball (x,r)
let r be Real; for x, y being Point of (Euclid 2) st y = |[0,0]| & x = q & r > 0 holds
(AffineMap (r,(q `1),r,(q `2))) .: (Ball (y,1)) = Ball (x,r)
let x, y be Point of (Euclid 2); ( y = |[0,0]| & x = q & r > 0 implies (AffineMap (r,(q `1),r,(q `2))) .: (Ball (y,1)) = Ball (x,r) )
assume that
A1:
y = |[0,0]|
and
A2:
x = q
and
A3:
r > 0
; (AffineMap (r,(q `1),r,(q `2))) .: (Ball (y,1)) = Ball (x,r)
reconsider A = Ball (y,1), B = Ball (x,r) as Subset of (TOP-REAL 2) by TOPREAL3:8;
A4:
B c= (AffineMap (r,(q `1),r,(q `2))) .: A
proof
let u be
object ;
TARSKI:def 3 ( not u in B or u in (AffineMap (r,(q `1),r,(q `2))) .: A )
assume A5:
u in B
;
u in (AffineMap (r,(q `1),r,(q `2))) .: A
then reconsider q1 =
u as
Point of
(TOP-REAL 2) ;
reconsider x1 =
q1 as
Element of
(Euclid 2) by TOPREAL3:8;
set q2 =
(AffineMap ((1 / r),(- ((q `1) / r)),(1 / r),(- ((q `2) / r)))) . q1;
consider z1,
z2 being
Point of
(Euclid 2) such that A6:
z1 = q
and A7:
z2 = (r * ((AffineMap ((1 / r),(- ((q `1) / r)),(1 / r),(- ((q `2) / r)))) . q1)) + q
and A8:
dist (
q,
((r * ((AffineMap ((1 / r),(- ((q `1) / r)),(1 / r),(- ((q `2) / r)))) . q1)) + q))
= dist (
z1,
z2)
by TOPREAL6:def 1;
consider z3,
z4 being
Point of
(Euclid 2) such that A9:
z3 = |[0,0]|
and A10:
z4 = (AffineMap ((1 / r),(- ((q `1) / r)),(1 / r),(- ((q `2) / r)))) . q1
and A11:
dist (
|[0,0]|,
((AffineMap ((1 / r),(- ((q `1) / r)),(1 / r),(- ((q `2) / r)))) . q1))
= dist (
z3,
z4)
by TOPREAL6:def 1;
z2 =
(AffineMap (r,(q `1),r,(q `2))) . ((AffineMap ((1 / r),(- ((q `1) / r)),(1 / r),(- ((q `2) / r)))) . q1)
by A7, Th33
.=
((AffineMap (r,(q `1),r,(q `2))) * (AffineMap ((1 / r),(- ((q `1) / r)),(1 / r),(- ((q `2) / r))))) . q1
by FUNCT_2:15
.=
(id (REAL 2)) . q1
by A3, Th34
.=
x1
;
then dist (
x,
x1) =
dist (
(|[0,0]| + q),
((r * ((AffineMap ((1 / r),(- ((q `1) / r)),(1 / r),(- ((q `2) / r)))) . q1)) + q))
by A2, A6, A8, EUCLID:54, RLVECT_1:4
.=
dist (
|[0,0]|,
(r * ((AffineMap ((1 / r),(- ((q `1) / r)),(1 / r),(- ((q `2) / r)))) . q1)))
by Th21
.=
|.r.| * (dist (|[0,0]|,((AffineMap ((1 / r),(- ((q `1) / r)),(1 / r),(- ((q `2) / r)))) . q1)))
by Th20
.=
r * (dist (y,z4))
by A1, A3, A9, A11, ABSVALUE:def 1
;
then
r * (dist (y,z4)) < 1
* r
by A5, METRIC_1:11;
then
dist (
y,
z4)
< 1
by A3, XREAL_1:64;
then A12:
(AffineMap ((1 / r),(- ((q `1) / r)),(1 / r),(- ((q `2) / r)))) . q1 in A
by A10, METRIC_1:11;
(AffineMap (r,(q `1),r,(q `2))) . ((AffineMap ((1 / r),(- ((q `1) / r)),(1 / r),(- ((q `2) / r)))) . q1) =
((AffineMap (r,(q `1),r,(q `2))) * (AffineMap ((1 / r),(- ((q `1) / r)),(1 / r),(- ((q `2) / r))))) . q1
by FUNCT_2:15
.=
(id (REAL 2)) . q1
by A3, Th34
.=
(id (TOP-REAL 2)) . q1
by EUCLID:22
.=
q1
;
hence
u in (AffineMap (r,(q `1),r,(q `2))) .: A
by A12, FUNCT_2:35;
verum
end;
(AffineMap (r,(q `1),r,(q `2))) .: A c= B
proof
let u be
object ;
TARSKI:def 3 ( not u in (AffineMap (r,(q `1),r,(q `2))) .: A or u in B )
assume A13:
u in (AffineMap (r,(q `1),r,(q `2))) .: A
;
u in B
then reconsider q1 =
u as
Point of
(TOP-REAL 2) ;
consider q2 being
Point of
(TOP-REAL 2) such that A14:
q2 in A
and A15:
q1 = (AffineMap (r,(q `1),r,(q `2))) . q2
by A13, FUNCT_2:65;
reconsider x1 =
q1,
x2 =
q2 as
Element of
(Euclid 2) by TOPREAL3:8;
A16:
dist (
y,
x2)
< 1
by A14, METRIC_1:11;
A17:
ex
z3,
z4 being
Point of
(Euclid 2) st
(
z3 = |[0,0]| &
z4 = q2 &
dist (
|[0,0]|,
q2)
= dist (
z3,
z4) )
by TOPREAL6:def 1;
A18:
ex
z1,
z2 being
Point of
(Euclid 2) st
(
z1 = q &
z2 = (r * q2) + q &
dist (
q,
((r * q2) + q))
= dist (
z1,
z2) )
by TOPREAL6:def 1;
q1 = (r * q2) + q
by A15, Th33;
then dist (
x,
x1) =
dist (
(|[0,0]| + q),
((r * q2) + q))
by A2, A18, EUCLID:54, RLVECT_1:4
.=
dist (
|[0,0]|,
(r * q2))
by Th21
.=
|.r.| * (dist (|[0,0]|,q2))
by Th20
.=
r * (dist (y,x2))
by A1, A3, A17, ABSVALUE:def 1
;
then
dist (
x,
x1)
< r
by A3, A16, XREAL_1:157;
hence
u in B
by METRIC_1:11;
verum
end;
hence
(AffineMap (r,(q `1),r,(q `2))) .: (Ball (y,1)) = Ball (x,r)
by A4; verum