let A be Subset of (TOP-REAL 2); for p1, p2, q1, q2 being Point of (TOP-REAL 2) st A is_an_arc_of p1,p2 & LE q1,q2,A,p1,p2 & q1 <> q2 holds
Segment (A,p1,p2,q1,q2) is_an_arc_of q1,q2
let p1, p2, q1, q2 be Point of (TOP-REAL 2); ( A is_an_arc_of p1,p2 & LE q1,q2,A,p1,p2 & q1 <> q2 implies Segment (A,p1,p2,q1,q2) is_an_arc_of q1,q2 )
assume that
A1:
A is_an_arc_of p1,p2
and
A2:
( LE q1,q2,A,p1,p2 & q1 <> q2 )
; Segment (A,p1,p2,q1,q2) is_an_arc_of q1,q2
consider g being Function of I[01],((TOP-REAL 2) | A), s1, s2 being Real such that
A3:
g is being_homeomorphism
and
A4:
( g . 0 = p1 & g . 1 = p2 )
and
A5:
g . s1 = q1
and
A6:
g . s2 = q2
and
A7:
0 <= s1
and
A8:
s1 < s2
and
A9:
s2 <= 1
by A1, A2, Th17;
reconsider A9 = A as non empty Subset of (TOP-REAL 2) by A1, TOPREAL1:1;
set S = Segment (A,p1,p2,q1,q2);
A10:
Segment (A,p1,p2,q1,q2) = { q where q is Point of (TOP-REAL 2) : ( LE q1,q,A,p1,p2 & LE q,q2,A,p1,p2 ) }
by JORDAN6:26;
A11:
0 < s2 - s1
by A8, XREAL_1:50;
set f = (g * (AffineMap ((s2 - s1),s1))) | [.0,1.];
reconsider g = g as Function of I[01],((TOP-REAL 2) | A9) ;
reconsider m = AffineMap ((s2 - s1),s1) as Function of R^1,R^1 by TOPMETR:17;
for x being Real holds m . x = ((s2 - s1) * x) + s1
by FCONT_1:def 4;
then reconsider m = m as continuous Function of R^1,R^1 by TOPMETR:21;
set h = m | I[01];
A12:
m | I[01] = m | [.0,1.]
by BORSUK_1:40, TMAP_1:def 4;
then A13: rng (m | I[01]) =
m .: [.0,1.]
by RELAT_1:115
.=
[.s1,((s2 - s1) + s1).]
by A8, FCONT_1:57, XREAL_1:50
.=
[.s1,s2.]
;
then A14:
rng (m | I[01]) c= [.0,1.]
by A7, A9, XXREAL_1:34;
A15:
dom m = REAL
by FUNCT_2:def 1;
then A16:
dom (m | I[01]) = [.0,1.]
by A12, RELAT_1:62;
then reconsider h = m | I[01] as Function of I[01],I[01] by A14, BORSUK_1:40, RELSET_1:4;
A17:
(g * (AffineMap ((s2 - s1),s1))) | [.0,1.] = g * h
by A12, RELAT_1:83;
A18:
[.0,1.] = dom g
by BORSUK_1:40, FUNCT_2:def 1;
m .: [.0,1.] c= dom g
proof
let e be
object ;
TARSKI:def 3 ( not e in m .: [.0,1.] or e in dom g )
assume
e in m .: [.0,1.]
;
e in dom g
then A19:
e in [.s1,((s2 - s1) + s1).]
by A8, FCONT_1:57, XREAL_1:50;
[.s1,s2.] c= [.0,1.]
by A7, A9, XXREAL_1:34;
hence
e in dom g
by A18, A19;
verum
end;
then A20:
[.0,1.] c= dom (g * m)
by A15, FUNCT_3:3;
then A21:
dom ((g * (AffineMap ((s2 - s1),s1))) | [.0,1.]) = [#] I[01]
by BORSUK_1:40, RELAT_1:62;
reconsider CIT = Closed-Interval-TSpace (s1,s2) as non empty SubSpace of I[01] by A7, A8, A9, TOPMETR:20, TREAL_1:3;
[.s1,s2.] c= [.0,1.]
by A7, A9, XXREAL_1:34;
then A22:
the carrier of CIT c= dom g
by A8, A18, TOPMETR:18;
A23:
rng h = the carrier of CIT
by A8, A13, TOPMETR:18;
A24:
dom ((g * (AffineMap ((s2 - s1),s1))) | [.0,1.]) = the carrier of I[01]
by A20, BORSUK_1:40, RELAT_1:62;
A25:
s1 < 1
by A8, A9, XXREAL_0:2;
for y being object holds
( y in [#] ((TOP-REAL 2) | (Segment (A,p1,p2,q1,q2))) iff ex x being object st
( x in dom ((g * (AffineMap ((s2 - s1),s1))) | [.0,1.]) & y = ((g * (AffineMap ((s2 - s1),s1))) | [.0,1.]) . x ) )
proof
let y be
object ;
( y in [#] ((TOP-REAL 2) | (Segment (A,p1,p2,q1,q2))) iff ex x being object st
( x in dom ((g * (AffineMap ((s2 - s1),s1))) | [.0,1.]) & y = ((g * (AffineMap ((s2 - s1),s1))) | [.0,1.]) . x ) )
thus
(
y in [#] ((TOP-REAL 2) | (Segment (A,p1,p2,q1,q2))) implies ex
x being
object st
(
x in dom ((g * (AffineMap ((s2 - s1),s1))) | [.0,1.]) &
y = ((g * (AffineMap ((s2 - s1),s1))) | [.0,1.]) . x ) )
( ex x being object st
( x in dom ((g * (AffineMap ((s2 - s1),s1))) | [.0,1.]) & y = ((g * (AffineMap ((s2 - s1),s1))) | [.0,1.]) . x ) implies y in [#] ((TOP-REAL 2) | (Segment (A,p1,p2,q1,q2))) )proof
assume
y in [#] ((TOP-REAL 2) | (Segment (A,p1,p2,q1,q2)))
;
ex x being object st
( x in dom ((g * (AffineMap ((s2 - s1),s1))) | [.0,1.]) & y = ((g * (AffineMap ((s2 - s1),s1))) | [.0,1.]) . x )
then
y in Segment (
A,
p1,
p2,
q1,
q2)
by PRE_TOPC:def 5;
then consider q0 being
Point of
(TOP-REAL 2) such that A26:
y = q0
and A27:
LE q1,
q0,
A,
p1,
p2
and A28:
LE q0,
q2,
A,
p1,
p2
by A10;
q0 in A
by A27, JORDAN5C:def 3;
then
q0 in [#] ((TOP-REAL 2) | A)
by PRE_TOPC:def 5;
then
q0 in rng g
by A3;
then consider s being
object such that A29:
s in dom g
and A30:
q0 = g . s
by FUNCT_1:def 3;
reconsider s =
s as
Real by A29;
take x =
(s - s1) / (s2 - s1);
( x in dom ((g * (AffineMap ((s2 - s1),s1))) | [.0,1.]) & y = ((g * (AffineMap ((s2 - s1),s1))) | [.0,1.]) . x )
A31:
s <= 1
by A29, BORSUK_1:40, XXREAL_1:1;
then
s <= s2
by A3, A4, A6, A7, A8, A9, A28, A30, JORDAN5C:def 3;
then
s - s1 <= s2 - s1
by XREAL_1:9;
then
x <= (s2 - s1) / (s2 - s1)
by A11, XREAL_1:72;
then A32:
x <= 1
by A11, XCMPLX_1:60;
0 <= s
by A29, BORSUK_1:40, XXREAL_1:1;
then
s1 + 0 <= s
by A3, A4, A5, A25, A27, A30, A31, JORDAN5C:def 3;
then
0 <= s - s1
by XREAL_1:19;
hence A33:
x in dom ((g * (AffineMap ((s2 - s1),s1))) | [.0,1.])
by A11, A21, A32, BORSUK_1:40, XXREAL_1:1;
y = ((g * (AffineMap ((s2 - s1),s1))) | [.0,1.]) . x
A34:
x in REAL
by XREAL_0:def 1;
m . x =
((s2 - s1) * x) + s1
by FCONT_1:def 4
.=
(s - s1) + s1
by A11, XCMPLX_1:87
.=
s
;
hence y =
(g * m) . x
by A15, A26, A30, FUNCT_1:13, A34
.=
((g * (AffineMap ((s2 - s1),s1))) | [.0,1.]) . x
by A33, FUNCT_1:47
;
verum
end;
given x being
object such that A35:
x in dom ((g * (AffineMap ((s2 - s1),s1))) | [.0,1.])
and A36:
y = ((g * (AffineMap ((s2 - s1),s1))) | [.0,1.]) . x
;
y in [#] ((TOP-REAL 2) | (Segment (A,p1,p2,q1,q2)))
reconsider x =
x as
Element of
REAL by A35;
(AffineMap ((s2 - s1),s1)) . x in REAL
;
then reconsider s =
m . x as
Element of
REAL ;
h . x = m . x
by A12, A16, A21, A35, BORSUK_1:40, FUNCT_1:47;
then A37:
s in rng h
by A16, A21, A35, BORSUK_1:40, FUNCT_1:def 3;
then A38:
s1 <= s
by A13, XXREAL_1:1;
y in rng ((g * (AffineMap ((s2 - s1),s1))) | [.0,1.])
by A35, A36, FUNCT_1:def 3;
then
y in [#] ((TOP-REAL 2) | A)
;
then
y in A
by PRE_TOPC:def 5;
then reconsider q =
y as
Point of
(TOP-REAL 2) ;
A39:
s <= s2
by A13, A37, XXREAL_1:1;
then A40:
s <= 1
by A9, XXREAL_0:2;
A41:
q =
(g * m) . x
by A35, A36, FUNCT_1:47
.=
g . s
by A15, FUNCT_1:13
;
then A42:
LE q1,
q,
A,
p1,
p2
by A1, A3, A4, A5, A7, A25, A38, A40, JORDAN5C:8;
LE q,
q2,
A,
p1,
p2
by A1, A3, A4, A6, A7, A9, A41, A38, A39, A40, JORDAN5C:8;
then
q in Segment (
A,
p1,
p2,
q1,
q2)
by A10, A42;
hence
y in [#] ((TOP-REAL 2) | (Segment (A,p1,p2,q1,q2)))
by PRE_TOPC:def 5;
verum
end;
then A43:
rng ((g * (AffineMap ((s2 - s1),s1))) | [.0,1.]) = [#] ((TOP-REAL 2) | (Segment (A,p1,p2,q1,q2)))
by FUNCT_1:def 3;
then A44:
[#] ((TOP-REAL 2) | (Segment (A,p1,p2,q1,q2))) <> {}
by A21, RELAT_1:42;
then reconsider f = (g * (AffineMap ((s2 - s1),s1))) | [.0,1.] as Function of I[01],((TOP-REAL 2) | (Segment (A,p1,p2,q1,q2))) by A24, A43, FUNCT_2:def 1, RELSET_1:4;
reconsider TS = (TOP-REAL 2) | (Segment (A,p1,p2,q1,q2)) as non empty SubSpace of (TOP-REAL 2) | A9 by A44, Th2, TOPMETR:22;
take
f
; TOPREAL1:def 1 ( f is being_homeomorphism & f . 0 = q1 & f . 1 = q2 )
A45:
(AffineMap ((s2 - s1),s1)) . 0 = s1
by FCONT_1:48;
set o = g | CIT;
A46: dom (g | CIT) =
dom (g | the carrier of CIT)
by TMAP_1:def 4
.=
(dom g) /\ the carrier of CIT
by RELAT_1:61
.=
the carrier of CIT
by A22, XBOOLE_1:28
;
reconsider h = h as Function of I[01],CIT by A16, A23, RELSET_1:4;
h is onto
by A23, FUNCT_2:def 3;
then A47:
h is being_homeomorphism
by A11, Th9, Th20;
A48:
the carrier of CIT = [.s1,s2.]
by A8, TOPMETR:18;
then
g | CIT = g | (rng h)
by A13, TMAP_1:def 4;
then A49:
f = (g | CIT) * h
by A17, FUNCT_4:2;
then A50:
rng (g | CIT) = rng f
by A13, A46, A48, RELAT_1:28;
then reconsider o = g | CIT as Function of CIT,TS by A46, RELSET_1:4;
o is onto
by A43, A50, FUNCT_2:def 3;
then
o is being_homeomorphism
by A3, Th9;
hence
f is being_homeomorphism
by A49, A47, TOPS_2:57; ( f . 0 = q1 & f . 1 = q2 )
A51:
dom (AffineMap ((s2 - s1),s1)) = REAL
by FUNCT_2:def 1;
A52:
0 in REAL
by XREAL_0:def 1;
0 in [.0,1.]
by XXREAL_1:1;
hence f . 0 =
(g * m) . 0
by FUNCT_1:49
.=
q1
by A5, A45, A51, FUNCT_1:13, A52
;
f . 1 = q2
A53: (AffineMap ((s2 - s1),s1)) . 1 =
(s2 - s1) + s1
by FCONT_1:49
.=
s2
;
A54:
1 in REAL
by XREAL_0:def 1;
1 in [.0,1.]
by XXREAL_1:1;
hence f . 1 =
(g * m) . 1
by FUNCT_1:49
.=
q2
by A6, A53, A51, FUNCT_1:13, A54
;
verum