let o, p be Point of (TOP-REAL 2); for r being positive Real st p is Point of (Tdisk (o,r)) holds
DiskProj (o,r,p) is continuous
let r be positive Real; ( p is Point of (Tdisk (o,r)) implies DiskProj (o,r,p) is continuous )
assume A1:
p is Point of (Tdisk (o,r))
; DiskProj (o,r,p) is continuous
set D = Tdisk (o,r);
set cB = cl_Ball (o,r);
set Bp = (cl_Ball (o,r)) \ {p};
set OK = [:((cl_Ball (o,r)) \ {p}),{p}:];
set D1 = (TOP-REAL 2) | ((cl_Ball (o,r)) \ {p});
set D2 = (TOP-REAL 2) | {p};
set S1 = Tcircle (o,r);
A2:
p in {p}
by TARSKI:def 1;
A3:
the carrier of (Tdisk (o,r)) = cl_Ball (o,r)
by BROUWER:3;
A4:
the carrier of ((TOP-REAL 2) | ((cl_Ball (o,r)) \ {p})) = (cl_Ball (o,r)) \ {p}
by PRE_TOPC:8;
A5:
the carrier of ((TOP-REAL 2) | {p}) = {p}
by PRE_TOPC:8;
set TD = [:(TOP-REAL 2),(TOP-REAL 2):] | [:((cl_Ball (o,r)) \ {p}),{p}:];
set gg = DiskProj (o,r,p);
set xo = diffX2_1 o;
set yo = diffX2_2 o;
set dx = diffX1_X2_1 ;
set dy = diffX1_X2_2 ;
set fx2 = Proj2_1 ;
set fy2 = Proj2_2 ;
reconsider rr = r ^2 as Element of REAL by XREAL_0:def 1;
set f1 = the carrier of [:(TOP-REAL 2),(TOP-REAL 2):] --> rr;
reconsider f1 = the carrier of [:(TOP-REAL 2),(TOP-REAL 2):] --> rr as continuous RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] by Lm6;
set Zf1 = f1 | [:((cl_Ball (o,r)) \ {p}),{p}:];
set Zfx2 = Proj2_1 | [:((cl_Ball (o,r)) \ {p}),{p}:];
set Zfy2 = Proj2_2 | [:((cl_Ball (o,r)) \ {p}),{p}:];
set Zdx = diffX1_X2_1 | [:((cl_Ball (o,r)) \ {p}),{p}:];
set Zdy = diffX1_X2_2 | [:((cl_Ball (o,r)) \ {p}),{p}:];
set Zxo = (diffX2_1 o) | [:((cl_Ball (o,r)) \ {p}),{p}:];
set Zyo = (diffX2_2 o) | [:((cl_Ball (o,r)) \ {p}),{p}:];
set xx = ((diffX2_1 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_1 | [:((cl_Ball (o,r)) \ {p}),{p}:]);
set yy = ((diffX2_2 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_2 | [:((cl_Ball (o,r)) \ {p}),{p}:]);
set m = ((diffX1_X2_1 | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_1 | [:((cl_Ball (o,r)) \ {p}),{p}:])) + ((diffX1_X2_2 | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_2 | [:((cl_Ball (o,r)) \ {p}),{p}:]));
A6:
the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | [:((cl_Ball (o,r)) \ {p}),{p}:]) = [:((cl_Ball (o,r)) \ {p}),{p}:]
by PRE_TOPC:8;
A7:
for y being Point of ((TOP-REAL 2) | ((cl_Ball (o,r)) \ {p}))
for z being Point of ((TOP-REAL 2) | {p}) holds (diffX1_X2_1 | [:((cl_Ball (o,r)) \ {p}),{p}:]) . [y,z] = diffX1_X2_1 . [y,z]
proof
let y be
Point of
((TOP-REAL 2) | ((cl_Ball (o,r)) \ {p}));
for z being Point of ((TOP-REAL 2) | {p}) holds (diffX1_X2_1 | [:((cl_Ball (o,r)) \ {p}),{p}:]) . [y,z] = diffX1_X2_1 . [y,z]let z be
Point of
((TOP-REAL 2) | {p});
(diffX1_X2_1 | [:((cl_Ball (o,r)) \ {p}),{p}:]) . [y,z] = diffX1_X2_1 . [y,z]
[y,z] in [:((cl_Ball (o,r)) \ {p}),{p}:]
by A4, A5, ZFMISC_1:def 2;
hence
(diffX1_X2_1 | [:((cl_Ball (o,r)) \ {p}),{p}:]) . [y,z] = diffX1_X2_1 . [y,z]
by FUNCT_1:49;
verum
end;
A8:
for y being Point of ((TOP-REAL 2) | ((cl_Ball (o,r)) \ {p}))
for z being Point of ((TOP-REAL 2) | {p}) holds (diffX1_X2_2 | [:((cl_Ball (o,r)) \ {p}),{p}:]) . [y,z] = diffX1_X2_2 . [y,z]
proof
let y be
Point of
((TOP-REAL 2) | ((cl_Ball (o,r)) \ {p}));
for z being Point of ((TOP-REAL 2) | {p}) holds (diffX1_X2_2 | [:((cl_Ball (o,r)) \ {p}),{p}:]) . [y,z] = diffX1_X2_2 . [y,z]let z be
Point of
((TOP-REAL 2) | {p});
(diffX1_X2_2 | [:((cl_Ball (o,r)) \ {p}),{p}:]) . [y,z] = diffX1_X2_2 . [y,z]
[y,z] in [:((cl_Ball (o,r)) \ {p}),{p}:]
by A4, A5, ZFMISC_1:def 2;
hence
(diffX1_X2_2 | [:((cl_Ball (o,r)) \ {p}),{p}:]) . [y,z] = diffX1_X2_2 . [y,z]
by FUNCT_1:49;
verum
end;
A9:
for y being Point of ((TOP-REAL 2) | ((cl_Ball (o,r)) \ {p}))
for z being Point of ((TOP-REAL 2) | {p}) holds (Proj2_1 | [:((cl_Ball (o,r)) \ {p}),{p}:]) . [y,z] = Proj2_1 . [y,z]
proof
let y be
Point of
((TOP-REAL 2) | ((cl_Ball (o,r)) \ {p}));
for z being Point of ((TOP-REAL 2) | {p}) holds (Proj2_1 | [:((cl_Ball (o,r)) \ {p}),{p}:]) . [y,z] = Proj2_1 . [y,z]let z be
Point of
((TOP-REAL 2) | {p});
(Proj2_1 | [:((cl_Ball (o,r)) \ {p}),{p}:]) . [y,z] = Proj2_1 . [y,z]
[y,z] in [:((cl_Ball (o,r)) \ {p}),{p}:]
by A4, A5, ZFMISC_1:def 2;
hence
(Proj2_1 | [:((cl_Ball (o,r)) \ {p}),{p}:]) . [y,z] = Proj2_1 . [y,z]
by FUNCT_1:49;
verum
end;
A10:
for y being Point of ((TOP-REAL 2) | ((cl_Ball (o,r)) \ {p}))
for z being Point of ((TOP-REAL 2) | {p}) holds (Proj2_2 | [:((cl_Ball (o,r)) \ {p}),{p}:]) . [y,z] = Proj2_2 . [y,z]
proof
let y be
Point of
((TOP-REAL 2) | ((cl_Ball (o,r)) \ {p}));
for z being Point of ((TOP-REAL 2) | {p}) holds (Proj2_2 | [:((cl_Ball (o,r)) \ {p}),{p}:]) . [y,z] = Proj2_2 . [y,z]let z be
Point of
((TOP-REAL 2) | {p});
(Proj2_2 | [:((cl_Ball (o,r)) \ {p}),{p}:]) . [y,z] = Proj2_2 . [y,z]
[y,z] in [:((cl_Ball (o,r)) \ {p}),{p}:]
by A4, A5, ZFMISC_1:def 2;
hence
(Proj2_2 | [:((cl_Ball (o,r)) \ {p}),{p}:]) . [y,z] = Proj2_2 . [y,z]
by FUNCT_1:49;
verum
end;
A11:
for y being Point of ((TOP-REAL 2) | ((cl_Ball (o,r)) \ {p}))
for z being Point of ((TOP-REAL 2) | {p}) holds (f1 | [:((cl_Ball (o,r)) \ {p}),{p}:]) . [y,z] = f1 . [y,z]
proof
let y be
Point of
((TOP-REAL 2) | ((cl_Ball (o,r)) \ {p}));
for z being Point of ((TOP-REAL 2) | {p}) holds (f1 | [:((cl_Ball (o,r)) \ {p}),{p}:]) . [y,z] = f1 . [y,z]let z be
Point of
((TOP-REAL 2) | {p});
(f1 | [:((cl_Ball (o,r)) \ {p}),{p}:]) . [y,z] = f1 . [y,z]
[y,z] in [:((cl_Ball (o,r)) \ {p}),{p}:]
by A4, A5, ZFMISC_1:def 2;
hence
(f1 | [:((cl_Ball (o,r)) \ {p}),{p}:]) . [y,z] = f1 . [y,z]
by FUNCT_1:49;
verum
end;
A12:
for y being Point of ((TOP-REAL 2) | ((cl_Ball (o,r)) \ {p}))
for z being Point of ((TOP-REAL 2) | {p}) holds ((diffX2_1 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) . [y,z] = (diffX2_1 o) . [y,z]
proof
let y be
Point of
((TOP-REAL 2) | ((cl_Ball (o,r)) \ {p}));
for z being Point of ((TOP-REAL 2) | {p}) holds ((diffX2_1 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) . [y,z] = (diffX2_1 o) . [y,z]let z be
Point of
((TOP-REAL 2) | {p});
((diffX2_1 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) . [y,z] = (diffX2_1 o) . [y,z]
[y,z] in [:((cl_Ball (o,r)) \ {p}),{p}:]
by A4, A5, ZFMISC_1:def 2;
hence
((diffX2_1 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) . [y,z] = (diffX2_1 o) . [y,z]
by FUNCT_1:49;
verum
end;
A13:
for y being Point of ((TOP-REAL 2) | ((cl_Ball (o,r)) \ {p}))
for z being Point of ((TOP-REAL 2) | {p}) holds ((diffX2_2 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) . [y,z] = (diffX2_2 o) . [y,z]
proof
let y be
Point of
((TOP-REAL 2) | ((cl_Ball (o,r)) \ {p}));
for z being Point of ((TOP-REAL 2) | {p}) holds ((diffX2_2 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) . [y,z] = (diffX2_2 o) . [y,z]let z be
Point of
((TOP-REAL 2) | {p});
((diffX2_2 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) . [y,z] = (diffX2_2 o) . [y,z]
[y,z] in [:((cl_Ball (o,r)) \ {p}),{p}:]
by A4, A5, ZFMISC_1:def 2;
hence
((diffX2_2 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) . [y,z] = (diffX2_2 o) . [y,z]
by FUNCT_1:49;
verum
end;
now for b being Real st b in rng (((diffX1_X2_1 | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_1 | [:((cl_Ball (o,r)) \ {p}),{p}:])) + ((diffX1_X2_2 | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_2 | [:((cl_Ball (o,r)) \ {p}),{p}:]))) holds
0 < blet b be
Real;
( b in rng (((diffX1_X2_1 | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_1 | [:((cl_Ball (o,r)) \ {p}),{p}:])) + ((diffX1_X2_2 | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_2 | [:((cl_Ball (o,r)) \ {p}),{p}:]))) implies 0 < b )assume
b in rng (((diffX1_X2_1 | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_1 | [:((cl_Ball (o,r)) \ {p}),{p}:])) + ((diffX1_X2_2 | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_2 | [:((cl_Ball (o,r)) \ {p}),{p}:])))
;
0 < bthen consider a being
object such that A14:
a in dom (((diffX1_X2_1 | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_1 | [:((cl_Ball (o,r)) \ {p}),{p}:])) + ((diffX1_X2_2 | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_2 | [:((cl_Ball (o,r)) \ {p}),{p}:])))
and A15:
(((diffX1_X2_1 | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_1 | [:((cl_Ball (o,r)) \ {p}),{p}:])) + ((diffX1_X2_2 | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_2 | [:((cl_Ball (o,r)) \ {p}),{p}:]))) . a = b
by FUNCT_1:def 3;
consider y,
z being
object such that A16:
y in (cl_Ball (o,r)) \ {p}
and A17:
z in {p}
and A18:
a = [y,z]
by A14, ZFMISC_1:def 2;
A19:
z = p
by A17, TARSKI:def 1;
reconsider y =
y,
z =
z as
Point of
(TOP-REAL 2) by A16, A17;
A20:
y <> z
by A16, A19, ZFMISC_1:56;
A21:
diffX1_X2_1 . [y,z] = (([y,z] `1) `1) - (([y,z] `2) `1)
by Def3;
A22:
diffX1_X2_2 . [y,z] = (([y,z] `1) `2) - (([y,z] `2) `2)
by Def4;
set r1 =
(y `1) - (z `1);
set r2 =
(y `2) - (z `2);
A23:
(diffX1_X2_1 | [:((cl_Ball (o,r)) \ {p}),{p}:]) . [y,z] = diffX1_X2_1 . [y,z]
by A4, A5, A7, A16, A17;
A24:
(diffX1_X2_2 | [:((cl_Ball (o,r)) \ {p}),{p}:]) . [y,z] = diffX1_X2_2 . [y,z]
by A4, A5, A8, A16, A17;
dom (((diffX1_X2_1 | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_1 | [:((cl_Ball (o,r)) \ {p}),{p}:])) + ((diffX1_X2_2 | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_2 | [:((cl_Ball (o,r)) \ {p}),{p}:]))) c= the
carrier of
([:(TOP-REAL 2),(TOP-REAL 2):] | [:((cl_Ball (o,r)) \ {p}),{p}:])
by RELAT_1:def 18;
then
a in the
carrier of
([:(TOP-REAL 2),(TOP-REAL 2):] | [:((cl_Ball (o,r)) \ {p}),{p}:])
by A14;
then A25:
(((diffX1_X2_1 | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_1 | [:((cl_Ball (o,r)) \ {p}),{p}:])) + ((diffX1_X2_2 | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_2 | [:((cl_Ball (o,r)) \ {p}),{p}:]))) . [y,z] =
(((diffX1_X2_1 | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_1 | [:((cl_Ball (o,r)) \ {p}),{p}:])) . [y,z]) + (((diffX1_X2_2 | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_2 | [:((cl_Ball (o,r)) \ {p}),{p}:])) . [y,z])
by A18, VALUED_1:1
.=
(((diffX1_X2_1 | [:((cl_Ball (o,r)) \ {p}),{p}:]) . [y,z]) * ((diffX1_X2_1 | [:((cl_Ball (o,r)) \ {p}),{p}:]) . [y,z])) + (((diffX1_X2_2 | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_2 | [:((cl_Ball (o,r)) \ {p}),{p}:])) . [y,z])
by VALUED_1:5
.=
(((y `1) - (z `1)) ^2) + (((y `2) - (z `2)) ^2)
by A21, A22, A23, A24, VALUED_1:5
;
hence
0 < b
by A15, A18, A25;
verum end;
then reconsider m = ((diffX1_X2_1 | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_1 | [:((cl_Ball (o,r)) \ {p}),{p}:])) + ((diffX1_X2_2 | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_2 | [:((cl_Ball (o,r)) \ {p}),{p}:])) as positive-yielding continuous RealMap of ([:(TOP-REAL 2),(TOP-REAL 2):] | [:((cl_Ball (o,r)) \ {p}),{p}:]) by PARTFUN3:def 1;
set p1 = ((((diffX2_1 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_1 | [:((cl_Ball (o,r)) \ {p}),{p}:])) + (((diffX2_2 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_2 | [:((cl_Ball (o,r)) \ {p}),{p}:]))) (#) ((((diffX2_1 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_1 | [:((cl_Ball (o,r)) \ {p}),{p}:])) + (((diffX2_2 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_2 | [:((cl_Ball (o,r)) \ {p}),{p}:])));
set p2 = ((((diffX2_1 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) ((diffX2_1 o) | [:((cl_Ball (o,r)) \ {p}),{p}:])) + (((diffX2_2 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) ((diffX2_2 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]))) - (f1 | [:((cl_Ball (o,r)) \ {p}),{p}:]);
A28:
dom (((((diffX2_1 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) ((diffX2_1 o) | [:((cl_Ball (o,r)) \ {p}),{p}:])) + (((diffX2_2 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) ((diffX2_2 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]))) - (f1 | [:((cl_Ball (o,r)) \ {p}),{p}:])) = the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | [:((cl_Ball (o,r)) \ {p}),{p}:])
by FUNCT_2:def 1;
now for b being Real st b in rng (((((diffX2_1 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) ((diffX2_1 o) | [:((cl_Ball (o,r)) \ {p}),{p}:])) + (((diffX2_2 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) ((diffX2_2 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]))) - (f1 | [:((cl_Ball (o,r)) \ {p}),{p}:])) holds
0 >= blet b be
Real;
( b in rng (((((diffX2_1 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) ((diffX2_1 o) | [:((cl_Ball (o,r)) \ {p}),{p}:])) + (((diffX2_2 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) ((diffX2_2 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]))) - (f1 | [:((cl_Ball (o,r)) \ {p}),{p}:])) implies 0 >= b )assume
b in rng (((((diffX2_1 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) ((diffX2_1 o) | [:((cl_Ball (o,r)) \ {p}),{p}:])) + (((diffX2_2 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) ((diffX2_2 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]))) - (f1 | [:((cl_Ball (o,r)) \ {p}),{p}:]))
;
0 >= bthen consider a being
object such that A29:
a in dom (((((diffX2_1 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) ((diffX2_1 o) | [:((cl_Ball (o,r)) \ {p}),{p}:])) + (((diffX2_2 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) ((diffX2_2 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]))) - (f1 | [:((cl_Ball (o,r)) \ {p}),{p}:]))
and A30:
(((((diffX2_1 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) ((diffX2_1 o) | [:((cl_Ball (o,r)) \ {p}),{p}:])) + (((diffX2_2 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) ((diffX2_2 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]))) - (f1 | [:((cl_Ball (o,r)) \ {p}),{p}:])) . a = b
by FUNCT_1:def 3;
consider y,
z being
object such that A31:
y in (cl_Ball (o,r)) \ {p}
and A32:
z in {p}
and A33:
a = [y,z]
by A29, ZFMISC_1:def 2;
reconsider y =
y,
z =
z as
Point of
(TOP-REAL 2) by A31, A32;
set r3 =
(z `1) - (o `1);
set r4 =
(z `2) - (o `2);
A34:
(f1 | [:((cl_Ball (o,r)) \ {p}),{p}:]) . [y,z] = f1 . [y,z]
by A4, A5, A11, A31, A32;
A35:
((diffX2_1 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) . [y,z] = (diffX2_1 o) . [y,z]
by A4, A5, A12, A31, A32;
A36:
((diffX2_2 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) . [y,z] = (diffX2_2 o) . [y,z]
by A4, A5, A13, A31, A32;
A37:
(diffX2_1 o) . [y,z] = (([y,z] `2) `1) - (o `1)
by Def1;
A38:
(diffX2_2 o) . [y,z] = (([y,z] `2) `2) - (o `2)
by Def2;
dom (((((diffX2_1 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) ((diffX2_1 o) | [:((cl_Ball (o,r)) \ {p}),{p}:])) + (((diffX2_2 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) ((diffX2_2 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]))) - (f1 | [:((cl_Ball (o,r)) \ {p}),{p}:])) c= the
carrier of
([:(TOP-REAL 2),(TOP-REAL 2):] | [:((cl_Ball (o,r)) \ {p}),{p}:])
by RELAT_1:def 18;
then A39:
a in the
carrier of
([:(TOP-REAL 2),(TOP-REAL 2):] | [:((cl_Ball (o,r)) \ {p}),{p}:])
by A29;
A40:
(((((diffX2_1 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) ((diffX2_1 o) | [:((cl_Ball (o,r)) \ {p}),{p}:])) + (((diffX2_2 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) ((diffX2_2 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]))) - (f1 | [:((cl_Ball (o,r)) \ {p}),{p}:])) . [y,z] =
(((((diffX2_1 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) ((diffX2_1 o) | [:((cl_Ball (o,r)) \ {p}),{p}:])) + (((diffX2_2 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) ((diffX2_2 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]))) . [y,z]) - ((f1 | [:((cl_Ball (o,r)) \ {p}),{p}:]) . [y,z])
by A29, A33, VALUED_1:13
.=
(((((diffX2_1 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) ((diffX2_1 o) | [:((cl_Ball (o,r)) \ {p}),{p}:])) + (((diffX2_2 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) ((diffX2_2 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]))) . [y,z]) - (r ^2)
by A34, FUNCOP_1:7
.=
(((((diffX2_1 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) ((diffX2_1 o) | [:((cl_Ball (o,r)) \ {p}),{p}:])) . [y,z]) + ((((diffX2_2 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) ((diffX2_2 o) | [:((cl_Ball (o,r)) \ {p}),{p}:])) . [y,z])) - (r ^2)
by A33, A39, VALUED_1:1
.=
(((((diffX2_1 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) . [y,z]) * (((diffX2_1 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) . [y,z])) + ((((diffX2_2 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) ((diffX2_2 o) | [:((cl_Ball (o,r)) \ {p}),{p}:])) . [y,z])) - (r ^2)
by VALUED_1:5
.=
((((z `1) - (o `1)) ^2) + (((z `2) - (o `2)) ^2)) - (r ^2)
by A35, A36, A37, A38, VALUED_1:5
;
z = p
by A32, TARSKI:def 1;
then
|.(z - o).| <= r
by A1, A3, TOPREAL9:8;
then A41:
|.(z - o).| ^2 <= r ^2
by SQUARE_1:15;
|.(z - o).| ^2 =
(((z - o) `1) ^2) + (((z - o) `2) ^2)
by JGRAPH_1:29
.=
(((z `1) - (o `1)) ^2) + (((z - o) `2) ^2)
by TOPREAL3:3
.=
(((z `1) - (o `1)) ^2) + (((z `2) - (o `2)) ^2)
by TOPREAL3:3
;
then
((((z `1) - (o `1)) ^2) + (((z `2) - (o `2)) ^2)) - (r ^2) <= (r ^2) - (r ^2)
by A41, XREAL_1:9;
hence
0 >= b
by A30, A33, A40;
verum end;
then reconsider p2 = ((((diffX2_1 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) ((diffX2_1 o) | [:((cl_Ball (o,r)) \ {p}),{p}:])) + (((diffX2_2 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) ((diffX2_2 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]))) - (f1 | [:((cl_Ball (o,r)) \ {p}),{p}:]) as nonpositive-yielding continuous RealMap of ([:(TOP-REAL 2),(TOP-REAL 2):] | [:((cl_Ball (o,r)) \ {p}),{p}:]) by PARTFUN3:def 3;
set pp = (((((diffX2_1 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_1 | [:((cl_Ball (o,r)) \ {p}),{p}:])) + (((diffX2_2 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_2 | [:((cl_Ball (o,r)) \ {p}),{p}:]))) (#) ((((diffX2_1 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_1 | [:((cl_Ball (o,r)) \ {p}),{p}:])) + (((diffX2_2 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_2 | [:((cl_Ball (o,r)) \ {p}),{p}:])))) - (m (#) p2);
set k = ((- ((((diffX2_1 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_1 | [:((cl_Ball (o,r)) \ {p}),{p}:])) + (((diffX2_2 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_2 | [:((cl_Ball (o,r)) \ {p}),{p}:])))) + (sqrt ((((((diffX2_1 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_1 | [:((cl_Ball (o,r)) \ {p}),{p}:])) + (((diffX2_2 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_2 | [:((cl_Ball (o,r)) \ {p}),{p}:]))) (#) ((((diffX2_1 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_1 | [:((cl_Ball (o,r)) \ {p}),{p}:])) + (((diffX2_2 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_2 | [:((cl_Ball (o,r)) \ {p}),{p}:])))) - (m (#) p2)))) / m;
set x3 = (Proj2_1 | [:((cl_Ball (o,r)) \ {p}),{p}:]) + ((((- ((((diffX2_1 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_1 | [:((cl_Ball (o,r)) \ {p}),{p}:])) + (((diffX2_2 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_2 | [:((cl_Ball (o,r)) \ {p}),{p}:])))) + (sqrt ((((((diffX2_1 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_1 | [:((cl_Ball (o,r)) \ {p}),{p}:])) + (((diffX2_2 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_2 | [:((cl_Ball (o,r)) \ {p}),{p}:]))) (#) ((((diffX2_1 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_1 | [:((cl_Ball (o,r)) \ {p}),{p}:])) + (((diffX2_2 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_2 | [:((cl_Ball (o,r)) \ {p}),{p}:])))) - (m (#) p2)))) / m) (#) (diffX1_X2_1 | [:((cl_Ball (o,r)) \ {p}),{p}:]));
set y3 = (Proj2_2 | [:((cl_Ball (o,r)) \ {p}),{p}:]) + ((((- ((((diffX2_1 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_1 | [:((cl_Ball (o,r)) \ {p}),{p}:])) + (((diffX2_2 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_2 | [:((cl_Ball (o,r)) \ {p}),{p}:])))) + (sqrt ((((((diffX2_1 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_1 | [:((cl_Ball (o,r)) \ {p}),{p}:])) + (((diffX2_2 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_2 | [:((cl_Ball (o,r)) \ {p}),{p}:]))) (#) ((((diffX2_1 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_1 | [:((cl_Ball (o,r)) \ {p}),{p}:])) + (((diffX2_2 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_2 | [:((cl_Ball (o,r)) \ {p}),{p}:])))) - (m (#) p2)))) / m) (#) (diffX1_X2_2 | [:((cl_Ball (o,r)) \ {p}),{p}:]));
reconsider X3 = (Proj2_1 | [:((cl_Ball (o,r)) \ {p}),{p}:]) + ((((- ((((diffX2_1 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_1 | [:((cl_Ball (o,r)) \ {p}),{p}:])) + (((diffX2_2 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_2 | [:((cl_Ball (o,r)) \ {p}),{p}:])))) + (sqrt ((((((diffX2_1 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_1 | [:((cl_Ball (o,r)) \ {p}),{p}:])) + (((diffX2_2 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_2 | [:((cl_Ball (o,r)) \ {p}),{p}:]))) (#) ((((diffX2_1 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_1 | [:((cl_Ball (o,r)) \ {p}),{p}:])) + (((diffX2_2 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_2 | [:((cl_Ball (o,r)) \ {p}),{p}:])))) - (m (#) p2)))) / m) (#) (diffX1_X2_1 | [:((cl_Ball (o,r)) \ {p}),{p}:])), Y3 = (Proj2_2 | [:((cl_Ball (o,r)) \ {p}),{p}:]) + ((((- ((((diffX2_1 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_1 | [:((cl_Ball (o,r)) \ {p}),{p}:])) + (((diffX2_2 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_2 | [:((cl_Ball (o,r)) \ {p}),{p}:])))) + (sqrt ((((((diffX2_1 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_1 | [:((cl_Ball (o,r)) \ {p}),{p}:])) + (((diffX2_2 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_2 | [:((cl_Ball (o,r)) \ {p}),{p}:]))) (#) ((((diffX2_1 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_1 | [:((cl_Ball (o,r)) \ {p}),{p}:])) + (((diffX2_2 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_2 | [:((cl_Ball (o,r)) \ {p}),{p}:])))) - (m (#) p2)))) / m) (#) (diffX1_X2_2 | [:((cl_Ball (o,r)) \ {p}),{p}:])) as Function of ([:(TOP-REAL 2),(TOP-REAL 2):] | [:((cl_Ball (o,r)) \ {p}),{p}:]),R^1 by TOPMETR:17;
set F = <:X3,Y3:>;
set R = R2Homeomorphism ;
A42:
for x being Point of ((TOP-REAL 2) | ((cl_Ball (o,r)) \ {p})) holds (DiskProj (o,r,p)) . x = (R2Homeomorphism * <:X3,Y3:>) . [x,p]
proof
let x be
Point of
((TOP-REAL 2) | ((cl_Ball (o,r)) \ {p}));
(DiskProj (o,r,p)) . x = (R2Homeomorphism * <:X3,Y3:>) . [x,p]
consider y being
Point of
(TOP-REAL 2) such that A43:
x = y
and A44:
(DiskProj (o,r,p)) . x = HC (
p,
y,
o,
r)
by A1, Def7;
A45:
x <> p
by A4, ZFMISC_1:56;
A46:
[y,p] in [:((cl_Ball (o,r)) \ {p}),{p}:]
by A2, A4, A43, ZFMISC_1:def 2;
set r1 =
(y `1) - (p `1);
set r2 =
(y `2) - (p `2);
set r3 =
(p `1) - (o `1);
set r4 =
(p `2) - (o `2);
set l =
((- ((((p `1) - (o `1)) * ((y `1) - (p `1))) + (((p `2) - (o `2)) * ((y `2) - (p `2))))) + (sqrt ((((((p `1) - (o `1)) * ((y `1) - (p `1))) + (((p `2) - (o `2)) * ((y `2) - (p `2)))) ^2) - (((((y `1) - (p `1)) ^2) + (((y `2) - (p `2)) ^2)) * (((((p `1) - (o `1)) ^2) + (((p `2) - (o `2)) ^2)) - (r ^2)))))) / ((((y `1) - (p `1)) ^2) + (((y `2) - (p `2)) ^2));
A47:
Proj2_1 . [y,p] = ([y,p] `2) `1
by Def5;
A48:
Proj2_2 . [y,p] = ([y,p] `2) `2
by Def6;
A49:
diffX1_X2_1 . [y,p] = (([y,p] `1) `1) - (([y,p] `2) `1)
by Def3;
A50:
diffX1_X2_2 . [y,p] = (([y,p] `1) `2) - (([y,p] `2) `2)
by Def4;
A51:
(diffX2_1 o) . [y,p] = (([y,p] `2) `1) - (o `1)
by Def1;
A52:
(diffX2_2 o) . [y,p] = (([y,p] `2) `2) - (o `2)
by Def2;
A53:
dom X3 = the
carrier of
([:(TOP-REAL 2),(TOP-REAL 2):] | [:((cl_Ball (o,r)) \ {p}),{p}:])
by FUNCT_2:def 1;
A54:
dom Y3 = the
carrier of
([:(TOP-REAL 2),(TOP-REAL 2):] | [:((cl_Ball (o,r)) \ {p}),{p}:])
by FUNCT_2:def 1;
A55:
dom ((((((diffX2_1 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_1 | [:((cl_Ball (o,r)) \ {p}),{p}:])) + (((diffX2_2 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_2 | [:((cl_Ball (o,r)) \ {p}),{p}:]))) (#) ((((diffX2_1 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_1 | [:((cl_Ball (o,r)) \ {p}),{p}:])) + (((diffX2_2 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_2 | [:((cl_Ball (o,r)) \ {p}),{p}:])))) - (m (#) p2)) = the
carrier of
([:(TOP-REAL 2),(TOP-REAL 2):] | [:((cl_Ball (o,r)) \ {p}),{p}:])
by FUNCT_2:def 1;
A56:
p is
Point of
((TOP-REAL 2) | {p})
by A5, TARSKI:def 1;
then A57:
(diffX1_X2_1 | [:((cl_Ball (o,r)) \ {p}),{p}:]) . [y,p] = diffX1_X2_1 . [y,p]
by A7, A43;
A58:
(diffX1_X2_2 | [:((cl_Ball (o,r)) \ {p}),{p}:]) . [y,p] = diffX1_X2_2 . [y,p]
by A8, A43, A56;
A59:
(f1 | [:((cl_Ball (o,r)) \ {p}),{p}:]) . [y,p] = f1 . [y,p]
by A11, A43, A56;
A60:
((diffX2_1 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) . [y,p] = (diffX2_1 o) . [y,p]
by A12, A43, A56;
A61:
((diffX2_2 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) . [y,p] = (diffX2_2 o) . [y,p]
by A13, A43, A56;
A62:
m . [y,p] =
(((diffX1_X2_1 | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_1 | [:((cl_Ball (o,r)) \ {p}),{p}:])) . [y,p]) + (((diffX1_X2_2 | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_2 | [:((cl_Ball (o,r)) \ {p}),{p}:])) . [y,p])
by A6, A46, VALUED_1:1
.=
(((diffX1_X2_1 | [:((cl_Ball (o,r)) \ {p}),{p}:]) . [y,p]) * ((diffX1_X2_1 | [:((cl_Ball (o,r)) \ {p}),{p}:]) . [y,p])) + (((diffX1_X2_2 | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_2 | [:((cl_Ball (o,r)) \ {p}),{p}:])) . [y,p])
by VALUED_1:5
.=
(((y `1) - (p `1)) ^2) + (((y `2) - (p `2)) ^2)
by A49, A50, A57, A58, VALUED_1:5
;
A63:
(((diffX2_1 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_1 | [:((cl_Ball (o,r)) \ {p}),{p}:])) . [y,p] = (((diffX2_1 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) . [y,p]) * ((diffX1_X2_1 | [:((cl_Ball (o,r)) \ {p}),{p}:]) . [y,p])
by VALUED_1:5;
A64:
(((diffX2_2 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_2 | [:((cl_Ball (o,r)) \ {p}),{p}:])) . [y,p] = (((diffX2_2 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) . [y,p]) * ((diffX1_X2_2 | [:((cl_Ball (o,r)) \ {p}),{p}:]) . [y,p])
by VALUED_1:5;
A65:
((((diffX2_1 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_1 | [:((cl_Ball (o,r)) \ {p}),{p}:])) + (((diffX2_2 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_2 | [:((cl_Ball (o,r)) \ {p}),{p}:]))) . [y,p] = ((((diffX2_1 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_1 | [:((cl_Ball (o,r)) \ {p}),{p}:])) . [y,p]) + ((((diffX2_2 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_2 | [:((cl_Ball (o,r)) \ {p}),{p}:])) . [y,p])
by A6, A46, VALUED_1:1;
then A66:
(((((diffX2_1 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_1 | [:((cl_Ball (o,r)) \ {p}),{p}:])) + (((diffX2_2 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_2 | [:((cl_Ball (o,r)) \ {p}),{p}:]))) (#) ((((diffX2_1 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_1 | [:((cl_Ball (o,r)) \ {p}),{p}:])) + (((diffX2_2 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_2 | [:((cl_Ball (o,r)) \ {p}),{p}:])))) . [y,p] = ((((p `1) - (o `1)) * ((y `1) - (p `1))) + (((p `2) - (o `2)) * ((y `2) - (p `2)))) ^2
by A49, A50, A51, A52, A57, A58, A60, A61, A63, A64, VALUED_1:5;
A67:
p2 . [y,p] =
(((((diffX2_1 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) ((diffX2_1 o) | [:((cl_Ball (o,r)) \ {p}),{p}:])) + (((diffX2_2 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) ((diffX2_2 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]))) . [y,p]) - ((f1 | [:((cl_Ball (o,r)) \ {p}),{p}:]) . [y,p])
by A6, A28, A46, VALUED_1:13
.=
(((((diffX2_1 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) ((diffX2_1 o) | [:((cl_Ball (o,r)) \ {p}),{p}:])) + (((diffX2_2 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) ((diffX2_2 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]))) . [y,p]) - (r ^2)
by A59, FUNCOP_1:7
.=
(((((diffX2_1 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) ((diffX2_1 o) | [:((cl_Ball (o,r)) \ {p}),{p}:])) . [y,p]) + ((((diffX2_2 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) ((diffX2_2 o) | [:((cl_Ball (o,r)) \ {p}),{p}:])) . [y,p])) - (r ^2)
by A6, A46, VALUED_1:1
.=
(((((diffX2_1 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) . [y,p]) * (((diffX2_1 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) . [y,p])) + ((((diffX2_2 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) ((diffX2_2 o) | [:((cl_Ball (o,r)) \ {p}),{p}:])) . [y,p])) - (r ^2)
by VALUED_1:5
.=
((((p `1) - (o `1)) ^2) + (((p `2) - (o `2)) ^2)) - (r ^2)
by A51, A52, A60, A61, VALUED_1:5
;
dom (sqrt ((((((diffX2_1 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_1 | [:((cl_Ball (o,r)) \ {p}),{p}:])) + (((diffX2_2 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_2 | [:((cl_Ball (o,r)) \ {p}),{p}:]))) (#) ((((diffX2_1 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_1 | [:((cl_Ball (o,r)) \ {p}),{p}:])) + (((diffX2_2 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_2 | [:((cl_Ball (o,r)) \ {p}),{p}:])))) - (m (#) p2))) = the
carrier of
([:(TOP-REAL 2),(TOP-REAL 2):] | [:((cl_Ball (o,r)) \ {p}),{p}:])
by FUNCT_2:def 1;
then A68:
(sqrt ((((((diffX2_1 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_1 | [:((cl_Ball (o,r)) \ {p}),{p}:])) + (((diffX2_2 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_2 | [:((cl_Ball (o,r)) \ {p}),{p}:]))) (#) ((((diffX2_1 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_1 | [:((cl_Ball (o,r)) \ {p}),{p}:])) + (((diffX2_2 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_2 | [:((cl_Ball (o,r)) \ {p}),{p}:])))) - (m (#) p2))) . [y,p] =
sqrt (((((((diffX2_1 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_1 | [:((cl_Ball (o,r)) \ {p}),{p}:])) + (((diffX2_2 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_2 | [:((cl_Ball (o,r)) \ {p}),{p}:]))) (#) ((((diffX2_1 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_1 | [:((cl_Ball (o,r)) \ {p}),{p}:])) + (((diffX2_2 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_2 | [:((cl_Ball (o,r)) \ {p}),{p}:])))) - (m (#) p2)) . [y,p])
by A6, A46, PARTFUN3:def 5
.=
sqrt (((((((diffX2_1 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_1 | [:((cl_Ball (o,r)) \ {p}),{p}:])) + (((diffX2_2 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_2 | [:((cl_Ball (o,r)) \ {p}),{p}:]))) (#) ((((diffX2_1 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_1 | [:((cl_Ball (o,r)) \ {p}),{p}:])) + (((diffX2_2 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_2 | [:((cl_Ball (o,r)) \ {p}),{p}:])))) . [y,p]) - ((m (#) p2) . [y,p]))
by A6, A46, A55, VALUED_1:13
.=
sqrt ((((((p `1) - (o `1)) * ((y `1) - (p `1))) + (((p `2) - (o `2)) * ((y `2) - (p `2)))) ^2) - (((((y `1) - (p `1)) ^2) + (((y `2) - (p `2)) ^2)) * (((((p `1) - (o `1)) ^2) + (((p `2) - (o `2)) ^2)) - (r ^2))))
by A62, A66, A67, VALUED_1:5
;
dom (((- ((((diffX2_1 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_1 | [:((cl_Ball (o,r)) \ {p}),{p}:])) + (((diffX2_2 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_2 | [:((cl_Ball (o,r)) \ {p}),{p}:])))) + (sqrt ((((((diffX2_1 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_1 | [:((cl_Ball (o,r)) \ {p}),{p}:])) + (((diffX2_2 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_2 | [:((cl_Ball (o,r)) \ {p}),{p}:]))) (#) ((((diffX2_1 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_1 | [:((cl_Ball (o,r)) \ {p}),{p}:])) + (((diffX2_2 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_2 | [:((cl_Ball (o,r)) \ {p}),{p}:])))) - (m (#) p2)))) / m) = the
carrier of
([:(TOP-REAL 2),(TOP-REAL 2):] | [:((cl_Ball (o,r)) \ {p}),{p}:])
by FUNCT_2:def 1;
then A69:
(((- ((((diffX2_1 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_1 | [:((cl_Ball (o,r)) \ {p}),{p}:])) + (((diffX2_2 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_2 | [:((cl_Ball (o,r)) \ {p}),{p}:])))) + (sqrt ((((((diffX2_1 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_1 | [:((cl_Ball (o,r)) \ {p}),{p}:])) + (((diffX2_2 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_2 | [:((cl_Ball (o,r)) \ {p}),{p}:]))) (#) ((((diffX2_1 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_1 | [:((cl_Ball (o,r)) \ {p}),{p}:])) + (((diffX2_2 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_2 | [:((cl_Ball (o,r)) \ {p}),{p}:])))) - (m (#) p2)))) / m) . [y,p] =
(((- ((((diffX2_1 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_1 | [:((cl_Ball (o,r)) \ {p}),{p}:])) + (((diffX2_2 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_2 | [:((cl_Ball (o,r)) \ {p}),{p}:])))) + (sqrt ((((((diffX2_1 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_1 | [:((cl_Ball (o,r)) \ {p}),{p}:])) + (((diffX2_2 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_2 | [:((cl_Ball (o,r)) \ {p}),{p}:]))) (#) ((((diffX2_1 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_1 | [:((cl_Ball (o,r)) \ {p}),{p}:])) + (((diffX2_2 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_2 | [:((cl_Ball (o,r)) \ {p}),{p}:])))) - (m (#) p2)))) . [y,p]) * ((m . [y,p]) ")
by A6, A46, RFUNCT_1:def 1
.=
(((- ((((diffX2_1 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_1 | [:((cl_Ball (o,r)) \ {p}),{p}:])) + (((diffX2_2 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_2 | [:((cl_Ball (o,r)) \ {p}),{p}:])))) + (sqrt ((((((diffX2_1 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_1 | [:((cl_Ball (o,r)) \ {p}),{p}:])) + (((diffX2_2 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_2 | [:((cl_Ball (o,r)) \ {p}),{p}:]))) (#) ((((diffX2_1 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_1 | [:((cl_Ball (o,r)) \ {p}),{p}:])) + (((diffX2_2 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_2 | [:((cl_Ball (o,r)) \ {p}),{p}:])))) - (m (#) p2)))) . [y,p]) / (m . [y,p])
by XCMPLX_0:def 9
.=
(((- ((((diffX2_1 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_1 | [:((cl_Ball (o,r)) \ {p}),{p}:])) + (((diffX2_2 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_2 | [:((cl_Ball (o,r)) \ {p}),{p}:])))) . [y,p]) + ((sqrt ((((((diffX2_1 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_1 | [:((cl_Ball (o,r)) \ {p}),{p}:])) + (((diffX2_2 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_2 | [:((cl_Ball (o,r)) \ {p}),{p}:]))) (#) ((((diffX2_1 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_1 | [:((cl_Ball (o,r)) \ {p}),{p}:])) + (((diffX2_2 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_2 | [:((cl_Ball (o,r)) \ {p}),{p}:])))) - (m (#) p2))) . [y,p])) / ((((y `1) - (p `1)) ^2) + (((y `2) - (p `2)) ^2))
by A6, A46, A62, VALUED_1:1
.=
((- ((((p `1) - (o `1)) * ((y `1) - (p `1))) + (((p `2) - (o `2)) * ((y `2) - (p `2))))) + (sqrt ((((((p `1) - (o `1)) * ((y `1) - (p `1))) + (((p `2) - (o `2)) * ((y `2) - (p `2)))) ^2) - (((((y `1) - (p `1)) ^2) + (((y `2) - (p `2)) ^2)) * (((((p `1) - (o `1)) ^2) + (((p `2) - (o `2)) ^2)) - (r ^2)))))) / ((((y `1) - (p `1)) ^2) + (((y `2) - (p `2)) ^2))
by A49, A50, A51, A52, A57, A58, A60, A61, A63, A64, A65, A68, VALUED_1:8
;
A70:
X3 . [y,p] =
((Proj2_1 | [:((cl_Ball (o,r)) \ {p}),{p}:]) . [y,p]) + (((((- ((((diffX2_1 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_1 | [:((cl_Ball (o,r)) \ {p}),{p}:])) + (((diffX2_2 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_2 | [:((cl_Ball (o,r)) \ {p}),{p}:])))) + (sqrt ((((((diffX2_1 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_1 | [:((cl_Ball (o,r)) \ {p}),{p}:])) + (((diffX2_2 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_2 | [:((cl_Ball (o,r)) \ {p}),{p}:]))) (#) ((((diffX2_1 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_1 | [:((cl_Ball (o,r)) \ {p}),{p}:])) + (((diffX2_2 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_2 | [:((cl_Ball (o,r)) \ {p}),{p}:])))) - (m (#) p2)))) / m) (#) (diffX1_X2_1 | [:((cl_Ball (o,r)) \ {p}),{p}:])) . [y,p])
by A6, A46, VALUED_1:1
.=
(p `1) + (((((- ((((diffX2_1 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_1 | [:((cl_Ball (o,r)) \ {p}),{p}:])) + (((diffX2_2 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_2 | [:((cl_Ball (o,r)) \ {p}),{p}:])))) + (sqrt ((((((diffX2_1 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_1 | [:((cl_Ball (o,r)) \ {p}),{p}:])) + (((diffX2_2 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_2 | [:((cl_Ball (o,r)) \ {p}),{p}:]))) (#) ((((diffX2_1 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_1 | [:((cl_Ball (o,r)) \ {p}),{p}:])) + (((diffX2_2 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_2 | [:((cl_Ball (o,r)) \ {p}),{p}:])))) - (m (#) p2)))) / m) (#) (diffX1_X2_1 | [:((cl_Ball (o,r)) \ {p}),{p}:])) . [y,p])
by A9, A43, A47, A56
.=
(p `1) + ((((- ((((p `1) - (o `1)) * ((y `1) - (p `1))) + (((p `2) - (o `2)) * ((y `2) - (p `2))))) + (sqrt ((((((p `1) - (o `1)) * ((y `1) - (p `1))) + (((p `2) - (o `2)) * ((y `2) - (p `2)))) ^2) - (((((y `1) - (p `1)) ^2) + (((y `2) - (p `2)) ^2)) * (((((p `1) - (o `1)) ^2) + (((p `2) - (o `2)) ^2)) - (r ^2)))))) / ((((y `1) - (p `1)) ^2) + (((y `2) - (p `2)) ^2))) * ((y `1) - (p `1)))
by A49, A57, A69, VALUED_1:5
;
A71:
Y3 . [y,p] =
((Proj2_2 | [:((cl_Ball (o,r)) \ {p}),{p}:]) . [y,p]) + (((((- ((((diffX2_1 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_1 | [:((cl_Ball (o,r)) \ {p}),{p}:])) + (((diffX2_2 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_2 | [:((cl_Ball (o,r)) \ {p}),{p}:])))) + (sqrt ((((((diffX2_1 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_1 | [:((cl_Ball (o,r)) \ {p}),{p}:])) + (((diffX2_2 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_2 | [:((cl_Ball (o,r)) \ {p}),{p}:]))) (#) ((((diffX2_1 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_1 | [:((cl_Ball (o,r)) \ {p}),{p}:])) + (((diffX2_2 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_2 | [:((cl_Ball (o,r)) \ {p}),{p}:])))) - (m (#) p2)))) / m) (#) (diffX1_X2_2 | [:((cl_Ball (o,r)) \ {p}),{p}:])) . [y,p])
by A6, A46, VALUED_1:1
.=
(p `2) + (((((- ((((diffX2_1 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_1 | [:((cl_Ball (o,r)) \ {p}),{p}:])) + (((diffX2_2 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_2 | [:((cl_Ball (o,r)) \ {p}),{p}:])))) + (sqrt ((((((diffX2_1 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_1 | [:((cl_Ball (o,r)) \ {p}),{p}:])) + (((diffX2_2 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_2 | [:((cl_Ball (o,r)) \ {p}),{p}:]))) (#) ((((diffX2_1 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_1 | [:((cl_Ball (o,r)) \ {p}),{p}:])) + (((diffX2_2 o) | [:((cl_Ball (o,r)) \ {p}),{p}:]) (#) (diffX1_X2_2 | [:((cl_Ball (o,r)) \ {p}),{p}:])))) - (m (#) p2)))) / m) (#) (diffX1_X2_2 | [:((cl_Ball (o,r)) \ {p}),{p}:])) . [y,p])
by A10, A43, A48, A56
.=
(p `2) + ((((- ((((p `1) - (o `1)) * ((y `1) - (p `1))) + (((p `2) - (o `2)) * ((y `2) - (p `2))))) + (sqrt ((((((p `1) - (o `1)) * ((y `1) - (p `1))) + (((p `2) - (o `2)) * ((y `2) - (p `2)))) ^2) - (((((y `1) - (p `1)) ^2) + (((y `2) - (p `2)) ^2)) * (((((p `1) - (o `1)) ^2) + (((p `2) - (o `2)) ^2)) - (r ^2)))))) / ((((y `1) - (p `1)) ^2) + (((y `2) - (p `2)) ^2))) * ((y `2) - (p `2)))
by A50, A58, A69, VALUED_1:5
;
A72:
y in (cl_Ball (o,r)) \ {p}
by A4, A43;
(cl_Ball (o,r)) \ {p} c= cl_Ball (
o,
r)
by XBOOLE_1:36;
hence (DiskProj (o,r,p)) . x =
|[((p `1) + ((((- ((((p `1) - (o `1)) * ((y `1) - (p `1))) + (((p `2) - (o `2)) * ((y `2) - (p `2))))) + (sqrt ((((((p `1) - (o `1)) * ((y `1) - (p `1))) + (((p `2) - (o `2)) * ((y `2) - (p `2)))) ^2) - (((((y `1) - (p `1)) ^2) + (((y `2) - (p `2)) ^2)) * (((((p `1) - (o `1)) ^2) + (((p `2) - (o `2)) ^2)) - (r ^2)))))) / ((((y `1) - (p `1)) ^2) + (((y `2) - (p `2)) ^2))) * ((y `1) - (p `1)))),((p `2) + ((((- ((((p `1) - (o `1)) * ((y `1) - (p `1))) + (((p `2) - (o `2)) * ((y `2) - (p `2))))) + (sqrt ((((((p `1) - (o `1)) * ((y `1) - (p `1))) + (((p `2) - (o `2)) * ((y `2) - (p `2)))) ^2) - (((((y `1) - (p `1)) ^2) + (((y `2) - (p `2)) ^2)) * (((((p `1) - (o `1)) ^2) + (((p `2) - (o `2)) ^2)) - (r ^2)))))) / ((((y `1) - (p `1)) ^2) + (((y `2) - (p `2)) ^2))) * ((y `2) - (p `2))))]|
by A1, A3, A43, A44, A45, A72, BROUWER:8
.=
R2Homeomorphism . [(X3 . [y,p]),(Y3 . [y,p])]
by A70, A71, TOPREALA:def 2
.=
R2Homeomorphism . (<:X3,Y3:> . [y,p])
by A6, A46, A53, A54, FUNCT_3:49
.=
(R2Homeomorphism * <:X3,Y3:>) . [x,p]
by A6, A43, A46, FUNCT_2:15
;
verum
end;
A73:
X3 is continuous
by JORDAN5A:27;
Y3 is continuous
by JORDAN5A:27;
then reconsider F = <:X3,Y3:> as continuous Function of ([:(TOP-REAL 2),(TOP-REAL 2):] | [:((cl_Ball (o,r)) \ {p}),{p}:]),[:R^1,R^1:] by A73, YELLOW12:41;
for pp being Point of ((TOP-REAL 2) | ((cl_Ball (o,r)) \ {p}))
for V being Subset of (Tcircle (o,r)) st (DiskProj (o,r,p)) . pp in V & V is open holds
ex W being Subset of ((TOP-REAL 2) | ((cl_Ball (o,r)) \ {p})) st
( pp in W & W is open & (DiskProj (o,r,p)) .: W c= V )
proof
let pp be
Point of
((TOP-REAL 2) | ((cl_Ball (o,r)) \ {p}));
for V being Subset of (Tcircle (o,r)) st (DiskProj (o,r,p)) . pp in V & V is open holds
ex W being Subset of ((TOP-REAL 2) | ((cl_Ball (o,r)) \ {p})) st
( pp in W & W is open & (DiskProj (o,r,p)) .: W c= V )let V be
Subset of
(Tcircle (o,r));
( (DiskProj (o,r,p)) . pp in V & V is open implies ex W being Subset of ((TOP-REAL 2) | ((cl_Ball (o,r)) \ {p})) st
( pp in W & W is open & (DiskProj (o,r,p)) .: W c= V ) )
assume that A74:
(DiskProj (o,r,p)) . pp in V
and A75:
V is
open
;
ex W being Subset of ((TOP-REAL 2) | ((cl_Ball (o,r)) \ {p})) st
( pp in W & W is open & (DiskProj (o,r,p)) .: W c= V )
reconsider p1 =
pp,
fp =
p as
Point of
(TOP-REAL 2) by PRE_TOPC:25;
A76:
[pp,p] in [:((cl_Ball (o,r)) \ {p}),{p}:]
by A2, A4, ZFMISC_1:def 2;
consider V1 being
Subset of
(TOP-REAL 2) such that A77:
V1 is
open
and A78:
V1 /\ ([#] (Tcircle (o,r))) = V
by A75, TOPS_2:24;
A79:
(DiskProj (o,r,p)) . pp = (R2Homeomorphism * F) . [pp,p]
by A42;
R2Homeomorphism " is
being_homeomorphism
by TOPREALA:34, TOPS_2:56;
then A80:
(R2Homeomorphism ") .: V1 is
open
by A77, TOPGRP_1:25;
A81:
dom F = the
carrier of
([:(TOP-REAL 2),(TOP-REAL 2):] | [:((cl_Ball (o,r)) \ {p}),{p}:])
by FUNCT_2:def 1;
A82:
dom R2Homeomorphism = the
carrier of
[:R^1,R^1:]
by FUNCT_2:def 1;
then A83:
rng F c= dom R2Homeomorphism
;
then A84:
dom (R2Homeomorphism * F) = dom F
by RELAT_1:27;
A85:
rng R2Homeomorphism = [#] (TOP-REAL 2)
by TOPREALA:34, TOPS_2:def 5;
A86:
(R2Homeomorphism ") * (R2Homeomorphism * F) =
((R2Homeomorphism ") * R2Homeomorphism) * F
by RELAT_1:36
.=
(id (dom R2Homeomorphism)) * F
by A85, TOPREALA:34, TOPS_2:52
;
dom (id (dom R2Homeomorphism)) = dom R2Homeomorphism
;
then A87:
dom ((id (dom R2Homeomorphism)) * F) = dom F
by A83, RELAT_1:27;
for
x being
object st
x in dom F holds
((id (dom R2Homeomorphism)) * F) . x = F . x
then A90:
(id (dom R2Homeomorphism)) * F = F
by A87, FUNCT_1:2;
(R2Homeomorphism * F) . [p1,fp] in V1
by A74, A78, A79, XBOOLE_0:def 4;
then
(R2Homeomorphism ") . ((R2Homeomorphism * F) . [p1,fp]) in (R2Homeomorphism ") .: V1
by FUNCT_2:35;
then
((R2Homeomorphism ") * (R2Homeomorphism * F)) . [p1,fp] in (R2Homeomorphism ") .: V1
by A6, A76, A81, A84, FUNCT_1:13;
then consider W being
Subset of
([:(TOP-REAL 2),(TOP-REAL 2):] | [:((cl_Ball (o,r)) \ {p}),{p}:]) such that A91:
[p1,fp] in W
and A92:
W is
open
and A93:
F .: W c= (R2Homeomorphism ") .: V1
by A6, A76, A80, A86, A90, JGRAPH_2:10;
consider WW being
Subset of
[:(TOP-REAL 2),(TOP-REAL 2):] such that A94:
WW is
open
and A95:
WW /\ ([#] ([:(TOP-REAL 2),(TOP-REAL 2):] | [:((cl_Ball (o,r)) \ {p}),{p}:])) = W
by A92, TOPS_2:24;
consider SF being
Subset-Family of
[:(TOP-REAL 2),(TOP-REAL 2):] such that A96:
WW = union SF
and A97:
for
e being
set st
e in SF holds
ex
X1,
Y1 being
Subset of
(TOP-REAL 2) st
(
e = [:X1,Y1:] &
X1 is
open &
Y1 is
open )
by A94, BORSUK_1:5;
[p1,fp] in WW
by A91, A95, XBOOLE_0:def 4;
then consider Z being
set such that A98:
[p1,fp] in Z
and A99:
Z in SF
by A96, TARSKI:def 4;
consider X1,
Y1 being
Subset of
(TOP-REAL 2) such that A100:
Z = [:X1,Y1:]
and A101:
X1 is
open
and
Y1 is
open
by A97, A99;
set ZZ =
Z /\ ([#] ([:(TOP-REAL 2),(TOP-REAL 2):] | [:((cl_Ball (o,r)) \ {p}),{p}:]));
reconsider XX =
X1 /\ ([#] ((TOP-REAL 2) | ((cl_Ball (o,r)) \ {p}))) as
open Subset of
((TOP-REAL 2) | ((cl_Ball (o,r)) \ {p})) by A101, TOPS_2:24;
take
XX
;
( pp in XX & XX is open & (DiskProj (o,r,p)) .: XX c= V )
pp in X1
by A98, A100, ZFMISC_1:87;
hence
pp in XX
by XBOOLE_0:def 4;
( XX is open & (DiskProj (o,r,p)) .: XX c= V )
thus
XX is
open
;
(DiskProj (o,r,p)) .: XX c= V
let b be
object ;
TARSKI:def 3 ( not b in (DiskProj (o,r,p)) .: XX or b in V )
assume
b in (DiskProj (o,r,p)) .: XX
;
b in V
then consider a being
Point of
((TOP-REAL 2) | ((cl_Ball (o,r)) \ {p})) such that A102:
a in XX
and A103:
b = (DiskProj (o,r,p)) . a
by FUNCT_2:65;
reconsider a1 =
a,
fa =
fp as
Point of
(TOP-REAL 2) by PRE_TOPC:25;
A104:
a in X1
by A102, XBOOLE_0:def 4;
A105:
[a,p] in [:((cl_Ball (o,r)) \ {p}),{p}:]
by A2, A4, ZFMISC_1:def 2;
fa in Y1
by A98, A100, ZFMISC_1:87;
then
[a,fa] in Z
by A100, A104, ZFMISC_1:def 2;
then
[a,fa] in Z /\ ([#] ([:(TOP-REAL 2),(TOP-REAL 2):] | [:((cl_Ball (o,r)) \ {p}),{p}:]))
by A6, A105, XBOOLE_0:def 4;
then A106:
F . [a1,fa] in F .: (Z /\ ([#] ([:(TOP-REAL 2),(TOP-REAL 2):] | [:((cl_Ball (o,r)) \ {p}),{p}:])))
by FUNCT_2:35;
A107:
R2Homeomorphism " = R2Homeomorphism "
by TOPREALA:34, TOPS_2:def 4;
A108:
dom (R2Homeomorphism ") = [#] (TOP-REAL 2)
by A85, TOPREALA:34, TOPS_2:49;
Z c= WW
by A96, A99, ZFMISC_1:74;
then
Z /\ ([#] ([:(TOP-REAL 2),(TOP-REAL 2):] | [:((cl_Ball (o,r)) \ {p}),{p}:])) c= WW /\ ([#] ([:(TOP-REAL 2),(TOP-REAL 2):] | [:((cl_Ball (o,r)) \ {p}),{p}:]))
by XBOOLE_1:27;
then
F .: (Z /\ ([#] ([:(TOP-REAL 2),(TOP-REAL 2):] | [:((cl_Ball (o,r)) \ {p}),{p}:]))) c= F .: W
by A95, RELAT_1:123;
then
F . [a1,fa] in F .: W
by A106;
then
R2Homeomorphism . (F . [a1,fa]) in R2Homeomorphism .: ((R2Homeomorphism ") .: V1)
by A93, FUNCT_2:35;
then
(R2Homeomorphism * F) . [a1,fa] in R2Homeomorphism .: ((R2Homeomorphism ") .: V1)
by A6, A105, FUNCT_2:15;
then
(R2Homeomorphism * F) . [a1,fa] in V1
by A107, A108, PARTFUN3:1, TOPREALA:34;
then
(DiskProj (o,r,p)) . a in V1
by A42;
hence
b in V
by A78, A103, XBOOLE_0:def 4;
verum
end;
hence
DiskProj (o,r,p) is continuous
by JGRAPH_2:10; verum