let o, p be Point of (TOP-REAL 2); :: thesis: 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 ; :: thesis: ( p in Ball o,r implies RotateCircle o,r,p is continuous )
assume A1:
p in Ball o,r
; :: thesis: 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:29;
A9:
the carrier of ((TOP-REAL 2) | (Sphere o,r)) = Sphere o,r
by PRE_TOPC:29;
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 Lm8;
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:29;
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});
:: thesis: 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));
:: thesis: (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:72;
:: thesis: 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});
:: thesis: 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));
:: thesis: (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:72;
:: thesis: 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});
:: thesis: 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));
:: thesis: (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:72;
:: thesis: 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});
:: thesis: 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));
:: thesis: (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:72;
:: thesis: 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});
:: thesis: 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));
:: thesis: (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:72;
:: thesis: 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});
:: thesis: 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));
:: thesis: ((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:72;
:: thesis: 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});
:: thesis: 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));
:: thesis: ((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:72;
:: thesis: verum
end;
now let b be
real number ;
:: thesis: ( 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):])))
;
:: thesis: 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 5;
consider y,
z being
set such that A20:
(
y in {p} &
z in Sphere o,
r &
a = [y,z] )
by A10, A18, ZFMISC_1:def 2;
A21:
y = p
by A20, TARSKI:def 1;
reconsider y =
y,
z =
z as
Point of
(TOP-REAL 2) by A20;
A22:
y <> z
by A1, A3, A20, A21, XBOOLE_0:3;
[y,z] = [([y,z] `1 ),([y,z] `2 )]
by Lm7, MCART_1:23;
then A23:
(
y = [y,z] `1 &
z = [y,z] `2 )
by ZFMISC_1:33;
A24:
diffX1_X2_1 . [y,z] = (([y,z] `1 ) `1 ) - (([y,z] `2 ) `1 )
by Def3;
A25:
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 );
A26:
(diffX1_X2_1 | [:{p},(Sphere o,r):]) . [y,z] = diffX1_X2_1 . [y,z]
by A8, A9, A11, A20;
A27:
(diffX1_X2_2 | [:{p},(Sphere o,r):]) . [y,z] = diffX1_X2_2 . [y,z]
by A8, A9, A12, A20;
A28:
(((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, A20, 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 A23, A24, A25, A26, A27, VALUED_1:5
;
hence
0 < b
by A19, A20, A28;
:: thesis: 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 continuous positive-yielding 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):]);
A30:
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 ;
:: thesis: ( 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):]))
;
:: thesis: 0 >= bthen consider a being
set such that A31:
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 A32:
(((((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 5;
consider y,
z being
set such that A33:
(
y in {p} &
z in Sphere o,
r &
a = [y,z] )
by A10, A31, ZFMISC_1:def 2;
reconsider y =
y,
z =
z as
Point of
(TOP-REAL 2) by A33;
set r3 =
(z `1 ) - (o `1 );
set r4 =
(z `2 ) - (o `2 );
A34:
(f1 | [:{p},(Sphere o,r):]) . [y,z] = f1 . [y,z]
by A8, A9, A15, A33;
A35:
((diffX2_1 o) | [:{p},(Sphere o,r):]) . [y,z] = (diffX2_1 o) . [y,z]
by A8, A9, A16, A33;
A36:
((diffX2_2 o) | [:{p},(Sphere o,r):]) . [y,z] = (diffX2_2 o) . [y,z]
by A8, A9, A17, A33;
[y,z] = [([y,z] `1 ),([y,z] `2 )]
by Lm7, MCART_1:23;
then A37:
(
y = [y,z] `1 &
z = [y,z] `2 )
by ZFMISC_1:33;
A38:
(diffX2_1 o) . [y,z] = (([y,z] `2 ) `1 ) - (o `1 )
by Def1;
A39:
(diffX2_2 o) . [y,z] = (([y,z] `2 ) `2 ) - (o `2 )
by Def2;
A40:
(((((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 A31, A33, 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 A34, FUNCOP_1:13
.=
(((((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 A31, A33, VALUED_1:1
.=
(((((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 A35, A36, A37, A38, A39, VALUED_1:5
;
|.(z - o).| <= r
by A5, A33, TOPREAL9:8;
then A41:
|.(z - o).| ^2 <= r ^2
by SQUARE_1:77;
|.(z - o).| ^2 =
(((z - o) `1 ) ^2 ) + (((z - o) `2 ) ^2 )
by JGRAPH_1:46
.=
(((z `1 ) - (o `1 )) ^2 ) + (((z - o) `2 ) ^2 )
by TOPREAL3:8
.=
(((z `1 ) - (o `1 )) ^2 ) + (((z `2 ) - (o `2 )) ^2 )
by TOPREAL3:8
;
then
((((z `1 ) - (o `1 )) ^2 ) + (((z `2 ) - (o `2 )) ^2 )) - (r ^2 ) <= (r ^2 ) - (r ^2 )
by A41, XREAL_1:11;
hence
0 >= b
by A32, A33, A40;
:: thesis: 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 continuous nonpositive-yielding 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:24;
set F = <:X3,Y3:>;
set R = R2Homeomorphism ;
A42:
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));
:: thesis: (RotateCircle o,r,p) . x = (R2Homeomorphism * <:X3,Y3:>) . [p,x]
consider y being
Point of
(TOP-REAL 2) such that A43:
(
x = y &
(RotateCircle o,r,p) . x = HC y,
p,
o,
r )
by A1, A2, Def8;
A44:
x <> p
by A1, A3, A9, XBOOLE_0:3;
A45:
[p,y] in [:{p},(Sphere o,r):]
by A4, A9, A43, 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 ));
[p,y] = [([p,y] `1 ),([p,y] `2 )]
by Lm7, MCART_1:23;
then A46:
(
p = [p,y] `1 &
y = [p,y] `2 )
by ZFMISC_1:33;
A47:
Proj2_1 . [p,y] = ([p,y] `2 ) `1
by Def5;
A48:
Proj2_2 . [p,y] = ([p,y] `2 ) `2
by Def6;
A49:
diffX1_X2_1 . [p,y] = (([p,y] `1 ) `1 ) - (([p,y] `2 ) `1 )
by Def3;
A50:
diffX1_X2_2 . [p,y] = (([p,y] `1 ) `2 ) - (([p,y] `2 ) `2 )
by Def4;
A51:
(diffX2_1 o) . [p,y] = (([p,y] `2 ) `1 ) - (o `1 )
by Def1;
A52:
(diffX2_2 o) . [p,y] = (([p,y] `2 ) `2 ) - (o `2 )
by Def2;
A53:
dom X3 = the
carrier of
([:(TOP-REAL 2),(TOP-REAL 2):] | [:{p},(Sphere o,r):])
by FUNCT_2:def 1;
A54:
dom Y3 = the
carrier of
([:(TOP-REAL 2),(TOP-REAL 2):] | [:{p},(Sphere o,r):])
by FUNCT_2:def 1;
A55:
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;
A56:
(
y is
Point of
((TOP-REAL 2) | (Sphere o,r)) &
p is
Point of
((TOP-REAL 2) | {p}) )
by A8, A43, TARSKI:def 1;
then A57:
(diffX1_X2_1 | [:{p},(Sphere o,r):]) . [p,y] = diffX1_X2_1 . [p,y]
by A11;
A58:
(diffX1_X2_2 | [:{p},(Sphere o,r):]) . [p,y] = diffX1_X2_2 . [p,y]
by A12, A56;
A59:
(f1 | [:{p},(Sphere o,r):]) . [p,y] = f1 . [p,y]
by A15, A56;
A60:
((diffX2_1 o) | [:{p},(Sphere o,r):]) . [p,y] = (diffX2_1 o) . [p,y]
by A16, A56;
A61:
((diffX2_2 o) | [:{p},(Sphere o,r):]) . [p,y] = (diffX2_2 o) . [p,y]
by A17, A56;
A62:
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, A45, 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 A46, A49, A50, A57, A58, VALUED_1:5
;
A63:
(((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;
A64:
(((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;
A65:
((((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, A45, VALUED_1:1;
then A66:
(((((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 A46, A49, A50, A51, A52, A57, A58, A60, A61, A63, A64, VALUED_1:5;
A67:
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, A30, A45, 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 A59, FUNCOP_1:13
.=
(((((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, A45, 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 A46, A51, A52, A60, A61, 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 A68:
(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, A45, 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, A45, A55, 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 A62, A66, A67, 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 A69:
(((- ((((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, A45, RFUNCT_1:def 4
.=
(((- ((((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, A45, A62, 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 A46, A49, A50, A51, A52, A57, A58, A60, A61, A63, A64, A65, A68, VALUED_1:8
;
A70:
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, A45, 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, A46, A47, A56
.=
(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 A46, A49, A57, A69, VALUED_1:5
;
A71:
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, A45, 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, A46, A48, A56
.=
(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 A46, A50, A58, A69, VALUED_1:5
;
y in the
carrier of
((TOP-REAL 2) | (Sphere o,r))
by A43;
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, A43, A44, BROUWER:8
.=
R2Homeomorphism . [(X3 . [p,y]),(Y3 . [p,y])]
by A70, A71, TOPREALA:def 2
.=
R2Homeomorphism . (<:X3,Y3:> . [p,y])
by A10, A45, A53, A54, FUNCT_3:69
.=
(R2Homeomorphism * <:X3,Y3:>) . [p,x]
by A10, A43, A45, FUNCT_2:21
;
:: thesis: verum
end;
( X3 is continuous & Y3 is continuous )
by TOPREAL6:83;
then reconsider F = <:X3,Y3:> as continuous Function of ([:(TOP-REAL 2),(TOP-REAL 2):] | [:{p},(Sphere o,r):]),[:R^1 ,R^1 :] by 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));
:: thesis: 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);
:: thesis: ( (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 A72:
(RotateCircle o,r,p) . pp in V
and A73:
V is
open
;
:: thesis: 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:55;
A74:
[p,pp] in [:{p},(Sphere o,r):]
by A4, A9, ZFMISC_1:def 2;
consider V1 being
Subset of
(TOP-REAL 2) such that A75:
V1 is
open
and A76:
V1 /\ ([#] (Tcircle o,r)) = V
by A73, TOPS_2:32;
A77:
(RotateCircle o,r,p) . pp = (R2Homeomorphism * F) . [p,pp]
by A42;
R2Homeomorphism " is
being_homeomorphism
by TOPREALA:56, TOPS_2:70;
then A78:
(R2Homeomorphism " ) .: V1 is
open
by A75, TOPGRP_1:25;
A79:
dom F = the
carrier of
([:(TOP-REAL 2),(TOP-REAL 2):] | [:{p},(Sphere o,r):])
by FUNCT_2:def 1;
A80:
dom R2Homeomorphism = the
carrier of
[:R^1 ,R^1 :]
by FUNCT_2:def 1;
then A81:
rng F c= dom R2Homeomorphism
;
then A82:
dom (R2Homeomorphism * F) = dom F
by RELAT_1:46;
A83:
(
rng R2Homeomorphism = [#] (TOP-REAL 2) &
R2Homeomorphism is
one-to-one )
by TOPREALA:56, TOPS_2:def 5;
A84:
(R2Homeomorphism " ) * (R2Homeomorphism * F) =
((R2Homeomorphism " ) * R2Homeomorphism ) * F
by RELAT_1:55
.=
(id (dom R2Homeomorphism )) * F
by A83, TOPS_2:65
;
dom (id (dom R2Homeomorphism )) = dom R2Homeomorphism
by RELAT_1:71;
then A85:
dom ((id (dom R2Homeomorphism )) * F) = dom F
by A81, RELAT_1:46;
for
x being
set st
x in dom F holds
((id (dom R2Homeomorphism )) * F) . x = F . x
then A88:
(id (dom R2Homeomorphism )) * F = F
by A85, FUNCT_1:9;
(R2Homeomorphism * F) . [fp,p1] in V1
by A72, A76, A77, XBOOLE_0:def 4;
then
(R2Homeomorphism " ) . ((R2Homeomorphism * F) . [fp,p1]) in (R2Homeomorphism " ) .: V1
by FUNCT_2:43;
then
((R2Homeomorphism " ) * (R2Homeomorphism * F)) . [fp,p1] in (R2Homeomorphism " ) .: V1
by A10, A74, A79, A82, FUNCT_1:23;
then consider W being
Subset of
([:(TOP-REAL 2),(TOP-REAL 2):] | [:{p},(Sphere o,r):]) such that A89:
[fp,p1] in W
and A90:
W is
open
and A91:
F .: W c= (R2Homeomorphism " ) .: V1
by A10, A74, A78, A84, A88, JGRAPH_2:20;
consider WW being
Subset of
[:(TOP-REAL 2),(TOP-REAL 2):] such that A92:
WW is
open
and A93:
WW /\ ([#] ([:(TOP-REAL 2),(TOP-REAL 2):] | [:{p},(Sphere o,r):])) = W
by A90, TOPS_2:32;
consider SF being
Subset-Family of
[:(TOP-REAL 2),(TOP-REAL 2):] such that A94:
WW = union SF
and A95:
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 A92, BORSUK_1:45;
[fp,p1] in WW
by A89, A93, XBOOLE_0:def 4;
then consider Z being
set such that A96:
[fp,p1] in Z
and A97:
Z in SF
by A94, TARSKI:def 4;
consider X1,
Y1 being
Subset of
(TOP-REAL 2) such that A98:
Z = [:X1,Y1:]
and
X1 is
open
and A99:
Y1 is
open
by A95, A97;
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 A99, TOPS_2:32;
take
XX
;
:: thesis: ( pp in XX & XX is open & (RotateCircle o,r,p) .: XX c= V )
pp in Y1
by A96, A98, ZFMISC_1:106;
hence
pp in XX
by XBOOLE_0:def 4;
:: thesis: ( XX is open & (RotateCircle o,r,p) .: XX c= V )
thus
XX is
open
;
:: thesis: (RotateCircle o,r,p) .: XX c= V
let b be
set ;
:: according to TARSKI:def 3 :: thesis: ( not b in (RotateCircle o,r,p) .: XX or b in V )
assume
b in (RotateCircle o,r,p) .: XX
;
:: thesis: b in V
then consider a being
Point of
((TOP-REAL 2) | (Sphere o,r)) such that A100:
a in XX
and A101:
b = (RotateCircle o,r,p) . a
by A2, FUNCT_2:116;
reconsider a1 =
a,
fa =
fp as
Point of
(TOP-REAL 2) by PRE_TOPC:55;
A102:
a in Y1
by A100, XBOOLE_0:def 4;
A103:
[p,a] in [:{p},(Sphere o,r):]
by A4, A9, ZFMISC_1:def 2;
fa in X1
by A96, A98, ZFMISC_1:106;
then
[fa,a] in Z
by A98, A102, ZFMISC_1:def 2;
then
[fa,a] in Z /\ ([#] ([:(TOP-REAL 2),(TOP-REAL 2):] | [:{p},(Sphere o,r):]))
by A10, A103, XBOOLE_0:def 4;
then A104:
F . [fa,a1] in F .: (Z /\ ([#] ([:(TOP-REAL 2),(TOP-REAL 2):] | [:{p},(Sphere o,r):])))
by FUNCT_2:43;
A105:
R2Homeomorphism " = R2Homeomorphism "
by A83, TOPS_2:def 4;
A106:
dom (R2Homeomorphism " ) = [#] (TOP-REAL 2)
by A83, TOPS_2:62;
A107:
(RotateCircle o,r,p) . a1 in the
carrier of
(Tcircle o,r)
by A2, FUNCT_2:7;
Z c= WW
by A94, A97, ZFMISC_1:92;
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 A93, RELAT_1:156;
then
F . [fa,a1] in F .: W
by A104;
then
R2Homeomorphism . (F . [fa,a1]) in R2Homeomorphism .: ((R2Homeomorphism " ) .: V1)
by A91, FUNCT_2:43;
then
(R2Homeomorphism * F) . [fa,a1] in R2Homeomorphism .: ((R2Homeomorphism " ) .: V1)
by A10, A103, FUNCT_2:21;
then
(R2Homeomorphism * F) . [fa,a1] in V1
by A83, A105, A106, PARTFUN3:1;
then
(RotateCircle o,r,p) . a in V1
by A42;
hence
b in V
by A76, A101, A107, XBOOLE_0:def 4;
:: thesis: verum
end;
hence
RotateCircle o,r,p is continuous
by A2, JGRAPH_2:20; :: thesis: verum