let aX1 be Subset of (Topen_unit_circle c[10] ); :: thesis: ( 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 ) }
; :: thesis: Circle2IntervalR | ((Topen_unit_circle c[10] ) | aX1) is continuous
reconsider c1 = c[-10] as Point of (TOP-REAL 2) ;
A2:
c1 `2 = 0
by EUCLID:56;
c[-10] is Point of (Topen_unit_circle c[10] )
by Lm16, Th24;
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:
aX1 = the carrier of ((Topen_unit_circle c[10] ) | aX1)
by PRE_TOPC:29;
A4:
[#] ((Topen_unit_circle c[10] ) | aX1) is Subset of (Tunit_circle 2)
by Lm10;
the carrier of (Tunit_circle 2) is Subset of (TOP-REAL 2)
by TSEP_1:1;
then reconsider B = [#] ((Topen_unit_circle c[10] ) | aX1) as non empty Subset of (TOP-REAL 2) by A4, XBOOLE_1:1;
(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 A5:
(TOP-REAL 2) | B = (Topen_unit_circle c[10] ) | aX1
by PRE_TOPC:def 10;
set f = p | B;
A6:
the carrier of ((TOP-REAL 2) | B) = B
by PRE_TOPC:29;
A7:
dom (p | B) = B
by Lm41, RELAT_1:91;
rng (p | B) c= Q
then reconsider f = p | B as Function of ((TOP-REAL 2) | B),(R^1 | (R^1 Q)) by A6, A7, Lm27, FUNCT_2:4;
f is continuous
by Lm42, TOPREALA:29;
then
c * f is continuous
by Lm40;
then A13:
Af * (c * f) is continuous
;
for a being Point of ((Topen_unit_circle c[10] ) | aX1) holds (Circle2IntervalR | ((Topen_unit_circle c[10] ) | aX1)) . a = (Af * (c * f)) . a
proof
let a be
Point of
((Topen_unit_circle c[10] ) | aX1);
:: thesis: (Circle2IntervalR | ((Topen_unit_circle c[10] ) | aX1)) . a = (Af * (c * f)) . a
reconsider b =
a as
Point of
(Topen_unit_circle c[10] ) by PRE_TOPC:55;
consider x,
y being
real number such that A14:
b = |[x,y]|
and A15:
(
y >= 0 implies
Circle2IntervalR . b = (arccos x) / (2 * PI ) )
and
(
y <= 0 implies
Circle2IntervalR . b = 1
- ((arccos x) / (2 * PI )) )
by Def13;
a in aX1
by A3;
then A16:
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;
A17:
|[x,y]| `1 = x
by EUCLID:56;
A18:
- 1
<= |[x,y]| `1
by A14, Th27;
|[x,y]| `1 < 1
by A14, Th28;
then A19:
x in Q
by A17, A18, XXREAL_1:3;
then
arccos . x = c . x
by FUNCT_1:72;
then A20:
arccos . x in rng c
by A19, Lm38, FUNCT_1:def 5;
thus (Circle2IntervalR | ((Topen_unit_circle c[10] ) | aX1)) . a =
(arccos x) / (2 * PI )
by A14, A15, A16, EUCLID:56, FUNCT_1:72
.=
(arccos . x) / (2 * PI )
by SIN_COS6:def 4
.=
((1 / (2 * PI )) * (arccos . x)) + 0
by XCMPLX_1:100
.=
(AffineMap (1 / (2 * PI )),0 ) . (arccos . x)
by JORDAN16:def 3
.=
Af . (arccos . x)
by A20, Lm39, FUNCT_1:72
.=
Af . (c . x)
by A19, FUNCT_1:72
.=
Af . (c . (|[x,y]| `1 ))
by EUCLID:56
.=
Af . (c . (p . a))
by A14, PSCOMP_1:def 28
.=
Af . (c . (f . a))
by FUNCT_1:72
.=
Af . ((c * f) . a)
by A5, FUNCT_2:21
.=
(Af * (c * f)) . a
by A5, FUNCT_2:21
;
:: thesis: verum
end;
hence
Circle2IntervalR | ((Topen_unit_circle c[10] ) | aX1) is continuous
by A5, A13, FUNCT_2:113; :: thesis: verum