let n be Nat; for p being Point of (TOP-REAL n)
for A being Subset of (TOP-REAL n)
for r being Real st not p in A & r > 0 holds
ex h being Function of ((TOP-REAL n) | A),((TOP-REAL n) | (Sphere (p,r))) st
( h is continuous & h | (Sphere (p,r)) = id (A /\ (Sphere (p,r))) )
let p be Point of (TOP-REAL n); for A being Subset of (TOP-REAL n)
for r being Real st not p in A & r > 0 holds
ex h being Function of ((TOP-REAL n) | A),((TOP-REAL n) | (Sphere (p,r))) st
( h is continuous & h | (Sphere (p,r)) = id (A /\ (Sphere (p,r))) )
let A be Subset of (TOP-REAL n); for r being Real st not p in A & r > 0 holds
ex h being Function of ((TOP-REAL n) | A),((TOP-REAL n) | (Sphere (p,r))) st
( h is continuous & h | (Sphere (p,r)) = id (A /\ (Sphere (p,r))) )
let r be Real; ( not p in A & r > 0 implies ex h being Function of ((TOP-REAL n) | A),((TOP-REAL n) | (Sphere (p,r))) st
( h is continuous & h | (Sphere (p,r)) = id (A /\ (Sphere (p,r))) ) )
set TR = TOP-REAL n;
assume that
A1:
not p in A
and
A2:
r > 0
; ex h being Function of ((TOP-REAL n) | A),((TOP-REAL n) | (Sphere (p,r))) st
( h is continuous & h | (Sphere (p,r)) = id (A /\ (Sphere (p,r))) )
set S = Sphere (p,r);
per cases
( A is empty or not A is empty )
;
suppose A4:
not
A is
empty
;
ex h being Function of ((TOP-REAL n) | A),((TOP-REAL n) | (Sphere (p,r))) st
( h is continuous & h | (Sphere (p,r)) = id (A /\ (Sphere (p,r))) )
A <> {p}
by A1, TARSKI:def 1;
then A5:
A \ {p} <> {}
by A4, ZFMISC_1:58;
set TRS =
(TOP-REAL n) | (Sphere (p,r));
set nN =
n NormF ;
set t =
transl (
(- p),
(TOP-REAL n));
set P =
transl (
p,
(TOP-REAL n));
A6:
A \ {p} c= the
carrier of
(TOP-REAL n) \ {p}
by XBOOLE_1:33;
the
carrier of
(TOP-REAL n) \ {p} = {p} `
by SUBSET_1:def 4;
then reconsider cTRp = the
carrier of
(TOP-REAL n) \ {p} as non
empty open Subset of
(TOP-REAL n) by A5, A6;
set TRp =
(TOP-REAL n) | cTRp;
set tt =
(transl ((- p),(TOP-REAL n))) | ((TOP-REAL n) | cTRp);
A7:
[#] ((TOP-REAL n) | cTRp) = cTRp
by PRE_TOPC:def 5;
then reconsider AA =
A as
Subset of
((TOP-REAL n) | cTRp) by A1, ZFMISC_1:57, A6;
reconsider Ir =
((transl ((- p),(TOP-REAL n))) | ((TOP-REAL n) | cTRp)) [#] r as
Function of
((TOP-REAL n) | cTRp),
(TOP-REAL n) by TOPREALC:37;
reconsider IrNt =
Ir </> ((n NormF) * ((transl ((- p),(TOP-REAL n))) | ((TOP-REAL n) | cTRp))) as
Function of
((TOP-REAL n) | cTRp),
(TOP-REAL n) by TOPREALC:46;
A8:
(transl ((- p),(TOP-REAL n))) | ((TOP-REAL n) | cTRp) = (transl ((- p),(TOP-REAL n))) | the
carrier of
((TOP-REAL n) | cTRp)
by TMAP_1:def 4;
not
0 in rng ((n NormF) * ((transl ((- p),(TOP-REAL n))) | ((TOP-REAL n) | cTRp)))
proof
assume
0 in rng ((n NormF) * ((transl ((- p),(TOP-REAL n))) | ((TOP-REAL n) | cTRp)))
;
contradiction
then consider x being
object such that A9:
x in dom ((n NormF) * ((transl ((- p),(TOP-REAL n))) | ((TOP-REAL n) | cTRp)))
and A10:
((n NormF) * ((transl ((- p),(TOP-REAL n))) | ((TOP-REAL n) | cTRp))) . x = 0
by FUNCT_1:def 3;
((transl ((- p),(TOP-REAL n))) | ((TOP-REAL n) | cTRp)) . x in dom (n NormF)
by A9, FUNCT_1:11;
then reconsider Tx =
((transl ((- p),(TOP-REAL n))) | ((TOP-REAL n) | cTRp)) . x as
Point of
(TOP-REAL n) ;
reconsider Tx =
Tx as
Element of
REAL n by EUCLID:22;
A11:
x in dom ((transl ((- p),(TOP-REAL n))) | ((TOP-REAL n) | cTRp))
by A9, FUNCT_1:11;
then A12:
(transl ((- p),(TOP-REAL n))) . x = ((transl ((- p),(TOP-REAL n))) | ((TOP-REAL n) | cTRp)) . x
by A8, FUNCT_1:47;
x in dom (transl ((- p),(TOP-REAL n)))
by A11, A8, RELAT_1:57;
then reconsider X =
x as
Point of
(TOP-REAL n) ;
0 =
(n NormF) . Tx
by A9, FUNCT_1:12, A10
.=
|.Tx.|
by JGRAPH_4:def 1
;
then
0* n = Tx
by EUCLID:8;
then 0. (TOP-REAL n) =
Tx
by EUCLID:70
.=
(- p) + X
by A12, RLTOPSP1:def 10
;
then X =
- (- p)
by RLVECT_1:def 10
.=
p
;
then
x in {p}
by TARSKI:def 1;
hence
contradiction
by A9, A7, XBOOLE_0:def 5;
verum
end; then
(n NormF) * ((transl ((- p),(TOP-REAL n))) | ((TOP-REAL n) | cTRp)) is
non-empty
by RELAT_1:def 9;
then reconsider IrNt =
IrNt as
continuous Function of
((TOP-REAL n) | cTRp),
(TOP-REAL n) ;
set h =
((transl (p,(TOP-REAL n))) * IrNt) | (((TOP-REAL n) | cTRp) | AA);
A13:
((transl (p,(TOP-REAL n))) * IrNt) | (((TOP-REAL n) | cTRp) | AA) = ((transl (p,(TOP-REAL n))) * IrNt) | the
carrier of
(((TOP-REAL n) | cTRp) | AA)
by TMAP_1:def 4;
reconsider h =
((transl (p,(TOP-REAL n))) * IrNt) | (((TOP-REAL n) | cTRp) | AA) as
continuous Function of
(((TOP-REAL n) | cTRp) | AA),
(TOP-REAL n) by A4;
((TOP-REAL n) | cTRp) | AA = (TOP-REAL n) | A
by PRE_TOPC:7, A7;
then reconsider h =
h as
continuous Function of
((TOP-REAL n) | A),
(TOP-REAL n) ;
A14:
[#] ((TOP-REAL n) | A) = A
by PRE_TOPC:def 5;
then A15:
dom h = A
by FUNCT_2:def 1;
A16:
dom ((transl ((- p),(TOP-REAL n))) | ((TOP-REAL n) | cTRp)) = cTRp
by A7, FUNCT_2:def 1;
A17:
rng h c= Sphere (
p,
r)
proof
let y be
object ;
TARSKI:def 3 ( not y in rng h or y in Sphere (p,r) )
assume
y in rng h
;
y in Sphere (p,r)
then consider x being
object such that A18:
x in dom h
and A19:
h . x = y
by FUNCT_1:def 3;
reconsider x =
x as
Point of
(TOP-REAL n) by A18, A15;
((transl ((- p),(TOP-REAL n))) | ((TOP-REAL n) | cTRp)) . x = (transl ((- p),(TOP-REAL n))) . x
by A7, A18, A15, FUNCT_1:47, A8, A16;
then A20:
((transl ((- p),(TOP-REAL n))) | ((TOP-REAL n) | cTRp)) . x = (- p) + x
by RLTOPSP1:def 10;
dom ((n NormF) * ((transl ((- p),(TOP-REAL n))) | ((TOP-REAL n) | cTRp))) = cTRp
by A7, FUNCT_2:def 1;
then
((n NormF) * ((transl ((- p),(TOP-REAL n))) | ((TOP-REAL n) | cTRp))) . x = (n NormF) . (((transl ((- p),(TOP-REAL n))) | ((TOP-REAL n) | cTRp)) . x)
by A7, A18, A15, FUNCT_1:12;
then A21:
((n NormF) * ((transl ((- p),(TOP-REAL n))) | ((TOP-REAL n) | cTRp))) . x = |.((- p) + x).|
by A20, JGRAPH_4:def 1;
A22:
x in dom ((transl (p,(TOP-REAL n))) * IrNt)
by A13, A18, RELAT_1:57;
then
x in dom IrNt
by FUNCT_1:11;
then A23:
IrNt . x = (Ir . x) (/) (((n NormF) * ((transl ((- p),(TOP-REAL n))) | ((TOP-REAL n) | cTRp))) . x)
by VALUED_2:72;
dom Ir = cTRp
by A7, FUNCT_2:def 1;
then
Ir . x = r * ((- p) + x)
by A20, A7, A18, A15, VALUED_2:def 39;
then A24:
IrNt . x = (1 / |.((- p) + x).|) * (r * ((- p) + x))
by A21, A23, VALUED_2:def 32;
then reconsider Fx =
IrNt . x as
Point of
(TOP-REAL n) ;
h . x = ((transl (p,(TOP-REAL n))) * IrNt) . x
by A13, A18, FUNCT_1:47;
then A25:
h . x =
(transl (p,(TOP-REAL n))) . Fx
by A22, FUNCT_1:12
.=
p + Fx
by RLTOPSP1:def 10
;
- (- p) = p
;
then
(- p) + x <> 0. (TOP-REAL n)
by A18, A1, A15, RLVECT_1:6;
then A26:
(- p) + x <> 0* n
by EUCLID:70;
A27:
(- p) + x is
Element of
REAL n
by EUCLID:22;
A28:
(p + Fx) - p =
Fx + (p + (- p))
by RLVECT_1:def 3
.=
Fx + (0. (TOP-REAL n))
by RLVECT_1:def 10
.=
Fx
by RLVECT_1:def 4
;
|.Fx.| =
|.(((1 / |.((- p) + x).|) * r) * ((- p) + x)).|
by A24, RLVECT_1:def 7
.=
|.((1 / |.((- p) + x).|) * r).| * |.((- p) + x).|
by EUCLID:11
.=
(|.(1 / |.((- p) + x).|).| * |.r.|) * |.((- p) + x).|
by COMPLEX1:65
.=
(|.(1 / |.((- p) + x).|).| * r) * |.((- p) + x).|
by ABSVALUE:def 1, A2
.=
(|.(1 / |.((- p) + x).|).| * r) * |.|.((- p) + x).|.|
by ABSVALUE:def 1
.=
(|.(1 / |.((- p) + x).|).| * |.|.((- p) + x).|.|) * r
.=
1
* r
by ABSVALUE:6, A26, EUCLID:8, A27
.=
r
;
hence
y in Sphere (
p,
r)
by A28, A25, A19;
verum
end;
[#] ((TOP-REAL n) | (Sphere (p,r))) = Sphere (
p,
r)
by PRE_TOPC:def 5;
then reconsider h =
h as
Function of
((TOP-REAL n) | A),
((TOP-REAL n) | (Sphere (p,r))) by A17, A14, A15, FUNCT_2:2;
A29:
dom (h | (Sphere (p,r))) = A /\ (Sphere (p,r))
by A15, RELAT_1:61;
A31:
for
x being
object st
x in dom (h | (Sphere (p,r))) holds
(h | (Sphere (p,r))) . x = (id (A /\ (Sphere (p,r)))) . x
proof
let y be
object ;
( y in dom (h | (Sphere (p,r))) implies (h | (Sphere (p,r))) . y = (id (A /\ (Sphere (p,r)))) . y )
assume A32:
y in dom (h | (Sphere (p,r)))
;
(h | (Sphere (p,r))) . y = (id (A /\ (Sphere (p,r)))) . y
then reconsider x =
y as
Point of
(TOP-REAL n) by A29;
A33:
x in dom h
by A32, RELAT_1:57;
then A34:
h . x = ((transl (p,(TOP-REAL n))) * IrNt) . x
by A13, FUNCT_1:47;
((transl ((- p),(TOP-REAL n))) | ((TOP-REAL n) | cTRp)) . x = (transl ((- p),(TOP-REAL n))) . x
by A7, A33, A15, FUNCT_1:47, A8, A16;
then A35:
((transl ((- p),(TOP-REAL n))) | ((TOP-REAL n) | cTRp)) . x = (- p) + x
by RLTOPSP1:def 10;
x - p = (- p) + x
;
then A36:
|.((- p) + x).| = r
by A32, TOPREAL9:9;
A37:
x in dom ((transl (p,(TOP-REAL n))) * IrNt)
by A13, A33, RELAT_1:57;
then
x in dom IrNt
by FUNCT_1:11;
then A38:
IrNt . x = (Ir . x) (/) (((n NormF) * ((transl ((- p),(TOP-REAL n))) | ((TOP-REAL n) | cTRp))) . x)
by VALUED_2:72;
dom ((n NormF) * ((transl ((- p),(TOP-REAL n))) | ((TOP-REAL n) | cTRp))) = cTRp
by A7, FUNCT_2:def 1;
then
((n NormF) * ((transl ((- p),(TOP-REAL n))) | ((TOP-REAL n) | cTRp))) . x = (n NormF) . (((transl ((- p),(TOP-REAL n))) | ((TOP-REAL n) | cTRp)) . x)
by A7, A33, A15, FUNCT_1:12;
then A39:
((n NormF) * ((transl ((- p),(TOP-REAL n))) | ((TOP-REAL n) | cTRp))) . x = |.((- p) + x).|
by A35, JGRAPH_4:def 1;
dom Ir = cTRp
by A7, FUNCT_2:def 1;
then
Ir . x = r * ((- p) + x)
by A35, A7, A33, A15, VALUED_2:def 39;
then A40:
IrNt . x =
(1 / |.((- p) + x).|) * (r * ((- p) + x))
by A39, A38, VALUED_2:def 32
.=
((1 / r) * r) * ((- p) + x)
by A36, RLVECT_1:def 7
.=
1
* ((- p) + x)
by XCMPLX_1:87, A2
.=
(- p) + x
by RLVECT_1:def 8
;
thus (h | (Sphere (p,r))) . y =
h . x
by A32, FUNCT_1:47
.=
(transl (p,(TOP-REAL n))) . ((- p) + x)
by A34, A37, FUNCT_1:12, A40
.=
p + ((- p) + x)
by RLTOPSP1:def 10
.=
(p + (- p)) + x
by RLVECT_1:def 3
.=
(0. (TOP-REAL n)) + x
by RLVECT_1:def 10
.=
x
by RLVECT_1:def 4
.=
(id (A /\ (Sphere (p,r)))) . y
by A32, A29, FUNCT_1:17
;
verum
end; take
h
;
( h is continuous & h | (Sphere (p,r)) = id (A /\ (Sphere (p,r))) )thus
(
h is
continuous &
h | (Sphere (p,r)) = id (A /\ (Sphere (p,r))) )
by A31, A15, PRE_TOPC:27, RELAT_1:61;
verum end;