let T be non empty TopSpace; for a, b being Point of T
for P, Q, R being Path of a,b st P,Q are_homotopic & Q,R are_homotopic holds
P,R are_homotopic
let a, b be Point of T; for P, Q, R being Path of a,b st P,Q are_homotopic & Q,R are_homotopic holds
P,R are_homotopic
1 / 2 in [.0 ,(1 / 2).]
by XXREAL_1:1;
then A1:
1 / 2 in the carrier of (Closed-Interval-TSpace 0 ,(1 / 2))
by TOPMETR:25;
reconsider B02 = [.(1 / 2),1.] as non empty Subset of I[01] by BORSUK_1:83, XXREAL_1:1, XXREAL_1:34;
A2:
1 in [.0 ,1.]
by XXREAL_1:1;
A3:
1 / 2 in [.(1 / 2),1.]
by XXREAL_1:1;
then A4:
1 / 2 in the carrier of (Closed-Interval-TSpace (1 / 2),1)
by TOPMETR:25;
[.0 ,(1 / 2).] c= the carrier of I[01]
by BORSUK_1:83, XXREAL_1:34;
then A5:
[:[.0 ,1.],[.0 ,(1 / 2).]:] c= [:the carrier of I[01] ,the carrier of I[01] :]
by BORSUK_1:83, ZFMISC_1:119;
A6:
the carrier of (Closed-Interval-TSpace 0 ,(1 / 2)) = [.0 ,(1 / 2).]
by TOPMETR:25;
0 in [.0 ,(1 / 2).]
by XXREAL_1:1;
then reconsider Ewa = [:[.0 ,1.],[.0 ,(1 / 2).]:] as non empty Subset of [:I[01] ,I[01] :] by A5, A2, BORSUK_1:def 5;
set T1 = [:I[01] ,I[01] :] | Ewa;
reconsider P2 = P[01] (1 / 2),1,((#) 0 ,1),(0 ,1 (#) ) as continuous Function of (Closed-Interval-TSpace (1 / 2),1),I[01] by TOPMETR:27, TREAL_1:15;
reconsider P1 = P[01] 0 ,(1 / 2),((#) 0 ,1),(0 ,1 (#) ) as continuous Function of (Closed-Interval-TSpace 0 ,(1 / 2)),I[01] by TOPMETR:27, TREAL_1:15;
let P, Q, R be Path of a,b; ( P,Q are_homotopic & Q,R are_homotopic implies P,R are_homotopic )
assume that
A7:
P,Q are_homotopic
and
A8:
Q,R are_homotopic
; P,R are_homotopic
consider f being Function of [:I[01] ,I[01] :],T such that
A9:
f is continuous
and
A10:
for s being Point of I[01] holds
( f . s,0 = P . s & f . s,1 = Q . s & ( for t being Point of I[01] holds
( f . 0 ,t = a & f . 1,t = b ) ) )
by A7, BORSUK_2:def 7;
A11:
the carrier of (Closed-Interval-TSpace (1 / 2),1) = [.(1 / 2),1.]
by TOPMETR:25;
[.0 ,1.] c= the carrier of I[01]
by BORSUK_1:83;
then reconsider A01 = [.0 ,1.] as non empty Subset of I[01] by XXREAL_1:1;
reconsider B01 = [.0 ,(1 / 2).] as non empty Subset of I[01] by BORSUK_1:83, XXREAL_1:1, XXREAL_1:34;
A12:
the carrier of (Closed-Interval-TSpace (1 / 2),1) = [.(1 / 2),1.]
by TOPMETR:25;
A01 = [#] I[01]
by BORSUK_1:83;
then A13:
I[01] = I[01] | A01
by TSEP_1:100;
[.(1 / 2),1.] c= the carrier of I[01]
by BORSUK_1:83, XXREAL_1:34;
then A14:
[:[.0 ,1.],[.(1 / 2),1.]:] c= [:the carrier of I[01] ,the carrier of I[01] :]
by BORSUK_1:83, ZFMISC_1:119;
A15:
1 in the carrier of I[01]
by BORSUK_1:86;
1 in [.(1 / 2),1.]
by XXREAL_1:1;
then reconsider Ewa1 = [:[.0 ,1.],[.(1 / 2),1.]:] as non empty Subset of [:I[01] ,I[01] :] by A2, A14, BORSUK_1:def 5;
set T2 = [:I[01] ,I[01] :] | Ewa1;
set e1 = [:(id I[01] ),P1:];
set e2 = [:(id I[01] ),P2:];
A16:
( dom (id I[01] ) = the carrier of I[01] & dom (P[01] (1 / 2),1,((#) 0 ,1),(0 ,1 (#) )) = the carrier of (Closed-Interval-TSpace (1 / 2),1) )
by FUNCT_2:def 1;
A17:
rng [:(id I[01] ),P2:] = [:(rng (id I[01] )),(rng (P[01] (1 / 2),1,((#) 0 ,1),(0 ,1 (#) ))):]
by FUNCT_3:88;
consider g being Function of [:I[01] ,I[01] :],T such that
A18:
g is continuous
and
A19:
for s being Point of I[01] holds
( g . s,0 = Q . s & g . s,1 = R . s & ( for t being Point of I[01] holds
( g . 0 ,t = a & g . 1,t = b ) ) )
by A8, BORSUK_2:def 7;
set f1 = f * [:(id I[01] ),P1:];
set g1 = g * [:(id I[01] ),P2:];
dom g =
the carrier of [:I[01] ,I[01] :]
by FUNCT_2:def 1
.=
[:the carrier of I[01] ,the carrier of I[01] :]
by BORSUK_1:def 5
;
then A20: dom (g * [:(id I[01] ),P2:]) =
dom [:(id I[01] ),P2:]
by A17, RELAT_1:46, TOPMETR:27, ZFMISC_1:119
.=
[:the carrier of I[01] ,the carrier of (Closed-Interval-TSpace (1 / 2),1):]
by A16, FUNCT_3:def 9
;
Closed-Interval-TSpace (1 / 2),1 = I[01] | B02
by TOPMETR:31;
then
( [:(id I[01] ),P2:] is continuous Function of [:I[01] ,(Closed-Interval-TSpace (1 / 2),1):],[:I[01] ,I[01] :] & [:I[01] ,I[01] :] | Ewa1 = [:I[01] ,(Closed-Interval-TSpace (1 / 2),1):] )
by A13, BORSUK_3:26;
then reconsider g1 = g * [:(id I[01] ),P2:] as continuous Function of ([:I[01] ,I[01] :] | Ewa1),T by A18;
Closed-Interval-TSpace 0 ,(1 / 2) = I[01] | B01
by TOPMETR:31;
then
( [:(id I[01] ),P1:] is continuous Function of [:I[01] ,(Closed-Interval-TSpace 0 ,(1 / 2)):],[:I[01] ,I[01] :] & [:I[01] ,I[01] :] | Ewa = [:I[01] ,(Closed-Interval-TSpace 0 ,(1 / 2)):] )
by A13, BORSUK_3:26;
then reconsider f1 = f * [:(id I[01] ),P1:] as continuous Function of ([:I[01] ,I[01] :] | Ewa),T by A9;
A21:
1 is Point of I[01]
by BORSUK_1:86;
A22:
0 is Point of I[01]
by BORSUK_1:86;
then A23:
[.0 ,1.] is compact Subset of I[01]
by A21, BORSUK_4:49;
A24:
1 / 2 is Point of I[01]
by BORSUK_1:86;
then
[.0 ,(1 / 2).] is compact Subset of I[01]
by A22, BORSUK_4:49;
then A25:
Ewa is compact Subset of [:I[01] ,I[01] :]
by A23, BORSUK_3:27;
[.(1 / 2),1.] is compact Subset of I[01]
by A21, A24, BORSUK_4:49;
then A26:
Ewa1 is compact Subset of [:I[01] ,I[01] :]
by A23, BORSUK_3:27;
A27: dom [:(id I[01] ),P1:] =
the carrier of [:I[01] ,(Closed-Interval-TSpace 0 ,(1 / 2)):]
by FUNCT_2:def 1
.=
[:the carrier of I[01] ,the carrier of (Closed-Interval-TSpace 0 ,(1 / 2)):]
by BORSUK_1:def 5
;
A28:
dom [:(id I[01] ),P2:] = [:(dom (id I[01] )),(dom P2):]
by FUNCT_3:def 9;
A29:
dom [:(id I[01] ),P1:] = [:(dom (id I[01] )),(dom P1):]
by FUNCT_3:def 9;
A30: dom [:(id I[01] ),P2:] =
the carrier of [:I[01] ,(Closed-Interval-TSpace (1 / 2),1):]
by FUNCT_2:def 1
.=
[:the carrier of I[01] ,the carrier of (Closed-Interval-TSpace (1 / 2),1):]
by BORSUK_1:def 5
;
A31:
( [#] ([:I[01] ,I[01] :] | Ewa) = Ewa & [#] ([:I[01] ,I[01] :] | Ewa1) = Ewa1 )
by PRE_TOPC:def 10;
then A32: ([#] ([:I[01] ,I[01] :] | Ewa)) /\ ([#] ([:I[01] ,I[01] :] | Ewa1)) =
[:[.0 ,1.],([.0 ,(1 / 2).] /\ [.(1 / 2),1.]):]
by ZFMISC_1:122
.=
[:[.0 ,1.],{(1 / 2)}:]
by XXREAL_1:418
;
A33:
for p being set st p in ([#] ([:I[01] ,I[01] :] | Ewa)) /\ ([#] ([:I[01] ,I[01] :] | Ewa1)) holds
f1 . p = g1 . p
proof
let p be
set ;
( p in ([#] ([:I[01] ,I[01] :] | Ewa)) /\ ([#] ([:I[01] ,I[01] :] | Ewa1)) implies f1 . p = g1 . p )
assume
p in ([#] ([:I[01] ,I[01] :] | Ewa)) /\ ([#] ([:I[01] ,I[01] :] | Ewa1))
;
f1 . p = g1 . p
then consider x,
y being
set such that A34:
x in [.0 ,1.]
and A35:
y in {(1 / 2)}
and A36:
p = [x,y]
by A32, ZFMISC_1:def 2;
x in { r where r is Real : ( 0 <= r & r <= 1 ) }
by A34, RCOMP_1:def 1;
then A37:
ex
r1 being
Real st
(
r1 = x &
0 <= r1 &
r1 <= 1 )
;
then reconsider x9 =
x as
Point of
I[01] by BORSUK_1:86;
A38:
y = 1
/ 2
by A35, TARSKI:def 1;
f1 . p = g1 . p
proof
1
/ 2
in [.0 ,(1 / 2).]
by XXREAL_1:1;
then reconsider y9 = 1
/ 2 as
Point of
(Closed-Interval-TSpace 0 ,(1 / 2)) by TOPMETR:25;
set t9 = 1
/ 2;
reconsider r1 =
(#) 0 ,1,
r2 =
0 ,1
(#) as
Real by BORSUK_1:def 17, BORSUK_1:def 18, TREAL_1:8;
A39:
P1 . y9 =
(((r2 - r1) / ((1 / 2) - 0 )) * (1 / 2)) + ((((1 / 2) * r1) - (0 * r2)) / ((1 / 2) - 0 ))
by TREAL_1:14
.=
(((1 - r1) / ((1 / 2) - 0 )) * (1 / 2)) + ((((1 / 2) * r1) - (0 * r2)) / ((1 / 2) - 0 ))
by TREAL_1:def 2
.=
(((1 - 0 ) / ((1 / 2) - 0 )) * (1 / 2)) + ((((1 / 2) * r1) - (0 * r2)) / ((1 / 2) - 0 ))
by TREAL_1:def 1
.=
(((1 - 0 ) / ((1 / 2) - 0 )) * (1 / 2)) + ((((1 / 2) * 0 ) - (0 * 1)) / ((1 / 2) - 0 ))
by TREAL_1:def 1
.=
1
;
reconsider y9 = 1
/ 2 as
Point of
(Closed-Interval-TSpace (1 / 2),1) by A3, TOPMETR:25;
A40:
P2 . y9 =
(((r2 - r1) / (1 - (1 / 2))) * (1 / 2)) + (((1 * r1) - ((1 / 2) * r2)) / (1 - (1 / 2)))
by TREAL_1:14
.=
0
by BORSUK_1:def 17, TREAL_1:8
;
A41:
x in the
carrier of
I[01]
by A37, BORSUK_1:86;
then A42:
[x,y] in dom [:(id I[01] ),P2:]
by A30, A4, A38, ZFMISC_1:106;
A43:
[x,y] in dom [:(id I[01] ),P1:]
by A1, A27, A38, A41, ZFMISC_1:106;
then f1 . p =
f . ([:(id I[01] ),P1:] . x,y)
by A36, FUNCT_1:23
.=
f . ((id I[01] ) . x),
(P1 . y)
by A29, A43, FUNCT_3:86
.=
f . x9,1
by A38, A39, FUNCT_1:35
.=
Q . x9
by A10
.=
g . x9,
0
by A19
.=
g . ((id I[01] ) . x9),
(P2 . y)
by A38, A40, FUNCT_1:35
.=
g . ([:(id I[01] ),P2:] . x,y)
by A28, A42, FUNCT_3:86
.=
g1 . p
by A36, A42, FUNCT_1:23
;
hence
f1 . p = g1 . p
;
verum
end;
hence
f1 . p = g1 . p
;
verum
end;
([#] ([:I[01] ,I[01] :] | Ewa)) \/ ([#] ([:I[01] ,I[01] :] | Ewa1)) =
[:[.0 ,1.],([.0 ,(1 / 2).] \/ [.(1 / 2),1.]):]
by A31, ZFMISC_1:120
.=
[:the carrier of I[01] ,the carrier of I[01] :]
by BORSUK_1:83, XXREAL_1:174
.=
[#] [:I[01] ,I[01] :]
by BORSUK_1:def 5
;
then consider h being Function of [:I[01] ,I[01] :],T such that
A44:
h = f1 +* g1
and
A45:
h is continuous
by A25, A26, A33, BORSUK_2:1;
A46:
the carrier of (Closed-Interval-TSpace 0 ,(1 / 2)) = [.0 ,(1 / 2).]
by TOPMETR:25;
A47:
for t being Point of I[01] holds
( h . 0 ,t = a & h . 1,t = b )
proof
let t be
Point of
I[01] ;
( h . 0 ,t = a & h . 1,t = b )
per cases
( t < 1 / 2 or t >= 1 / 2 )
;
suppose A48:
t < 1
/ 2
;
( h . 0 ,t = a & h . 1,t = b )reconsider r1 =
(#) 0 ,1,
r2 =
0 ,1
(#) as
Real by BORSUK_1:def 17, BORSUK_1:def 18, TREAL_1:8;
A49:
0 <= t
by BORSUK_1:86;
then A50:
t in the
carrier of
(Closed-Interval-TSpace 0 ,(1 / 2))
by A6, A48, XXREAL_1:1;
0 in the
carrier of
I[01]
by BORSUK_1:86;
then A51:
[0 ,t] in dom [:(id I[01] ),P1:]
by A27, A50, ZFMISC_1:106;
A52:
t is
Real
by XREAL_0:def 1;
then P1 . t =
(((r2 - r1) / ((1 / 2) - 0 )) * t) + ((((1 / 2) * r1) - (0 * r2)) / ((1 / 2) - 0 ))
by A50, TREAL_1:14
.=
(((1 - r1) / (1 / 2)) * t) + (((1 / 2) * r1) / (1 / 2))
by TREAL_1:def 2
.=
(((1 - 0 ) / (1 / 2)) * t) + (((1 / 2) * r1) / (1 / 2))
by TREAL_1:def 1
.=
((1 / (1 / 2)) * t) + (((1 / 2) * 0 ) / (1 / 2))
by TREAL_1:def 1
.=
2
* t
;
then A53:
P1 . t is
Point of
I[01]
by A48, Th6;
not
t in the
carrier of
(Closed-Interval-TSpace (1 / 2),1)
by A11, A48, XXREAL_1:1;
then
not
[0 ,t] in dom g1
by A20, ZFMISC_1:106;
hence h . 0 ,
t =
f1 . 0 ,
t
by A44, FUNCT_4:12
.=
f . ([:(id I[01] ),P1:] . 0 ,t)
by A51, FUNCT_1:23
.=
f . ((id I[01] ) . 0 ),
(P1 . t)
by A29, A51, FUNCT_3:86
.=
f . 0 ,
(P1 . t)
by A22, FUNCT_1:35
.=
a
by A10, A53
;
h . 1,t = b
t in the
carrier of
(Closed-Interval-TSpace 0 ,(1 / 2))
by A46, A48, A49, XXREAL_1:1;
then A54:
[1,t] in dom [:(id I[01] ),P1:]
by A27, A15, ZFMISC_1:106;
P1 . t =
(((r2 - r1) / ((1 / 2) - 0 )) * t) + ((((1 / 2) * r1) - (0 * r2)) / ((1 / 2) - 0 ))
by A50, A52, TREAL_1:14
.=
(((1 - r1) / (1 / 2)) * t) + (((1 / 2) * r1) / (1 / 2))
by TREAL_1:def 2
.=
(((1 - 0 ) / (1 / 2)) * t) + (((1 / 2) * r1) / (1 / 2))
by TREAL_1:def 1
.=
((1 / (1 / 2)) * t) + (((1 / 2) * 0 ) / (1 / 2))
by TREAL_1:def 1
.=
2
* t
;
then A55:
P1 . t is
Point of
I[01]
by A48, Th6;
not
t in the
carrier of
(Closed-Interval-TSpace (1 / 2),1)
by A12, A48, XXREAL_1:1;
then
not
[1,t] in dom g1
by A20, ZFMISC_1:106;
hence h . 1,
t =
f1 . 1,
t
by A44, FUNCT_4:12
.=
f . ([:(id I[01] ),P1:] . 1,t)
by A54, FUNCT_1:23
.=
f . ((id I[01] ) . 1),
(P1 . t)
by A29, A54, FUNCT_3:86
.=
f . 1,
(P1 . t)
by A21, FUNCT_1:35
.=
b
by A10, A55
;
verum end; suppose A56:
t >= 1
/ 2
;
( h . 0 ,t = a & h . 1,t = b )reconsider r1 =
(#) 0 ,1,
r2 =
0 ,1
(#) as
Real by BORSUK_1:def 17, BORSUK_1:def 18, TREAL_1:8;
t <= 1
by BORSUK_1:86;
then A57:
t in the
carrier of
(Closed-Interval-TSpace (1 / 2),1)
by A11, A56, XXREAL_1:1;
then A58:
[1,t] in dom [:(id I[01] ),P2:]
by A30, A15, ZFMISC_1:106;
A59:
t is
Real
by XREAL_0:def 1;
then P2 . t =
(((r2 - r1) / (1 - (1 / 2))) * t) + (((1 * r1) - ((1 / 2) * r2)) / (1 - (1 / 2)))
by A57, TREAL_1:14
.=
(((1 - r1) / (1 / 2)) * t) + (((1 * r1) - ((1 / 2) * r2)) / (1 / 2))
by TREAL_1:def 2
.=
(((1 - 0 ) / (1 / 2)) * t) + (((1 * r1) - ((1 / 2) * r2)) / (1 / 2))
by TREAL_1:def 1
.=
(2 * t) + (((1 * 0 ) - ((1 / 2) * r2)) / (1 / 2))
by TREAL_1:def 1
.=
(2 * t) + ((- ((1 / 2) * r2)) / (1 / 2))
.=
(2 * t) + ((- ((1 / 2) * 1)) / (1 / 2))
by TREAL_1:def 2
.=
(2 * t) - 1
;
then A60:
P2 . t is
Point of
I[01]
by A56, Th7;
P2 . t =
(((r2 - r1) / (1 - (1 / 2))) * t) + (((1 * r1) - ((1 / 2) * r2)) / (1 - (1 / 2)))
by A57, A59, TREAL_1:14
.=
(((1 - r1) / (1 / 2)) * t) + (((1 * r1) - ((1 / 2) * r2)) / (1 / 2))
by TREAL_1:def 2
.=
(((1 - 0 ) / (1 / 2)) * t) + (((1 * r1) - ((1 / 2) * r2)) / (1 / 2))
by TREAL_1:def 1
.=
((1 / (1 / 2)) * t) + (((1 * 0 ) - ((1 / 2) * r2)) / (1 / 2))
by TREAL_1:def 1
.=
((1 / (1 / 2)) * t) + (((1 * 0 ) - ((1 / 2) * 1)) / (1 / 2))
by TREAL_1:def 2
.=
(2 * t) - 1
;
then A61:
P2 . t is
Point of
I[01]
by A56, Th7;
A62:
0 in the
carrier of
I[01]
by BORSUK_1:86;
then A63:
[0 ,t] in dom [:(id I[01] ),P2:]
by A30, A57, ZFMISC_1:106;
[0 ,t] in dom g1
by A20, A62, A57, ZFMISC_1:106;
hence h . 0 ,
t =
g1 . 0 ,
t
by A44, FUNCT_4:14
.=
g . ([:(id I[01] ),P2:] . 0 ,t)
by A63, FUNCT_1:23
.=
g . ((id I[01] ) . 0 ),
(P2 . t)
by A28, A63, FUNCT_3:86
.=
g . 0 ,
(P2 . t)
by A22, FUNCT_1:35
.=
a
by A19, A61
;
h . 1,t = b
[1,t] in dom g1
by A20, A15, A57, ZFMISC_1:106;
hence h . 1,
t =
g1 . 1,
t
by A44, FUNCT_4:14
.=
g . ([:(id I[01] ),P2:] . 1,t)
by A58, FUNCT_1:23
.=
g . ((id I[01] ) . 1),
(P2 . t)
by A28, A58, FUNCT_3:86
.=
g . 1,
(P2 . t)
by A21, FUNCT_1:35
.=
b
by A19, A60
;
verum end;
end;
for s being Point of I[01] holds
( h . s,0 = P . s & h . s,1 = R . s )
proof
reconsider r1 =
(#) 0 ,1,
r2 =
0 ,1
(#) as
Real by BORSUK_1:def 17, BORSUK_1:def 18, TREAL_1:8;
let s be
Point of
I[01] ;
( h . s,0 = P . s & h . s,1 = R . s )
( 1
= 0 ,1
(#) & 1
= (1 / 2),1
(#) )
by TREAL_1:def 2;
then A64:
P2 . 1
= 1
by TREAL_1:16;
A65:
the
carrier of
(Closed-Interval-TSpace (1 / 2),1) = [.(1 / 2),1.]
by TOPMETR:25;
then A66:
1
in the
carrier of
(Closed-Interval-TSpace (1 / 2),1)
by XXREAL_1:1;
then A67:
[s,1] in dom [:(id I[01] ),P2:]
by A30, ZFMISC_1:106;
[s,1] in dom g1
by A20, A66, ZFMISC_1:106;
then A68:
h . s,1 =
g1 . s,1
by A44, FUNCT_4:14
.=
g . ([:(id I[01] ),P2:] . s,1)
by A67, FUNCT_1:23
.=
g . ((id I[01] ) . s),
(P2 . 1)
by A28, A67, FUNCT_3:86
.=
g . s,1
by A64, FUNCT_1:35
.=
R . s
by A19
;
A69:
0 in the
carrier of
(Closed-Interval-TSpace 0 ,(1 / 2))
by A6, XXREAL_1:1;
then A70:
P1 . 0 =
(((r2 - r1) / ((1 / 2) - 0 )) * 0 ) + ((((1 / 2) * r1) - (0 * r2)) / ((1 / 2) - 0 ))
by TREAL_1:14
.=
(((1 / 2) * 0 ) - (0 * r2)) / ((1 / 2) - 0 )
by TREAL_1:def 1
;
A71:
[s,0 ] in dom [:(id I[01] ),P1:]
by A27, A69, ZFMISC_1:106;
not
0 in the
carrier of
(Closed-Interval-TSpace (1 / 2),1)
by A65, XXREAL_1:1;
then
not
[s,0 ] in dom g1
by A20, ZFMISC_1:106;
then h . s,
0 =
f1 . s,
0
by A44, FUNCT_4:12
.=
f . ([:(id I[01] ),P1:] . s,0 )
by A71, FUNCT_1:23
.=
f . ((id I[01] ) . s),
(P1 . 0 )
by A29, A71, FUNCT_3:86
.=
f . s,
0
by A70, FUNCT_1:35
.=
P . s
by A10
;
hence
(
h . s,
0 = P . s &
h . s,1
= R . s )
by A68;
verum
end;
hence
P,R are_homotopic
by A45, A47, BORSUK_2:def 7; verum