let q be Point of (TOP-REAL 2); :: thesis: for r being Real
for y, x 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 y, x 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 y, x 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:13;
A4: B c= (AffineMap r,(q `1 ),r,(q `2 )) .: A

proof

let u be set ; :: 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:13;
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:21
.= (id (REAL 2)) . q1 by A3, Th34
.= x1 by FUNCT_1:35 ;
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:31, EUCLID:58
.= dist |[0 ,0 ]|,(r * ((AffineMap (1 / r),(- ((q `1 ) / r)),(1 / r),(- ((q `2 ) / r))) . q1)) by Th21
.= (abs 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:12;
then dist y,z4 < 1 by A3, XREAL_1:66;
then A12: (AffineMap (1 / r),(- ((q `1 ) / r)),(1 / r),(- ((q `2 ) / r))) . q1 in A by A10, METRIC_1:12;
(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:21
.= (id (REAL 2)) . q1 by A3, Th34
.= (id (TOP-REAL 2)) . q1 by EUCLID:25
.= q1 by FUNCT_1:35 ;
hence u in (AffineMap r,(q `1 ),r,(q `2 )) .: A by A12, FUNCT_2:43; :: thesis: verum

end;

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

proof

let u be set ; :: 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:116;
reconsider x1 = q1, x2 = q2 as Element of (Euclid 2) by TOPREAL3:13;
A16: dist y,x2 < 1 by A14, METRIC_1:12;
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:31, EUCLID:58
.= dist |[0 ,0 ]|,(r * q2) by Th21
.= (abs 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:159;
hence u in B by METRIC_1:12; :: thesis: verum

end;

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