reconsider h2 = proj2 as Function of (TOP-REAL 2),R^1 by TOPMETR:17;
let P be non empty compact Subset of (TOP-REAL 2); ( P = { q where q is Point of (TOP-REAL 2) : |.q.| = 1 } implies Upper_Arc P = { p where p is Point of (TOP-REAL 2) : ( p in P & p `2 >= 0 ) } )
set P4 = Lower_Arc P;
set P1 = Upper_Arc P;
set P2 = Lower_Arc P;
set Q = Vertical_Line 0;
set p8 = First_Point ((Upper_Arc P),(W-min P),(E-max P),(Vertical_Line 0));
set pj = Last_Point ((Lower_Arc P),(E-max P),(W-min P),(Vertical_Line 0));
A1:
LSeg (|[0,(- 1)]|,|[0,1]|) c= Vertical_Line 0
proof
let x be
object ;
TARSKI:def 3 ( not x in LSeg (|[0,(- 1)]|,|[0,1]|) or x in Vertical_Line 0 )
assume
x in LSeg (
|[0,(- 1)]|,
|[0,1]|)
;
x in Vertical_Line 0
then consider l being
Real such that A2:
x = ((1 - l) * |[0,(- 1)]|) + (l * |[0,1]|)
and
0 <= l
and
l <= 1
;
(((1 - l) * |[0,(- 1)]|) + (l * |[0,1]|)) `1 =
(((1 - l) * |[0,(- 1)]|) `1) + ((l * |[0,1]|) `1)
by TOPREAL3:2
.=
((1 - l) * (|[0,(- 1)]| `1)) + ((l * |[0,1]|) `1)
by TOPREAL3:4
.=
((1 - l) * (|[0,(- 1)]| `1)) + (l * (|[0,1]| `1))
by TOPREAL3:4
.=
((1 - l) * 0) + (l * (|[0,1]| `1))
by EUCLID:52
.=
((1 - l) * 0) + (l * 0)
by EUCLID:52
.=
0
;
hence
x in Vertical_Line 0
by A2;
verum
end;
reconsider R = Upper_Arc P as non empty Subset of (TOP-REAL 2) ;
assume A3:
P = { q where q is Point of (TOP-REAL 2) : |.q.| = 1 }
; Upper_Arc P = { p where p is Point of (TOP-REAL 2) : ( p in P & p `2 >= 0 ) }
then A4:
P is being_simple_closed_curve
by JGRAPH_3:26;
then A5:
Upper_Arc P is_an_arc_of W-min P, E-max P
by JORDAN6:def 8;
then consider f being Function of I[01],((TOP-REAL 2) | R) such that
A6:
f is being_homeomorphism
and
A7:
f . 0 = W-min P
and
A8:
f . 1 = E-max P
by TOPREAL1:def 1;
A9:
( dom f = the carrier of I[01] & dom h2 = the carrier of (TOP-REAL 2) )
by FUNCT_2:def 1;
A10:
ex P2 being non empty Subset of (TOP-REAL 2) st
( P2 is_an_arc_of E-max P, W-min P & (Upper_Arc P) /\ P2 = {(W-min P),(E-max P)} & (Upper_Arc P) \/ P2 = P & (First_Point ((Upper_Arc P),(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point (P2,(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 )
by A4, JORDAN6:def 8;
then A11:
Upper_Arc P c= P
by XBOOLE_1:7;
A12: rng f =
[#] ((TOP-REAL 2) | R)
by A6, TOPS_2:def 5
.=
R
by PRE_TOPC:def 5
;
A13:
( S-bound P = - 1 & N-bound P = 1 )
by A3, Th28;
A14:
Vertical_Line 0 is closed
by JORDAN6:30;
A15:
for p being Point of (TOP-REAL 2) holds h2 . p = proj2 . p
;
A16:
( W-bound P = - 1 & E-bound P = 1 )
by A3, Th28;
then A17:
Upper_Arc P meets Vertical_Line 0
by A4, A13, A1, JORDAN6:69, XBOOLE_1:64;
A18:
Lower_Arc P meets Vertical_Line 0
by A4, A16, A13, A1, JORDAN6:70, XBOOLE_1:64;
A19:
(First_Point ((Upper_Arc P),(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2 > (Last_Point ((Lower_Arc P),(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2)))) `2
by A4, JORDAN6:def 9;
Upper_Arc P is closed
by A5, JORDAN6:11;
then
(Upper_Arc P) /\ (Vertical_Line 0) is closed
by A14, TOPS_1:8;
then A20:
First_Point ((Upper_Arc P),(W-min P),(E-max P),(Vertical_Line 0)) in (Upper_Arc P) /\ (Vertical_Line 0)
by A5, A17, JORDAN5C:def 1;
then
First_Point ((Upper_Arc P),(W-min P),(E-max P),(Vertical_Line 0)) in Upper_Arc P
by XBOOLE_0:def 4;
then consider x8 being object such that
A21:
x8 in dom f
and
A22:
First_Point ((Upper_Arc P),(W-min P),(E-max P),(Vertical_Line 0)) = f . x8
by A12, FUNCT_1:def 3;
dom f = [.0,1.]
by BORSUK_1:40, FUNCT_2:def 1;
then
x8 in { r where r is Real : ( 0 <= r & r <= 1 ) }
by A21, RCOMP_1:def 1;
then consider r8 being Real such that
A23:
x8 = r8
and
A24:
0 <= r8
and
A25:
r8 <= 1
;
A26:
Vertical_Line 0 is closed
by JORDAN6:30;
(Upper_Arc P) /\ (Vertical_Line 0) c= {|[0,(- 1)]|,|[0,1]|}
proof
let x be
object ;
TARSKI:def 3 ( not x in (Upper_Arc P) /\ (Vertical_Line 0) or x in {|[0,(- 1)]|,|[0,1]|} )
assume A27:
x in (Upper_Arc P) /\ (Vertical_Line 0)
;
x in {|[0,(- 1)]|,|[0,1]|}
then
x in Upper_Arc P
by XBOOLE_0:def 4;
then
x in P
by A10, XBOOLE_0:def 3;
then consider q being
Point of
(TOP-REAL 2) such that A28:
q = x
and A29:
|.q.| = 1
by A3;
x in Vertical_Line 0
by A27, XBOOLE_0:def 4;
then A30:
ex
p being
Point of
(TOP-REAL 2) st
(
p = x &
p `1 = 0 )
;
then
(0 ^2) + ((q `2) ^2) = 1
^2
by A28, A29, JGRAPH_3:1;
then
(
q `2 = 1 or
q `2 = - 1 )
by SQUARE_1:41;
then
(
x = |[0,(- 1)]| or
x = |[0,1]| )
by A30, A28, EUCLID:53;
hence
x in {|[0,(- 1)]|,|[0,1]|}
by TARSKI:def 2;
verum
end;
then
( First_Point ((Upper_Arc P),(W-min P),(E-max P),(Vertical_Line 0)) = |[0,(- 1)]| or First_Point ((Upper_Arc P),(W-min P),(E-max P),(Vertical_Line 0)) = |[0,1]| )
by A20, TARSKI:def 2;
then A31:
( (First_Point ((Upper_Arc P),(W-min P),(E-max P),(Vertical_Line 0))) `2 = - 1 or (First_Point ((Upper_Arc P),(W-min P),(E-max P),(Vertical_Line 0))) `2 = 1 )
by EUCLID:52;
A33:
rng (h2 * f) c= the carrier of R^1
;
A34:
the carrier of ((TOP-REAL 2) | R) = R
by PRE_TOPC:8;
then
rng f c= the carrier of (TOP-REAL 2)
by XBOOLE_1:1;
then
dom (h2 * f) = the carrier of I[01]
by A9, RELAT_1:27;
then reconsider g0 = h2 * f as Function of I[01],R^1 by A33, FUNCT_2:2;
A35:
f is one-to-one
by A6, TOPS_2:def 5;
A36:
f is continuous
by A6, TOPS_2:def 5;
A37:
( ex p being Point of (TOP-REAL 2) ex t being Real st
( 0 < t & t < 1 & f . t = p & p `2 > 0 ) implies for q being Point of (TOP-REAL 2) st q in Upper_Arc P holds
q `2 >= 0 )
proof
given p being
Point of
(TOP-REAL 2),
t being
Real such that A38:
0 < t
and A39:
t < 1
and A40:
f . t = p
and A41:
p `2 > 0
;
for q being Point of (TOP-REAL 2) st q in Upper_Arc P holds
q `2 >= 0
now for q being Point of (TOP-REAL 2) holds
( not q in Upper_Arc P or not q `2 < 0 )assume
ex
q being
Point of
(TOP-REAL 2) st
(
q in Upper_Arc P &
q `2 < 0 )
;
contradictionthen consider q being
Point of
(TOP-REAL 2) such that A42:
q in Upper_Arc P
and A43:
q `2 < 0
;
rng f =
[#] ((TOP-REAL 2) | R)
by A6, TOPS_2:def 5
.=
R
by PRE_TOPC:def 5
;
then consider x being
object such that A44:
x in dom f
and A45:
q = f . x
by A42, FUNCT_1:def 3;
A46:
dom f = [.0,1.]
by BORSUK_1:40, FUNCT_2:def 1;
then A47:
x in { r where r is Real : ( 0 <= r & r <= 1 ) }
by A44, RCOMP_1:def 1;
t in { v where v is Real : ( 0 <= v & v <= 1 ) }
by A38, A39;
then A48:
t in [.0,1.]
by RCOMP_1:def 1;
then A49:
(h2 * f) . t =
h2 . p
by A40, A46, FUNCT_1:13
.=
p `2
by PSCOMP_1:def 6
;
consider r being
Real such that A50:
x = r
and A51:
0 <= r
and A52:
r <= 1
by A47;
A53:
(h2 * f) . r =
h2 . q
by A44, A45, A50, FUNCT_1:13
.=
q `2
by PSCOMP_1:def 6
;
now ( ( r < t & contradiction ) or ( t < r & contradiction ) or ( t = r & contradiction ) )per cases
( r < t or t < r or t = r )
by XXREAL_0:1;
case A54:
r < t
;
contradictionthen reconsider B =
[.r,t.] as non
empty Subset of
I[01] by A44, A50, A48, BORSUK_1:40, XXREAL_1:1, XXREAL_2:def 12;
reconsider B0 =
B as
Subset of
I[01] ;
reconsider g =
g0 | B0 as
Function of
(I[01] | B0),
R^1 by PRE_TOPC:9;
A55:
(q `2) * (p `2) < 0
by A41, A43, XREAL_1:132;
t in { r4 where r4 is Real : ( r <= r4 & r4 <= t ) }
by A54;
then
t in B
by RCOMP_1:def 1;
then A56:
p `2 = g . t
by A49, FUNCT_1:49;
r in { r4 where r4 is Real : ( r <= r4 & r4 <= t ) }
by A54;
then
r in B
by RCOMP_1:def 1;
then A57:
q `2 = g . r
by A53, FUNCT_1:49;
g0 is
continuous
by A36, A15, Th7, Th32;
then A58:
g is
continuous
by TOPMETR:7;
Closed-Interval-TSpace (
r,
t)
= I[01] | B
by A39, A51, A54, TOPMETR:20, TOPMETR:23;
then consider r1 being
Real such that A59:
g . r1 = 0
and A60:
r < r1
and A61:
r1 < t
by A54, A58, A55, A57, A56, TOPREAL5:8;
r1 in { r4 where r4 is Real : ( r <= r4 & r4 <= t ) }
by A60, A61;
then A62:
r1 in B
by RCOMP_1:def 1;
r1 < 1
by A39, A61, XXREAL_0:2;
then
r1 in { r2 where r2 is Real : ( 0 <= r2 & r2 <= 1 ) }
by A51, A60;
then A63:
r1 in dom f
by A46, RCOMP_1:def 1;
then
f . r1 in rng f
by FUNCT_1:def 3;
then
f . r1 in R
by A34;
then
f . r1 in P
by A11;
then consider q3 being
Point of
(TOP-REAL 2) such that A64:
q3 = f . r1
and A65:
|.q3.| = 1
by A3;
A66:
q3 `2 =
h2 . (f . r1)
by A64, PSCOMP_1:def 6
.=
g0 . r1
by A63, FUNCT_1:13
.=
0
by A59, A62, FUNCT_1:49
;
then A67: 1
^2 =
((q3 `1) ^2) + (0 ^2)
by A65, JGRAPH_3:1
.=
(q3 `1) ^2
;
now ( ( q3 `1 = 1 & contradiction ) or ( q3 `1 = - 1 & contradiction ) )per cases
( q3 `1 = 1 or q3 `1 = - 1 )
by A67, SQUARE_1:41;
case A68:
q3 `1 = 1
;
contradictionA69:
1
in dom f
by A46, XXREAL_1:1;
q3 =
|[1,0]|
by A66, A68, EUCLID:53
.=
E-max P
by A3, Th30
;
hence
contradiction
by A8, A35, A39, A61, A63, A64, A69, FUNCT_1:def 4;
verum end; case A70:
q3 `1 = - 1
;
contradictionA71:
0 in dom f
by A46, XXREAL_1:1;
q3 =
|[(- 1),0]|
by A66, A70, EUCLID:53
.=
W-min P
by A3, Th29
;
hence
contradiction
by A7, A35, A51, A60, A63, A64, A71, FUNCT_1:def 4;
verum end; hence
contradiction
;
verum end; case A72:
t < r
;
contradictionthen reconsider B =
[.t,r.] as non
empty Subset of
I[01] by A44, A50, A48, BORSUK_1:40, XXREAL_1:1, XXREAL_2:def 12;
reconsider B0 =
B as
Subset of
I[01] ;
reconsider g =
g0 | B0 as
Function of
(I[01] | B0),
R^1 by PRE_TOPC:9;
A73:
(q `2) * (p `2) < 0
by A41, A43, XREAL_1:132;
t in { r4 where r4 is Real : ( t <= r4 & r4 <= r ) }
by A72;
then
t in B
by RCOMP_1:def 1;
then A74:
p `2 = g . t
by A49, FUNCT_1:49;
r in { r4 where r4 is Real : ( t <= r4 & r4 <= r ) }
by A72;
then
r in B
by RCOMP_1:def 1;
then A75:
q `2 = g . r
by A53, FUNCT_1:49;
g0 is
continuous
by A36, A15, Th7, Th32;
then A76:
g is
continuous
by TOPMETR:7;
Closed-Interval-TSpace (
t,
r)
= I[01] | B
by A38, A52, A72, TOPMETR:20, TOPMETR:23;
then consider r1 being
Real such that A77:
g . r1 = 0
and A78:
t < r1
and A79:
r1 < r
by A72, A76, A73, A75, A74, TOPREAL5:8;
r1 in { r4 where r4 is Real : ( t <= r4 & r4 <= r ) }
by A78, A79;
then A80:
r1 in B
by RCOMP_1:def 1;
r1 < 1
by A52, A79, XXREAL_0:2;
then
r1 in { r2 where r2 is Real : ( 0 <= r2 & r2 <= 1 ) }
by A38, A78;
then A81:
r1 in dom f
by A46, RCOMP_1:def 1;
then
f . r1 in rng f
by FUNCT_1:def 3;
then
f . r1 in R
by A34;
then
f . r1 in P
by A11;
then consider q3 being
Point of
(TOP-REAL 2) such that A82:
q3 = f . r1
and A83:
|.q3.| = 1
by A3;
A84:
q3 `2 =
h2 . (f . r1)
by A82, PSCOMP_1:def 6
.=
(h2 * f) . r1
by A81, FUNCT_1:13
.=
0
by A77, A80, FUNCT_1:49
;
then A85: 1
^2 =
((q3 `1) ^2) + (0 ^2)
by A83, JGRAPH_3:1
.=
(q3 `1) ^2
;
now ( ( q3 `1 = 1 & contradiction ) or ( q3 `1 = - 1 & contradiction ) )per cases
( q3 `1 = 1 or q3 `1 = - 1 )
by A85, SQUARE_1:41;
case A86:
q3 `1 = 1
;
contradictionA87:
1
in dom f
by A46, XXREAL_1:1;
q3 =
|[1,0]|
by A84, A86, EUCLID:53
.=
E-max P
by A3, Th30
;
hence
contradiction
by A8, A35, A52, A79, A81, A82, A87, FUNCT_1:def 4;
verum end; case A88:
q3 `1 = - 1
;
contradictionA89:
0 in dom f
by A46, XXREAL_1:1;
q3 =
|[(- 1),0]|
by A84, A88, EUCLID:53
.=
W-min P
by A3, Th29
;
hence
contradiction
by A7, A35, A38, A78, A81, A82, A89, FUNCT_1:def 4;
verum end; hence
contradiction
;
verum end; case
t = r
;
contradictionend; hence
contradiction
;
verum end;
hence
for
q being
Point of
(TOP-REAL 2) st
q in Upper_Arc P holds
q `2 >= 0
;
verum
end;
reconsider R = Lower_Arc P as non empty Subset of (TOP-REAL 2) ;
A90:
Lower_Arc P is_an_arc_of E-max P, W-min P
by A4, JORDAN6:def 9;
then consider f2 being Function of I[01],((TOP-REAL 2) | R) such that
A91:
f2 is being_homeomorphism
and
A92:
f2 . 0 = E-max P
and
A93:
f2 . 1 = W-min P
by TOPREAL1:def 1;
A94:
( dom f2 = the carrier of I[01] & dom h2 = the carrier of (TOP-REAL 2) )
by FUNCT_2:def 1;
A95:
rng (h2 * f2) c= the carrier of R^1
;
A96:
the carrier of ((TOP-REAL 2) | R) = R
by PRE_TOPC:8;
then
rng f2 c= the carrier of (TOP-REAL 2)
by XBOOLE_1:1;
then
dom (h2 * f2) = the carrier of I[01]
by A94, RELAT_1:27;
then reconsider g1 = h2 * f2 as Function of I[01],R^1 by A95, FUNCT_2:2;
A97:
f2 is one-to-one
by A91, TOPS_2:def 5;
A98:
(Upper_Arc P) \/ (Lower_Arc P) = P
by A4, JORDAN6:def 9;
then A99:
Lower_Arc P c= P
by XBOOLE_1:7;
A100:
(Lower_Arc P) /\ (Vertical_Line 0) c= {|[0,(- 1)]|,|[0,1]|}
proof
let x be
object ;
TARSKI:def 3 ( not x in (Lower_Arc P) /\ (Vertical_Line 0) or x in {|[0,(- 1)]|,|[0,1]|} )
assume A101:
x in (Lower_Arc P) /\ (Vertical_Line 0)
;
x in {|[0,(- 1)]|,|[0,1]|}
then
x in Lower_Arc P
by XBOOLE_0:def 4;
then
x in P
by A98, XBOOLE_0:def 3;
then consider q being
Point of
(TOP-REAL 2) such that A102:
q = x
and A103:
|.q.| = 1
by A3;
x in Vertical_Line 0
by A101, XBOOLE_0:def 4;
then A104:
ex
p being
Point of
(TOP-REAL 2) st
(
p = x &
p `1 = 0 )
;
then
(0 ^2) + ((q `2) ^2) = 1
^2
by A102, A103, JGRAPH_3:1;
then
(
q `2 = 1 or
q `2 = - 1 )
by SQUARE_1:41;
then
(
x = |[0,(- 1)]| or
x = |[0,1]| )
by A104, A102, EUCLID:53;
hence
x in {|[0,(- 1)]|,|[0,1]|}
by TARSKI:def 2;
verum
end;
A105:
for p being Point of (TOP-REAL 2) holds h2 . p = proj2 . p
;
A106:
f2 is continuous
by A91, TOPS_2:def 5;
A107:
( ex p being Point of (TOP-REAL 2) ex t being Real st
( 0 < t & t < 1 & f2 . t = p & p `2 > 0 ) implies for q being Point of (TOP-REAL 2) st q in Lower_Arc P holds
q `2 >= 0 )
proof
given p being
Point of
(TOP-REAL 2),
t being
Real such that A108:
0 < t
and A109:
t < 1
and A110:
f2 . t = p
and A111:
p `2 > 0
;
for q being Point of (TOP-REAL 2) st q in Lower_Arc P holds
q `2 >= 0
now for q being Point of (TOP-REAL 2) holds
( not q in Lower_Arc P or not q `2 < 0 )assume
ex
q being
Point of
(TOP-REAL 2) st
(
q in Lower_Arc P &
q `2 < 0 )
;
contradictionthen consider q being
Point of
(TOP-REAL 2) such that A112:
q in Lower_Arc P
and A113:
q `2 < 0
;
rng f2 =
[#] ((TOP-REAL 2) | R)
by A91, TOPS_2:def 5
.=
R
by PRE_TOPC:def 5
;
then consider x being
object such that A114:
x in dom f2
and A115:
q = f2 . x
by A112, FUNCT_1:def 3;
A116:
dom f2 = [.0,1.]
by BORSUK_1:40, FUNCT_2:def 1;
then A117:
x in { r where r is Real : ( 0 <= r & r <= 1 ) }
by A114, RCOMP_1:def 1;
t in { v where v is Real : ( 0 <= v & v <= 1 ) }
by A108, A109;
then A118:
t in [.0,1.]
by RCOMP_1:def 1;
then A119:
(h2 * f2) . t =
h2 . p
by A110, A116, FUNCT_1:13
.=
p `2
by PSCOMP_1:def 6
;
consider r being
Real such that A120:
x = r
and A121:
0 <= r
and A122:
r <= 1
by A117;
A123:
(h2 * f2) . r =
h2 . q
by A114, A115, A120, FUNCT_1:13
.=
q `2
by PSCOMP_1:def 6
;
now ( ( r < t & contradiction ) or ( t < r & contradiction ) or ( t = r & contradiction ) )per cases
( r < t or t < r or t = r )
by XXREAL_0:1;
case A124:
r < t
;
contradictionthen reconsider B =
[.r,t.] as non
empty Subset of
I[01] by A114, A120, A118, BORSUK_1:40, XXREAL_1:1, XXREAL_2:def 12;
reconsider B0 =
B as
Subset of
I[01] ;
reconsider g =
g1 | B0 as
Function of
(I[01] | B0),
R^1 by PRE_TOPC:9;
A125:
(q `2) * (p `2) < 0
by A111, A113, XREAL_1:132;
t in { r4 where r4 is Real : ( r <= r4 & r4 <= t ) }
by A124;
then
t in B
by RCOMP_1:def 1;
then A126:
p `2 = g . t
by A119, FUNCT_1:49;
r in { r4 where r4 is Real : ( r <= r4 & r4 <= t ) }
by A124;
then
r in B
by RCOMP_1:def 1;
then A127:
q `2 = g . r
by A123, FUNCT_1:49;
g1 is
continuous
by A106, A105, Th7, Th32;
then A128:
g is
continuous
by TOPMETR:7;
Closed-Interval-TSpace (
r,
t)
= I[01] | B
by A109, A121, A124, TOPMETR:20, TOPMETR:23;
then consider r1 being
Real such that A129:
g . r1 = 0
and A130:
r < r1
and A131:
r1 < t
by A124, A128, A125, A127, A126, TOPREAL5:8;
r1 in { r4 where r4 is Real : ( r <= r4 & r4 <= t ) }
by A130, A131;
then A132:
r1 in B
by RCOMP_1:def 1;
r1 < 1
by A109, A131, XXREAL_0:2;
then
r1 in { r2 where r2 is Real : ( 0 <= r2 & r2 <= 1 ) }
by A121, A130;
then A133:
r1 in dom f2
by A116, RCOMP_1:def 1;
then
f2 . r1 in rng f2
by FUNCT_1:def 3;
then
f2 . r1 in R
by A96;
then
f2 . r1 in P
by A99;
then consider q3 being
Point of
(TOP-REAL 2) such that A134:
q3 = f2 . r1
and A135:
|.q3.| = 1
by A3;
A136:
q3 `2 =
h2 . (f2 . r1)
by A134, PSCOMP_1:def 6
.=
(h2 * f2) . r1
by A133, FUNCT_1:13
.=
0
by A129, A132, FUNCT_1:49
;
then A137: 1
^2 =
((q3 `1) ^2) + (0 ^2)
by A135, JGRAPH_3:1
.=
(q3 `1) ^2
;
now ( ( q3 `1 = 1 & contradiction ) or ( q3 `1 = - 1 & contradiction ) )per cases
( q3 `1 = 1 or q3 `1 = - 1 )
by A137, SQUARE_1:41;
case A138:
q3 `1 = 1
;
contradictionA139:
0 in dom f2
by A116, XXREAL_1:1;
q3 =
|[1,0]|
by A136, A138, EUCLID:53
.=
E-max P
by A3, Th30
;
hence
contradiction
by A92, A97, A121, A130, A133, A134, A139, FUNCT_1:def 4;
verum end; case A140:
q3 `1 = - 1
;
contradictionA141:
1
in dom f2
by A116, XXREAL_1:1;
q3 =
|[(- 1),0]|
by A136, A140, EUCLID:53
.=
W-min P
by A3, Th29
;
hence
contradiction
by A93, A97, A109, A131, A133, A134, A141, FUNCT_1:def 4;
verum end; hence
contradiction
;
verum end; case A142:
t < r
;
contradictionthen reconsider B =
[.t,r.] as non
empty Subset of
I[01] by A114, A120, A118, BORSUK_1:40, XXREAL_1:1, XXREAL_2:def 12;
reconsider B0 =
B as
Subset of
I[01] ;
reconsider g =
g1 | B0 as
Function of
(I[01] | B0),
R^1 by PRE_TOPC:9;
A143:
(q `2) * (p `2) < 0
by A111, A113, XREAL_1:132;
t in { r4 where r4 is Real : ( t <= r4 & r4 <= r ) }
by A142;
then
t in B
by RCOMP_1:def 1;
then A144:
p `2 = g . t
by A119, FUNCT_1:49;
r in { r4 where r4 is Real : ( t <= r4 & r4 <= r ) }
by A142;
then
r in B
by RCOMP_1:def 1;
then A145:
q `2 = g . r
by A123, FUNCT_1:49;
g1 is
continuous
by A106, A105, Th7, Th32;
then A146:
g is
continuous
by TOPMETR:7;
Closed-Interval-TSpace (
t,
r)
= I[01] | B
by A108, A122, A142, TOPMETR:20, TOPMETR:23;
then consider r1 being
Real such that A147:
g . r1 = 0
and A148:
t < r1
and A149:
r1 < r
by A142, A146, A143, A145, A144, TOPREAL5:8;
r1 in { r4 where r4 is Real : ( t <= r4 & r4 <= r ) }
by A148, A149;
then A150:
r1 in B
by RCOMP_1:def 1;
r1 < 1
by A122, A149, XXREAL_0:2;
then
r1 in { r2 where r2 is Real : ( 0 <= r2 & r2 <= 1 ) }
by A108, A148;
then A151:
r1 in dom f2
by A116, RCOMP_1:def 1;
then
f2 . r1 in rng f2
by FUNCT_1:def 3;
then
f2 . r1 in R
by A96;
then
f2 . r1 in P
by A99;
then consider q3 being
Point of
(TOP-REAL 2) such that A152:
q3 = f2 . r1
and A153:
|.q3.| = 1
by A3;
A154:
q3 `2 =
h2 . (f2 . r1)
by A152, PSCOMP_1:def 6
.=
g1 . r1
by A151, FUNCT_1:13
.=
0
by A147, A150, FUNCT_1:49
;
then A155: 1
^2 =
((q3 `1) ^2) + (0 ^2)
by A153, JGRAPH_3:1
.=
(q3 `1) ^2
;
now ( ( q3 `1 = 1 & contradiction ) or ( q3 `1 = - 1 & contradiction ) )per cases
( q3 `1 = 1 or q3 `1 = - 1 )
by A155, SQUARE_1:41;
case A156:
q3 `1 = 1
;
contradictionA157:
0 in dom f2
by A116, XXREAL_1:1;
q3 =
|[1,0]|
by A154, A156, EUCLID:53
.=
E-max P
by A3, Th30
;
hence
contradiction
by A92, A97, A108, A148, A151, A152, A157, FUNCT_1:def 4;
verum end; case A158:
q3 `1 = - 1
;
contradictionA159:
1
in dom f2
by A116, XXREAL_1:1;
q3 =
|[(- 1),0]|
by A154, A158, EUCLID:53
.=
W-min P
by A3, Th29
;
hence
contradiction
by A93, A97, A122, A149, A151, A152, A159, FUNCT_1:def 4;
verum end; hence
contradiction
;
verum end; case
t = r
;
contradictionend; hence
contradiction
;
verum end;
hence
for
q being
Point of
(TOP-REAL 2) st
q in Lower_Arc P holds
q `2 >= 0
;
verum
end;
W-min P in {(W-min P),(E-max P)}
by TARSKI:def 2;
then A160:
W-min P in Upper_Arc P
by A10, XBOOLE_0:def 4;
A161:
( W-bound P = - 1 & E-bound P = 1 )
by A3, Th28;
then A162:
1 > r8
by A25, XXREAL_0:1;
Lower_Arc P is closed
by A90, JORDAN6:11;
then
(Lower_Arc P) /\ (Vertical_Line 0) is closed
by A26, TOPS_1:8;
then
Last_Point ((Lower_Arc P),(E-max P),(W-min P),(Vertical_Line 0)) in (Lower_Arc P) /\ (Vertical_Line 0)
by A90, A18, JORDAN5C:def 2;
then A163:
( Last_Point ((Lower_Arc P),(E-max P),(W-min P),(Vertical_Line 0)) = |[0,(- 1)]| or Last_Point ((Lower_Arc P),(E-max P),(W-min P),(Vertical_Line 0)) = |[0,1]| )
by A100, TARSKI:def 2;
E-max P in {(W-min P),(E-max P)}
by TARSKI:def 2;
then A164:
E-max P in Upper_Arc P
by A10, XBOOLE_0:def 4;
A165:
{ p where p is Point of (TOP-REAL 2) : ( p in P & p `2 >= 0 ) } c= Upper_Arc P
proof
let x be
object ;
TARSKI:def 3 ( not x in { p where p is Point of (TOP-REAL 2) : ( p in P & p `2 >= 0 ) } or x in Upper_Arc P )
assume
x in { p where p is Point of (TOP-REAL 2) : ( p in P & p `2 >= 0 ) }
;
x in Upper_Arc P
then consider p being
Point of
(TOP-REAL 2) such that A166:
p = x
and A167:
p in P
and A168:
p `2 >= 0
;
now ( ( p `2 = 0 & x in Upper_Arc P ) or ( p `2 > 0 & x in Upper_Arc P ) )per cases
( p `2 = 0 or p `2 > 0 )
by A168;
case A169:
p `2 = 0
;
x in Upper_Arc P
ex
p8 being
Point of
(TOP-REAL 2) st
(
p8 = p &
|.p8.| = 1 )
by A3, A167;
then 1 =
sqrt (((p `1) ^2) + ((p `2) ^2))
by JGRAPH_3:1
.=
|.(p `1).|
by A169, COMPLEX1:72
;
then
(
p = |[(p `1),(p `2)]| &
(p `1) ^2 = 1
^2 )
by COMPLEX1:75, EUCLID:53;
then
(
p = |[1,0]| or
p = |[(- 1),0]| )
by A169, SQUARE_1:41;
hence
x in Upper_Arc P
by A3, A164, A160, A166, Th29, Th30;
verum case A170:
p `2 > 0
;
x in Upper_Arc Pnow x in Upper_Arc Passume
not
x in Upper_Arc P
;
contradictionthen A171:
x in Lower_Arc P
by A98, A166, A167, XBOOLE_0:def 3;
rng f2 =
[#] ((TOP-REAL 2) | R)
by A91, TOPS_2:def 5
.=
R
by PRE_TOPC:def 5
;
then consider x2 being
object such that A172:
x2 in dom f2
and A173:
p = f2 . x2
by A166, A171, FUNCT_1:def 3;
dom f2 = [.0,1.]
by BORSUK_1:40, FUNCT_2:def 1;
then
x2 in { r where r is Real : ( 0 <= r & r <= 1 ) }
by A172, RCOMP_1:def 1;
then consider t2 being
Real such that A174:
x2 = t2
and A175:
0 <= t2
and A176:
t2 <= 1
;
A177:
|[0,(- 1)]| `2 = - 1
by EUCLID:52;
then A178:
t2 < 1
by A176, XXREAL_0:1;
A179:
now not t2 = 0 end;
|[0,(- 1)]| `1 = 0
by EUCLID:52;
then |.|[0,(- 1)]|.| =
sqrt ((0 ^2) + ((- 1) ^2))
by A177, JGRAPH_3:1
.=
1
;
then A180:
|[0,(- 1)]| in { q where q is Point of (TOP-REAL 2) : |.q.| = 1 }
;
now ( ( |[0,(- 1)]| in Upper_Arc P & contradiction ) or ( |[0,(- 1)]| in Lower_Arc P & contradiction ) )per cases
( |[0,(- 1)]| in Upper_Arc P or |[0,(- 1)]| in Lower_Arc P )
by A3, A98, A180, XBOOLE_0:def 3;
case
|[0,(- 1)]| in Upper_Arc P
;
contradictionhence
contradiction
by A19, A161, A31, A163, A22, A23, A24, A32, A162, A37, A177, EUCLID:52;
verum end; hence
contradiction
;
verum end; hence
x in Upper_Arc P
;
verum
hence
x in Upper_Arc P
;
verum
end;
Upper_Arc P c= { p where p is Point of (TOP-REAL 2) : ( p in P & p `2 >= 0 ) }
proof
let x2 be
object ;
TARSKI:def 3 ( not x2 in Upper_Arc P or x2 in { p where p is Point of (TOP-REAL 2) : ( p in P & p `2 >= 0 ) } )
assume A181:
x2 in Upper_Arc P
;
x2 in { p where p is Point of (TOP-REAL 2) : ( p in P & p `2 >= 0 ) }
then reconsider q3 =
x2 as
Point of
(TOP-REAL 2) ;
q3 `2 >= 0
by A19, A161, A31, A163, A22, A23, A24, A32, A162, A37, A181, EUCLID:52;
hence
x2 in { p where p is Point of (TOP-REAL 2) : ( p in P & p `2 >= 0 ) }
by A11, A181;
verum
end;
hence
Upper_Arc P = { p where p is Point of (TOP-REAL 2) : ( p in P & p `2 >= 0 ) }
by A165, XBOOLE_0:def 10; verum