let n be non zero Element of NAT ; :: thesis: for o, p being Point of (TOP-REAL n)
for r being positive Real st p in Ball (o,r) holds
(DiskProj (o,r,p)) | (Sphere (o,r)) = id (Sphere (o,r))
let o, p be Point of (TOP-REAL n); :: thesis: for r being positive Real st p in Ball (o,r) holds
(DiskProj (o,r,p)) | (Sphere (o,r)) = id (Sphere (o,r))
let r be positive Real; :: thesis: ( p in Ball (o,r) implies (DiskProj (o,r,p)) | (Sphere (o,r)) = id (Sphere (o,r)) )
assume A1: p in Ball (o,r) ; :: thesis: (DiskProj (o,r,p)) | (Sphere (o,r)) = id (Sphere (o,r))
A2: the carrier of (Tdisk (o,r)) = cl_Ball (o,r) by BROUWER:3;
A3: the carrier of ((TOP-REAL n) | ((cl_Ball (o,r)) \ {p})) = (cl_Ball (o,r)) \ {p} by PRE_TOPC:8;
A4: dom (DiskProj (o,r,p)) = the carrier of ((TOP-REAL n) | ((cl_Ball (o,r)) \ {p})) by FUNCT_2:def 1;
A5: Sphere (o,r) misses Ball (o,r) by TOPREAL9:19;
A6: Sphere (o,r) c= cl_Ball (o,r) by TOPREAL9:17;
A7: Ball (o,r) c= cl_Ball (o,r) by TOPREAL9:16;
A8: Sphere (o,r) c= (cl_Ball (o,r)) \ {p}
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in Sphere (o,r) or a in (cl_Ball (o,r)) \ {p} )
assume A9: a in Sphere (o,r) ; :: thesis: a in (cl_Ball (o,r)) \ {p}
then a <> p by A1, A5, XBOOLE_0:3;
hence a in (cl_Ball (o,r)) \ {p} by A6, A9, ZFMISC_1:56; :: thesis: verum
end;
then A10: dom ((DiskProj (o,r,p)) | (Sphere (o,r))) = Sphere (o,r) by A3, A4, RELAT_1:62;
A11: dom (id (Sphere (o,r))) = Sphere (o,r) ;
now :: thesis: for x being object st x in dom ((DiskProj (o,r,p)) | (Sphere (o,r))) holds
((DiskProj (o,r,p)) | (Sphere (o,r))) . x = (id (Sphere (o,r))) . x
let x be object ; :: thesis: ( x in dom ((DiskProj (o,r,p)) | (Sphere (o,r))) implies ((DiskProj (o,r,p)) | (Sphere (o,r))) . x = (id (Sphere (o,r))) . x )
assume A12: x in dom ((DiskProj (o,r,p)) | (Sphere (o,r))) ; :: thesis: ((DiskProj (o,r,p)) | (Sphere (o,r))) . x = (id (Sphere (o,r))) . x
then x in dom (DiskProj (o,r,p)) by RELAT_1:57;
then consider y being Point of (TOP-REAL n) such that
A13: x = y and
A14: (DiskProj (o,r,p)) . x = HC (p,y,o,r) by A1, A2, A7, Def7;
y in halfline (p,y) by TOPREAL9:28;
then A15: x in (halfline (p,y)) /\ (Sphere (o,r)) by A12, A13, XBOOLE_0:def 4;
A16: x <> p by A1, A5, A12, XBOOLE_0:3;
thus ((DiskProj (o,r,p)) | (Sphere (o,r))) . x = (DiskProj (o,r,p)) . x by A12, FUNCT_1:47
.= x by A1, A2, A6, A7, A10, A12, A13, A14, A15, A16, BROUWER:def 3
.= (id (Sphere (o,r))) . x by A12, FUNCT_1:18 ; :: thesis: verum
end;
hence (DiskProj (o,r,p)) | (Sphere (o,r)) = id (Sphere (o,r)) by A3, A4, A8, A11, FUNCT_1:2, RELAT_1:62; :: thesis: verum