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 Circle2IntervalL | ((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 ) }
; Circle2IntervalL | ((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, Th28;
A12:
q `1 <= 1
by A10, Th28;
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:2;
verum
end;
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, Lm46, 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 A13:
(TOP-REAL 2) | B = (Topen_unit_circle c[-10]) | aX1
by PRE_TOPC:def 5;
A14:
for a being Point of ((Topen_unit_circle c[-10]) | aX1) holds (Circle2IntervalL | ((Topen_unit_circle c[-10]) | aX1)) . a = (Af1 * (c * f)) . a
proof
let a be
Point of
((Topen_unit_circle c[-10]) | aX1);
(Circle2IntervalL | ((Topen_unit_circle c[-10]) | aX1)) . a = (Af1 * (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 A15:
b = |[x,y]|
and A16:
(
y >= 0 implies
Circle2IntervalL . b = 1
+ ((arccos x) / (2 * PI)) )
and
(
y <= 0 implies
Circle2IntervalL . b = 1
- ((arccos x) / (2 * PI)) )
by Def14;
A17:
|[x,y]| `1 <= 1
by A15, Th28;
A18:
|[x,y]| `1 = x
by EUCLID:52;
- 1
< |[x,y]| `1
by A15, Th28;
then A19:
x in Q
by A18, A17, XXREAL_1:2;
then
arccos . x = c . x
by FUNCT_1:49;
then A20:
arccos . x in rng c
by A19, Lm55, FUNCT_1:def 3;
a in aX1
by A5;
then
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;
hence (Circle2IntervalL | ((Topen_unit_circle c[-10]) | aX1)) . a =
1
+ ((arccos x) / (2 * PI))
by A15, A16, EUCLID:52, FUNCT_1:49
.=
1
+ ((arccos . x) / (2 * PI))
by SIN_COS6:def 4
.=
1
+ ((1 / (2 * PI)) * (arccos . x))
by XCMPLX_1:99
.=
(AffineMap ((1 / (2 * PI)),1)) . (arccos . x)
by FCONT_1:def 4
.=
Af1 . (arccos . x)
by A20, Lm56, FUNCT_1:49
.=
Af1 . (c . x)
by A19, FUNCT_1:49
.=
Af1 . (c . (|[x,y]| `1))
by EUCLID:52
.=
Af1 . (c . (p . a))
by A15, PSCOMP_1:def 5
.=
Af1 . (c . (f . a))
by FUNCT_1:49
.=
Af1 . ((c * f) . a)
by A13, FUNCT_2:15
.=
(Af1 * (c * f)) . a
by A13, FUNCT_2:15
;
verum
end;
f is continuous
by Lm41, TOPREALA:8;
hence
Circle2IntervalL | ((Topen_unit_circle c[-10]) | aX1) is continuous
by A13, A14, Lm58, FUNCT_2:63; verum