let q be Point of (TOP-REAL 2); :: thesis: 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; :: thesis: 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); :: thesis: ( 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 ; :: thesis: (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 ; :: according to TARSKI:def 3 :: thesis: ( not u in B or u in (AffineMap (r,(q `1),r,(q `2))) .: A )
assume A5: u in B ; :: thesis: 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; :: thesis: verum

end;

(AffineMap (r,(q `1),r,(q `2))) .: A c= B

proof

let u be object ; :: according to TARSKI:def 3 :: thesis: ( 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 ; :: thesis: 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; :: thesis: verum

end;

hence (AffineMap (r,(q `1),r,(q `2))) .: (Ball (y,1)) = Ball (x,r) by A4; :: thesis: verum