let n be Element of NAT ; for X being non empty SubSpace of Tdisk ((0. (TOP-REAL n)),1) st X = Tcircle ((0. (TOP-REAL n)),1) holds
not X is_a_retract_of Tdisk ((0. (TOP-REAL n)),1)
set TR = TOP-REAL n;
set Td = Tdisk ((0. (TOP-REAL n)),1);
A1:
Sphere ((0. (TOP-REAL n)),1) c= cl_Ball ((0. (TOP-REAL n)),1)
by TOPREAL9:17;
set M = mlt ((- jj),(TOP-REAL n));
let X be non empty SubSpace of Tdisk ((0. (TOP-REAL n)),1); ( X = Tcircle ((0. (TOP-REAL n)),1) implies not X is_a_retract_of Tdisk ((0. (TOP-REAL n)),1) )
assume A2:
X = Tcircle ((0. (TOP-REAL n)),1)
; not X is_a_retract_of Tdisk ((0. (TOP-REAL n)),1)
A3:
the carrier of X = Sphere ((0. (TOP-REAL n)),1)
by A2, TOPREALB:9;
assume
X is_a_retract_of Tdisk ((0. (TOP-REAL n)),1)
; contradiction
then consider F being continuous Function of (Tdisk ((0. (TOP-REAL n)),1)),X such that
A4:
F is being_a_retraction
;
A5:
the carrier of (Tdisk ((0. (TOP-REAL n)),1)) = cl_Ball ((0. (TOP-REAL n)),1)
by BROUWER:3;
then reconsider f = F as Function of (Tdisk ((0. (TOP-REAL n)),1)),(Tdisk ((0. (TOP-REAL n)),1)) by A3, A1, FUNCT_2:7;
set Mf = ((mlt ((- jj),(TOP-REAL n))) | (Tdisk ((0. (TOP-REAL n)),1))) * f;
A6:
(mlt ((- jj),(TOP-REAL n))) | (Tdisk ((0. (TOP-REAL n)),1)) = (mlt ((- jj),(TOP-REAL n))) | the carrier of (Tdisk ((0. (TOP-REAL n)),1))
by TMAP_1:def 4;
A7:
rng (((mlt ((- jj),(TOP-REAL n))) | (Tdisk ((0. (TOP-REAL n)),1))) * f) c= Sphere ((0. (TOP-REAL n)),1)
proof
let y be
object ;
TARSKI:def 3 ( not y in rng (((mlt ((- jj),(TOP-REAL n))) | (Tdisk ((0. (TOP-REAL n)),1))) * f) or y in Sphere ((0. (TOP-REAL n)),1) )
assume
y in rng (((mlt ((- jj),(TOP-REAL n))) | (Tdisk ((0. (TOP-REAL n)),1))) * f)
;
y in Sphere ((0. (TOP-REAL n)),1)
then consider x being
object such that A8:
x in dom (((mlt ((- jj),(TOP-REAL n))) | (Tdisk ((0. (TOP-REAL n)),1))) * f)
and A9:
(((mlt ((- jj),(TOP-REAL n))) | (Tdisk ((0. (TOP-REAL n)),1))) * f) . x = y
by FUNCT_1:def 3;
A10:
f . x in dom ((mlt ((- jj),(TOP-REAL n))) | (Tdisk ((0. (TOP-REAL n)),1)))
by A8, FUNCT_1:11;
then
f . x in dom (mlt ((- jj),(TOP-REAL n)))
by A6, RELAT_1:57;
then reconsider fx =
f . x as
Point of
(TOP-REAL n) ;
x in dom f
by A8, FUNCT_1:11;
then
f . x in rng F
by FUNCT_1:def 3;
then A11: 1 =
|.fx.|
by A3, TOPREAL9:12
.=
|.(- fx).|
by EUCLID:10
.=
|.((- fx) - (0. (TOP-REAL n))).|
;
y = ((mlt ((- jj),(TOP-REAL n))) | (Tdisk ((0. (TOP-REAL n)),1))) . (f . x)
by A8, A9, FUNCT_1:12;
then
y = (mlt ((- jj),(TOP-REAL n))) . (f . x)
by A6, A10, FUNCT_1:47;
then y =
(- 1) * fx
by RLTOPSP1:def 13
.=
- fx
by RLVECT_1:16
;
hence
y in Sphere (
(0. (TOP-REAL n)),1)
by A11;
verum
end;
then
rng (((mlt ((- jj),(TOP-REAL n))) | (Tdisk ((0. (TOP-REAL n)),1))) * f) c= cl_Ball ((0. (TOP-REAL n)),1)
by A1;
then reconsider MF = ((mlt ((- jj),(TOP-REAL n))) | (Tdisk ((0. (TOP-REAL n)),1))) * f as Function of (Tdisk ((0. (TOP-REAL n)),1)),(Tdisk ((0. (TOP-REAL n)),1)) by A5, FUNCT_2:6;
A12:
not cl_Ball ((0. (TOP-REAL n)),1) is boundary
by Lm5;
f is continuous
by PRE_TOPC:26;
then
MF is continuous
by PRE_TOPC:27;
then
MF is with_fixpoint
by A12, Th8;
then consider p being object such that
A13:
p is_a_fixpoint_of MF
by ABIAN:def 5;
A14:
p in dom MF
by A13, ABIAN:def 3;
A15:
p = MF . p
by A13, ABIAN:def 3;
then A16:
p in rng MF
by A14, FUNCT_1:def 3;
then reconsider p = p as Point of (TOP-REAL n) by A7;
A17:
f . p = p
by A4, A3, A7, A16;
then A18:
p in dom ((mlt ((- jj),(TOP-REAL n))) | (Tdisk ((0. (TOP-REAL n)),1)))
by A14, FUNCT_1:11;
p = ((mlt ((- jj),(TOP-REAL n))) | (Tdisk ((0. (TOP-REAL n)),1))) . p
by A14, A15, A17, FUNCT_1:12;
then
p = (mlt ((- jj),(TOP-REAL n))) . p
by A6, A18, FUNCT_1:47;
then p =
(- 1) * p
by RLTOPSP1:def 13
.=
- p
by RLVECT_1:16
;
then A19:
p = 0. (TOP-REAL n)
by RLVECT_1:19;
|.p.| = 1
by A7, A16, TOPREAL9:12;
hence
contradiction
by A19, TOPRNS_1:23; verum