let T be non empty TopSpace; :: thesis: 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; :: thesis: 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:18;
reconsider B02 = [.(1 / 2),1.] as non empty Subset of I[01] by BORSUK_1:40, 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:18;
[.0,(1 / 2).] c= the carrier of I[01] by BORSUK_1:40, XXREAL_1:34;
then A5: [:[.0,1.],[.0,(1 / 2).]:] c= [: the carrier of I[01], the carrier of I[01]:] by BORSUK_1:40, ZFMISC_1:96;
A6: the carrier of (Closed-Interval-TSpace (0,(1 / 2))) = [.0,(1 / 2).] by TOPMETR:18;
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 2;
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:20, TREAL_1:12;
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:20, TREAL_1:12;
let P, Q, R be Path of a,b; :: thesis: ( 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 ; :: thesis: 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;
A11: the carrier of (Closed-Interval-TSpace ((1 / 2),1)) = [.(1 / 2),1.] by TOPMETR:18;
[.0,1.] c= the carrier of I[01] by BORSUK_1:40;
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:40, XXREAL_1:1, XXREAL_1:34;
A12: the carrier of (Closed-Interval-TSpace ((1 / 2),1)) = [.(1 / 2),1.] by TOPMETR:18;
A01 = [#] I[01] by BORSUK_1:40;
then A13: I[01] = I[01] | A01 by TSEP_1:93;
[.(1 / 2),1.] c= the carrier of I[01] by BORSUK_1:40, XXREAL_1:34;
then A14: [:[.0,1.],[.(1 / 2),1.]:] c= [: the carrier of I[01], the carrier of I[01]:] by BORSUK_1:40, ZFMISC_1:96;
A15: 1 in the carrier of I[01] by BORSUK_1:43;
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 2;
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:67;
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;
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 2 ;
then A20: dom (g * [:(id I[01]),P2:]) = dom [:(id I[01]),P2:] by A17, RELAT_1:27, TOPMETR:20, ZFMISC_1:96
.= [: the carrier of I[01], the carrier of (Closed-Interval-TSpace ((1 / 2),1)):] by A16, FUNCT_3:def 8 ;
Closed-Interval-TSpace ((1 / 2),1) = I[01] | B02 by TOPMETR:24;
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:22;
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:24;
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:22;
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:43;
A22: 0 is Point of I[01] by BORSUK_1:43;
then A23: [.0,1.] is compact Subset of I[01] by A21, BORSUK_4:24;
A24: 1 / 2 is Point of I[01] by BORSUK_1:43;
then [.0,(1 / 2).] is compact Subset of I[01] by A22, BORSUK_4:24;
then A25: Ewa is compact Subset of [:I[01],I[01]:] by A23, BORSUK_3:23;
[.(1 / 2),1.] is compact Subset of I[01] by A21, A24, BORSUK_4:24;
then A26: Ewa1 is compact Subset of [:I[01],I[01]:] by A23, BORSUK_3:23;
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 2 ;
A28: dom [:(id I[01]),P2:] = [:(dom (id I[01])),(dom P2):] by FUNCT_3:def 8;
A29: dom [:(id I[01]),P1:] = [:(dom (id I[01])),(dom P1):] by FUNCT_3:def 8;
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 2 ;
A31: ( [#] ([:I[01],I[01]:] | Ewa) = Ewa & [#] ([:I[01],I[01]:] | Ewa1) = Ewa1 ) by PRE_TOPC:def 5;
then A32: ([#] ([:I[01],I[01]:] | Ewa)) /\ ([#] ([:I[01],I[01]:] | Ewa1)) = [:[.0,1.],([.0,(1 / 2).] /\ [.(1 / 2),1.]):] by ZFMISC_1:99
.= [:[.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 ; :: thesis: ( 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)) ; :: thesis: f1 . p = g1 . p
then consider x, y being object 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:43;
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:18;
set t9 = 1 / 2;
reconsider r1 = (#) (0,1), r2 = (0,1) (#) as Real ;
A39: P1 . y9 = (((r2 - r1) / ((1 / 2) - 0)) * (1 / 2)) + ((((1 / 2) * r1) - (0 * r2)) / ((1 / 2) - 0)) by TREAL_1:11
.= (((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:18;
A40: P2 . y9 = (((r2 - r1) / (1 - (1 / 2))) * (1 / 2)) + (((1 * r1) - ((1 / 2) * r2)) / (1 - (1 / 2))) by TREAL_1:11
.= 0 by BORSUK_1:def 14, TREAL_1:5 ;
A41: x in the carrier of I[01] by A37, BORSUK_1:43;
then A42: [x,y] in dom [:(id I[01]),P2:] by A30, A4, A38, ZFMISC_1:87;
A43: [x,y] in dom [:(id I[01]),P1:] by A1, A27, A38, A41, ZFMISC_1:87;
then f1 . p = f . ([:(id I[01]),P1:] . (x,y)) by A36, FUNCT_1:13
.= f . (((id I[01]) . x),(P1 . y)) by A29, A43, FUNCT_3:65
.= f . (x9,1) by A38, A39, FUNCT_1:18
.= Q . x9 by A10
.= g . (x9,0) by A19
.= g . (((id I[01]) . x9),(P2 . y)) by A38, A40, FUNCT_1:18
.= g . ([:(id I[01]),P2:] . (x,y)) by A28, A42, FUNCT_3:65
.= g1 . p by A36, A42, FUNCT_1:13 ;
hence f1 . p = g1 . p ; :: thesis: verum

end;

hence f1 . p = g1 . p ; :: thesis: verum

end;

([#] ([:I[01],I[01]:] | Ewa)) \/ ([#] ([:I[01],I[01]:] | Ewa1)) = [:[.0,1.],([.0,(1 / 2).] \/ [.(1 / 2),1.]):] by A31, ZFMISC_1:97
.= [: the carrier of I[01], the carrier of I[01]:] by BORSUK_1:40, XXREAL_1:174
.= [#] [:I[01],I[01]:] by BORSUK_1:def 2 ;
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:18;
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]; :: thesis: ( h . (0,t) = a & h . (1,t) = b )

per cases ( t < 1 / 2 or t >= 1 / 2 ) ;

suppose A48: t < 1 / 2 ; :: thesis: ( h . (0,t) = a & h . (1,t) = b )

reconsider r1 = (#) (0,1), r2 = (0,1) (#) as Real ;
A49: 0 <= t by BORSUK_1:43;
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:43;
then A51: [0,t] in dom [:(id I[01]),P1:] by A27, A50, ZFMISC_1:87;
P1 . t = (((r2 - r1) / ((1 / 2) - 0)) * t) + ((((1 / 2) * r1) - (0 * r2)) / ((1 / 2) - 0)) by A50, TREAL_1:11
.= (((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 A52: P1 . t is Point of I[01] by A48, Th3;
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:87;
hence h . (0,t) = f1 . (0,t) by A44, FUNCT_4:11
.= f . ([:(id I[01]),P1:] . (0,t)) by A51, FUNCT_1:13
.= f . (((id I[01]) . 0),(P1 . t)) by A29, A51, FUNCT_3:65
.= f . (0,(P1 . t)) by A22, FUNCT_1:18
.= a by A10, A52 ;
:: thesis: h . (1,t) = b
t in the carrier of (Closed-Interval-TSpace (0,(1 / 2))) by A46, A48, A49, XXREAL_1:1;
then A53: [1,t] in dom [:(id I[01]),P1:] by A27, A15, ZFMISC_1:87;
P1 . t = (((r2 - r1) / ((1 / 2) - 0)) * t) + ((((1 / 2) * r1) - (0 * r2)) / ((1 / 2) - 0)) by A50, TREAL_1:11
.= (((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 A54: P1 . t is Point of I[01] by A48, Th3;
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:87;
hence h . (1,t) = f1 . (1,t) by A44, FUNCT_4:11
.= f . ([:(id I[01]),P1:] . (1,t)) by A53, FUNCT_1:13
.= f . (((id I[01]) . 1),(P1 . t)) by A29, A53, FUNCT_3:65
.= f . (1,(P1 . t)) by A21, FUNCT_1:18
.= b by A10, A54 ;
:: thesis: verum

end;

suppose A55: t >= 1 / 2 ; :: thesis: ( h . (0,t) = a & h . (1,t) = b )

reconsider r1 = (#) (0,1), r2 = (0,1) (#) as Real ;
t <= 1 by BORSUK_1:43;
then A56: t in the carrier of (Closed-Interval-TSpace ((1 / 2),1)) by A11, A55, XXREAL_1:1;
then A57: [1,t] in dom [:(id I[01]),P2:] by A30, A15, ZFMISC_1:87;
P2 . t = (((r2 - r1) / (1 - (1 / 2))) * t) + (((1 * r1) - ((1 / 2) * r2)) / (1 - (1 / 2))) by A56, TREAL_1:11
.= (((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 A58: P2 . t is Point of I[01] by A55, Th4;
P2 . t = (((r2 - r1) / (1 - (1 / 2))) * t) + (((1 * r1) - ((1 / 2) * r2)) / (1 - (1 / 2))) by A56, TREAL_1:11
.= (((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 A59: P2 . t is Point of I[01] by A55, Th4;
A60: 0 in the carrier of I[01] by BORSUK_1:43;
then A61: [0,t] in dom [:(id I[01]),P2:] by A30, A56, ZFMISC_1:87;
[0,t] in dom g1 by A20, A60, A56, ZFMISC_1:87;
hence h . (0,t) = g1 . (0,t) by A44, FUNCT_4:13
.= g . ([:(id I[01]),P2:] . (0,t)) by A61, FUNCT_1:13
.= g . (((id I[01]) . 0),(P2 . t)) by A28, A61, FUNCT_3:65
.= g . (0,(P2 . t)) by A22, FUNCT_1:18
.= a by A19, A59 ;
:: thesis: h . (1,t) = b
[1,t] in dom g1 by A20, A15, A56, ZFMISC_1:87;
hence h . (1,t) = g1 . (1,t) by A44, FUNCT_4:13
.= g . ([:(id I[01]),P2:] . (1,t)) by A57, FUNCT_1:13
.= g . (((id I[01]) . 1),(P2 . t)) by A28, A57, FUNCT_3:65
.= g . (1,(P2 . t)) by A21, FUNCT_1:18
.= b by A19, A58 ;
:: thesis: verum

end;

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 ;
let s be Point of I[01]; :: thesis: ( h . (s,0) = P . s & h . (s,1) = R . s )
( 1 = (0,1) (#) & 1 = ((1 / 2),1) (#) ) by TREAL_1:def 2;
then A62: P2 . 1 = 1 by TREAL_1:13;
A63: the carrier of (Closed-Interval-TSpace ((1 / 2),1)) = [.(1 / 2),1.] by TOPMETR:18;
then A64: 1 in the carrier of (Closed-Interval-TSpace ((1 / 2),1)) by XXREAL_1:1;
then A65: [s,1] in dom [:(id I[01]),P2:] by A30, ZFMISC_1:87;
[s,1] in dom g1 by A20, A64, ZFMISC_1:87;
then A66: h . (s,1) = g1 . (s,1) by A44, FUNCT_4:13
.= g . ([:(id I[01]),P2:] . (s,1)) by A65, FUNCT_1:13
.= g . (((id I[01]) . s),(P2 . 1)) by A28, A65, FUNCT_3:65
.= g . (s,1) by A62, FUNCT_1:18
.= R . s by A19 ;
A67: 0 in the carrier of (Closed-Interval-TSpace (0,(1 / 2))) by A6, XXREAL_1:1;
then A68: P1 . 0 = (((r2 - r1) / ((1 / 2) - 0)) * 0) + ((((1 / 2) * r1) - (0 * r2)) / ((1 / 2) - 0)) by TREAL_1:11
.= (((1 / 2) * 0) - (0 * r2)) / ((1 / 2) - 0) by TREAL_1:def 1 ;
A69: [s,0] in dom [:(id I[01]),P1:] by A27, A67, ZFMISC_1:87;
not 0 in the carrier of (Closed-Interval-TSpace ((1 / 2),1)) by A63, XXREAL_1:1;
then not [s,0] in dom g1 by A20, ZFMISC_1:87;
then h . (s,0) = f1 . (s,0) by A44, FUNCT_4:11
.= f . ([:(id I[01]),P1:] . (s,0)) by A69, FUNCT_1:13
.= f . (((id I[01]) . s),(P1 . 0)) by A29, A69, FUNCT_3:65
.= f . (s,0) by A68, FUNCT_1:18
.= P . s by A10 ;
hence ( h . (s,0) = P . s & h . (s,1) = R . s ) by A66; :: thesis: verum

end;

hence P,R are_homotopic by A45, A47; :: thesis: verum