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