reconsider c1 = c[-10] as Point of (TOP-REAL 2) ;
let aX1 be Subset of (Topen_unit_circle c[10]); ( aX1 = { q where q is Point of (TOP-REAL 2) : ( q in the carrier of (Topen_unit_circle c[10]) & 0 >= q `2 ) } implies Circle2IntervalR | ((Topen_unit_circle c[10]) | aX1) is continuous )
assume A1:
aX1 = { q where q is Point of (TOP-REAL 2) : ( q in the carrier of (Topen_unit_circle c[10]) & 0 >= q `2 ) }
; Circle2IntervalR | ((Topen_unit_circle c[10]) | aX1) is continuous
A2:
c1 `2 = 0
by EUCLID:52;
c[-10] is Point of (Topen_unit_circle c[10])
by Lm15, Th23;
then
c[-10] in aX1
by A1, A2;
then reconsider aX1 = aX1 as non empty Subset of (Topen_unit_circle c[10]) ;
set X1 = (Topen_unit_circle c[10]) | aX1;
A3:
the carrier of (Tunit_circle 2) is Subset of (TOP-REAL 2)
by TSEP_1:1;
[#] ((Topen_unit_circle c[10]) | aX1) is Subset of (Tunit_circle 2)
by Lm9;
then reconsider B = [#] ((Topen_unit_circle c[10]) | aX1) as non empty Subset of (TOP-REAL 2) by A3, XBOOLE_1:1;
set f = p | B;
A4:
dom (p | B) = B
by Lm40, RELAT_1:62;
A5:
aX1 = the carrier of ((Topen_unit_circle c[10]) | aX1)
by PRE_TOPC:8;
A6:
rng (p | B) c= Q
proof
let y be
object ;
TARSKI:def 3 ( not y in rng (p | B) or y in Q )
assume
y in rng (p | B)
;
y in Q
then consider x being
object such that A7:
x in dom (p | B)
and A8:
(p | B) . x = y
by FUNCT_1:def 3;
consider q being
Point of
(TOP-REAL 2) such that A9:
q = x
and A10:
q in the
carrier of
(Topen_unit_circle c[10])
and
0 >= q `2
by A1, A5, A4, A7;
A11:
- 1
<= q `1
by A10, Th27;
A12:
q `1 < 1
by A10, Th27;
y =
p . x
by A4, A7, A8, FUNCT_1:49
.=
q `1
by A9, PSCOMP_1:def 5
;
hence
y in Q
by A11, A12, XXREAL_1:3;
verum
end;
A13:
the carrier of ((TOP-REAL 2) | B) = B
by PRE_TOPC:8;
then reconsider f = p | B as Function of ((TOP-REAL 2) | B),(R^1 | (R^1 Q)) by A4, A6, Lm25, FUNCT_2:2;
(Topen_unit_circle c[10]) | aX1 is SubSpace of Tunit_circle 2
by TSEP_1:7;
then
(Topen_unit_circle c[10]) | aX1 is SubSpace of TOP-REAL 2
by TSEP_1:7;
then A14:
(TOP-REAL 2) | B = (Topen_unit_circle c[10]) | aX1
by PRE_TOPC:def 5;
A15:
for a being Point of ((Topen_unit_circle c[10]) | aX1) holds (Circle2IntervalR | ((Topen_unit_circle c[10]) | aX1)) . a = (L * (Af * (c * f))) . a
proof
let a be
Point of
((Topen_unit_circle c[10]) | aX1);
(Circle2IntervalR | ((Topen_unit_circle c[10]) | aX1)) . a = (L * (Af * (c * f))) . a
reconsider b =
a as
Point of
(Topen_unit_circle c[10]) by PRE_TOPC:25;
consider x,
y being
Real such that A16:
b = |[x,y]|
and
(
y >= 0 implies
Circle2IntervalR . b = (arccos x) / (2 * PI) )
and A17:
(
y <= 0 implies
Circle2IntervalR . b = 1
- ((arccos x) / (2 * PI)) )
by Def13;
A18:
|[x,y]| `1 < 1
by A16, Th27;
reconsider r =
(Af * (c * f)) . a as
Real ;
dom (Af * (c * f)) = the
carrier of
((TOP-REAL 2) | B)
by FUNCT_2:def 1;
then A19:
r in rng (Af * (c * f))
by A13, FUNCT_1:def 3;
A99:
rng (Af * (c * f)) c= the
carrier of
(R^1 | (R^1 ].0,1.[))
by RELAT_1:def 19;
a in aX1
by A5;
then A20:
ex
q being
Point of
(TOP-REAL 2) st
(
a = q &
q in the
carrier of
(Topen_unit_circle c[10]) &
0 >= q `2 )
by A1;
A21:
|[x,y]| `1 = x
by EUCLID:52;
- 1
<= |[x,y]| `1
by A16, Th26;
then A22:
x in Q
by A21, A18, XXREAL_1:3;
then
arccos . x = c . x
by FUNCT_1:49;
then A23:
arccos . x in rng c
by A22, Lm36, FUNCT_1:def 3;
(arccos x) / (2 * PI) =
(arccos . x) / (2 * PI)
by SIN_COS6:def 4
.=
((1 / (2 * PI)) * (arccos . x)) + 0
by XCMPLX_1:99
.=
(AffineMap ((1 / (2 * PI)),0)) . (arccos . x)
by FCONT_1:def 4
.=
Af . (arccos . x)
by A23, Lm37, FUNCT_1:49
.=
Af . (c . x)
by A22, FUNCT_1:49
.=
Af . (c . (|[x,y]| `1))
by EUCLID:52
.=
Af . (c . (p . a))
by A16, PSCOMP_1:def 5
.=
Af . (c . (f . a))
by FUNCT_1:49
.=
Af . ((c * f) . a)
by A14, FUNCT_2:15
.=
(Af * (c * f)) . a
by A14, FUNCT_2:15
;
hence (Circle2IntervalR | ((Topen_unit_circle c[10]) | aX1)) . a =
((- 1) * r) + 1
by A16, A17, A20, EUCLID:52, FUNCT_1:49
.=
(R^1 (AffineMap ((- 1),1))) . r
by FCONT_1:def 4
.=
L . r
by A19, A99, Lm27, FUNCT_1:49
.=
(L * (Af * (c * f))) . a
by A14, FUNCT_2:15
;
verum
end;
f is continuous
by Lm41, TOPREALA:8;
hence
Circle2IntervalR | ((Topen_unit_circle c[10]) | aX1) is continuous
by A14, A15, Lm39, FUNCT_2:63; verum