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:
(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 A5:
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 A6:
q2 in A
and A7:
q1 = (AffineMap r,(q `1 ),r,(q `2 )) . q2
by A5, FUNCT_2:116;
A8:
q1 = (r * q2) + q
by A7, Th33;
reconsider x1 =
q1,
x2 =
q2 as
Element of
(Euclid 2) by TOPREAL3:13;
A9:
dist y,
x2 < 1
by A6, METRIC_1:12;
consider z1,
z2 being
Point of
(Euclid 2) such that A10:
(
z1 = q &
z2 = (r * q2) + q )
and A11:
dist q,
((r * q2) + q) = dist z1,
z2
by TOPREAL6:def 1;
consider z3,
z4 being
Point of
(Euclid 2) such that A12:
(
z3 = |[0 ,0 ]| &
z4 = q2 )
and A13:
dist |[0 ,0 ]|,
q2 = dist z3,
z4
by TOPREAL6:def 1;
dist x,
x1 =
dist (|[0 ,0 ]| + q),
((r * q2) + q)
by A2, A8, A10, A11, 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, A12, A13, ABSVALUE:def 1
;
then
dist x,
x1 < r
by A3, A9, XREAL_1:159;
hence
u in B
by METRIC_1:12;
:: thesis: verum
end;
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 A14:
u in B
;
:: thesis: u in (AffineMap r,(q `1 ),r,(q `2 )) .: A
then reconsider q1 =
u as
Point of
(TOP-REAL 2) ;
set q2 =
(AffineMap (1 / r),(- ((q `1 ) / r)),(1 / r),(- ((q `2 ) / r))) . q1;
consider z1,
z2 being
Point of
(Euclid 2) such that A15:
(
z1 = q &
z2 = (r * ((AffineMap (1 / r),(- ((q `1 ) / r)),(1 / r),(- ((q `2 ) / r))) . q1)) + q )
and A16:
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 A17:
(
z3 = |[0 ,0 ]| &
z4 = (AffineMap (1 / r),(- ((q `1 ) / r)),(1 / r),(- ((q `2 ) / r))) . q1 )
and A18:
dist |[0 ,0 ]|,
((AffineMap (1 / r),(- ((q `1 ) / r)),(1 / r),(- ((q `2 ) / r))) . q1) = dist z3,
z4
by TOPREAL6:def 1;
reconsider x1 =
q1 as
Element of
(Euclid 2) by TOPREAL3:13;
z2 =
(AffineMap r,(q `1 ),r,(q `2 )) . ((AffineMap (1 / r),(- ((q `1 ) / r)),(1 / r),(- ((q `2 ) / r))) . q1)
by A15, 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, A15, A16, 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, A17, A18, ABSVALUE:def 1
;
then
r * (dist y,z4) < 1
* r
by A14, METRIC_1:12;
then
dist y,
z4 < 1
by A3, XREAL_1:66;
then A19:
(AffineMap (1 / r),(- ((q `1 ) / r)),(1 / r),(- ((q `2 ) / r))) . q1 in A
by A17, 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 A19, FUNCT_2:43;
:: 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