:: BROUWER semantic presentation
begin
set T2 = TOP-REAL 2;
definition
let S, T be non empty TopSpace;
func DiffElems (S,T) -> Subset of [:S,T:] equals :: BROUWER:def 1
{ [s,t] where s is Point of S, t is Point of T : s <> t } ;
coherence
{ [s,t] where s is Point of S, t is Point of T : s <> t } is Subset of [:S,T:]
proof
set A = { [s,t] where s is Point of S, t is Point of T : s <> t } ;
{ [s,t] where s is Point of S, t is Point of T : s <> t } c= the carrier of [:S,T:]
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { [s,t] where s is Point of S, t is Point of T : s <> t } or a in the carrier of [:S,T:] )
assume a in { [s,t] where s is Point of S, t is Point of T : s <> t } ; ::_thesis: a in the carrier of [:S,T:]
then ex s being Point of S ex t being Point of T st
( a = [s,t] & s <> t ) ;
hence a in the carrier of [:S,T:] ; ::_thesis: verum
end;
hence { [s,t] where s is Point of S, t is Point of T : s <> t } is Subset of [:S,T:] ; ::_thesis: verum
end;
end;
:: deftheorem defines DiffElems BROUWER:def_1_:_
for S, T being non empty TopSpace holds DiffElems (S,T) = { [s,t] where s is Point of S, t is Point of T : s <> t } ;
theorem :: BROUWER:1
for S, T being non empty TopSpace
for x being set holds
( x in DiffElems (S,T) iff ex s being Point of S ex t being Point of T st
( x = [s,t] & s <> t ) ) ;
registration
let S be non trivial TopSpace;
let T be non empty TopSpace;
cluster DiffElems (S,T) -> non empty ;
coherence
not DiffElems (S,T) is empty
proof
set t1 = the Element of T;
consider s1, s2 being Element of S such that
A1: s1 <> s2 by SUBSET_1:def_7;
percases ( s1 = the Element of T or s1 <> the Element of T ) ;
suppose s1 = the Element of T ; ::_thesis: not DiffElems (S,T) is empty
then [s2, the Element of T] in DiffElems (S,T) by A1;
hence not DiffElems (S,T) is empty ; ::_thesis: verum
end;
suppose s1 <> the Element of T ; ::_thesis: not DiffElems (S,T) is empty
then [s1, the Element of T] in DiffElems (S,T) ;
hence not DiffElems (S,T) is empty ; ::_thesis: verum
end;
end;
end;
end;
registration
let S be non empty TopSpace;
let T be non trivial TopSpace;
cluster DiffElems (S,T) -> non empty ;
coherence
not DiffElems (S,T) is empty
proof
set s1 = the Element of S;
consider t1, t2 being Element of T such that
A1: t1 <> t2 by SUBSET_1:def_7;
percases ( the Element of S = t1 or the Element of S <> t1 ) ;
suppose the Element of S = t1 ; ::_thesis: not DiffElems (S,T) is empty
then [ the Element of S,t2] in DiffElems (S,T) by A1;
hence not DiffElems (S,T) is empty ; ::_thesis: verum
end;
suppose the Element of S <> t1 ; ::_thesis: not DiffElems (S,T) is empty
then [ the Element of S,t1] in DiffElems (S,T) ;
hence not DiffElems (S,T) is empty ; ::_thesis: verum
end;
end;
end;
end;
theorem Th2: :: BROUWER:2
for n being Element of NAT
for x being Point of (TOP-REAL n) holds cl_Ball (x,0) = {x}
proof
let n be Element of NAT ; ::_thesis: for x being Point of (TOP-REAL n) holds cl_Ball (x,0) = {x}
let x be Point of (TOP-REAL n); ::_thesis: cl_Ball (x,0) = {x}
thus cl_Ball (x,0) c= {x} :: according to XBOOLE_0:def_10 ::_thesis: {x} c= cl_Ball (x,0)
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in cl_Ball (x,0) or a in {x} )
assume A1: a in cl_Ball (x,0) ; ::_thesis: a in {x}
then reconsider a = a as Point of (TOP-REAL n) ;
|.(a - x).| = 0 by A1, TOPREAL9:8;
then a = x by TOPRNS_1:28;
hence a in {x} by TARSKI:def_1; ::_thesis: verum
end;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in {x} or a in cl_Ball (x,0) )
assume a in {x} ; ::_thesis: a in cl_Ball (x,0)
then A2: a = x by TARSKI:def_1;
|.(x - x).| = 0 by TOPRNS_1:28;
hence a in cl_Ball (x,0) by A2, TOPREAL9:8; ::_thesis: verum
end;
definition
let n be Element of NAT ;
let x be Point of (TOP-REAL n);
let r be real number ;
func Tdisk (x,r) -> SubSpace of TOP-REAL n equals :: BROUWER:def 2
(TOP-REAL n) | (cl_Ball (x,r));
coherence
(TOP-REAL n) | (cl_Ball (x,r)) is SubSpace of TOP-REAL n ;
end;
:: deftheorem defines Tdisk BROUWER:def_2_:_
for n being Element of NAT
for x being Point of (TOP-REAL n)
for r being real number holds Tdisk (x,r) = (TOP-REAL n) | (cl_Ball (x,r));
registration
let n be Element of NAT ;
let x be Point of (TOP-REAL n);
let r be non negative real number ;
cluster Tdisk (x,r) -> non empty ;
coherence
not Tdisk (x,r) is empty ;
end;
theorem Th3: :: BROUWER:3
for n being Element of NAT
for r being real number
for x being Point of (TOP-REAL n) holds the carrier of (Tdisk (x,r)) = cl_Ball (x,r)
proof
let n be Element of NAT ; ::_thesis: for r being real number
for x being Point of (TOP-REAL n) holds the carrier of (Tdisk (x,r)) = cl_Ball (x,r)
let r be real number ; ::_thesis: for x being Point of (TOP-REAL n) holds the carrier of (Tdisk (x,r)) = cl_Ball (x,r)
let x be Point of (TOP-REAL n); ::_thesis: the carrier of (Tdisk (x,r)) = cl_Ball (x,r)
[#] (Tdisk (x,r)) = cl_Ball (x,r) by PRE_TOPC:def_5;
hence the carrier of (Tdisk (x,r)) = cl_Ball (x,r) ; ::_thesis: verum
end;
registration
let n be Element of NAT ;
let x be Point of (TOP-REAL n);
let r be real number ;
cluster Tdisk (x,r) -> convex ;
coherence
Tdisk (x,r) is convex
proof
thus [#] (Tdisk (x,r)) is convex Subset of (TOP-REAL n) by Th3; :: according to TOPALG_2:def_1 ::_thesis: verum
end;
end;
theorem Th4: :: BROUWER:4
for n being Element of NAT
for r being non negative real number
for s, t, x being Point of (TOP-REAL n) st s <> t & s is Point of (Tdisk (x,r)) & s is not Point of (Tcircle (x,r)) holds
ex e being Point of (Tcircle (x,r)) st {e} = (halfline (s,t)) /\ (Sphere (x,r))
proof
let n be Element of NAT ; ::_thesis: for r being non negative real number
for s, t, x being Point of (TOP-REAL n) st s <> t & s is Point of (Tdisk (x,r)) & s is not Point of (Tcircle (x,r)) holds
ex e being Point of (Tcircle (x,r)) st {e} = (halfline (s,t)) /\ (Sphere (x,r))
let r be non negative real number ; ::_thesis: for s, t, x being Point of (TOP-REAL n) st s <> t & s is Point of (Tdisk (x,r)) & s is not Point of (Tcircle (x,r)) holds
ex e being Point of (Tcircle (x,r)) st {e} = (halfline (s,t)) /\ (Sphere (x,r))
let s, t, x be Point of (TOP-REAL n); ::_thesis: ( s <> t & s is Point of (Tdisk (x,r)) & s is not Point of (Tcircle (x,r)) implies ex e being Point of (Tcircle (x,r)) st {e} = (halfline (s,t)) /\ (Sphere (x,r)) )
assume that
A1: s <> t and
A2: s is Point of (Tdisk (x,r)) and
A3: s is not Point of (Tcircle (x,r)) ; ::_thesis: ex e being Point of (Tcircle (x,r)) st {e} = (halfline (s,t)) /\ (Sphere (x,r))
reconsider S = s, T = t, X = x as Element of REAL n by EUCLID:22;
set a = ((- (2 * |((t - s),(s - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((t - s),(s - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))));
the carrier of (Tdisk (x,r)) = cl_Ball (x,r) by Th3;
then A4: |.(s - x).| <= r by A2, TOPREAL9:8;
A5: the carrier of (Tcircle (x,r)) = Sphere (x,r) by TOPREALB:9;
then |.(s - x).| <> r by A3, TOPREAL9:9;
then |.(s - x).| < r by A4, XXREAL_0:1;
then s in Ball (x,r) by TOPREAL9:7;
then consider e1 being Point of (TOP-REAL n) such that
A6: {e1} = (halfline (s,t)) /\ (Sphere (x,r)) and
e1 = ((1 - (((- (2 * |((t - s),(s - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((t - s),(s - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))))) * s) + ((((- (2 * |((t - s),(s - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((t - s),(s - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))) * t) by A1, TOPREAL9:37;
e1 in {e1} by TARSKI:def_1;
then e1 in Sphere (x,r) by A6, XBOOLE_0:def_4;
hence ex e being Point of (Tcircle (x,r)) st {e} = (halfline (s,t)) /\ (Sphere (x,r)) by A5, A6; ::_thesis: verum
end;
theorem Th5: :: BROUWER:5
for n being Element of NAT
for r being non negative real number
for s, t, x being Point of (TOP-REAL n) st s <> t & s in the carrier of (Tcircle (x,r)) & t is Point of (Tdisk (x,r)) holds
ex e being Point of (Tcircle (x,r)) st
( e <> s & {s,e} = (halfline (s,t)) /\ (Sphere (x,r)) )
proof
let n be Element of NAT ; ::_thesis: for r being non negative real number
for s, t, x being Point of (TOP-REAL n) st s <> t & s in the carrier of (Tcircle (x,r)) & t is Point of (Tdisk (x,r)) holds
ex e being Point of (Tcircle (x,r)) st
( e <> s & {s,e} = (halfline (s,t)) /\ (Sphere (x,r)) )
let r be non negative real number ; ::_thesis: for s, t, x being Point of (TOP-REAL n) st s <> t & s in the carrier of (Tcircle (x,r)) & t is Point of (Tdisk (x,r)) holds
ex e being Point of (Tcircle (x,r)) st
( e <> s & {s,e} = (halfline (s,t)) /\ (Sphere (x,r)) )
let s, t, x be Point of (TOP-REAL n); ::_thesis: ( s <> t & s in the carrier of (Tcircle (x,r)) & t is Point of (Tdisk (x,r)) implies ex e being Point of (Tcircle (x,r)) st
( e <> s & {s,e} = (halfline (s,t)) /\ (Sphere (x,r)) ) )
assume A1: ( s <> t & s in the carrier of (Tcircle (x,r)) & t is Point of (Tdisk (x,r)) ) ; ::_thesis: ex e being Point of (Tcircle (x,r)) st
( e <> s & {s,e} = (halfline (s,t)) /\ (Sphere (x,r)) )
reconsider S = ((1 / 2) * s) + ((1 / 2) * t), T = t, X = x as Element of REAL n by EUCLID:22;
A2: the carrier of (Tcircle (x,r)) = Sphere (x,r) by TOPREALB:9;
set a = ((- (2 * |((t - (((1 / 2) * s) + ((1 / 2) * t))),((((1 / 2) * s) + ((1 / 2) * t)) - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((t - (((1 / 2) * s) + ((1 / 2) * t))),((((1 / 2) * s) + ((1 / 2) * t)) - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))));
the carrier of (Tdisk (x,r)) = cl_Ball (x,r) by Th3;
then consider e1 being Point of (TOP-REAL n) such that
A3: e1 <> s and
A4: {s,e1} = (halfline (s,t)) /\ (Sphere (x,r)) and
( t in Sphere (x,r) implies e1 = t ) and
( not t in Sphere (x,r) & ((- (2 * |((t - (((1 / 2) * s) + ((1 / 2) * t))),((((1 / 2) * s) + ((1 / 2) * t)) - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((t - (((1 / 2) * s) + ((1 / 2) * t))),((((1 / 2) * s) + ((1 / 2) * t)) - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))) = ((- (2 * |((t - (((1 / 2) * s) + ((1 / 2) * t))),((((1 / 2) * s) + ((1 / 2) * t)) - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((t - (((1 / 2) * s) + ((1 / 2) * t))),((((1 / 2) * s) + ((1 / 2) * t)) - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))) implies e1 = ((1 - (((- (2 * |((t - (((1 / 2) * s) + ((1 / 2) * t))),((((1 / 2) * s) + ((1 / 2) * t)) - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((t - (((1 / 2) * s) + ((1 / 2) * t))),((((1 / 2) * s) + ((1 / 2) * t)) - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))))) * (((1 / 2) * s) + ((1 / 2) * t))) + ((((- (2 * |((t - (((1 / 2) * s) + ((1 / 2) * t))),((((1 / 2) * s) + ((1 / 2) * t)) - x))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((t - (((1 / 2) * s) + ((1 / 2) * t))),((((1 / 2) * s) + ((1 / 2) * t)) - x))|),((Sum (sqr (S - X))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))) * t) ) by A1, A2, TOPREAL9:38;
e1 in {s,e1} by TARSKI:def_2;
then e1 in Sphere (x,r) by A4, XBOOLE_0:def_4;
hence ex e being Point of (Tcircle (x,r)) st
( e <> s & {s,e} = (halfline (s,t)) /\ (Sphere (x,r)) ) by A2, A3, A4; ::_thesis: verum
end;
definition
let n be non empty Element of NAT ;
let o be Point of (TOP-REAL n);
let s, t be Point of (TOP-REAL n);
let r be non negative real number ;
assume that
A1: s is Point of (Tdisk (o,r)) and
A2: t is Point of (Tdisk (o,r)) and
A3: s <> t ;
func HC (s,t,o,r) -> Point of (TOP-REAL n) means :Def3: :: BROUWER:def 3
( it in (halfline (s,t)) /\ (Sphere (o,r)) & it <> s );
existence
ex b1 being Point of (TOP-REAL n) st
( b1 in (halfline (s,t)) /\ (Sphere (o,r)) & b1 <> s )
proof
percases ( s is Point of (Tcircle (o,r)) or not s is Point of (Tcircle (o,r)) ) ;
suppose s is Point of (Tcircle (o,r)) ; ::_thesis: ex b1 being Point of (TOP-REAL n) st
( b1 in (halfline (s,t)) /\ (Sphere (o,r)) & b1 <> s )
then consider e being Point of (Tcircle (o,r)) such that
A4: ( e <> s & {s,e} = (halfline (s,t)) /\ (Sphere (o,r)) ) by A2, A3, Th5;
reconsider e = e as Point of (TOP-REAL n) by PRE_TOPC:25;
take e ; ::_thesis: ( e in (halfline (s,t)) /\ (Sphere (o,r)) & e <> s )
thus ( e in (halfline (s,t)) /\ (Sphere (o,r)) & e <> s ) by A4, TARSKI:def_2; ::_thesis: verum
end;
supposeA5: s is not Point of (Tcircle (o,r)) ; ::_thesis: ex b1 being Point of (TOP-REAL n) st
( b1 in (halfline (s,t)) /\ (Sphere (o,r)) & b1 <> s )
then consider e1 being Point of (Tcircle (o,r)) such that
A6: {e1} = (halfline (s,t)) /\ (Sphere (o,r)) by A1, A3, Th4;
reconsider e1 = e1 as Point of (TOP-REAL n) by PRE_TOPC:25;
take e1 ; ::_thesis: ( e1 in (halfline (s,t)) /\ (Sphere (o,r)) & e1 <> s )
thus ( e1 in (halfline (s,t)) /\ (Sphere (o,r)) & e1 <> s ) by A5, A6, TARSKI:def_1; ::_thesis: verum
end;
end;
end;
uniqueness
for b1, b2 being Point of (TOP-REAL n) st b1 in (halfline (s,t)) /\ (Sphere (o,r)) & b1 <> s & b2 in (halfline (s,t)) /\ (Sphere (o,r)) & b2 <> s holds
b1 = b2
proof
let m, u be Point of (TOP-REAL n); ::_thesis: ( m in (halfline (s,t)) /\ (Sphere (o,r)) & m <> s & u in (halfline (s,t)) /\ (Sphere (o,r)) & u <> s implies m = u )
assume that
A7: m in (halfline (s,t)) /\ (Sphere (o,r)) and
A8: m <> s and
A9: u in (halfline (s,t)) /\ (Sphere (o,r)) and
A10: u <> s ; ::_thesis: m = u
percases ( s is Point of (Tcircle (o,r)) or not s is Point of (Tcircle (o,r)) ) ;
suppose s is Point of (Tcircle (o,r)) ; ::_thesis: m = u
then consider f1 being Point of (Tcircle (o,r)) such that
f1 <> s and
A11: {s,f1} = (halfline (s,t)) /\ (Sphere (o,r)) by A2, A3, Th5;
percases ( ( m = f1 & u = f1 ) or ( m = f1 & u = s ) or ( m = s & u = f1 ) or ( m = s & u = s ) ) by A7, A9, A11, TARSKI:def_2;
suppose ( m = f1 & u = f1 ) ; ::_thesis: m = u
hence m = u ; ::_thesis: verum
end;
suppose ( m = f1 & u = s ) ; ::_thesis: m = u
hence m = u by A10; ::_thesis: verum
end;
suppose ( m = s & u = f1 ) ; ::_thesis: m = u
hence m = u by A8; ::_thesis: verum
end;
suppose ( m = s & u = s ) ; ::_thesis: m = u
hence m = u ; ::_thesis: verum
end;
end;
end;
suppose s is not Point of (Tcircle (o,r)) ; ::_thesis: m = u
then consider e being Point of (Tcircle (o,r)) such that
A12: {e} = (halfline (s,t)) /\ (Sphere (o,r)) by A1, A3, Th4;
m = e by A7, A12, TARSKI:def_1;
hence m = u by A9, A12, TARSKI:def_1; ::_thesis: verum
end;
end;
end;
end;
:: deftheorem Def3 defines HC BROUWER:def_3_:_
for n being non empty Element of NAT
for o, s, t being Point of (TOP-REAL n)
for r being non negative real number st s is Point of (Tdisk (o,r)) & t is Point of (Tdisk (o,r)) & s <> t holds
for b6 being Point of (TOP-REAL n) holds
( b6 = HC (s,t,o,r) iff ( b6 in (halfline (s,t)) /\ (Sphere (o,r)) & b6 <> s ) );
theorem Th6: :: BROUWER:6
for r being non negative real number
for n being non empty Element of NAT
for s, o, t being Point of (TOP-REAL n) st s is Point of (Tdisk (o,r)) & t is Point of (Tdisk (o,r)) & s <> t holds
HC (s,t,o,r) is Point of (Tcircle (o,r))
proof
let r be non negative real number ; ::_thesis: for n being non empty Element of NAT
for s, o, t being Point of (TOP-REAL n) st s is Point of (Tdisk (o,r)) & t is Point of (Tdisk (o,r)) & s <> t holds
HC (s,t,o,r) is Point of (Tcircle (o,r))
let n be non empty Element of NAT ; ::_thesis: for s, o, t being Point of (TOP-REAL n) st s is Point of (Tdisk (o,r)) & t is Point of (Tdisk (o,r)) & s <> t holds
HC (s,t,o,r) is Point of (Tcircle (o,r))
let s, o, t be Point of (TOP-REAL n); ::_thesis: ( s is Point of (Tdisk (o,r)) & t is Point of (Tdisk (o,r)) & s <> t implies HC (s,t,o,r) is Point of (Tcircle (o,r)) )
assume ( s is Point of (Tdisk (o,r)) & t is Point of (Tdisk (o,r)) & s <> t ) ; ::_thesis: HC (s,t,o,r) is Point of (Tcircle (o,r))
then ( the carrier of (Tcircle (o,r)) = Sphere (o,r) & HC (s,t,o,r) in (halfline (s,t)) /\ (Sphere (o,r)) ) by Def3, TOPREALB:9;
hence HC (s,t,o,r) is Point of (Tcircle (o,r)) by XBOOLE_0:def_4; ::_thesis: verum
end;
theorem :: BROUWER:7
for a being real number
for r being non negative real number
for n being non empty Element of NAT
for s, t, o being Point of (TOP-REAL n)
for S, T, O being Element of REAL n st S = s & T = t & O = o & s is Point of (Tdisk (o,r)) & t is Point of (Tdisk (o,r)) & s <> t & a = ((- |((t - s),(s - o))|) + (sqrt ((|((t - s),(s - o))| ^2) - ((Sum (sqr (T - S))) * ((Sum (sqr (S - O))) - (r ^2)))))) / (Sum (sqr (T - S))) holds
HC (s,t,o,r) = ((1 - a) * s) + (a * t)
proof
let a be real number ; ::_thesis: for r being non negative real number
for n being non empty Element of NAT
for s, t, o being Point of (TOP-REAL n)
for S, T, O being Element of REAL n st S = s & T = t & O = o & s is Point of (Tdisk (o,r)) & t is Point of (Tdisk (o,r)) & s <> t & a = ((- |((t - s),(s - o))|) + (sqrt ((|((t - s),(s - o))| ^2) - ((Sum (sqr (T - S))) * ((Sum (sqr (S - O))) - (r ^2)))))) / (Sum (sqr (T - S))) holds
HC (s,t,o,r) = ((1 - a) * s) + (a * t)
let r be non negative real number ; ::_thesis: for n being non empty Element of NAT
for s, t, o being Point of (TOP-REAL n)
for S, T, O being Element of REAL n st S = s & T = t & O = o & s is Point of (Tdisk (o,r)) & t is Point of (Tdisk (o,r)) & s <> t & a = ((- |((t - s),(s - o))|) + (sqrt ((|((t - s),(s - o))| ^2) - ((Sum (sqr (T - S))) * ((Sum (sqr (S - O))) - (r ^2)))))) / (Sum (sqr (T - S))) holds
HC (s,t,o,r) = ((1 - a) * s) + (a * t)
let n be non empty Element of NAT ; ::_thesis: for s, t, o being Point of (TOP-REAL n)
for S, T, O being Element of REAL n st S = s & T = t & O = o & s is Point of (Tdisk (o,r)) & t is Point of (Tdisk (o,r)) & s <> t & a = ((- |((t - s),(s - o))|) + (sqrt ((|((t - s),(s - o))| ^2) - ((Sum (sqr (T - S))) * ((Sum (sqr (S - O))) - (r ^2)))))) / (Sum (sqr (T - S))) holds
HC (s,t,o,r) = ((1 - a) * s) + (a * t)
let s, t, o be Point of (TOP-REAL n); ::_thesis: for S, T, O being Element of REAL n st S = s & T = t & O = o & s is Point of (Tdisk (o,r)) & t is Point of (Tdisk (o,r)) & s <> t & a = ((- |((t - s),(s - o))|) + (sqrt ((|((t - s),(s - o))| ^2) - ((Sum (sqr (T - S))) * ((Sum (sqr (S - O))) - (r ^2)))))) / (Sum (sqr (T - S))) holds
HC (s,t,o,r) = ((1 - a) * s) + (a * t)
let S, T, O be Element of REAL n; ::_thesis: ( S = s & T = t & O = o & s is Point of (Tdisk (o,r)) & t is Point of (Tdisk (o,r)) & s <> t & a = ((- |((t - s),(s - o))|) + (sqrt ((|((t - s),(s - o))| ^2) - ((Sum (sqr (T - S))) * ((Sum (sqr (S - O))) - (r ^2)))))) / (Sum (sqr (T - S))) implies HC (s,t,o,r) = ((1 - a) * s) + (a * t) )
assume that
A1: S = s and
A2: T = t and
A3: O = o and
A4: s is Point of (Tdisk (o,r)) and
A5: t is Point of (Tdisk (o,r)) and
A6: s <> t ; ::_thesis: ( not a = ((- |((t - s),(s - o))|) + (sqrt ((|((t - s),(s - o))| ^2) - ((Sum (sqr (T - S))) * ((Sum (sqr (S - O))) - (r ^2)))))) / (Sum (sqr (T - S))) or HC (s,t,o,r) = ((1 - a) * s) + (a * t) )
A7: ( |.(T - S).| = sqrt (Sum (sqr (T - S))) & Sum (sqr (T - S)) >= 0 ) by EUCLID:def_5, RVSUM_1:86;
set H = HC (s,t,o,r);
A8: HC (s,t,o,r) in (halfline (s,t)) /\ (Sphere (o,r)) by A4, A5, A6, Def3;
then HC (s,t,o,r) in halfline (s,t) by XBOOLE_0:def_4;
then consider l being real number such that
A9: HC (s,t,o,r) = ((1 - l) * s) + (l * t) and
A10: 0 <= l by TOPREAL9:26;
HC (s,t,o,r) in Sphere (o,r) by A8, XBOOLE_0:def_4;
then r = |.((((1 - l) * s) + (l * t)) - o).| by A9, TOPREAL9:9
.= |.((((1 * s) - (l * s)) + (l * t)) - o).| by EUCLID:50
.= |.(((s - (l * s)) + (l * t)) - o).| by EUCLID:29
.= |.((s - ((l * s) - (l * t))) - o).| by EUCLID:47
.= |.((s + (- ((l * s) - (l * t)))) + (- o)).|
.= |.((s + (- o)) + (- ((l * s) - (l * t)))).| by EUCLID:26
.= |.((s - o) - ((l * s) - (l * t))).|
.= |.((s - o) + (- (l * (s - t)))).| by EUCLID:49
.= |.((s - o) + (l * (- (s - t)))).| by EUCLID:40
.= |.((s - o) + (l * (t - s))).| by EUCLID:44 ;
then A11: r ^2 = ((|.(s - o).| ^2) + (2 * |((l * (t - s)),(s - o))|)) + (|.(l * (t - s)).| ^2) by EUCLID_2:45
.= ((|.(s - o).| ^2) + (2 * (l * |((t - s),(s - o))|))) + (|.(l * (t - s)).| ^2) by EUCLID_2:19 ;
set A = Sum (sqr (T - S));
A12: |.(T - S).| <> 0 by A1, A2, A6, EUCLID:16;
A13: now__::_thesis:_not_Sum_(sqr_(T_-_S))_<=_0
assume Sum (sqr (T - S)) <= 0 ; ::_thesis: contradiction
then Sum (sqr (T - S)) = 0 by RVSUM_1:86;
hence contradiction by A12, EUCLID:def_5, SQUARE_1:17; ::_thesis: verum
end;
set C = (Sum (sqr (S - O))) - (r ^2);
set M = |((t - s),(s - o))|;
set B = 2 * |((t - s),(s - o))|;
set l1 = ((- (2 * |((t - s),(s - o))|)) - (sqrt (delta ((Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))));
set l2 = ((- (2 * |((t - s),(s - o))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))));
A14: |.(S - O).| = sqrt (Sum (sqr (S - O))) by EUCLID:def_5;
Sum (sqr (S - O)) >= 0 by RVSUM_1:86;
then A15: |.(S - O).| ^2 = Sum (sqr (S - O)) by A14, SQUARE_1:def_2;
A16: delta ((Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2))) = ((2 * |((t - s),(s - o))|) ^2) - ((4 * (Sum (sqr (T - S)))) * ((Sum (sqr (S - O))) - (r ^2))) by QUIN_1:def_1;
the carrier of (Tdisk (o,r)) = cl_Ball (o,r) by Th3;
then |.(s - o).| <= r by A4, TOPREAL9:8;
then A17: (sqrt (Sum (sqr (S - O)))) ^2 <= r ^2 by A1, A3, A14, SQUARE_1:15;
then A18: (Sum (sqr (S - O))) - (r ^2) <= 0 by A14, A15, XREAL_1:47;
now__::_thesis:_for_x_being_real_number_holds_Polynom_((Sum_(sqr_(T_-_S))),(2_*_|((t_-_s),(s_-_o))|),((Sum_(sqr_(S_-_O)))_-_(r_^2)),x)_=_Quard_((Sum_(sqr_(T_-_S))),(((-_(2_*_|((t_-_s),(s_-_o))|))_-_(sqrt_(delta_((Sum_(sqr_(T_-_S))),(2_*_|((t_-_s),(s_-_o))|),((Sum_(sqr_(S_-_O)))_-_(r_^2))))))_/_(2_*_(Sum_(sqr_(T_-_S))))),(((-_(2_*_|((t_-_s),(s_-_o))|))_+_(sqrt_(delta_((Sum_(sqr_(T_-_S))),(2_*_|((t_-_s),(s_-_o))|),((Sum_(sqr_(S_-_O)))_-_(r_^2))))))_/_(2_*_(Sum_(sqr_(T_-_S))))),x)
let x be real number ; ::_thesis: Polynom ((Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2)),x) = Quard ((Sum (sqr (T - S))),(((- (2 * |((t - s),(s - o))|)) - (sqrt (delta ((Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))),(((- (2 * |((t - s),(s - o))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))),x)
thus Polynom ((Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2)),x) = (((Sum (sqr (T - S))) * (x ^2)) + ((2 * |((t - s),(s - o))|) * x)) + ((Sum (sqr (S - O))) - (r ^2)) by POLYEQ_1:def_2
.= ((Sum (sqr (T - S))) * (x - (((- (2 * |((t - s),(s - o))|)) - (sqrt (delta ((Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))))) * (x - (((- (2 * |((t - s),(s - o))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))))) by A13, A18, A16, QUIN_1:16
.= (Sum (sqr (T - S))) * ((x - (((- (2 * |((t - s),(s - o))|)) - (sqrt (delta ((Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))))) * (x - (((- (2 * |((t - s),(s - o))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))))))
.= Quard ((Sum (sqr (T - S))),(((- (2 * |((t - s),(s - o))|)) - (sqrt (delta ((Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))),(((- (2 * |((t - s),(s - o))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))),x) by POLYEQ_1:def_3 ; ::_thesis: verum
end;
then A19: ((Sum (sqr (S - O))) - (r ^2)) / (Sum (sqr (T - S))) = (((- (2 * |((t - s),(s - o))|)) - (sqrt (delta ((Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))) * (((- (2 * |((t - s),(s - o))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2)))))) / (2 * (Sum (sqr (T - S))))) by A13, POLYEQ_1:11;
A20: now__::_thesis:_not_((-_(2_*_|((t_-_s),(s_-_o))|))_-_(sqrt_(delta_((Sum_(sqr_(T_-_S))),(2_*_|((t_-_s),(s_-_o))|),((Sum_(sqr_(S_-_O)))_-_(r_^2))))))_/_(2_*_(Sum_(sqr_(T_-_S))))_>_((-_(2_*_|((t_-_s),(s_-_o))|))_+_(sqrt_(delta_((Sum_(sqr_(T_-_S))),(2_*_|((t_-_s),(s_-_o))|),((Sum_(sqr_(S_-_O)))_-_(r_^2))))))_/_(2_*_(Sum_(sqr_(T_-_S))))
set D = sqrt (delta ((Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2))));
assume ((- (2 * |((t - s),(s - o))|)) - (sqrt (delta ((Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))) > ((- (2 * |((t - s),(s - o))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))) ; ::_thesis: contradiction
then (- (sqrt (delta ((Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2)))))) - (2 * |((t - s),(s - o))|) > (sqrt (delta ((Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2))))) - (2 * |((t - s),(s - o))|) by A13, XREAL_1:72;
hence contradiction by A13, A18, A16, XREAL_1:9; ::_thesis: verum
end;
assume A21: a = ((- |((t - s),(s - o))|) + (sqrt ((|((t - s),(s - o))| ^2) - ((Sum (sqr (T - S))) * ((Sum (sqr (S - O))) - (r ^2)))))) / (Sum (sqr (T - S))) ; ::_thesis: HC (s,t,o,r) = ((1 - a) * s) + (a * t)
delta ((Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2))) = ((2 * |((t - s),(s - o))|) ^2) - ((4 * (Sum (sqr (T - S)))) * ((Sum (sqr (S - O))) - (r ^2))) by QUIN_1:def_1
.= 4 * ((|((t - s),(s - o))| ^2) - ((Sum (sqr (T - S))) * ((Sum (sqr (S - O))) - (r ^2)))) ;
then A22: ((- (2 * |((t - s),(s - o))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))) = ((- (2 * |((t - s),(s - o))|)) + ((sqrt 4) * (sqrt ((|((t - s),(s - o))| ^2) - ((Sum (sqr (T - S))) * ((Sum (sqr (S - O))) - (r ^2))))))) / (2 * (Sum (sqr (T - S)))) by A13, A18, SQUARE_1:29
.= (2 * (- (|((t - s),(s - o))| - (sqrt ((|((t - s),(s - o))| ^2) - ((Sum (sqr (T - S))) * ((Sum (sqr (S - O))) - (r ^2)))))))) / (2 * (Sum (sqr (T - S)))) by SQUARE_1:20
.= a by A21, XCMPLX_1:91 ;
A23: HC (s,t,o,r) = ((1 * s) - (l * s)) + (l * t) by A9, EUCLID:50
.= (s - (l * s)) + (l * t) by EUCLID:29
.= (s + (l * t)) - (l * s) by EUCLID:26
.= s + ((l * t) - (l * s)) by EUCLID:45
.= s + (l * (t - s)) by EUCLID:49 ;
l is Real by XREAL_0:def_1;
then A24: |.(l * (t - s)).| ^2 = ((abs l) * |.(t - s).|) ^2 by TOPRNS_1:7
.= ((abs l) ^2) * (|.(t - s).| ^2)
.= (l ^2) * (|.(t - s).| ^2) by COMPLEX1:75 ;
(((Sum (sqr (T - S))) * (l ^2)) + ((2 * |((t - s),(s - o))|) * l)) + ((Sum (sqr (S - O))) - (r ^2)) = (((Sum (sqr (T - S))) * (l ^2)) + ((2 * |((t - s),(s - o))|) * l)) + ((Sum (sqr (S - O))) - (r ^2))
.= (((|.(T - S).| ^2) * (l ^2)) + ((2 * |((t - s),(s - o))|) * l)) + ((|.(S - O).| ^2) - (r ^2)) by A7, A15, SQUARE_1:def_2
.= (((|.(t - s).| ^2) * (l ^2)) + ((2 * |((t - s),(s - o))|) * l)) + ((|.(s - o).| ^2) - (r ^2)) by A1, A2, A3
.= 0 by A24, A11 ;
then Polynom ((Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2)),l) = 0 by POLYEQ_1:def_2;
then A25: ( l = ((- (2 * |((t - s),(s - o))|)) - (sqrt (delta ((Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))) or l = ((- (2 * |((t - s),(s - o))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))) ) by A13, A18, A16, POLYEQ_1:5;
percases ( (Sum (sqr (S - O))) - (r ^2) < 0 or ((- (2 * |((t - s),(s - o))|)) - (sqrt (delta ((Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))) = ((- (2 * |((t - s),(s - o))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))) or (Sum (sqr (S - O))) - (r ^2) = 0 ) by A14, A15, A17, XREAL_1:47;
suppose (Sum (sqr (S - O))) - (r ^2) < 0 ; ::_thesis: HC (s,t,o,r) = ((1 - a) * s) + (a * t)
hence HC (s,t,o,r) = ((1 - a) * s) + (a * t) by A9, A10, A13, A22, A25, A19, A20, XREAL_1:141; ::_thesis: verum
end;
suppose ((- (2 * |((t - s),(s - o))|)) - (sqrt (delta ((Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))) = ((- (2 * |((t - s),(s - o))|)) + (sqrt (delta ((Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))) ; ::_thesis: HC (s,t,o,r) = ((1 - a) * s) + (a * t)
hence HC (s,t,o,r) = ((1 - a) * s) + (a * t) by A9, A22, A25; ::_thesis: verum
end;
supposeA26: (Sum (sqr (S - O))) - (r ^2) = 0 ; ::_thesis: HC (s,t,o,r) = ((1 - a) * s) + (a * t)
now__::_thesis:_not_l_=_((-_(2_*_|((t_-_s),(s_-_o))|))_-_(sqrt_(delta_((Sum_(sqr_(T_-_S))),(2_*_|((t_-_s),(s_-_o))|),((Sum_(sqr_(S_-_O)))_-_(r_^2))))))_/_(2_*_(Sum_(sqr_(T_-_S))))
A27: now__::_thesis:_not_l_=_0
assume l = 0 ; ::_thesis: contradiction
then HC (s,t,o,r) = s + (0. (TOP-REAL n)) by A23, EUCLID:29
.= s by EUCLID:27 ;
hence contradiction by A4, A5, A6, Def3; ::_thesis: verum
end;
assume A28: l = ((- (2 * |((t - s),(s - o))|)) - (sqrt (delta ((Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))) ; ::_thesis: contradiction
percases ( 0 < 2 * |((t - s),(s - o))| or 2 * |((t - s),(s - o))| <= 0 ) ;
supposeA29: 0 < 2 * |((t - s),(s - o))| ; ::_thesis: contradiction
then ((- (2 * |((t - s),(s - o))|)) - (sqrt (delta ((Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))) = ((- (2 * |((t - s),(s - o))|)) - (2 * |((t - s),(s - o))|)) / (2 * (Sum (sqr (T - S)))) by A16, A26, SQUARE_1:22;
hence contradiction by A10, A13, A28, A29, XREAL_1:129, XREAL_1:141; ::_thesis: verum
end;
suppose 2 * |((t - s),(s - o))| <= 0 ; ::_thesis: contradiction
then ((- (2 * |((t - s),(s - o))|)) - (sqrt (delta ((Sum (sqr (T - S))),(2 * |((t - s),(s - o))|),((Sum (sqr (S - O))) - (r ^2)))))) / (2 * (Sum (sqr (T - S)))) = ((- (2 * |((t - s),(s - o))|)) - (- (2 * |((t - s),(s - o))|))) / (2 * (Sum (sqr (T - S)))) by A16, A26, SQUARE_1:23
.= 0 ;
hence contradiction by A28, A27; ::_thesis: verum
end;
end;
end;
hence HC (s,t,o,r) = ((1 - a) * s) + (a * t) by A9, A22, A25; ::_thesis: verum
end;
end;
end;
theorem Th8: :: BROUWER:8
for a being real number
for r being non negative real number
for r1, r2, s1, s2 being real number
for s, t, o being Point of (TOP-REAL 2) st s is Point of (Tdisk (o,r)) & t is Point of (Tdisk (o,r)) & s <> t & r1 = (t `1) - (s `1) & r2 = (t `2) - (s `2) & s1 = (s `1) - (o `1) & s2 = (s `2) - (o `2) & a = ((- ((s1 * r1) + (s2 * r2))) + (sqrt ((((s1 * r1) + (s2 * r2)) ^2) - (((r1 ^2) + (r2 ^2)) * (((s1 ^2) + (s2 ^2)) - (r ^2)))))) / ((r1 ^2) + (r2 ^2)) holds
HC (s,t,o,r) = |[((s `1) + (a * r1)),((s `2) + (a * r2))]|
proof
let a be real number ; ::_thesis: for r being non negative real number
for r1, r2, s1, s2 being real number
for s, t, o being Point of (TOP-REAL 2) st s is Point of (Tdisk (o,r)) & t is Point of (Tdisk (o,r)) & s <> t & r1 = (t `1) - (s `1) & r2 = (t `2) - (s `2) & s1 = (s `1) - (o `1) & s2 = (s `2) - (o `2) & a = ((- ((s1 * r1) + (s2 * r2))) + (sqrt ((((s1 * r1) + (s2 * r2)) ^2) - (((r1 ^2) + (r2 ^2)) * (((s1 ^2) + (s2 ^2)) - (r ^2)))))) / ((r1 ^2) + (r2 ^2)) holds
HC (s,t,o,r) = |[((s `1) + (a * r1)),((s `2) + (a * r2))]|
let r be non negative real number ; ::_thesis: for r1, r2, s1, s2 being real number
for s, t, o being Point of (TOP-REAL 2) st s is Point of (Tdisk (o,r)) & t is Point of (Tdisk (o,r)) & s <> t & r1 = (t `1) - (s `1) & r2 = (t `2) - (s `2) & s1 = (s `1) - (o `1) & s2 = (s `2) - (o `2) & a = ((- ((s1 * r1) + (s2 * r2))) + (sqrt ((((s1 * r1) + (s2 * r2)) ^2) - (((r1 ^2) + (r2 ^2)) * (((s1 ^2) + (s2 ^2)) - (r ^2)))))) / ((r1 ^2) + (r2 ^2)) holds
HC (s,t,o,r) = |[((s `1) + (a * r1)),((s `2) + (a * r2))]|
let r1, r2, s1, s2 be real number ; ::_thesis: for s, t, o being Point of (TOP-REAL 2) st s is Point of (Tdisk (o,r)) & t is Point of (Tdisk (o,r)) & s <> t & r1 = (t `1) - (s `1) & r2 = (t `2) - (s `2) & s1 = (s `1) - (o `1) & s2 = (s `2) - (o `2) & a = ((- ((s1 * r1) + (s2 * r2))) + (sqrt ((((s1 * r1) + (s2 * r2)) ^2) - (((r1 ^2) + (r2 ^2)) * (((s1 ^2) + (s2 ^2)) - (r ^2)))))) / ((r1 ^2) + (r2 ^2)) holds
HC (s,t,o,r) = |[((s `1) + (a * r1)),((s `2) + (a * r2))]|
let s, t, o be Point of (TOP-REAL 2); ::_thesis: ( s is Point of (Tdisk (o,r)) & t is Point of (Tdisk (o,r)) & s <> t & r1 = (t `1) - (s `1) & r2 = (t `2) - (s `2) & s1 = (s `1) - (o `1) & s2 = (s `2) - (o `2) & a = ((- ((s1 * r1) + (s2 * r2))) + (sqrt ((((s1 * r1) + (s2 * r2)) ^2) - (((r1 ^2) + (r2 ^2)) * (((s1 ^2) + (s2 ^2)) - (r ^2)))))) / ((r1 ^2) + (r2 ^2)) implies HC (s,t,o,r) = |[((s `1) + (a * r1)),((s `2) + (a * r2))]| )
assume that
A1: s is Point of (Tdisk (o,r)) and
A2: t is Point of (Tdisk (o,r)) and
A3: s <> t and
A4: ( r1 = (t `1) - (s `1) & r2 = (t `2) - (s `2) ) and
A5: s1 = (s `1) - (o `1) and
A6: s2 = (s `2) - (o `2) and
A7: a = ((- ((s1 * r1) + (s2 * r2))) + (sqrt ((((s1 * r1) + (s2 * r2)) ^2) - (((r1 ^2) + (r2 ^2)) * (((s1 ^2) + (s2 ^2)) - (r ^2)))))) / ((r1 ^2) + (r2 ^2)) ; ::_thesis: HC (s,t,o,r) = |[((s `1) + (a * r1)),((s `2) + (a * r2))]|
the carrier of (Tdisk (o,r)) = cl_Ball (o,r) by Th3;
then |.(s - o).| <= r by A1, TOPREAL9:8;
then A8: |.(s - o).| ^2 <= r ^2 by SQUARE_1:15;
set C = ((s1 ^2) + (s2 ^2)) - (r ^2);
set A = (r1 ^2) + (r2 ^2);
set M = (s1 * r1) + (s2 * r2);
set B = 2 * ((s1 * r1) + (s2 * r2));
set l1 = ((- (2 * ((s1 * r1) + (s2 * r2)))) - (sqrt (delta (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2)))))) / (2 * ((r1 ^2) + (r2 ^2)));
set l2 = ((- (2 * ((s1 * r1) + (s2 * r2)))) + (sqrt (delta (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2)))))) / (2 * ((r1 ^2) + (r2 ^2)));
A9: delta (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2))) = ((2 * ((s1 * r1) + (s2 * r2))) ^2) - ((4 * ((r1 ^2) + (r2 ^2))) * (((s1 ^2) + (s2 ^2)) - (r ^2))) by QUIN_1:def_1;
|.(s - o).| ^2 = (((s - o) `1) ^2) + (((s - o) `2) ^2) by JGRAPH_1:29
.= (s1 ^2) + (((s - o) `2) ^2) by A5, TOPREAL3:3
.= (s1 ^2) + (s2 ^2) by A6, TOPREAL3:3 ;
then A10: ((s1 ^2) + (s2 ^2)) - (r ^2) <= (r ^2) - (r ^2) by A8, XREAL_1:9;
then A11: ((2 * ((s1 * r1) + (s2 * r2))) ^2) - ((4 * ((r1 ^2) + (r2 ^2))) * (((s1 ^2) + (s2 ^2)) - (r ^2))) >= 0 ;
A12: now__::_thesis:_not_((-_(2_*_((s1_*_r1)_+_(s2_*_r2))))_-_(sqrt_(delta_(((r1_^2)_+_(r2_^2)),(2_*_((s1_*_r1)_+_(s2_*_r2))),(((s1_^2)_+_(s2_^2))_-_(r_^2))))))_/_(2_*_((r1_^2)_+_(r2_^2)))_>_((-_(2_*_((s1_*_r1)_+_(s2_*_r2))))_+_(sqrt_(delta_(((r1_^2)_+_(r2_^2)),(2_*_((s1_*_r1)_+_(s2_*_r2))),(((s1_^2)_+_(s2_^2))_-_(r_^2))))))_/_(2_*_((r1_^2)_+_(r2_^2)))
set D = sqrt (delta (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2))));
assume ((- (2 * ((s1 * r1) + (s2 * r2)))) - (sqrt (delta (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2)))))) / (2 * ((r1 ^2) + (r2 ^2))) > ((- (2 * ((s1 * r1) + (s2 * r2)))) + (sqrt (delta (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2)))))) / (2 * ((r1 ^2) + (r2 ^2))) ; ::_thesis: contradiction
then (- (sqrt (delta (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2)))))) - (2 * ((s1 * r1) + (s2 * r2))) > (sqrt (delta (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2))))) - (2 * ((s1 * r1) + (s2 * r2))) by XREAL_1:72;
then - (sqrt (delta (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2))))) > sqrt (delta (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2)))) by XREAL_1:9;
then (- (sqrt (delta (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2)))))) + (sqrt (delta (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2))))) > (sqrt (delta (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2))))) + (sqrt (delta (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2))))) by XREAL_1:6;
hence contradiction by A9, A11; ::_thesis: verum
end;
( r1 <> 0 or r2 <> 0 ) by A3, A4, TOPREAL3:6;
then A13: 0 + 0 < (r1 ^2) + (r2 ^2) by SQUARE_1:12, XREAL_1:8;
for x being real number holds Polynom (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2)),x) = Quard (((r1 ^2) + (r2 ^2)),(((- (2 * ((s1 * r1) + (s2 * r2)))) - (sqrt (delta (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2)))))) / (2 * ((r1 ^2) + (r2 ^2)))),(((- (2 * ((s1 * r1) + (s2 * r2)))) + (sqrt (delta (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2)))))) / (2 * ((r1 ^2) + (r2 ^2)))),x)
proof
let x be real number ; ::_thesis: Polynom (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2)),x) = Quard (((r1 ^2) + (r2 ^2)),(((- (2 * ((s1 * r1) + (s2 * r2)))) - (sqrt (delta (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2)))))) / (2 * ((r1 ^2) + (r2 ^2)))),(((- (2 * ((s1 * r1) + (s2 * r2)))) + (sqrt (delta (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2)))))) / (2 * ((r1 ^2) + (r2 ^2)))),x)
thus Polynom (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2)),x) = ((((r1 ^2) + (r2 ^2)) * (x ^2)) + ((2 * ((s1 * r1) + (s2 * r2))) * x)) + (((s1 ^2) + (s2 ^2)) - (r ^2)) by POLYEQ_1:def_2
.= (((r1 ^2) + (r2 ^2)) * (x - (((- (2 * ((s1 * r1) + (s2 * r2)))) - (sqrt (delta (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2)))))) / (2 * ((r1 ^2) + (r2 ^2)))))) * (x - (((- (2 * ((s1 * r1) + (s2 * r2)))) + (sqrt (delta (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2)))))) / (2 * ((r1 ^2) + (r2 ^2))))) by A13, A9, A10, QUIN_1:16
.= ((r1 ^2) + (r2 ^2)) * ((x - (((- (2 * ((s1 * r1) + (s2 * r2)))) - (sqrt (delta (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2)))))) / (2 * ((r1 ^2) + (r2 ^2))))) * (x - (((- (2 * ((s1 * r1) + (s2 * r2)))) + (sqrt (delta (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2)))))) / (2 * ((r1 ^2) + (r2 ^2))))))
.= Quard (((r1 ^2) + (r2 ^2)),(((- (2 * ((s1 * r1) + (s2 * r2)))) - (sqrt (delta (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2)))))) / (2 * ((r1 ^2) + (r2 ^2)))),(((- (2 * ((s1 * r1) + (s2 * r2)))) + (sqrt (delta (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2)))))) / (2 * ((r1 ^2) + (r2 ^2)))),x) by POLYEQ_1:def_3 ; ::_thesis: verum
end;
then A14: (((s1 ^2) + (s2 ^2)) - (r ^2)) / ((r1 ^2) + (r2 ^2)) = (((- (2 * ((s1 * r1) + (s2 * r2)))) - (sqrt (delta (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2)))))) / (2 * ((r1 ^2) + (r2 ^2)))) * (((- (2 * ((s1 * r1) + (s2 * r2)))) + (sqrt (delta (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2)))))) / (2 * ((r1 ^2) + (r2 ^2)))) by A13, POLYEQ_1:11;
delta (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2))) = ((2 * ((s1 * r1) + (s2 * r2))) ^2) - ((4 * ((r1 ^2) + (r2 ^2))) * (((s1 ^2) + (s2 ^2)) - (r ^2))) by QUIN_1:def_1
.= 4 * ((((s1 * r1) + (s2 * r2)) ^2) - (((r1 ^2) + (r2 ^2)) * (((s1 ^2) + (s2 ^2)) - (r ^2)))) ;
then A15: ((- (2 * ((s1 * r1) + (s2 * r2)))) + (sqrt (delta (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2)))))) / (2 * ((r1 ^2) + (r2 ^2))) = ((- (2 * ((s1 * r1) + (s2 * r2)))) + ((sqrt 4) * (sqrt ((((s1 * r1) + (s2 * r2)) ^2) - (((r1 ^2) + (r2 ^2)) * (((s1 ^2) + (s2 ^2)) - (r ^2))))))) / (2 * ((r1 ^2) + (r2 ^2))) by A10, SQUARE_1:29
.= (2 * (- (((s1 * r1) + (s2 * r2)) - (sqrt ((((s1 * r1) + (s2 * r2)) ^2) - (((r1 ^2) + (r2 ^2)) * (((s1 ^2) + (s2 ^2)) - (r ^2)))))))) / (2 * ((r1 ^2) + (r2 ^2))) by SQUARE_1:20
.= a by A7, XCMPLX_1:91 ;
set H = HC (s,t,o,r);
A16: HC (s,t,o,r) in (halfline (s,t)) /\ (Sphere (o,r)) by A1, A2, A3, Def3;
then HC (s,t,o,r) in halfline (s,t) by XBOOLE_0:def_4;
then consider l being real number such that
A17: HC (s,t,o,r) = ((1 - l) * s) + (l * t) and
A18: 0 <= l by TOPREAL9:26;
A19: HC (s,t,o,r) = ((1 * s) - (l * s)) + (l * t) by A17, EUCLID:50
.= (s - (l * s)) + (l * t) by EUCLID:29
.= (s + (l * t)) - (l * s) by EUCLID:26
.= s + ((l * t) - (l * s)) by EUCLID:45
.= s + (l * (t - s)) by EUCLID:49 ;
then A20: (HC (s,t,o,r)) `1 = (s `1) + ((l * (t - s)) `1) by TOPREAL3:2
.= (s `1) + (l * ((t - s) `1)) by TOPREAL3:4
.= (s `1) + (l * ((t `1) - (s `1))) by TOPREAL3:3 ;
HC (s,t,o,r) in Sphere (o,r) by A16, XBOOLE_0:def_4;
then |.((HC (s,t,o,r)) - o).| = r by TOPREAL9:9;
then r ^2 = ((((HC (s,t,o,r)) - o) `1) ^2) + ((((HC (s,t,o,r)) - o) `2) ^2) by JGRAPH_1:29
.= ((((HC (s,t,o,r)) `1) - (o `1)) ^2) + ((((HC (s,t,o,r)) - o) `2) ^2) by TOPREAL3:3
.= ((((HC (s,t,o,r)) `1) - (o `1)) ^2) + ((((HC (s,t,o,r)) `2) - (o `2)) ^2) by TOPREAL3:3
.= (((((1 - l) * (s `1)) + (l * (t `1))) - (o `1)) ^2) + ((((HC (s,t,o,r)) `2) - (o `2)) ^2) by A17, TOPREAL9:41
.= (((((1 - l) * (s `1)) + (l * (t `1))) - (o `1)) ^2) + (((((1 - l) * (s `2)) + (l * (t `2))) - (o `2)) ^2) by A17, TOPREAL9:42
.= ((((l ^2) * ((r1 ^2) + (r2 ^2))) + ((l * 2) * ((s1 * r1) + (s2 * r2)))) + (s1 ^2)) + (s2 ^2) by A4, A5, A6 ;
then ((((r1 ^2) + (r2 ^2)) * (l ^2)) + ((2 * ((s1 * r1) + (s2 * r2))) * l)) + (((s1 ^2) + (s2 ^2)) - (r ^2)) = 0 ;
then Polynom (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2)),l) = 0 by POLYEQ_1:def_2;
then A21: ( l = ((- (2 * ((s1 * r1) + (s2 * r2)))) - (sqrt (delta (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2)))))) / (2 * ((r1 ^2) + (r2 ^2))) or l = ((- (2 * ((s1 * r1) + (s2 * r2)))) + (sqrt (delta (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2)))))) / (2 * ((r1 ^2) + (r2 ^2))) ) by A13, A9, A10, POLYEQ_1:5;
A22: (HC (s,t,o,r)) `2 = (s `2) + ((l * (t - s)) `2) by A19, TOPREAL3:2
.= (s `2) + (l * ((t - s) `2)) by TOPREAL3:4
.= (s `2) + (l * ((t `2) - (s `2))) by TOPREAL3:3 ;
percases ( ((s1 ^2) + (s2 ^2)) - (r ^2) < 0 or ((- (2 * ((s1 * r1) + (s2 * r2)))) - (sqrt (delta (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2)))))) / (2 * ((r1 ^2) + (r2 ^2))) = ((- (2 * ((s1 * r1) + (s2 * r2)))) + (sqrt (delta (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2)))))) / (2 * ((r1 ^2) + (r2 ^2))) or ((s1 ^2) + (s2 ^2)) - (r ^2) = 0 ) by A10;
suppose ((s1 ^2) + (s2 ^2)) - (r ^2) < 0 ; ::_thesis: HC (s,t,o,r) = |[((s `1) + (a * r1)),((s `2) + (a * r2))]|
hence HC (s,t,o,r) = |[((s `1) + (a * r1)),((s `2) + (a * r2))]| by A4, A18, A20, A22, A13, A15, A21, A14, A12, EUCLID:53, XREAL_1:141; ::_thesis: verum
end;
suppose ((- (2 * ((s1 * r1) + (s2 * r2)))) - (sqrt (delta (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2)))))) / (2 * ((r1 ^2) + (r2 ^2))) = ((- (2 * ((s1 * r1) + (s2 * r2)))) + (sqrt (delta (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2)))))) / (2 * ((r1 ^2) + (r2 ^2))) ; ::_thesis: HC (s,t,o,r) = |[((s `1) + (a * r1)),((s `2) + (a * r2))]|
hence HC (s,t,o,r) = |[((s `1) + (a * r1)),((s `2) + (a * r2))]| by A4, A20, A22, A15, A21, EUCLID:53; ::_thesis: verum
end;
supposeA23: ((s1 ^2) + (s2 ^2)) - (r ^2) = 0 ; ::_thesis: HC (s,t,o,r) = |[((s `1) + (a * r1)),((s `2) + (a * r2))]|
now__::_thesis:_not_l_=_((-_(2_*_((s1_*_r1)_+_(s2_*_r2))))_-_(sqrt_(delta_(((r1_^2)_+_(r2_^2)),(2_*_((s1_*_r1)_+_(s2_*_r2))),(((s1_^2)_+_(s2_^2))_-_(r_^2))))))_/_(2_*_((r1_^2)_+_(r2_^2)))
A24: now__::_thesis:_not_l_=_0
assume l = 0 ; ::_thesis: contradiction
then HC (s,t,o,r) = s + (0. (TOP-REAL 2)) by A19, EUCLID:29
.= s by EUCLID:27 ;
hence contradiction by A1, A2, A3, Def3; ::_thesis: verum
end;
assume A25: l = ((- (2 * ((s1 * r1) + (s2 * r2)))) - (sqrt (delta (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2)))))) / (2 * ((r1 ^2) + (r2 ^2))) ; ::_thesis: contradiction
percases ( 0 < 2 * ((s1 * r1) + (s2 * r2)) or 2 * ((s1 * r1) + (s2 * r2)) <= 0 ) ;
supposeA26: 0 < 2 * ((s1 * r1) + (s2 * r2)) ; ::_thesis: contradiction
then ((- (2 * ((s1 * r1) + (s2 * r2)))) - (sqrt (delta (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2)))))) / (2 * ((r1 ^2) + (r2 ^2))) = ((- (2 * ((s1 * r1) + (s2 * r2)))) - (2 * ((s1 * r1) + (s2 * r2)))) / (2 * ((r1 ^2) + (r2 ^2))) by A9, A23, SQUARE_1:22;
hence contradiction by A18, A13, A25, A26, XREAL_1:129, XREAL_1:141; ::_thesis: verum
end;
suppose 2 * ((s1 * r1) + (s2 * r2)) <= 0 ; ::_thesis: contradiction
then ((- (2 * ((s1 * r1) + (s2 * r2)))) - (sqrt (delta (((r1 ^2) + (r2 ^2)),(2 * ((s1 * r1) + (s2 * r2))),(((s1 ^2) + (s2 ^2)) - (r ^2)))))) / (2 * ((r1 ^2) + (r2 ^2))) = ((- (2 * ((s1 * r1) + (s2 * r2)))) - (- (2 * ((s1 * r1) + (s2 * r2))))) / (2 * ((r1 ^2) + (r2 ^2))) by A9, A23, SQUARE_1:23
.= 0 ;
hence contradiction by A25, A24; ::_thesis: verum
end;
end;
end;
hence HC (s,t,o,r) = |[((s `1) + (a * r1)),((s `2) + (a * r2))]| by A4, A20, A22, A15, A21, EUCLID:53; ::_thesis: verum
end;
end;
end;
definition
let n be non empty Element of NAT ;
let o be Point of (TOP-REAL n);
let r be non negative real number ;
let x be Point of (Tdisk (o,r));
let f be Function of (Tdisk (o,r)),(Tdisk (o,r));
assume A1: not x is_a_fixpoint_of f ;
func HC (x,f) -> Point of (Tcircle (o,r)) means :Def4: :: BROUWER:def 4
ex y, z being Point of (TOP-REAL n) st
( y = x & z = f . x & it = HC (z,y,o,r) );
existence
ex b1 being Point of (Tcircle (o,r)) ex y, z being Point of (TOP-REAL n) st
( y = x & z = f . x & b1 = HC (z,y,o,r) )
proof
reconsider y = x, z = f . x as Point of (TOP-REAL n) by PRE_TOPC:25;
x <> f . x by A1, ABIAN:def_4;
then reconsider a = HC (z,y,o,r) as Point of (Tcircle (o,r)) by Th6;
take a ; ::_thesis: ex y, z being Point of (TOP-REAL n) st
( y = x & z = f . x & a = HC (z,y,o,r) )
thus ex y, z being Point of (TOP-REAL n) st
( y = x & z = f . x & a = HC (z,y,o,r) ) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being Point of (Tcircle (o,r)) st ex y, z being Point of (TOP-REAL n) st
( y = x & z = f . x & b1 = HC (z,y,o,r) ) & ex y, z being Point of (TOP-REAL n) st
( y = x & z = f . x & b2 = HC (z,y,o,r) ) holds
b1 = b2 ;
end;
:: deftheorem Def4 defines HC BROUWER:def_4_:_
for n being non empty Element of NAT
for o being Point of (TOP-REAL n)
for r being non negative real number
for x being Point of (Tdisk (o,r))
for f being Function of (Tdisk (o,r)),(Tdisk (o,r)) st not x is_a_fixpoint_of f holds
for b6 being Point of (Tcircle (o,r)) holds
( b6 = HC (x,f) iff ex y, z being Point of (TOP-REAL n) st
( y = x & z = f . x & b6 = HC (z,y,o,r) ) );
theorem Th9: :: BROUWER:9
for r being non negative real number
for n being non empty Element of NAT
for o being Point of (TOP-REAL n)
for x being Point of (Tdisk (o,r))
for f being Function of (Tdisk (o,r)),(Tdisk (o,r)) st not x is_a_fixpoint_of f & x is Point of (Tcircle (o,r)) holds
HC (x,f) = x
proof
let r be non negative real number ; ::_thesis: for n being non empty Element of NAT
for o being Point of (TOP-REAL n)
for x being Point of (Tdisk (o,r))
for f being Function of (Tdisk (o,r)),(Tdisk (o,r)) st not x is_a_fixpoint_of f & x is Point of (Tcircle (o,r)) holds
HC (x,f) = x
let n be non empty Element of NAT ; ::_thesis: for o being Point of (TOP-REAL n)
for x being Point of (Tdisk (o,r))
for f being Function of (Tdisk (o,r)),(Tdisk (o,r)) st not x is_a_fixpoint_of f & x is Point of (Tcircle (o,r)) holds
HC (x,f) = x
let o be Point of (TOP-REAL n); ::_thesis: for x being Point of (Tdisk (o,r))
for f being Function of (Tdisk (o,r)),(Tdisk (o,r)) st not x is_a_fixpoint_of f & x is Point of (Tcircle (o,r)) holds
HC (x,f) = x
let x be Point of (Tdisk (o,r)); ::_thesis: for f being Function of (Tdisk (o,r)),(Tdisk (o,r)) st not x is_a_fixpoint_of f & x is Point of (Tcircle (o,r)) holds
HC (x,f) = x
let f be Function of (Tdisk (o,r)),(Tdisk (o,r)); ::_thesis: ( not x is_a_fixpoint_of f & x is Point of (Tcircle (o,r)) implies HC (x,f) = x )
assume that
A1: not x is_a_fixpoint_of f and
A2: x is Point of (Tcircle (o,r)) ; ::_thesis: HC (x,f) = x
A3: x <> f . x by A1, ABIAN:def_4;
A4: the carrier of (Tcircle (o,r)) = Sphere (o,r) by TOPREALB:9;
consider y, z being Point of (TOP-REAL n) such that
A5: y = x and
A6: ( z = f . x & HC (x,f) = HC (z,y,o,r) ) by A1, Def4;
x in halfline (z,y) by A5, TOPREAL9:28;
then x in (halfline (z,y)) /\ (Sphere (o,r)) by A2, A4, XBOOLE_0:def_4;
hence HC (x,f) = x by A3, A5, A6, Def3; ::_thesis: verum
end;
theorem Th10: :: BROUWER:10
for r being positive real number
for o being Point of (TOP-REAL 2)
for Y being non empty SubSpace of Tdisk (o,r) st Y = Tcircle (o,r) holds
not Y is_a_retract_of Tdisk (o,r)
proof
let r be positive real number ; ::_thesis: for o being Point of (TOP-REAL 2)
for Y being non empty SubSpace of Tdisk (o,r) st Y = Tcircle (o,r) holds
not Y is_a_retract_of Tdisk (o,r)
let o be Point of (TOP-REAL 2); ::_thesis: for Y being non empty SubSpace of Tdisk (o,r) st Y = Tcircle (o,r) holds
not Y is_a_retract_of Tdisk (o,r)
let Y be non empty SubSpace of Tdisk (o,r); ::_thesis: ( Y = Tcircle (o,r) implies not Y is_a_retract_of Tdisk (o,r) )
assume A1: Y = Tcircle (o,r) ; ::_thesis: not Y is_a_retract_of Tdisk (o,r)
set y0 = the Point of Y;
set X = Tdisk (o,r);
A2: the Point of Y in the carrier of Y ;
( the carrier of (Tcircle (o,r)) = Sphere (o,r) & Sphere (o,r) c= cl_Ball (o,r) ) by TOPREAL9:17, TOPREALB:9;
then reconsider x0 = the Point of Y as Point of (Tdisk (o,r)) by A1, A2, Th3;
reconsider a0 = 0 , a1 = 1 as Point of I[01] by BORSUK_1:def_14, BORSUK_1:def_15;
set C = the constant Loop of x0;
A3: the constant Loop of x0 = I[01] --> x0 by BORSUK_2:5
.= the carrier of I[01] --> the Point of Y ;
then reconsider D = the constant Loop of x0 as Function of I[01],Y ;
A4: ( D = I[01] --> the Point of Y & D . a0 = the Point of Y ) by A3, FUNCOP_1:7;
( the Point of Y, the Point of Y are_connected & D . a1 = the Point of Y ) by A3, FUNCOP_1:7;
then reconsider D = D as constant Loop of the Point of Y by A4, BORSUK_2:def_2;
given R being continuous Function of (Tdisk (o,r)),Y such that A5: R is being_a_retraction ; :: according to BORSUK_1:def_17 ::_thesis: contradiction
the carrier of (pi_1 (Y, the Point of Y)) = {(Class ((EqRel (Y, the Point of Y)),D))}
proof
set E = EqRel (Y, the Point of Y);
hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: {(Class ((EqRel (Y, the Point of Y)),D))} c= the carrier of (pi_1 (Y, the Point of Y))
let x be set ; ::_thesis: ( x in the carrier of (pi_1 (Y, the Point of Y)) implies x in {(Class ((EqRel (Y, the Point of Y)),D))} )
assume x in the carrier of (pi_1 (Y, the Point of Y)) ; ::_thesis: x in {(Class ((EqRel (Y, the Point of Y)),D))}
then consider f0 being Loop of the Point of Y such that
A6: x = Class ((EqRel (Y, the Point of Y)),f0) by TOPALG_1:47;
reconsider g0 = f0 as Loop of x0 by TOPALG_2:1;
g0, the constant Loop of x0 are_homotopic by TOPALG_2:2;
then consider f being Function of [:I[01],I[01]:],(Tdisk (o,r)) such that
A7: f is continuous and
A8: for s being Point of I[01] holds
( f . (s,0) = g0 . s & f . (s,1) = the constant Loop of x0 . s & ( for t being Point of I[01] holds
( f . (0,t) = x0 & f . (1,t) = x0 ) ) ) by BORSUK_2:def_7;
f0,D are_homotopic
proof
take F = R * f; :: according to BORSUK_2:def_7 ::_thesis: ( F is continuous & ( for b1 being Element of the carrier of K582() holds
( F . (b1,0) = f0 . b1 & F . (b1,1) = D . b1 & F . (0,b1) = the Point of Y & F . (1,b1) = the Point of Y ) ) )
thus F is continuous by A7; ::_thesis: for b1 being Element of the carrier of K582() holds
( F . (b1,0) = f0 . b1 & F . (b1,1) = D . b1 & F . (0,b1) = the Point of Y & F . (1,b1) = the Point of Y )
let s be Point of I[01]; ::_thesis: ( F . (s,0) = f0 . s & F . (s,1) = D . s & F . (0,s) = the Point of Y & F . (1,s) = the Point of Y )
thus F . (s,0) = F . [s,a0]
.= R . (f . (s,0)) by FUNCT_2:15
.= R . (g0 . s) by A8
.= f0 . s by A5, BORSUK_1:def_16 ; ::_thesis: ( F . (s,1) = D . s & F . (0,s) = the Point of Y & F . (1,s) = the Point of Y )
thus F . (s,1) = F . [s,a1]
.= R . (f . (s,1)) by FUNCT_2:15
.= R . ( the constant Loop of x0 . s) by A8
.= D . s by A5, BORSUK_1:def_16 ; ::_thesis: ( F . (0,s) = the Point of Y & F . (1,s) = the Point of Y )
thus F . (0,s) = F . [a0,s]
.= R . (f . (0,s)) by FUNCT_2:15
.= R . x0 by A8
.= the Point of Y by A5, BORSUK_1:def_16 ; ::_thesis: F . (1,s) = the Point of Y
thus F . (1,s) = F . [a1,s]
.= R . (f . (1,s)) by FUNCT_2:15
.= R . x0 by A8
.= the Point of Y by A5, BORSUK_1:def_16 ; ::_thesis: verum
end;
then x = Class ((EqRel (Y, the Point of Y)),D) by A6, TOPALG_1:46;
hence x in {(Class ((EqRel (Y, the Point of Y)),D))} by TARSKI:def_1; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {(Class ((EqRel (Y, the Point of Y)),D))} or x in the carrier of (pi_1 (Y, the Point of Y)) )
assume x in {(Class ((EqRel (Y, the Point of Y)),D))} ; ::_thesis: x in the carrier of (pi_1 (Y, the Point of Y))
then A9: x = Class ((EqRel (Y, the Point of Y)),D) by TARSKI:def_1;
D in Loops the Point of Y by TOPALG_1:def_1;
then x in Class (EqRel (Y, the Point of Y)) by A9, EQREL_1:def_3;
hence x in the carrier of (pi_1 (Y, the Point of Y)) by TOPALG_1:def_5; ::_thesis: verum
end;
hence contradiction by A1; ::_thesis: verum
end;
definition
let n be non empty Element of NAT ;
let r be non negative real number ;
let o be Point of (TOP-REAL n);
let f be Function of (Tdisk (o,r)),(Tdisk (o,r));
func BR-map f -> Function of (Tdisk (o,r)),(Tcircle (o,r)) means :Def5: :: BROUWER:def 5
for x being Point of (Tdisk (o,r)) holds it . x = HC (x,f);
existence
ex b1 being Function of (Tdisk (o,r)),(Tcircle (o,r)) st
for x being Point of (Tdisk (o,r)) holds b1 . x = HC (x,f)
proof
defpred S1[ Point of (Tdisk (o,r)), set ] means $2 = HC ($1,f);
A1: for x being Point of (Tdisk (o,r)) ex m being Point of (Tcircle (o,r)) st S1[x,m] ;
ex h being Function of (Tdisk (o,r)),(Tcircle (o,r)) st
for x being Point of (Tdisk (o,r)) holds S1[x,h . x] from FUNCT_2:sch_3(A1);
hence ex b1 being Function of (Tdisk (o,r)),(Tcircle (o,r)) st
for x being Point of (Tdisk (o,r)) holds b1 . x = HC (x,f) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being Function of (Tdisk (o,r)),(Tcircle (o,r)) st ( for x being Point of (Tdisk (o,r)) holds b1 . x = HC (x,f) ) & ( for x being Point of (Tdisk (o,r)) holds b2 . x = HC (x,f) ) holds
b1 = b2
proof
let f1, f2 be Function of (Tdisk (o,r)),(Tcircle (o,r)); ::_thesis: ( ( for x being Point of (Tdisk (o,r)) holds f1 . x = HC (x,f) ) & ( for x being Point of (Tdisk (o,r)) holds f2 . x = HC (x,f) ) implies f1 = f2 )
assume that
A2: for x being Point of (Tdisk (o,r)) holds f1 . x = HC (x,f) and
A3: for x being Point of (Tdisk (o,r)) holds f2 . x = HC (x,f) ; ::_thesis: f1 = f2
for x being Point of (Tdisk (o,r)) holds f1 . x = f2 . x
proof
let x be Point of (Tdisk (o,r)); ::_thesis: f1 . x = f2 . x
thus f1 . x = HC (x,f) by A2
.= f2 . x by A3 ; ::_thesis: verum
end;
hence f1 = f2 by FUNCT_2:63; ::_thesis: verum
end;
end;
:: deftheorem Def5 defines BR-map BROUWER:def_5_:_
for n being non empty Element of NAT
for r being non negative real number
for o being Point of (TOP-REAL n)
for f being Function of (Tdisk (o,r)),(Tdisk (o,r))
for b5 being Function of (Tdisk (o,r)),(Tcircle (o,r)) holds
( b5 = BR-map f iff for x being Point of (Tdisk (o,r)) holds b5 . x = HC (x,f) );
theorem Th11: :: BROUWER:11
for r being non negative real number
for n being non empty Element of NAT
for o being Point of (TOP-REAL n)
for x being Point of (Tdisk (o,r))
for f being Function of (Tdisk (o,r)),(Tdisk (o,r)) st not x is_a_fixpoint_of f & x is Point of (Tcircle (o,r)) holds
(BR-map f) . x = x
proof
let r be non negative real number ; ::_thesis: for n being non empty Element of NAT
for o being Point of (TOP-REAL n)
for x being Point of (Tdisk (o,r))
for f being Function of (Tdisk (o,r)),(Tdisk (o,r)) st not x is_a_fixpoint_of f & x is Point of (Tcircle (o,r)) holds
(BR-map f) . x = x
let n be non empty Element of NAT ; ::_thesis: for o being Point of (TOP-REAL n)
for x being Point of (Tdisk (o,r))
for f being Function of (Tdisk (o,r)),(Tdisk (o,r)) st not x is_a_fixpoint_of f & x is Point of (Tcircle (o,r)) holds
(BR-map f) . x = x
let o be Point of (TOP-REAL n); ::_thesis: for x being Point of (Tdisk (o,r))
for f being Function of (Tdisk (o,r)),(Tdisk (o,r)) st not x is_a_fixpoint_of f & x is Point of (Tcircle (o,r)) holds
(BR-map f) . x = x
let x be Point of (Tdisk (o,r)); ::_thesis: for f being Function of (Tdisk (o,r)),(Tdisk (o,r)) st not x is_a_fixpoint_of f & x is Point of (Tcircle (o,r)) holds
(BR-map f) . x = x
let f be Function of (Tdisk (o,r)),(Tdisk (o,r)); ::_thesis: ( not x is_a_fixpoint_of f & x is Point of (Tcircle (o,r)) implies (BR-map f) . x = x )
assume A1: ( not x is_a_fixpoint_of f & x is Point of (Tcircle (o,r)) ) ; ::_thesis: (BR-map f) . x = x
thus (BR-map f) . x = HC (x,f) by Def5
.= x by A1, Th9 ; ::_thesis: verum
end;
theorem :: BROUWER:12
for r being non negative real number
for n being non empty Element of NAT
for o being Point of (TOP-REAL n)
for f being continuous Function of (Tdisk (o,r)),(Tdisk (o,r)) st f is without_fixpoints holds
(BR-map f) | (Sphere (o,r)) = id (Tcircle (o,r))
proof
let r be non negative real number ; ::_thesis: for n being non empty Element of NAT
for o being Point of (TOP-REAL n)
for f being continuous Function of (Tdisk (o,r)),(Tdisk (o,r)) st f is without_fixpoints holds
(BR-map f) | (Sphere (o,r)) = id (Tcircle (o,r))
let n be non empty Element of NAT ; ::_thesis: for o being Point of (TOP-REAL n)
for f being continuous Function of (Tdisk (o,r)),(Tdisk (o,r)) st f is without_fixpoints holds
(BR-map f) | (Sphere (o,r)) = id (Tcircle (o,r))
let o be Point of (TOP-REAL n); ::_thesis: for f being continuous Function of (Tdisk (o,r)),(Tdisk (o,r)) st f is without_fixpoints holds
(BR-map f) | (Sphere (o,r)) = id (Tcircle (o,r))
let f be continuous Function of (Tdisk (o,r)),(Tdisk (o,r)); ::_thesis: ( f is without_fixpoints implies (BR-map f) | (Sphere (o,r)) = id (Tcircle (o,r)) )
assume A1: f is without_fixpoints ; ::_thesis: (BR-map f) | (Sphere (o,r)) = id (Tcircle (o,r))
set D = cl_Ball (o,r);
set C = Sphere (o,r);
set g = BR-map f;
( dom (BR-map f) = the carrier of (Tdisk (o,r)) & the carrier of (Tdisk (o,r)) = cl_Ball (o,r) ) by Th3, FUNCT_2:def_1;
then A2: dom ((BR-map f) | (Sphere (o,r))) = Sphere (o,r) by RELAT_1:62, TOPREAL9:17;
A3: the carrier of (Tcircle (o,r)) = Sphere (o,r) by TOPREALB:9;
A4: for x being set st x in dom ((BR-map f) | (Sphere (o,r))) holds
((BR-map f) | (Sphere (o,r))) . x = (id (Tcircle (o,r))) . x
proof
let x be set ; ::_thesis: ( x in dom ((BR-map f) | (Sphere (o,r))) implies ((BR-map f) | (Sphere (o,r))) . x = (id (Tcircle (o,r))) . x )
assume A5: x in dom ((BR-map f) | (Sphere (o,r))) ; ::_thesis: ((BR-map f) | (Sphere (o,r))) . x = (id (Tcircle (o,r))) . x
x in dom (BR-map f) by A5, RELAT_1:57;
then reconsider y = x as Point of (Tdisk (o,r)) ;
A6: not x is_a_fixpoint_of f by A1, ABIAN:def_5;
thus ((BR-map f) | (Sphere (o,r))) . x = (BR-map f) . x by A5, FUNCT_1:49
.= y by A3, A5, A6, Th11
.= (id (Tcircle (o,r))) . x by A3, A5, FUNCT_1:18 ; ::_thesis: verum
end;
dom (id (Tcircle (o,r))) = the carrier of (Tcircle (o,r)) by RELAT_1:45;
hence (BR-map f) | (Sphere (o,r)) = id (Tcircle (o,r)) by A2, A3, A4, FUNCT_1:2; ::_thesis: verum
end;
Lm1: now__::_thesis:_for_T_being_non_empty_TopSpace
for_a_being_Real_holds_the_carrier_of_T_-->_a_is_continuous
let T be non empty TopSpace; ::_thesis: for a being Real holds the carrier of T --> a is continuous
let a be Real; ::_thesis: the carrier of T --> a is continuous
set c = the carrier of T;
set f = the carrier of T --> a;
thus the carrier of T --> a is continuous ::_thesis: verum
proof
let Y be Subset of REAL; :: according to PSCOMP_1:def_3 ::_thesis: ( not Y is closed or ( the carrier of T --> a) " Y is closed )
A1: dom ( the carrier of T --> a) = the carrier of T by FUNCT_2:def_1;
assume Y is closed ; ::_thesis: ( the carrier of T --> a) " Y is closed
A2: rng ( the carrier of T --> a) = {a} by FUNCOP_1:8;
percases ( a in Y or not a in Y ) ;
suppose a in Y ; ::_thesis: ( the carrier of T --> a) " Y is closed
then A3: rng ( the carrier of T --> a) c= Y by A2, ZFMISC_1:31;
( the carrier of T --> a) " Y = ( the carrier of T --> a) " ((rng ( the carrier of T --> a)) /\ Y) by RELAT_1:133
.= ( the carrier of T --> a) " (rng ( the carrier of T --> a)) by A3, XBOOLE_1:28
.= [#] T by A1, RELAT_1:134 ;
hence ( the carrier of T --> a) " Y is closed ; ::_thesis: verum
end;
suppose not a in Y ; ::_thesis: ( the carrier of T --> a) " Y is closed
then A4: rng ( the carrier of T --> a) misses Y by A2, ZFMISC_1:50;
( the carrier of T --> a) " Y = ( the carrier of T --> a) " ((rng ( the carrier of T --> a)) /\ Y) by RELAT_1:133
.= ( the carrier of T --> a) " {} by A4, XBOOLE_0:def_7
.= {} T ;
hence ( the carrier of T --> a) " Y is closed ; ::_thesis: verum
end;
end;
end;
end;
theorem Th13: :: BROUWER:13
for r being positive real number
for o being Point of (TOP-REAL 2)
for f being continuous Function of (Tdisk (o,r)),(Tdisk (o,r)) st f is without_fixpoints holds
BR-map f is continuous
proof
set R = R2Homeomorphism ;
defpred S1[ set , set ] means ex x1, x2 being Point of (TOP-REAL 2) st
( $1 = [x1,x2] & $2 = x2 `1 );
defpred S2[ set , set ] means ex x1, x2 being Point of (TOP-REAL 2) st
( $1 = [x1,x2] & $2 = (x1 `1) - (x2 `1) );
let r be positive real number ; ::_thesis: for o being Point of (TOP-REAL 2)
for f being continuous Function of (Tdisk (o,r)),(Tdisk (o,r)) st f is without_fixpoints holds
BR-map f is continuous
let o be Point of (TOP-REAL 2); ::_thesis: for f being continuous Function of (Tdisk (o,r)),(Tdisk (o,r)) st f is without_fixpoints holds
BR-map f is continuous
defpred S3[ set , set ] means ex x1, x2 being Point of (TOP-REAL 2) st
( $1 = [x1,x2] & $2 = (x2 `1) - (o `1) );
defpred S4[ set , set ] means ex x1, x2 being Point of (TOP-REAL 2) st
( $1 = [x1,x2] & $2 = (x2 `2) - (o `2) );
reconsider rr = r ^2 as Real by XREAL_0:def_1;
set f1 = the carrier of [:(TOP-REAL 2),(TOP-REAL 2):] --> rr;
A1: for x being Element of [:(TOP-REAL 2),(TOP-REAL 2):] ex r being Real st S3[x,r]
proof
let x be Element of [:(TOP-REAL 2),(TOP-REAL 2):]; ::_thesis: ex r being Real st S3[x,r]
consider x1, x2 being Point of (TOP-REAL 2) such that
A2: x = [x1,x2] by BORSUK_1:10;
take (x2 `1) - (o `1) ; ::_thesis: S3[x,(x2 `1) - (o `1)]
take x1 ; ::_thesis: ex x2 being Point of (TOP-REAL 2) st
( x = [x1,x2] & (x2 `1) - (o `1) = (x2 `1) - (o `1) )
take x2 ; ::_thesis: ( x = [x1,x2] & (x2 `1) - (o `1) = (x2 `1) - (o `1) )
thus ( x = [x1,x2] & (x2 `1) - (o `1) = (x2 `1) - (o `1) ) by A2; ::_thesis: verum
end;
consider xo being RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] such that
A3: for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds S3[x,xo . x] from FUNCT_2:sch_3(A1);
A4: for x being Element of [:(TOP-REAL 2),(TOP-REAL 2):] ex r being Real st S1[x,r]
proof
let x be Element of [:(TOP-REAL 2),(TOP-REAL 2):]; ::_thesis: ex r being Real st S1[x,r]
consider x1, x2 being Point of (TOP-REAL 2) such that
A5: x = [x1,x2] by BORSUK_1:10;
take x2 `1 ; ::_thesis: S1[x,x2 `1 ]
take x1 ; ::_thesis: ex x2 being Point of (TOP-REAL 2) st
( x = [x1,x2] & x2 `1 = x2 `1 )
take x2 ; ::_thesis: ( x = [x1,x2] & x2 `1 = x2 `1 )
thus ( x = [x1,x2] & x2 `1 = x2 `1 ) by A5; ::_thesis: verum
end;
consider fx2 being RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] such that
A6: for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds S1[x,fx2 . x] from FUNCT_2:sch_3(A4);
A7: for x being Element of [:(TOP-REAL 2),(TOP-REAL 2):] ex r being Real st S4[x,r]
proof
let x be Element of [:(TOP-REAL 2),(TOP-REAL 2):]; ::_thesis: ex r being Real st S4[x,r]
consider x1, x2 being Point of (TOP-REAL 2) such that
A8: x = [x1,x2] by BORSUK_1:10;
take (x2 `2) - (o `2) ; ::_thesis: S4[x,(x2 `2) - (o `2)]
take x1 ; ::_thesis: ex x2 being Point of (TOP-REAL 2) st
( x = [x1,x2] & (x2 `2) - (o `2) = (x2 `2) - (o `2) )
take x2 ; ::_thesis: ( x = [x1,x2] & (x2 `2) - (o `2) = (x2 `2) - (o `2) )
thus ( x = [x1,x2] & (x2 `2) - (o `2) = (x2 `2) - (o `2) ) by A8; ::_thesis: verum
end;
consider yo being RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] such that
A9: for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds S4[x,yo . x] from FUNCT_2:sch_3(A7);
reconsider f1 = the carrier of [:(TOP-REAL 2),(TOP-REAL 2):] --> rr as continuous RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] by Lm1;
set D2 = Tdisk (o,r);
set S1 = Tcircle (o,r);
set OK = (DiffElems ((TOP-REAL 2),(TOP-REAL 2))) /\ the carrier of [:(Tdisk (o,r)),(Tdisk (o,r)):];
set s = the Point of (Tcircle (o,r));
A10: |.(o - o).| = |.(0. (TOP-REAL 2)).| by EUCLID:42
.= 0 by TOPRNS_1:23 ;
A11: the carrier of (Tcircle (o,r)) = Sphere (o,r) by TOPREALB:9;
A12: now__::_thesis:_not_o_=_the_Point_of_(Tcircle_(o,r))
assume A13: o = the Point of (Tcircle (o,r)) ; ::_thesis: contradiction
( Ball (o,r) misses Sphere (o,r) & o in Ball (o,r) ) by A10, TOPREAL9:7, TOPREAL9:19;
hence contradiction by A11, A13, XBOOLE_0:3; ::_thesis: verum
end;
the carrier of (Tdisk (o,r)) = cl_Ball (o,r) by Th3;
then A14: o is Point of (Tdisk (o,r)) by A10, TOPREAL9:8;
( the Point of (Tcircle (o,r)) in the carrier of (Tcircle (o,r)) & Sphere (o,r) c= cl_Ball (o,r) ) by TOPREAL9:17;
then the Point of (Tcircle (o,r)) is Point of (Tdisk (o,r)) by A11, Th3;
then [o, the Point of (Tcircle (o,r))] in [: the carrier of (Tdisk (o,r)), the carrier of (Tdisk (o,r)):] by A14, ZFMISC_1:87;
then A15: [o, the Point of (Tcircle (o,r))] in the carrier of [:(Tdisk (o,r)),(Tdisk (o,r)):] by BORSUK_1:def_2;
the Point of (Tcircle (o,r)) is Point of (TOP-REAL 2) by PRE_TOPC:25;
then [o, the Point of (Tcircle (o,r))] in DiffElems ((TOP-REAL 2),(TOP-REAL 2)) by A12;
then reconsider OK = (DiffElems ((TOP-REAL 2),(TOP-REAL 2))) /\ the carrier of [:(Tdisk (o,r)),(Tdisk (o,r)):] as non empty Subset of [:(TOP-REAL 2),(TOP-REAL 2):] by A15, XBOOLE_0:def_4;
set Zf1 = f1 | OK;
defpred S5[ set , set ] means ex x1, x2 being Point of (TOP-REAL 2) st
( $1 = [x1,x2] & $2 = x2 `2 );
defpred S6[ set , set ] means ex y1, y2 being Point of (TOP-REAL 2) st
( $1 = [y1,y2] & $2 = (y1 `2) - (y2 `2) );
set TD = [:(TOP-REAL 2),(TOP-REAL 2):] | OK;
let f be continuous Function of (Tdisk (o,r)),(Tdisk (o,r)); ::_thesis: ( f is without_fixpoints implies BR-map f is continuous )
assume A16: f is without_fixpoints ; ::_thesis: BR-map f is continuous
A17: for x being Element of [:(TOP-REAL 2),(TOP-REAL 2):] ex r being Real st S6[x,r]
proof
let x be Element of [:(TOP-REAL 2),(TOP-REAL 2):]; ::_thesis: ex r being Real st S6[x,r]
consider x1, x2 being Point of (TOP-REAL 2) such that
A18: x = [x1,x2] by BORSUK_1:10;
take (x1 `2) - (x2 `2) ; ::_thesis: S6[x,(x1 `2) - (x2 `2)]
take x1 ; ::_thesis: ex y2 being Point of (TOP-REAL 2) st
( x = [x1,y2] & (x1 `2) - (x2 `2) = (x1 `2) - (y2 `2) )
take x2 ; ::_thesis: ( x = [x1,x2] & (x1 `2) - (x2 `2) = (x1 `2) - (x2 `2) )
thus ( x = [x1,x2] & (x1 `2) - (x2 `2) = (x1 `2) - (x2 `2) ) by A18; ::_thesis: verum
end;
consider dy being RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] such that
A19: for y being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds S6[y,dy . y] from FUNCT_2:sch_3(A17);
A20: for x being Element of [:(TOP-REAL 2),(TOP-REAL 2):] ex r being Real st S5[x,r]
proof
let x be Element of [:(TOP-REAL 2),(TOP-REAL 2):]; ::_thesis: ex r being Real st S5[x,r]
consider x1, x2 being Point of (TOP-REAL 2) such that
A21: x = [x1,x2] by BORSUK_1:10;
take x2 `2 ; ::_thesis: S5[x,x2 `2 ]
take x1 ; ::_thesis: ex x2 being Point of (TOP-REAL 2) st
( x = [x1,x2] & x2 `2 = x2 `2 )
take x2 ; ::_thesis: ( x = [x1,x2] & x2 `2 = x2 `2 )
thus ( x = [x1,x2] & x2 `2 = x2 `2 ) by A21; ::_thesis: verum
end;
consider fy2 being RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] such that
A22: for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds S5[x,fy2 . x] from FUNCT_2:sch_3(A20);
A23: for x being Element of [:(TOP-REAL 2),(TOP-REAL 2):] ex r being Real st S2[x,r]
proof
let x be Element of [:(TOP-REAL 2),(TOP-REAL 2):]; ::_thesis: ex r being Real st S2[x,r]
consider x1, x2 being Point of (TOP-REAL 2) such that
A24: x = [x1,x2] by BORSUK_1:10;
take (x1 `1) - (x2 `1) ; ::_thesis: S2[x,(x1 `1) - (x2 `1)]
take x1 ; ::_thesis: ex x2 being Point of (TOP-REAL 2) st
( x = [x1,x2] & (x1 `1) - (x2 `1) = (x1 `1) - (x2 `1) )
take x2 ; ::_thesis: ( x = [x1,x2] & (x1 `1) - (x2 `1) = (x1 `1) - (x2 `1) )
thus ( x = [x1,x2] & (x1 `1) - (x2 `1) = (x1 `1) - (x2 `1) ) by A24; ::_thesis: verum
end;
consider dx being RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] such that
A25: for x being Point of [:(TOP-REAL 2),(TOP-REAL 2):] holds S2[x,dx . x] from FUNCT_2:sch_3(A23);
reconsider Dx = dx, Dy = dy, fX2 = fx2, fY2 = fy2, Xo = xo, Yo = yo as Function of [:(TOP-REAL 2),(TOP-REAL 2):],R^1 by TOPMETR:17;
for p being Point of [:(TOP-REAL 2),(TOP-REAL 2):]
for V being Subset of R^1 st Yo . p in V & V is open holds
ex W being Subset of [:(TOP-REAL 2),(TOP-REAL 2):] st
( p in W & W is open & Yo .: W c= V )
proof
let p be Point of [:(TOP-REAL 2),(TOP-REAL 2):]; ::_thesis: for V being Subset of R^1 st Yo . p in V & V is open holds
ex W being Subset of [:(TOP-REAL 2),(TOP-REAL 2):] st
( p in W & W is open & Yo .: W c= V )
let V be Subset of R^1; ::_thesis: ( Yo . p in V & V is open implies ex W being Subset of [:(TOP-REAL 2),(TOP-REAL 2):] st
( p in W & W is open & Yo .: W c= V ) )
assume that
A26: Yo . p in V and
A27: V is open ; ::_thesis: ex W being Subset of [:(TOP-REAL 2),(TOP-REAL 2):] st
( p in W & W is open & Yo .: W c= V )
reconsider V1 = V as open Subset of REAL by A27, BORSUK_5:39, TOPMETR:17;
consider p1, p2 being Point of (TOP-REAL 2) such that
A28: p = [p1,p2] and
A29: Yo . p = (p2 `2) - (o `2) by A9;
set r = (p2 `2) - (o `2);
consider g being real number such that
A30: 0 < g and
A31: ].(((p2 `2) - (o `2)) - g),(((p2 `2) - (o `2)) + g).[ c= V1 by A26, A29, RCOMP_1:19;
reconsider g = g as Element of REAL by XREAL_0:def_1;
set W2 = { |[x,y]| where x, y is Element of REAL : ( (p2 `2) - g < y & y < (p2 `2) + g ) } ;
{ |[x,y]| where x, y is Element of REAL : ( (p2 `2) - g < y & y < (p2 `2) + g ) } c= the carrier of (TOP-REAL 2)
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { |[x,y]| where x, y is Element of REAL : ( (p2 `2) - g < y & y < (p2 `2) + g ) } or a in the carrier of (TOP-REAL 2) )
assume a in { |[x,y]| where x, y is Element of REAL : ( (p2 `2) - g < y & y < (p2 `2) + g ) } ; ::_thesis: a in the carrier of (TOP-REAL 2)
then ex x, y being Element of REAL st
( a = |[x,y]| & (p2 `2) - g < y & y < (p2 `2) + g ) ;
hence a in the carrier of (TOP-REAL 2) ; ::_thesis: verum
end;
then reconsider W2 = { |[x,y]| where x, y is Element of REAL : ( (p2 `2) - g < y & y < (p2 `2) + g ) } as Subset of (TOP-REAL 2) ;
take [:([#] (TOP-REAL 2)),W2:] ; ::_thesis: ( p in [:([#] (TOP-REAL 2)),W2:] & [:([#] (TOP-REAL 2)),W2:] is open & Yo .: [:([#] (TOP-REAL 2)),W2:] c= V )
A32: p2 = |[(p2 `1),(p2 `2)]| by EUCLID:53;
( (p2 `2) - g < (p2 `2) - 0 & (p2 `2) + 0 < (p2 `2) + g ) by A30, XREAL_1:6, XREAL_1:15;
then p2 in W2 by A32;
hence p in [:([#] (TOP-REAL 2)),W2:] by A28, ZFMISC_1:def_2; ::_thesis: ( [:([#] (TOP-REAL 2)),W2:] is open & Yo .: [:([#] (TOP-REAL 2)),W2:] c= V )
W2 is open by PSCOMP_1:21;
hence [:([#] (TOP-REAL 2)),W2:] is open by BORSUK_1:6; ::_thesis: Yo .: [:([#] (TOP-REAL 2)),W2:] c= V
let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in Yo .: [:([#] (TOP-REAL 2)),W2:] or b in V )
assume b in Yo .: [:([#] (TOP-REAL 2)),W2:] ; ::_thesis: b in V
then consider a being Point of [:(TOP-REAL 2),(TOP-REAL 2):] such that
A33: a in [:([#] (TOP-REAL 2)),W2:] and
A34: Yo . a = b by FUNCT_2:65;
consider a1, a2 being Point of (TOP-REAL 2) such that
A35: a = [a1,a2] and
A36: yo . a = (a2 `2) - (o `2) by A9;
a2 in W2 by A33, A35, ZFMISC_1:87;
then consider x2, y2 being Element of REAL such that
A37: a2 = |[x2,y2]| and
A38: ( (p2 `2) - g < y2 & y2 < (p2 `2) + g ) ;
a2 `2 = y2 by A37, EUCLID:52;
then ( ((p2 `2) - g) - (o `2) < (a2 `2) - (o `2) & (a2 `2) - (o `2) < ((p2 `2) + g) - (o `2) ) by A38, XREAL_1:9;
then (a2 `2) - (o `2) in ].(((p2 `2) - (o `2)) - g),(((p2 `2) - (o `2)) + g).[ by XXREAL_1:4;
hence b in V by A31, A34, A36; ::_thesis: verum
end;
then Yo is continuous by JGRAPH_2:10;
then reconsider yo = yo as continuous RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] by JORDAN5A:27;
for p being Point of [:(TOP-REAL 2),(TOP-REAL 2):]
for V being Subset of R^1 st Xo . p in V & V is open holds
ex W being Subset of [:(TOP-REAL 2),(TOP-REAL 2):] st
( p in W & W is open & Xo .: W c= V )
proof
let p be Point of [:(TOP-REAL 2),(TOP-REAL 2):]; ::_thesis: for V being Subset of R^1 st Xo . p in V & V is open holds
ex W being Subset of [:(TOP-REAL 2),(TOP-REAL 2):] st
( p in W & W is open & Xo .: W c= V )
let V be Subset of R^1; ::_thesis: ( Xo . p in V & V is open implies ex W being Subset of [:(TOP-REAL 2),(TOP-REAL 2):] st
( p in W & W is open & Xo .: W c= V ) )
assume that
A39: Xo . p in V and
A40: V is open ; ::_thesis: ex W being Subset of [:(TOP-REAL 2),(TOP-REAL 2):] st
( p in W & W is open & Xo .: W c= V )
reconsider V1 = V as open Subset of REAL by A40, BORSUK_5:39, TOPMETR:17;
consider p1, p2 being Point of (TOP-REAL 2) such that
A41: p = [p1,p2] and
A42: Xo . p = (p2 `1) - (o `1) by A3;
set r = (p2 `1) - (o `1);
consider g being real number such that
A43: 0 < g and
A44: ].(((p2 `1) - (o `1)) - g),(((p2 `1) - (o `1)) + g).[ c= V1 by A39, A42, RCOMP_1:19;
reconsider g = g as Element of REAL by XREAL_0:def_1;
set W2 = { |[x,y]| where x, y is Element of REAL : ( (p2 `1) - g < x & x < (p2 `1) + g ) } ;
{ |[x,y]| where x, y is Element of REAL : ( (p2 `1) - g < x & x < (p2 `1) + g ) } c= the carrier of (TOP-REAL 2)
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { |[x,y]| where x, y is Element of REAL : ( (p2 `1) - g < x & x < (p2 `1) + g ) } or a in the carrier of (TOP-REAL 2) )
assume a in { |[x,y]| where x, y is Element of REAL : ( (p2 `1) - g < x & x < (p2 `1) + g ) } ; ::_thesis: a in the carrier of (TOP-REAL 2)
then ex x, y being Element of REAL st
( a = |[x,y]| & (p2 `1) - g < x & x < (p2 `1) + g ) ;
hence a in the carrier of (TOP-REAL 2) ; ::_thesis: verum
end;
then reconsider W2 = { |[x,y]| where x, y is Element of REAL : ( (p2 `1) - g < x & x < (p2 `1) + g ) } as Subset of (TOP-REAL 2) ;
take [:([#] (TOP-REAL 2)),W2:] ; ::_thesis: ( p in [:([#] (TOP-REAL 2)),W2:] & [:([#] (TOP-REAL 2)),W2:] is open & Xo .: [:([#] (TOP-REAL 2)),W2:] c= V )
A45: p2 = |[(p2 `1),(p2 `2)]| by EUCLID:53;
( (p2 `1) - g < (p2 `1) - 0 & (p2 `1) + 0 < (p2 `1) + g ) by A43, XREAL_1:6, XREAL_1:15;
then p2 in W2 by A45;
hence p in [:([#] (TOP-REAL 2)),W2:] by A41, ZFMISC_1:def_2; ::_thesis: ( [:([#] (TOP-REAL 2)),W2:] is open & Xo .: [:([#] (TOP-REAL 2)),W2:] c= V )
W2 is open by PSCOMP_1:19;
hence [:([#] (TOP-REAL 2)),W2:] is open by BORSUK_1:6; ::_thesis: Xo .: [:([#] (TOP-REAL 2)),W2:] c= V
let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in Xo .: [:([#] (TOP-REAL 2)),W2:] or b in V )
assume b in Xo .: [:([#] (TOP-REAL 2)),W2:] ; ::_thesis: b in V
then consider a being Point of [:(TOP-REAL 2),(TOP-REAL 2):] such that
A46: a in [:([#] (TOP-REAL 2)),W2:] and
A47: Xo . a = b by FUNCT_2:65;
consider a1, a2 being Point of (TOP-REAL 2) such that
A48: a = [a1,a2] and
A49: xo . a = (a2 `1) - (o `1) by A3;
a2 in W2 by A46, A48, ZFMISC_1:87;
then consider x2, y2 being Element of REAL such that
A50: a2 = |[x2,y2]| and
A51: ( (p2 `1) - g < x2 & x2 < (p2 `1) + g ) ;
a2 `1 = x2 by A50, EUCLID:52;
then ( ((p2 `1) - g) - (o `1) < (a2 `1) - (o `1) & (a2 `1) - (o `1) < ((p2 `1) + g) - (o `1) ) by A51, XREAL_1:9;
then (a2 `1) - (o `1) in ].(((p2 `1) - (o `1)) - g),(((p2 `1) - (o `1)) + g).[ by XXREAL_1:4;
hence b in V by A44, A47, A49; ::_thesis: verum
end;
then Xo is continuous by JGRAPH_2:10;
then reconsider xo = xo as continuous RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] by JORDAN5A:27;
set Zyo = yo | OK;
set Zxo = xo | OK;
set p2 = (((xo | OK) (#) (xo | OK)) + ((yo | OK) (#) (yo | OK))) - (f1 | OK);
set g = BR-map f;
A52: the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK) = OK by PRE_TOPC:8;
for p being Point of [:(TOP-REAL 2),(TOP-REAL 2):]
for V being Subset of R^1 st Dy . p in V & V is open holds
ex W being Subset of [:(TOP-REAL 2),(TOP-REAL 2):] st
( p in W & W is open & Dy .: W c= V )
proof
let p be Point of [:(TOP-REAL 2),(TOP-REAL 2):]; ::_thesis: for V being Subset of R^1 st Dy . p in V & V is open holds
ex W being Subset of [:(TOP-REAL 2),(TOP-REAL 2):] st
( p in W & W is open & Dy .: W c= V )
let V be Subset of R^1; ::_thesis: ( Dy . p in V & V is open implies ex W being Subset of [:(TOP-REAL 2),(TOP-REAL 2):] st
( p in W & W is open & Dy .: W c= V ) )
assume that
A53: Dy . p in V and
A54: V is open ; ::_thesis: ex W being Subset of [:(TOP-REAL 2),(TOP-REAL 2):] st
( p in W & W is open & Dy .: W c= V )
reconsider V1 = V as open Subset of REAL by A54, BORSUK_5:39, TOPMETR:17;
consider p1, p2 being Point of (TOP-REAL 2) such that
A55: p = [p1,p2] and
A56: dy . p = (p1 `2) - (p2 `2) by A19;
set r = (p1 `2) - (p2 `2);
consider g being real number such that
A57: 0 < g and
A58: ].(((p1 `2) - (p2 `2)) - g),(((p1 `2) - (p2 `2)) + g).[ c= V1 by A53, A56, RCOMP_1:19;
reconsider g = g as Element of REAL by XREAL_0:def_1;
set W2 = { |[x,y]| where x, y is Element of REAL : ( (p2 `2) - (g / 2) < y & y < (p2 `2) + (g / 2) ) } ;
A59: { |[x,y]| where x, y is Element of REAL : ( (p2 `2) - (g / 2) < y & y < (p2 `2) + (g / 2) ) } c= the carrier of (TOP-REAL 2)
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { |[x,y]| where x, y is Element of REAL : ( (p2 `2) - (g / 2) < y & y < (p2 `2) + (g / 2) ) } or a in the carrier of (TOP-REAL 2) )
assume a in { |[x,y]| where x, y is Element of REAL : ( (p2 `2) - (g / 2) < y & y < (p2 `2) + (g / 2) ) } ; ::_thesis: a in the carrier of (TOP-REAL 2)
then ex x, y being Element of REAL st
( a = |[x,y]| & (p2 `2) - (g / 2) < y & y < (p2 `2) + (g / 2) ) ;
hence a in the carrier of (TOP-REAL 2) ; ::_thesis: verum
end;
A60: p2 = |[(p2 `1),(p2 `2)]| by EUCLID:53;
reconsider W2 = { |[x,y]| where x, y is Element of REAL : ( (p2 `2) - (g / 2) < y & y < (p2 `2) + (g / 2) ) } as Subset of (TOP-REAL 2) by A59;
A61: 0 / 2 < g / 2 by A57, XREAL_1:74;
then ( (p2 `2) - (g / 2) < (p2 `2) - 0 & (p2 `2) + 0 < (p2 `2) + (g / 2) ) by XREAL_1:6, XREAL_1:15;
then A62: p2 in W2 by A60;
set W1 = { |[x,y]| where x, y is Element of REAL : ( (p1 `2) - (g / 2) < y & y < (p1 `2) + (g / 2) ) } ;
{ |[x,y]| where x, y is Element of REAL : ( (p1 `2) - (g / 2) < y & y < (p1 `2) + (g / 2) ) } c= the carrier of (TOP-REAL 2)
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { |[x,y]| where x, y is Element of REAL : ( (p1 `2) - (g / 2) < y & y < (p1 `2) + (g / 2) ) } or a in the carrier of (TOP-REAL 2) )
assume a in { |[x,y]| where x, y is Element of REAL : ( (p1 `2) - (g / 2) < y & y < (p1 `2) + (g / 2) ) } ; ::_thesis: a in the carrier of (TOP-REAL 2)
then ex x, y being Element of REAL st
( a = |[x,y]| & (p1 `2) - (g / 2) < y & y < (p1 `2) + (g / 2) ) ;
hence a in the carrier of (TOP-REAL 2) ; ::_thesis: verum
end;
then reconsider W1 = { |[x,y]| where x, y is Element of REAL : ( (p1 `2) - (g / 2) < y & y < (p1 `2) + (g / 2) ) } as Subset of (TOP-REAL 2) ;
take [:W1,W2:] ; ::_thesis: ( p in [:W1,W2:] & [:W1,W2:] is open & Dy .: [:W1,W2:] c= V )
A63: p1 = |[(p1 `1),(p1 `2)]| by EUCLID:53;
( (p1 `2) - (g / 2) < (p1 `2) - 0 & (p1 `2) + 0 < (p1 `2) + (g / 2) ) by A61, XREAL_1:6, XREAL_1:15;
then p1 in W1 by A63;
hence p in [:W1,W2:] by A55, A62, ZFMISC_1:def_2; ::_thesis: ( [:W1,W2:] is open & Dy .: [:W1,W2:] c= V )
( W1 is open & W2 is open ) by PSCOMP_1:21;
hence [:W1,W2:] is open by BORSUK_1:6; ::_thesis: Dy .: [:W1,W2:] c= V
let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in Dy .: [:W1,W2:] or b in V )
assume b in Dy .: [:W1,W2:] ; ::_thesis: b in V
then consider a being Point of [:(TOP-REAL 2),(TOP-REAL 2):] such that
A64: a in [:W1,W2:] and
A65: Dy . a = b by FUNCT_2:65;
consider a1, a2 being Point of (TOP-REAL 2) such that
A66: a = [a1,a2] and
A67: dy . a = (a1 `2) - (a2 `2) by A19;
a2 in W2 by A64, A66, ZFMISC_1:87;
then consider x2, y2 being Element of REAL such that
A68: a2 = |[x2,y2]| and
A69: (p2 `2) - (g / 2) < y2 and
A70: y2 < (p2 `2) + (g / 2) ;
A71: a2 `2 = y2 by A68, EUCLID:52;
(p2 `2) - y2 > (p2 `2) - ((p2 `2) + (g / 2)) by A70, XREAL_1:15;
then A72: (p2 `2) - y2 > - (g / 2) ;
((p2 `2) - (g / 2)) + (g / 2) < y2 + (g / 2) by A69, XREAL_1:6;
then (p2 `2) - y2 < (y2 + (g / 2)) - y2 by XREAL_1:9;
then A73: abs ((p2 `2) - y2) < g / 2 by A72, SEQ_2:1;
a1 in W1 by A64, A66, ZFMISC_1:87;
then consider x1, y1 being Element of REAL such that
A74: a1 = |[x1,y1]| and
A75: (p1 `2) - (g / 2) < y1 and
A76: y1 < (p1 `2) + (g / 2) ;
(p1 `2) - y1 > (p1 `2) - ((p1 `2) + (g / 2)) by A76, XREAL_1:15;
then A77: (p1 `2) - y1 > - (g / 2) ;
abs (((p1 `2) - y1) - ((p2 `2) - y2)) <= (abs ((p1 `2) - y1)) + (abs ((p2 `2) - y2)) by COMPLEX1:57;
then A78: abs (- (((p1 `2) - y1) - ((p2 `2) - y2))) <= (abs ((p1 `2) - y1)) + (abs ((p2 `2) - y2)) by COMPLEX1:52;
((p1 `2) - (g / 2)) + (g / 2) < y1 + (g / 2) by A75, XREAL_1:6;
then (p1 `2) - y1 < (y1 + (g / 2)) - y1 by XREAL_1:9;
then abs ((p1 `2) - y1) < g / 2 by A77, SEQ_2:1;
then (abs ((p1 `2) - y1)) + (abs ((p2 `2) - y2)) < (g / 2) + (g / 2) by A73, XREAL_1:8;
then A79: abs ((y1 - y2) - ((p1 `2) - (p2 `2))) < g by A78, XXREAL_0:2;
a1 `2 = y1 by A74, EUCLID:52;
then (a1 `2) - (a2 `2) in ].(((p1 `2) - (p2 `2)) - g),(((p1 `2) - (p2 `2)) + g).[ by A71, A79, RCOMP_1:1;
hence b in V by A58, A65, A67; ::_thesis: verum
end;
then Dy is continuous by JGRAPH_2:10;
then reconsider dy = dy as continuous RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] by JORDAN5A:27;
for p being Point of [:(TOP-REAL 2),(TOP-REAL 2):]
for V being Subset of R^1 st Dx . p in V & V is open holds
ex W being Subset of [:(TOP-REAL 2),(TOP-REAL 2):] st
( p in W & W is open & Dx .: W c= V )
proof
let p be Point of [:(TOP-REAL 2),(TOP-REAL 2):]; ::_thesis: for V being Subset of R^1 st Dx . p in V & V is open holds
ex W being Subset of [:(TOP-REAL 2),(TOP-REAL 2):] st
( p in W & W is open & Dx .: W c= V )
let V be Subset of R^1; ::_thesis: ( Dx . p in V & V is open implies ex W being Subset of [:(TOP-REAL 2),(TOP-REAL 2):] st
( p in W & W is open & Dx .: W c= V ) )
assume that
A80: Dx . p in V and
A81: V is open ; ::_thesis: ex W being Subset of [:(TOP-REAL 2),(TOP-REAL 2):] st
( p in W & W is open & Dx .: W c= V )
reconsider V1 = V as open Subset of REAL by A81, BORSUK_5:39, TOPMETR:17;
consider p1, p2 being Point of (TOP-REAL 2) such that
A82: p = [p1,p2] and
A83: dx . p = (p1 `1) - (p2 `1) by A25;
set r = (p1 `1) - (p2 `1);
consider g being real number such that
A84: 0 < g and
A85: ].(((p1 `1) - (p2 `1)) - g),(((p1 `1) - (p2 `1)) + g).[ c= V1 by A80, A83, RCOMP_1:19;
reconsider g = g as Element of REAL by XREAL_0:def_1;
set W2 = { |[x,y]| where x, y is Element of REAL : ( (p2 `1) - (g / 2) < x & x < (p2 `1) + (g / 2) ) } ;
A86: { |[x,y]| where x, y is Element of REAL : ( (p2 `1) - (g / 2) < x & x < (p2 `1) + (g / 2) ) } c= the carrier of (TOP-REAL 2)
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { |[x,y]| where x, y is Element of REAL : ( (p2 `1) - (g / 2) < x & x < (p2 `1) + (g / 2) ) } or a in the carrier of (TOP-REAL 2) )
assume a in { |[x,y]| where x, y is Element of REAL : ( (p2 `1) - (g / 2) < x & x < (p2 `1) + (g / 2) ) } ; ::_thesis: a in the carrier of (TOP-REAL 2)
then ex x, y being Element of REAL st
( a = |[x,y]| & (p2 `1) - (g / 2) < x & x < (p2 `1) + (g / 2) ) ;
hence a in the carrier of (TOP-REAL 2) ; ::_thesis: verum
end;
A87: p2 = |[(p2 `1),(p2 `2)]| by EUCLID:53;
reconsider W2 = { |[x,y]| where x, y is Element of REAL : ( (p2 `1) - (g / 2) < x & x < (p2 `1) + (g / 2) ) } as Subset of (TOP-REAL 2) by A86;
A88: 0 / 2 < g / 2 by A84, XREAL_1:74;
then ( (p2 `1) - (g / 2) < (p2 `1) - 0 & (p2 `1) + 0 < (p2 `1) + (g / 2) ) by XREAL_1:6, XREAL_1:15;
then A89: p2 in W2 by A87;
set W1 = { |[x,y]| where x, y is Element of REAL : ( (p1 `1) - (g / 2) < x & x < (p1 `1) + (g / 2) ) } ;
{ |[x,y]| where x, y is Element of REAL : ( (p1 `1) - (g / 2) < x & x < (p1 `1) + (g / 2) ) } c= the carrier of (TOP-REAL 2)
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { |[x,y]| where x, y is Element of REAL : ( (p1 `1) - (g / 2) < x & x < (p1 `1) + (g / 2) ) } or a in the carrier of (TOP-REAL 2) )
assume a in { |[x,y]| where x, y is Element of REAL : ( (p1 `1) - (g / 2) < x & x < (p1 `1) + (g / 2) ) } ; ::_thesis: a in the carrier of (TOP-REAL 2)
then ex x, y being Element of REAL st
( a = |[x,y]| & (p1 `1) - (g / 2) < x & x < (p1 `1) + (g / 2) ) ;
hence a in the carrier of (TOP-REAL 2) ; ::_thesis: verum
end;
then reconsider W1 = { |[x,y]| where x, y is Element of REAL : ( (p1 `1) - (g / 2) < x & x < (p1 `1) + (g / 2) ) } as Subset of (TOP-REAL 2) ;
take [:W1,W2:] ; ::_thesis: ( p in [:W1,W2:] & [:W1,W2:] is open & Dx .: [:W1,W2:] c= V )
A90: p1 = |[(p1 `1),(p1 `2)]| by EUCLID:53;
( (p1 `1) - (g / 2) < (p1 `1) - 0 & (p1 `1) + 0 < (p1 `1) + (g / 2) ) by A88, XREAL_1:6, XREAL_1:15;
then p1 in W1 by A90;
hence p in [:W1,W2:] by A82, A89, ZFMISC_1:def_2; ::_thesis: ( [:W1,W2:] is open & Dx .: [:W1,W2:] c= V )
( W1 is open & W2 is open ) by PSCOMP_1:19;
hence [:W1,W2:] is open by BORSUK_1:6; ::_thesis: Dx .: [:W1,W2:] c= V
let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in Dx .: [:W1,W2:] or b in V )
assume b in Dx .: [:W1,W2:] ; ::_thesis: b in V
then consider a being Point of [:(TOP-REAL 2),(TOP-REAL 2):] such that
A91: a in [:W1,W2:] and
A92: Dx . a = b by FUNCT_2:65;
consider a1, a2 being Point of (TOP-REAL 2) such that
A93: a = [a1,a2] and
A94: dx . a = (a1 `1) - (a2 `1) by A25;
a2 in W2 by A91, A93, ZFMISC_1:87;
then consider x2, y2 being Element of REAL such that
A95: a2 = |[x2,y2]| and
A96: (p2 `1) - (g / 2) < x2 and
A97: x2 < (p2 `1) + (g / 2) ;
A98: a2 `1 = x2 by A95, EUCLID:52;
(p2 `1) - x2 > (p2 `1) - ((p2 `1) + (g / 2)) by A97, XREAL_1:15;
then A99: (p2 `1) - x2 > - (g / 2) ;
((p2 `1) - (g / 2)) + (g / 2) < x2 + (g / 2) by A96, XREAL_1:6;
then (p2 `1) - x2 < (x2 + (g / 2)) - x2 by XREAL_1:9;
then A100: abs ((p2 `1) - x2) < g / 2 by A99, SEQ_2:1;
a1 in W1 by A91, A93, ZFMISC_1:87;
then consider x1, y1 being Element of REAL such that
A101: a1 = |[x1,y1]| and
A102: (p1 `1) - (g / 2) < x1 and
A103: x1 < (p1 `1) + (g / 2) ;
(p1 `1) - x1 > (p1 `1) - ((p1 `1) + (g / 2)) by A103, XREAL_1:15;
then A104: (p1 `1) - x1 > - (g / 2) ;
abs (((p1 `1) - x1) - ((p2 `1) - x2)) <= (abs ((p1 `1) - x1)) + (abs ((p2 `1) - x2)) by COMPLEX1:57;
then A105: abs (- (((p1 `1) - x1) - ((p2 `1) - x2))) <= (abs ((p1 `1) - x1)) + (abs ((p2 `1) - x2)) by COMPLEX1:52;
((p1 `1) - (g / 2)) + (g / 2) < x1 + (g / 2) by A102, XREAL_1:6;
then (p1 `1) - x1 < (x1 + (g / 2)) - x1 by XREAL_1:9;
then abs ((p1 `1) - x1) < g / 2 by A104, SEQ_2:1;
then (abs ((p1 `1) - x1)) + (abs ((p2 `1) - x2)) < (g / 2) + (g / 2) by A100, XREAL_1:8;
then A106: abs ((x1 - x2) - ((p1 `1) - (p2 `1))) < g by A105, XXREAL_0:2;
a1 `1 = x1 by A101, EUCLID:52;
then (a1 `1) - (a2 `1) in ].(((p1 `1) - (p2 `1)) - g),(((p1 `1) - (p2 `1)) + g).[ by A98, A106, RCOMP_1:1;
hence b in V by A85, A92, A94; ::_thesis: verum
end;
then Dx is continuous by JGRAPH_2:10;
then reconsider dx = dx as continuous RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] by JORDAN5A:27;
set Zdy = dy | OK;
set Zdx = dx | OK;
set m = ((dx | OK) (#) (dx | OK)) + ((dy | OK) (#) (dy | OK));
for p being Point of [:(TOP-REAL 2),(TOP-REAL 2):]
for V being Subset of R^1 st fY2 . p in V & V is open holds
ex W being Subset of [:(TOP-REAL 2),(TOP-REAL 2):] st
( p in W & W is open & fY2 .: W c= V )
proof
let p be Point of [:(TOP-REAL 2),(TOP-REAL 2):]; ::_thesis: for V being Subset of R^1 st fY2 . p in V & V is open holds
ex W being Subset of [:(TOP-REAL 2),(TOP-REAL 2):] st
( p in W & W is open & fY2 .: W c= V )
let V be Subset of R^1; ::_thesis: ( fY2 . p in V & V is open implies ex W being Subset of [:(TOP-REAL 2),(TOP-REAL 2):] st
( p in W & W is open & fY2 .: W c= V ) )
assume that
A107: fY2 . p in V and
A108: V is open ; ::_thesis: ex W being Subset of [:(TOP-REAL 2),(TOP-REAL 2):] st
( p in W & W is open & fY2 .: W c= V )
reconsider V1 = V as open Subset of REAL by A108, BORSUK_5:39, TOPMETR:17;
consider p1, p2 being Point of (TOP-REAL 2) such that
A109: p = [p1,p2] and
A110: fY2 . p = p2 `2 by A22;
consider g being real number such that
A111: 0 < g and
A112: ].((p2 `2) - g),((p2 `2) + g).[ c= V1 by A107, A110, RCOMP_1:19;
reconsider g = g as Element of REAL by XREAL_0:def_1;
set W1 = { |[x,y]| where x, y is Element of REAL : ( (p2 `2) - g < y & y < (p2 `2) + g ) } ;
{ |[x,y]| where x, y is Element of REAL : ( (p2 `2) - g < y & y < (p2 `2) + g ) } c= the carrier of (TOP-REAL 2)
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { |[x,y]| where x, y is Element of REAL : ( (p2 `2) - g < y & y < (p2 `2) + g ) } or a in the carrier of (TOP-REAL 2) )
assume a in { |[x,y]| where x, y is Element of REAL : ( (p2 `2) - g < y & y < (p2 `2) + g ) } ; ::_thesis: a in the carrier of (TOP-REAL 2)
then ex x, y being Element of REAL st
( a = |[x,y]| & (p2 `2) - g < y & y < (p2 `2) + g ) ;
hence a in the carrier of (TOP-REAL 2) ; ::_thesis: verum
end;
then reconsider W1 = { |[x,y]| where x, y is Element of REAL : ( (p2 `2) - g < y & y < (p2 `2) + g ) } as Subset of (TOP-REAL 2) ;
take [:([#] (TOP-REAL 2)),W1:] ; ::_thesis: ( p in [:([#] (TOP-REAL 2)),W1:] & [:([#] (TOP-REAL 2)),W1:] is open & fY2 .: [:([#] (TOP-REAL 2)),W1:] c= V )
A113: p2 = |[(p2 `1),(p2 `2)]| by EUCLID:53;
( (p2 `2) - g < (p2 `2) - 0 & (p2 `2) + 0 < (p2 `2) + g ) by A111, XREAL_1:6, XREAL_1:15;
then p2 in W1 by A113;
hence p in [:([#] (TOP-REAL 2)),W1:] by A109, ZFMISC_1:def_2; ::_thesis: ( [:([#] (TOP-REAL 2)),W1:] is open & fY2 .: [:([#] (TOP-REAL 2)),W1:] c= V )
W1 is open by PSCOMP_1:21;
hence [:([#] (TOP-REAL 2)),W1:] is open by BORSUK_1:6; ::_thesis: fY2 .: [:([#] (TOP-REAL 2)),W1:] c= V
let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in fY2 .: [:([#] (TOP-REAL 2)),W1:] or b in V )
assume b in fY2 .: [:([#] (TOP-REAL 2)),W1:] ; ::_thesis: b in V
then consider a being Point of [:(TOP-REAL 2),(TOP-REAL 2):] such that
A114: a in [:([#] (TOP-REAL 2)),W1:] and
A115: fY2 . a = b by FUNCT_2:65;
consider a1, a2 being Point of (TOP-REAL 2) such that
A116: a = [a1,a2] and
A117: fY2 . a = a2 `2 by A22;
a2 in W1 by A114, A116, ZFMISC_1:87;
then consider x1, y1 being Element of REAL such that
A118: a2 = |[x1,y1]| and
A119: (p2 `2) - g < y1 and
A120: y1 < (p2 `2) + g ;
(p2 `2) - y1 > (p2 `2) - ((p2 `2) + g) by A120, XREAL_1:15;
then A121: (p2 `2) - y1 > - g ;
((p2 `2) - g) + g < y1 + g by A119, XREAL_1:6;
then (p2 `2) - y1 < (y1 + g) - y1 by XREAL_1:9;
then abs ((p2 `2) - y1) < g by A121, SEQ_2:1;
then abs (- ((p2 `2) - y1)) < g by COMPLEX1:52;
then A122: abs (y1 - (p2 `2)) < g ;
a2 `2 = y1 by A118, EUCLID:52;
then a2 `2 in ].((p2 `2) - g),((p2 `2) + g).[ by A122, RCOMP_1:1;
hence b in V by A112, A115, A117; ::_thesis: verum
end;
then fY2 is continuous by JGRAPH_2:10;
then reconsider fy2 = fy2 as continuous RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] by JORDAN5A:27;
for p being Point of [:(TOP-REAL 2),(TOP-REAL 2):]
for V being Subset of R^1 st fX2 . p in V & V is open holds
ex W being Subset of [:(TOP-REAL 2),(TOP-REAL 2):] st
( p in W & W is open & fX2 .: W c= V )
proof
let p be Point of [:(TOP-REAL 2),(TOP-REAL 2):]; ::_thesis: for V being Subset of R^1 st fX2 . p in V & V is open holds
ex W being Subset of [:(TOP-REAL 2),(TOP-REAL 2):] st
( p in W & W is open & fX2 .: W c= V )
let V be Subset of R^1; ::_thesis: ( fX2 . p in V & V is open implies ex W being Subset of [:(TOP-REAL 2),(TOP-REAL 2):] st
( p in W & W is open & fX2 .: W c= V ) )
assume that
A123: fX2 . p in V and
A124: V is open ; ::_thesis: ex W being Subset of [:(TOP-REAL 2),(TOP-REAL 2):] st
( p in W & W is open & fX2 .: W c= V )
reconsider V1 = V as open Subset of REAL by A124, BORSUK_5:39, TOPMETR:17;
consider p1, p2 being Point of (TOP-REAL 2) such that
A125: p = [p1,p2] and
A126: fX2 . p = p2 `1 by A6;
consider g being real number such that
A127: 0 < g and
A128: ].((p2 `1) - g),((p2 `1) + g).[ c= V1 by A123, A126, RCOMP_1:19;
reconsider g = g as Element of REAL by XREAL_0:def_1;
set W1 = { |[x,y]| where x, y is Element of REAL : ( (p2 `1) - g < x & x < (p2 `1) + g ) } ;
{ |[x,y]| where x, y is Element of REAL : ( (p2 `1) - g < x & x < (p2 `1) + g ) } c= the carrier of (TOP-REAL 2)
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { |[x,y]| where x, y is Element of REAL : ( (p2 `1) - g < x & x < (p2 `1) + g ) } or a in the carrier of (TOP-REAL 2) )
assume a in { |[x,y]| where x, y is Element of REAL : ( (p2 `1) - g < x & x < (p2 `1) + g ) } ; ::_thesis: a in the carrier of (TOP-REAL 2)
then ex x, y being Element of REAL st
( a = |[x,y]| & (p2 `1) - g < x & x < (p2 `1) + g ) ;
hence a in the carrier of (TOP-REAL 2) ; ::_thesis: verum
end;
then reconsider W1 = { |[x,y]| where x, y is Element of REAL : ( (p2 `1) - g < x & x < (p2 `1) + g ) } as Subset of (TOP-REAL 2) ;
take [:([#] (TOP-REAL 2)),W1:] ; ::_thesis: ( p in [:([#] (TOP-REAL 2)),W1:] & [:([#] (TOP-REAL 2)),W1:] is open & fX2 .: [:([#] (TOP-REAL 2)),W1:] c= V )
A129: p2 = |[(p2 `1),(p2 `2)]| by EUCLID:53;
( (p2 `1) - g < (p2 `1) - 0 & (p2 `1) + 0 < (p2 `1) + g ) by A127, XREAL_1:6, XREAL_1:15;
then p2 in W1 by A129;
hence p in [:([#] (TOP-REAL 2)),W1:] by A125, ZFMISC_1:def_2; ::_thesis: ( [:([#] (TOP-REAL 2)),W1:] is open & fX2 .: [:([#] (TOP-REAL 2)),W1:] c= V )
W1 is open by PSCOMP_1:19;
hence [:([#] (TOP-REAL 2)),W1:] is open by BORSUK_1:6; ::_thesis: fX2 .: [:([#] (TOP-REAL 2)),W1:] c= V
let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in fX2 .: [:([#] (TOP-REAL 2)),W1:] or b in V )
assume b in fX2 .: [:([#] (TOP-REAL 2)),W1:] ; ::_thesis: b in V
then consider a being Point of [:(TOP-REAL 2),(TOP-REAL 2):] such that
A130: a in [:([#] (TOP-REAL 2)),W1:] and
A131: fX2 . a = b by FUNCT_2:65;
consider a1, a2 being Point of (TOP-REAL 2) such that
A132: a = [a1,a2] and
A133: fX2 . a = a2 `1 by A6;
a2 in W1 by A130, A132, ZFMISC_1:87;
then consider x1, y1 being Element of REAL such that
A134: a2 = |[x1,y1]| and
A135: (p2 `1) - g < x1 and
A136: x1 < (p2 `1) + g ;
(p2 `1) - x1 > (p2 `1) - ((p2 `1) + g) by A136, XREAL_1:15;
then A137: (p2 `1) - x1 > - g ;
((p2 `1) - g) + g < x1 + g by A135, XREAL_1:6;
then (p2 `1) - x1 < (x1 + g) - x1 by XREAL_1:9;
then abs ((p2 `1) - x1) < g by A137, SEQ_2:1;
then abs (- ((p2 `1) - x1)) < g by COMPLEX1:52;
then A138: abs (x1 - (p2 `1)) < g ;
a2 `1 = x1 by A134, EUCLID:52;
then a2 `1 in ].((p2 `1) - g),((p2 `1) + g).[ by A138, RCOMP_1:1;
hence b in V by A128, A131, A133; ::_thesis: verum
end;
then fX2 is continuous by JGRAPH_2:10;
then reconsider fx2 = fx2 as continuous RealMap of [:(TOP-REAL 2),(TOP-REAL 2):] by JORDAN5A:27;
set yy = (yo | OK) (#) (dy | OK);
set xx = (xo | OK) (#) (dx | OK);
set Zfy2 = fy2 | OK;
set Zfx2 = fx2 | OK;
set p1 = (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK))) (#) (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)));
A139: dom ((((xo | OK) (#) (xo | OK)) + ((yo | OK) (#) (yo | OK))) - (f1 | OK)) = the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK) by FUNCT_2:def_1;
A140: for y, z being Point of (Tdisk (o,r)) st y <> z holds
[y,z] in OK
proof
let y, z be Point of (Tdisk (o,r)); ::_thesis: ( y <> z implies [y,z] in OK )
A141: ( y is Point of (TOP-REAL 2) & z is Point of (TOP-REAL 2) ) by PRE_TOPC:25;
assume y <> z ; ::_thesis: [y,z] in OK
then [y,z] in DiffElems ((TOP-REAL 2),(TOP-REAL 2)) by A141;
hence [y,z] in OK by XBOOLE_0:def_4; ::_thesis: verum
end;
A142: now__::_thesis:_for_b_being_real_number_st_b_in_rng_((((xo_|_OK)_(#)_(xo_|_OK))_+_((yo_|_OK)_(#)_(yo_|_OK)))_-_(f1_|_OK))_holds_
0_>=_b
let b be real number ; ::_thesis: ( b in rng ((((xo | OK) (#) (xo | OK)) + ((yo | OK) (#) (yo | OK))) - (f1 | OK)) implies 0 >= b )
assume b in rng ((((xo | OK) (#) (xo | OK)) + ((yo | OK) (#) (yo | OK))) - (f1 | OK)) ; ::_thesis: 0 >= b
then consider a being set such that
A143: a in dom ((((xo | OK) (#) (xo | OK)) + ((yo | OK) (#) (yo | OK))) - (f1 | OK)) and
A144: ((((xo | OK) (#) (xo | OK)) + ((yo | OK) (#) (yo | OK))) - (f1 | OK)) . a = b by FUNCT_1:def_3;
a in DiffElems ((TOP-REAL 2),(TOP-REAL 2)) by A143, XBOOLE_0:def_4;
then consider y, z being Point of (TOP-REAL 2) such that
A145: a = [y,z] and
A146: y <> z ;
a in the carrier of [:(Tdisk (o,r)),(Tdisk (o,r)):] by A143, XBOOLE_0:def_4;
then consider a1, a2 being Point of (Tdisk (o,r)) such that
A147: a = [a1,a2] by BORSUK_1:10;
A148: a2 = z by A145, A147, XTUPLE_0:1;
A149: a1 = y by A145, A147, XTUPLE_0:1;
then A150: (f1 | OK) . [y,z] = f1 . [y,z] by A140, A146, A148, FUNCT_1:49;
set r3 = (z `1) - (o `1);
set r4 = (z `2) - (o `2);
consider x9, x10 being Point of (TOP-REAL 2) such that
A151: [y,z] = [x9,x10] and
A152: xo . [y,z] = (x10 `1) - (o `1) by A3;
A153: z = x10 by A151, XTUPLE_0:1;
the carrier of (Tdisk (o,r)) = cl_Ball (o,r) by Th3;
then |.(z - o).| <= r by A148, TOPREAL9:8;
then A154: |.(z - o).| ^2 <= r ^2 by SQUARE_1:15;
consider x11, x12 being Point of (TOP-REAL 2) such that
A155: [y,z] = [x11,x12] and
A156: yo . [y,z] = (x12 `2) - (o `2) by A9;
A157: z = x12 by A155, XTUPLE_0:1;
A158: ( (xo | OK) . [y,z] = xo . [y,z] & (yo | OK) . [y,z] = yo . [y,z] ) by A140, A146, A149, A148, FUNCT_1:49;
|.(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 A159: ((((z `1) - (o `1)) ^2) + (((z `2) - (o `2)) ^2)) - (r ^2) <= (r ^2) - (r ^2) by A154, XREAL_1:9;
A160: [y,z] is Element of [#] ([:(TOP-REAL 2),(TOP-REAL 2):] | OK) by A143, A145, PRE_TOPC:def_5;
((((xo | OK) (#) (xo | OK)) + ((yo | OK) (#) (yo | OK))) - (f1 | OK)) . [y,z] = ((((xo | OK) (#) (xo | OK)) + ((yo | OK) (#) (yo | OK))) . [y,z]) - ((f1 | OK) . [y,z]) by A143, A145, VALUED_1:13
.= ((((xo | OK) (#) (xo | OK)) + ((yo | OK) (#) (yo | OK))) . [y,z]) - (r ^2) by A150, FUNCOP_1:7
.= ((((xo | OK) (#) (xo | OK)) . [y,z]) + (((yo | OK) (#) (yo | OK)) . [y,z])) - (r ^2) by A160, VALUED_1:1
.= ((((xo | OK) . [y,z]) * ((xo | OK) . [y,z])) + (((yo | OK) (#) (yo | OK)) . [y,z])) - (r ^2) by VALUED_1:5
.= ((((z `1) - (o `1)) ^2) + (((z `2) - (o `2)) ^2)) - (r ^2) by A158, A152, A153, A156, A157, VALUED_1:5 ;
hence 0 >= b by A144, A145, A159; ::_thesis: verum
end;
now__::_thesis:_for_b_being_real_number_st_b_in_rng_(((dx_|_OK)_(#)_(dx_|_OK))_+_((dy_|_OK)_(#)_(dy_|_OK)))_holds_
0_<_b
let b be real number ; ::_thesis: ( b in rng (((dx | OK) (#) (dx | OK)) + ((dy | OK) (#) (dy | OK))) implies 0 < b )
assume b in rng (((dx | OK) (#) (dx | OK)) + ((dy | OK) (#) (dy | OK))) ; ::_thesis: 0 < b
then consider a being set such that
A161: a in dom (((dx | OK) (#) (dx | OK)) + ((dy | OK) (#) (dy | OK))) and
A162: (((dx | OK) (#) (dx | OK)) + ((dy | OK) (#) (dy | OK))) . a = b by FUNCT_1:def_3;
a in DiffElems ((TOP-REAL 2),(TOP-REAL 2)) by A161, XBOOLE_0:def_4;
then consider y, z being Point of (TOP-REAL 2) such that
A163: a = [y,z] and
A164: y <> z ;
a in the carrier of [:(Tdisk (o,r)),(Tdisk (o,r)):] by A161, XBOOLE_0:def_4;
then consider a1, a2 being Point of (Tdisk (o,r)) such that
A165: a = [a1,a2] by BORSUK_1:10;
set r1 = (y `1) - (z `1);
set r2 = (y `2) - (z `2);
A166: now__::_thesis:_not_(((y_`1)_-_(z_`1))_^2)_+_(((y_`2)_-_(z_`2))_^2)_=_0
assume (((y `1) - (z `1)) ^2) + (((y `2) - (z `2)) ^2) = 0 ; ::_thesis: contradiction
then ( (y `1) - (z `1) = 0 & (y `2) - (z `2) = 0 ) by COMPLEX1:1;
hence contradiction by A164, TOPREAL3:6; ::_thesis: verum
end;
consider x3, x4 being Point of (TOP-REAL 2) such that
A167: [y,z] = [x3,x4] and
A168: dx . [y,z] = (x3 `1) - (x4 `1) by A25;
A169: ( y = x3 & z = x4 ) by A167, XTUPLE_0:1;
( a1 = y & a2 = z ) by A163, A165, XTUPLE_0:1;
then A170: ( (dx | OK) . [y,z] = dx . [y,z] & (dy | OK) . [y,z] = dy . [y,z] ) by A140, A164, FUNCT_1:49;
consider x5, x6 being Point of (TOP-REAL 2) such that
A171: [y,z] = [x5,x6] and
A172: dy . [y,z] = (x5 `2) - (x6 `2) by A19;
A173: ( y = x5 & z = x6 ) by A171, XTUPLE_0:1;
A174: [y,z] is Element of [#] ([:(TOP-REAL 2),(TOP-REAL 2):] | OK) by A161, A163, PRE_TOPC:def_5;
(((dx | OK) (#) (dx | OK)) + ((dy | OK) (#) (dy | OK))) . [y,z] = (((dx | OK) (#) (dx | OK)) . [y,z]) + (((dy | OK) (#) (dy | OK)) . [y,z]) by A174, VALUED_1:1
.= (((dx | OK) . [y,z]) * ((dx | OK) . [y,z])) + (((dy | OK) (#) (dy | OK)) . [y,z]) by VALUED_1:5
.= (((y `1) - (z `1)) ^2) + (((y `2) - (z `2)) ^2) by A168, A169, A172, A173, A170, VALUED_1:5 ;
hence 0 < b by A162, A163, A166; ::_thesis: verum
end;
then reconsider m = ((dx | OK) (#) (dx | OK)) + ((dy | OK) (#) (dy | OK)) as positive-yielding continuous RealMap of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK) by PARTFUN3:def_1;
reconsider p2 = (((xo | OK) (#) (xo | OK)) + ((yo | OK) (#) (yo | OK))) - (f1 | OK) as nonpositive-yielding continuous RealMap of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK) by A142, PARTFUN3:def_3;
set pp = ((((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK))) (#) (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) - (m (#) p2);
set k = ((- (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) + (sqrt (((((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK))) (#) (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) - (m (#) p2)))) / m;
set x3 = (fx2 | OK) + ((((- (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) + (sqrt (((((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK))) (#) (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) - (m (#) p2)))) / m) (#) (dx | OK));
set y3 = (fy2 | OK) + ((((- (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) + (sqrt (((((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK))) (#) (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) - (m (#) p2)))) / m) (#) (dy | OK));
reconsider X3 = (fx2 | OK) + ((((- (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) + (sqrt (((((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK))) (#) (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) - (m (#) p2)))) / m) (#) (dx | OK)), Y3 = (fy2 | OK) + ((((- (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) + (sqrt (((((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK))) (#) (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) - (m (#) p2)))) / m) (#) (dy | OK)) as Function of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK),R^1 by TOPMETR:17;
set F = <:X3,Y3:>;
A175: for x being Point of (Tdisk (o,r)) holds (BR-map f) . x = (R2Homeomorphism * <:X3,Y3:>) . [x,(f . x)]
proof
A176: dom (((((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK))) (#) (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) - (m (#) p2)) = the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK) by FUNCT_2:def_1;
let x be Point of (Tdisk (o,r)); ::_thesis: (BR-map f) . x = (R2Homeomorphism * <:X3,Y3:>) . [x,(f . x)]
A177: ( dom X3 = the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK) & dom Y3 = the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK) ) by FUNCT_2:def_1;
A178: not x is_a_fixpoint_of f by A16, ABIAN:def_5;
then A179: x <> f . x by ABIAN:def_4;
consider y, z being Point of (TOP-REAL 2) such that
A180: ( y = x & z = f . x ) and
A181: HC (x,f) = HC (z,y,o,r) by A178, Def4;
A182: (f1 | OK) . [y,z] = f1 . [y,z] by A140, A180, A179, FUNCT_1:49;
A183: ( (xo | OK) . [y,z] = xo . [y,z] & (yo | OK) . [y,z] = yo . [y,z] ) by A140, A180, A179, FUNCT_1:49;
set r1 = (y `1) - (z `1);
set r2 = (y `2) - (z `2);
set r3 = (z `1) - (o `1);
set r4 = (z `2) - (o `2);
consider x9, x10 being Point of (TOP-REAL 2) such that
A184: [y,z] = [x9,x10] and
A185: xo . [y,z] = (x10 `1) - (o `1) by A3;
A186: z = x10 by A184, XTUPLE_0:1;
consider x11, x12 being Point of (TOP-REAL 2) such that
A187: [y,z] = [x11,x12] and
A188: yo . [y,z] = (x12 `2) - (o `2) by A9;
A189: z = x12 by A187, XTUPLE_0:1;
[x,(f . x)] in DiffElems ((TOP-REAL 2),(TOP-REAL 2)) by A180, A179;
then A190: [y,z] in OK by A180, XBOOLE_0:def_4;
then A191: p2 . [y,z] = ((((xo | OK) (#) (xo | OK)) + ((yo | OK) (#) (yo | OK))) . [y,z]) - ((f1 | OK) . [y,z]) by A52, A139, VALUED_1:13
.= ((((xo | OK) (#) (xo | OK)) + ((yo | OK) (#) (yo | OK))) . [y,z]) - (r ^2) by A182, FUNCOP_1:7
.= ((((xo | OK) (#) (xo | OK)) . [y,z]) + (((yo | OK) (#) (yo | OK)) . [y,z])) - (r ^2) by A52, A190, VALUED_1:1
.= ((((xo | OK) . [y,z]) * ((xo | OK) . [y,z])) + (((yo | OK) (#) (yo | OK)) . [y,z])) - (r ^2) by VALUED_1:5
.= ((((z `1) - (o `1)) ^2) + (((z `2) - (o `2)) ^2)) - (r ^2) by A185, A186, A188, A189, A183, VALUED_1:5 ;
A192: (dx | OK) . [y,z] = dx . [y,z] by A140, A180, A179, FUNCT_1:49;
consider x7, x8 being Point of (TOP-REAL 2) such that
A193: [y,z] = [x7,x8] and
A194: fy2 . [y,z] = x8 `2 by A22;
A195: z = x8 by A193, XTUPLE_0:1;
consider x1, x2 being Point of (TOP-REAL 2) such that
A196: [y,z] = [x1,x2] and
A197: fx2 . [y,z] = x2 `1 by A6;
A198: z = x2 by A196, XTUPLE_0:1;
consider x3, x4 being Point of (TOP-REAL 2) such that
A199: [y,z] = [x3,x4] and
A200: dx . [y,z] = (x3 `1) - (x4 `1) by A25;
A201: ( y = x3 & z = x4 ) by A199, XTUPLE_0:1;
set l = ((- ((((z `1) - (o `1)) * ((y `1) - (z `1))) + (((z `2) - (o `2)) * ((y `2) - (z `2))))) + (sqrt ((((((z `1) - (o `1)) * ((y `1) - (z `1))) + (((z `2) - (o `2)) * ((y `2) - (z `2)))) ^2) - (((((y `1) - (z `1)) ^2) + (((y `2) - (z `2)) ^2)) * (((((z `1) - (o `1)) ^2) + (((z `2) - (o `2)) ^2)) - (r ^2)))))) / ((((y `1) - (z `1)) ^2) + (((y `2) - (z `2)) ^2));
A202: ( ((xo | OK) (#) (dx | OK)) . [y,z] = ((xo | OK) . [y,z]) * ((dx | OK) . [y,z]) & ((yo | OK) (#) (dy | OK)) . [y,z] = ((yo | OK) . [y,z]) * ((dy | OK) . [y,z]) ) by VALUED_1:5;
A203: (dy | OK) . [y,z] = dy . [y,z] by A140, A180, A179, FUNCT_1:49;
consider x5, x6 being Point of (TOP-REAL 2) such that
A204: [y,z] = [x5,x6] and
A205: dy . [y,z] = (x5 `2) - (x6 `2) by A19;
A206: ( y = x5 & z = x6 ) by A204, XTUPLE_0:1;
A207: m . [y,z] = (((dx | OK) (#) (dx | OK)) . [y,z]) + (((dy | OK) (#) (dy | OK)) . [y,z]) by A52, A190, VALUED_1:1
.= (((dx | OK) . [y,z]) * ((dx | OK) . [y,z])) + (((dy | OK) (#) (dy | OK)) . [y,z]) by VALUED_1:5
.= (((y `1) - (z `1)) ^2) + (((y `2) - (z `2)) ^2) by A200, A201, A205, A206, A192, A203, VALUED_1:5 ;
A208: (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK))) . [y,z] = (((xo | OK) (#) (dx | OK)) . [y,z]) + (((yo | OK) (#) (dy | OK)) . [y,z]) by A52, A190, VALUED_1:1;
then A209: ((((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK))) (#) (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) . [y,z] = ((((z `1) - (o `1)) * ((y `1) - (z `1))) + (((z `2) - (o `2)) * ((y `2) - (z `2)))) ^2 by A200, A201, A205, A206, A185, A186, A188, A189, A192, A203, A183, A202, VALUED_1:5;
dom (sqrt (((((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK))) (#) (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) - (m (#) p2))) = the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK) by FUNCT_2:def_1;
then A210: (sqrt (((((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK))) (#) (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) - (m (#) p2))) . [y,z] = sqrt ((((((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK))) (#) (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) - (m (#) p2)) . [y,z]) by A52, A190, PARTFUN3:def_5
.= sqrt ((((((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK))) (#) (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) . [y,z]) - ((m (#) p2) . [y,z])) by A52, A190, A176, VALUED_1:13
.= sqrt ((((((z `1) - (o `1)) * ((y `1) - (z `1))) + (((z `2) - (o `2)) * ((y `2) - (z `2)))) ^2) - (((((y `1) - (z `1)) ^2) + (((y `2) - (z `2)) ^2)) * (((((z `1) - (o `1)) ^2) + (((z `2) - (o `2)) ^2)) - (r ^2)))) by A207, A209, A191, VALUED_1:5 ;
dom (((- (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) + (sqrt (((((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK))) (#) (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) - (m (#) p2)))) / m) = the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK) by FUNCT_2:def_1;
then A211: (((- (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) + (sqrt (((((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK))) (#) (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) - (m (#) p2)))) / m) . [y,z] = (((- (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) + (sqrt (((((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK))) (#) (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) - (m (#) p2)))) . [y,z]) * ((m . [y,z]) ") by A52, A190, RFUNCT_1:def_1
.= (((- (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) + (sqrt (((((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK))) (#) (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) - (m (#) p2)))) . [y,z]) / (m . [y,z]) by XCMPLX_0:def_9
.= (((- (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) . [y,z]) + ((sqrt (((((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK))) (#) (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) - (m (#) p2))) . [y,z])) / ((((y `1) - (z `1)) ^2) + (((y `2) - (z `2)) ^2)) by A52, A190, A207, VALUED_1:1
.= ((- ((((z `1) - (o `1)) * ((y `1) - (z `1))) + (((z `2) - (o `2)) * ((y `2) - (z `2))))) + (sqrt ((((((z `1) - (o `1)) * ((y `1) - (z `1))) + (((z `2) - (o `2)) * ((y `2) - (z `2)))) ^2) - (((((y `1) - (z `1)) ^2) + (((y `2) - (z `2)) ^2)) * (((((z `1) - (o `1)) ^2) + (((z `2) - (o `2)) ^2)) - (r ^2)))))) / ((((y `1) - (z `1)) ^2) + (((y `2) - (z `2)) ^2)) by A200, A201, A205, A206, A185, A186, A188, A189, A192, A203, A183, A202, A208, A210, VALUED_1:8 ;
A212: Y3 . [y,z] = ((fy2 | OK) . [y,z]) + (((((- (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) + (sqrt (((((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK))) (#) (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) - (m (#) p2)))) / m) (#) (dy | OK)) . [y,z]) by A52, A190, VALUED_1:1
.= (z `2) + (((((- (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) + (sqrt (((((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK))) (#) (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) - (m (#) p2)))) / m) (#) (dy | OK)) . [y,z]) by A140, A180, A179, A194, A195, FUNCT_1:49
.= (z `2) + ((((- ((((z `1) - (o `1)) * ((y `1) - (z `1))) + (((z `2) - (o `2)) * ((y `2) - (z `2))))) + (sqrt ((((((z `1) - (o `1)) * ((y `1) - (z `1))) + (((z `2) - (o `2)) * ((y `2) - (z `2)))) ^2) - (((((y `1) - (z `1)) ^2) + (((y `2) - (z `2)) ^2)) * (((((z `1) - (o `1)) ^2) + (((z `2) - (o `2)) ^2)) - (r ^2)))))) / ((((y `1) - (z `1)) ^2) + (((y `2) - (z `2)) ^2))) * ((y `2) - (z `2))) by A205, A206, A203, A211, VALUED_1:5 ;
A213: X3 . [y,z] = ((fx2 | OK) . [y,z]) + (((((- (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) + (sqrt (((((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK))) (#) (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) - (m (#) p2)))) / m) (#) (dx | OK)) . [y,z]) by A52, A190, VALUED_1:1
.= (z `1) + (((((- (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) + (sqrt (((((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK))) (#) (((xo | OK) (#) (dx | OK)) + ((yo | OK) (#) (dy | OK)))) - (m (#) p2)))) / m) (#) (dx | OK)) . [y,z]) by A140, A180, A179, A197, A198, FUNCT_1:49
.= (z `1) + ((((- ((((z `1) - (o `1)) * ((y `1) - (z `1))) + (((z `2) - (o `2)) * ((y `2) - (z `2))))) + (sqrt ((((((z `1) - (o `1)) * ((y `1) - (z `1))) + (((z `2) - (o `2)) * ((y `2) - (z `2)))) ^2) - (((((y `1) - (z `1)) ^2) + (((y `2) - (z `2)) ^2)) * (((((z `1) - (o `1)) ^2) + (((z `2) - (o `2)) ^2)) - (r ^2)))))) / ((((y `1) - (z `1)) ^2) + (((y `2) - (z `2)) ^2))) * ((y `1) - (z `1))) by A200, A201, A192, A211, VALUED_1:5 ;
thus (BR-map f) . x = HC (x,f) by Def5
.= |[((z `1) + ((((- ((((z `1) - (o `1)) * ((y `1) - (z `1))) + (((z `2) - (o `2)) * ((y `2) - (z `2))))) + (sqrt ((((((z `1) - (o `1)) * ((y `1) - (z `1))) + (((z `2) - (o `2)) * ((y `2) - (z `2)))) ^2) - (((((y `1) - (z `1)) ^2) + (((y `2) - (z `2)) ^2)) * (((((z `1) - (o `1)) ^2) + (((z `2) - (o `2)) ^2)) - (r ^2)))))) / ((((y `1) - (z `1)) ^2) + (((y `2) - (z `2)) ^2))) * ((y `1) - (z `1)))),((z `2) + ((((- ((((z `1) - (o `1)) * ((y `1) - (z `1))) + (((z `2) - (o `2)) * ((y `2) - (z `2))))) + (sqrt ((((((z `1) - (o `1)) * ((y `1) - (z `1))) + (((z `2) - (o `2)) * ((y `2) - (z `2)))) ^2) - (((((y `1) - (z `1)) ^2) + (((y `2) - (z `2)) ^2)) * (((((z `1) - (o `1)) ^2) + (((z `2) - (o `2)) ^2)) - (r ^2)))))) / ((((y `1) - (z `1)) ^2) + (((y `2) - (z `2)) ^2))) * ((y `2) - (z `2))))]| by A180, A181, A179, Th8
.= R2Homeomorphism . [(X3 . [y,z]),(Y3 . [y,z])] by A213, A212, TOPREALA:def_2
.= R2Homeomorphism . (<:X3,Y3:> . [y,z]) by A52, A190, A177, FUNCT_3:49
.= (R2Homeomorphism * <:X3,Y3:>) . [x,(f . x)] by A52, A180, A190, FUNCT_2:15 ; ::_thesis: verum
end;
( X3 is continuous & Y3 is continuous ) by JORDAN5A:27;
then reconsider F = <:X3,Y3:> as continuous Function of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK),[:R^1,R^1:] by YELLOW12:41;
for p being Point of (Tdisk (o,r))
for V being Subset of (Tcircle (o,r)) st (BR-map f) . p in V & V is open holds
ex W being Subset of (Tdisk (o,r)) st
( p in W & W is open & (BR-map f) .: W c= V )
proof
let p be Point of (Tdisk (o,r)); ::_thesis: for V being Subset of (Tcircle (o,r)) st (BR-map f) . p in V & V is open holds
ex W being Subset of (Tdisk (o,r)) st
( p in W & W is open & (BR-map f) .: W c= V )
let V be Subset of (Tcircle (o,r)); ::_thesis: ( (BR-map f) . p in V & V is open implies ex W being Subset of (Tdisk (o,r)) st
( p in W & W is open & (BR-map f) .: W c= V ) )
assume that
A214: (BR-map f) . p in V and
A215: V is open ; ::_thesis: ex W being Subset of (Tdisk (o,r)) st
( p in W & W is open & (BR-map f) .: W c= V )
consider V1 being Subset of (TOP-REAL 2) such that
A216: V1 is open and
A217: V1 /\ ([#] (Tcircle (o,r))) = V by A215, TOPS_2:24;
reconsider p1 = p, fp = f . p as Point of (TOP-REAL 2) by PRE_TOPC:25;
A218: rng R2Homeomorphism = [#] (TOP-REAL 2) by TOPREALA:34, TOPS_2:def_5;
R2Homeomorphism " is being_homeomorphism by TOPREALA:34, TOPS_2:56;
then A219: (R2Homeomorphism ") .: V1 is open by A216, TOPGRP_1:25;
not p is_a_fixpoint_of f by A16, ABIAN:def_5;
then p <> f . p by ABIAN:def_4;
then [p1,fp] in DiffElems ((TOP-REAL 2),(TOP-REAL 2)) ;
then A220: [p,(f . p)] in OK by XBOOLE_0:def_4;
(BR-map f) . p = (R2Homeomorphism * F) . [p,(f . p)] by A175;
then (R2Homeomorphism * F) . [p1,fp] in V1 by A214, A217, XBOOLE_0:def_4;
then A221: (R2Homeomorphism ") . ((R2Homeomorphism * F) . [p1,fp]) in (R2Homeomorphism ") .: V1 by FUNCT_2:35;
A222: R2Homeomorphism is one-to-one by TOPREALA:34, TOPS_2:def_5;
A223: dom R2Homeomorphism = the carrier of [:R^1,R^1:] by FUNCT_2:def_1;
then A224: rng F c= dom R2Homeomorphism ;
then ( dom F = the carrier of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK) & dom (R2Homeomorphism * F) = dom F ) by FUNCT_2:def_1, RELAT_1:27;
then A225: ((R2Homeomorphism ") * (R2Homeomorphism * F)) . [p1,fp] in (R2Homeomorphism ") .: V1 by A52, A220, A221, FUNCT_1:13;
A226: for x being set st x in dom F holds
((id (dom R2Homeomorphism)) * F) . x = F . x
proof
let x be set ; ::_thesis: ( x in dom F implies ((id (dom R2Homeomorphism)) * F) . x = F . x )
assume A227: x in dom F ; ::_thesis: ((id (dom R2Homeomorphism)) * F) . x = F . x
A228: F . x in rng F by A227, FUNCT_1:def_3;
thus ((id (dom R2Homeomorphism)) * F) . x = (id (dom R2Homeomorphism)) . (F . x) by A227, FUNCT_1:13
.= F . x by A223, A228, FUNCT_1:18 ; ::_thesis: verum
end;
dom (id (dom R2Homeomorphism)) = dom R2Homeomorphism ;
then dom ((id (dom R2Homeomorphism)) * F) = dom F by A224, RELAT_1:27;
then A229: (id (dom R2Homeomorphism)) * F = F by A226, FUNCT_1:2;
(R2Homeomorphism ") * (R2Homeomorphism * F) = ((R2Homeomorphism ") * R2Homeomorphism) * F by RELAT_1:36
.= (id (dom R2Homeomorphism)) * F by A218, A222, TOPS_2:52 ;
then consider W being Subset of ([:(TOP-REAL 2),(TOP-REAL 2):] | OK) such that
A230: [p1,fp] in W and
A231: W is open and
A232: F .: W c= (R2Homeomorphism ") .: V1 by A52, A220, A219, A229, A225, JGRAPH_2:10;
consider WW being Subset of [:(TOP-REAL 2),(TOP-REAL 2):] such that
A233: WW is open and
A234: WW /\ ([#] ([:(TOP-REAL 2),(TOP-REAL 2):] | OK)) = W by A231, TOPS_2:24;
consider SF being Subset-Family of [:(TOP-REAL 2),(TOP-REAL 2):] such that
A235: WW = union SF and
A236: 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 A233, BORSUK_1:5;
[p1,fp] in WW by A230, A234, XBOOLE_0:def_4;
then consider Z being set such that
A237: [p1,fp] in Z and
A238: Z in SF by A235, TARSKI:def_4;
set ZZ = Z /\ ([#] ([:(TOP-REAL 2),(TOP-REAL 2):] | OK));
Z c= WW by A235, A238, ZFMISC_1:74;
then Z /\ ([#] ([:(TOP-REAL 2),(TOP-REAL 2):] | OK)) c= WW /\ ([#] ([:(TOP-REAL 2),(TOP-REAL 2):] | OK)) by XBOOLE_1:27;
then A239: F .: (Z /\ ([#] ([:(TOP-REAL 2),(TOP-REAL 2):] | OK))) c= F .: W by A234, RELAT_1:123;
consider X1, Y1 being Subset of (TOP-REAL 2) such that
A240: Z = [:X1,Y1:] and
A241: ( X1 is open & Y1 is open ) by A236, A238;
reconsider XX = X1 /\ ([#] (Tdisk (o,r))), YY = Y1 /\ ([#] (Tdisk (o,r))) as open Subset of (Tdisk (o,r)) by A241, TOPS_2:24;
fp in Y1 by A237, A240, ZFMISC_1:87;
then fp in YY by XBOOLE_0:def_4;
then consider M being Subset of (Tdisk (o,r)) such that
A242: p in M and
A243: M is open and
A244: f .: M c= YY by JGRAPH_2:10;
take W1 = XX /\ M; ::_thesis: ( p in W1 & W1 is open & (BR-map f) .: W1 c= V )
p in X1 by A237, A240, ZFMISC_1:87;
then p in XX by XBOOLE_0:def_4;
hence p in W1 by A242, XBOOLE_0:def_4; ::_thesis: ( W1 is open & (BR-map f) .: W1 c= V )
thus W1 is open by A243; ::_thesis: (BR-map f) .: W1 c= V
let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in (BR-map f) .: W1 or b in V )
assume b in (BR-map f) .: W1 ; ::_thesis: b in V
then consider a being Point of (Tdisk (o,r)) such that
A245: a in W1 and
A246: b = (BR-map f) . a by FUNCT_2:65;
reconsider a1 = a, fa = f . a as Point of (TOP-REAL 2) by PRE_TOPC:25;
a in M by A245, XBOOLE_0:def_4;
then fa in f .: M by FUNCT_2:35;
then A247: f . a in Y1 by A244, XBOOLE_0:def_4;
not a is_a_fixpoint_of f by A16, ABIAN:def_5;
then a <> f . a by ABIAN:def_4;
then [a1,fa] in DiffElems ((TOP-REAL 2),(TOP-REAL 2)) ;
then A248: [a,(f . a)] in OK by XBOOLE_0:def_4;
a in XX by A245, XBOOLE_0:def_4;
then a in X1 by XBOOLE_0:def_4;
then [a,fa] in Z by A240, A247, ZFMISC_1:def_2;
then [a,fa] in Z /\ ([#] ([:(TOP-REAL 2),(TOP-REAL 2):] | OK)) by A52, A248, XBOOLE_0:def_4;
then F . [a1,fa] in F .: (Z /\ ([#] ([:(TOP-REAL 2),(TOP-REAL 2):] | OK))) by FUNCT_2:35;
then F . [a1,fa] in F .: W by A239;
then R2Homeomorphism . (F . [a1,fa]) in R2Homeomorphism .: ((R2Homeomorphism ") .: V1) by A232, FUNCT_2:35;
then A249: (R2Homeomorphism * F) . [a1,fa] in R2Homeomorphism .: ((R2Homeomorphism ") .: V1) by A52, A248, FUNCT_2:15;
R2Homeomorphism is onto by A218, FUNCT_2:def_3;
then ( R2Homeomorphism " = R2Homeomorphism " & dom (R2Homeomorphism ") = [#] (TOP-REAL 2) ) by A218, A222, TOPS_2:49, TOPS_2:def_4;
then (R2Homeomorphism * F) . [a1,fa] in V1 by A222, A249, PARTFUN3:1;
then (BR-map f) . a in V1 by A175;
hence b in V by A217, A246, XBOOLE_0:def_4; ::_thesis: verum
end;
hence BR-map f is continuous by JGRAPH_2:10; ::_thesis: verum
end;
theorem Th14: :: BROUWER:14
for r being non negative real number
for o being Point of (TOP-REAL 2)
for f being continuous Function of (Tdisk (o,r)),(Tdisk (o,r)) holds f is with_fixpoint
proof
let r be non negative real number ; ::_thesis: for o being Point of (TOP-REAL 2)
for f being continuous Function of (Tdisk (o,r)),(Tdisk (o,r)) holds f is with_fixpoint
let o be Point of (TOP-REAL 2); ::_thesis: for f being continuous Function of (Tdisk (o,r)),(Tdisk (o,r)) holds f is with_fixpoint
let f be continuous Function of (Tdisk (o,r)),(Tdisk (o,r)); ::_thesis: f is with_fixpoint
A1: the carrier of (Tcircle (o,r)) = Sphere (o,r) by TOPREALB:9;
A2: the carrier of (Tdisk (o,r)) = cl_Ball (o,r) by Th3;
percases ( r is positive or not r is positive ) ;
suppose r is positive ; ::_thesis: f is with_fixpoint
then reconsider r = r as positive real number ;
Sphere (o,r) c= cl_Ball (o,r) by TOPREAL9:17;
then reconsider Y = Tcircle (o,r) as non empty SubSpace of Tdisk (o,r) by A1, A2, TSEP_1:4;
reconsider g = BR-map f as Function of (Tdisk (o,r)),Y ;
A3: not Y is_a_retract_of Tdisk (o,r) by Th10;
assume A4: f is without_fixpoints ; ::_thesis: contradiction
A5: g is being_a_retraction
proof
let W be Point of (Tdisk (o,r)); :: according to BORSUK_1:def_16 ::_thesis: ( not W in the carrier of Y or g . W = W )
assume A6: W in the carrier of Y ; ::_thesis: g . W = W
not W is_a_fixpoint_of f by A4, ABIAN:def_5;
hence g . W = W by A6, Th11; ::_thesis: verum
end;
g is continuous by A4, Th13;
hence contradiction by A3, A5, BORSUK_1:def_17; ::_thesis: verum
end;
suppose not r is positive ; ::_thesis: f is with_fixpoint
then reconsider r = r as non positive non negative real number ;
take o ; :: according to ABIAN:def_5 ::_thesis: o is_a_fixpoint_of f
A7: cl_Ball (o,r) = {o} by Th2;
dom f = the carrier of (Tdisk (o,r)) by FUNCT_2:def_1;
hence o in dom f by A2, A7, TARSKI:def_1; :: according to ABIAN:def_3 ::_thesis: o = f . o
then f . o in rng f by FUNCT_1:def_3;
hence o = f . o by A2, A7, TARSKI:def_1; ::_thesis: verum
end;
end;
end;
theorem :: BROUWER:15
for r being non negative real number
for o being Point of (TOP-REAL 2)
for f being continuous Function of (Tdisk (o,r)),(Tdisk (o,r)) ex x being Point of (Tdisk (o,r)) st f . x = x
proof
let r be non negative real number ; ::_thesis: for o being Point of (TOP-REAL 2)
for f being continuous Function of (Tdisk (o,r)),(Tdisk (o,r)) ex x being Point of (Tdisk (o,r)) st f . x = x
let o be Point of (TOP-REAL 2); ::_thesis: for f being continuous Function of (Tdisk (o,r)),(Tdisk (o,r)) ex x being Point of (Tdisk (o,r)) st f . x = x
let f be continuous Function of (Tdisk (o,r)),(Tdisk (o,r)); ::_thesis: ex x being Point of (Tdisk (o,r)) st f . x = x
f is with_fixpoint by Th14;
then consider x being set such that
A1: x is_a_fixpoint_of f by ABIAN:def_5;
take x ; ::_thesis: ( x is Point of (Tdisk (o,r)) & f . x = x )
x in dom f by A1, ABIAN:def_3;
hence x is Point of (Tdisk (o,r)) ; ::_thesis: f . x = x
thus f . x = x by A1, ABIAN:def_3; ::_thesis: verum
end;