let T be non empty TopSpace; :: thesis: for a, b being Point of T
for P, Q being Path of a,b st a,b are_connected & P,Q are_homotopic holds
- P, - Q are_homotopic
let a, b be Point of T; :: thesis: for P, Q being Path of a,b st a,b are_connected & P,Q are_homotopic holds
- P, - Q are_homotopic
reconsider fF = id I[01] as continuous Function of I[01] ,I[01] ;
reconsider fB = L[01] (0 ,1 (#) ),((#) 0 ,1) as continuous Function of I[01] ,I[01] by TOPMETR:27, TREAL_1:11;
let P, Q be Path of a,b; :: thesis: ( a,b are_connected & P,Q are_homotopic implies - P, - Q are_homotopic )
assume A1: a,b are_connected ; :: thesis: ( not P,Q are_homotopic or - P, - Q are_homotopic )
set F = [:fB,fF:];
A2: dom fB = the carrier of I[01] by FUNCT_2:def 1;
assume P,Q are_homotopic ; :: thesis: - P, - Q are_homotopic
then consider f being Function of [:I[01] ,I[01] :],T such that
A3: f is continuous and
A4: 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 BORSUK_2:def 7;
reconsider ff = f * [:fB,fF:] as Function of [:I[01] ,I[01] :],T ;
take ff ; :: according to BORSUK_2:def 7 :: thesis: ( ff is continuous & ( for b1 being Element of the carrier of I[01] holds
( ff . b1,0 = (- P) . b1 & ff . b1,1 = (- Q) . b1 & ff . 0 ,b1 = b & ff . 1,b1 = a ) ) )
[:fB,fF:] is continuous ;
hence ff is continuous by A3; :: thesis: for b1 being Element of the carrier of I[01] holds
( ff . b1,0 = (- P) . b1 & ff . b1,1 = (- Q) . b1 & ff . 0 ,b1 = b & ff . 1,b1 = a )
A5: 0 is Point of I[01] by BORSUK_1:86;
A6: for t being Point of I[01] holds
( ff . 0 ,t = b & ff . 1,t = a )
proof
A7: for t being Point of I[01]
for t9 being Real st t = t9 holds
fB . t = 1 - t9
proof
let t be Point of I[01] ; :: thesis: for t9 being Real st t = t9 holds
fB . t = 1 - t9
let t9 be Real; :: thesis: ( t = t9 implies fB . t = 1 - t9 )
assume A8: t = t9 ; :: thesis: fB . t = 1 - t9
reconsider ee = t as Point of (Closed-Interval-TSpace 0 ,1) by TOPMETR:27;
A9: ( 0 ,1 (#) = 1 & (#) 0 ,1 = 0 ) by TREAL_1:def 1, TREAL_1:def 2;
fB . t = fB . ee
.= ((0 - 1) * t9) + 1 by A8, A9, TREAL_1:10
.= 1 - (1 * t9) ;
hence fB . t = 1 - t9 ; :: thesis: verum
end;
then A10: fB . 0 = 1 - 0 by A5
.= 1 ;
1 is Point of I[01] by BORSUK_1:86;
then A11: fB . 1 = 1 - 1 by A7
.= 0 ;
let t be Point of I[01] ; :: thesis: ( ff . 0 ,t = b & ff . 1,t = a )
A12: dom fF = the carrier of I[01] by FUNCT_2:def 1;
t in the carrier of I[01] ;
then reconsider tt = t as Real by BORSUK_1:83;
A13: dom fB = the carrier of I[01] by FUNCT_2:def 1;
then A14: 0 in dom fB by BORSUK_1:86;
A15: dom [:fB,fF:] = [:(dom fB),(dom fF):] by FUNCT_3:def 9;
then A16: [0 ,t] in dom [:fB,fF:] by A12, A14, ZFMISC_1:106;
A17: 1 in dom fB by A13, BORSUK_1:86;
then A18: [1,t] in dom [:fB,fF:] by A12, A15, ZFMISC_1:106;
[:fB,fF:] . 1,t = [(fB . 1),(fF . t)] by A12, A17, FUNCT_3:def 9
.= [0 ,tt] by A11, FUNCT_1:35 ;
then A19: ff . 1,t = f . 0 ,t by A18, FUNCT_1:23
.= a by A4 ;
[:fB,fF:] . 0 ,t = [(fB . 0 ),(fF . t)] by A12, A14, FUNCT_3:def 9
.= [1,tt] by A10, FUNCT_1:35 ;
then ff . 0 ,t = f . 1,t by A16, FUNCT_1:23
.= b by A4 ;
hence ( ff . 0 ,t = b & ff . 1,t = a ) by A19; :: thesis: verum
end;
A20: dom fF = the carrier of I[01] by FUNCT_2:def 1;
for s being Point of I[01] holds
( ff . s,0 = (- P) . s & ff . s,1 = (- Q) . s )
proof
let s be Point of I[01] ; :: thesis: ( ff . s,0 = (- P) . s & ff . s,1 = (- Q) . s )
A21: for t being Point of I[01]
for t9 being Real st t = t9 holds
fB . t = 1 - t9
proof
let t be Point of I[01] ; :: thesis: for t9 being Real st t = t9 holds
fB . t = 1 - t9
let t9 be Real; :: thesis: ( t = t9 implies fB . t = 1 - t9 )
assume A22: t = t9 ; :: thesis: fB . t = 1 - t9
reconsider ee = t as Point of (Closed-Interval-TSpace 0 ,1) by TOPMETR:27;
A23: ( 0 ,1 (#) = 1 & (#) 0 ,1 = 0 ) by TREAL_1:def 1, TREAL_1:def 2;
fB . t = fB . ee
.= ((0 - 1) * t9) + 1 by A22, A23, TREAL_1:10
.= 1 - (1 * t9) ;
hence fB . t = 1 - t9 ; :: thesis: verum
end;
s is Real by XREAL_0:def 1;
then A24: fB . s = 1 - s by A21;
A25: 1 is Point of I[01] by BORSUK_1:86;
A26: dom [:fB,fF:] = [:(dom fB),(dom fF):] by FUNCT_3:def 9;
A27: 1 in dom fF by A20, BORSUK_1:86;
then A28: [s,1] in dom [:fB,fF:] by A2, A26, ZFMISC_1:106;
A29: 0 in dom fF by A20, BORSUK_1:86;
then A30: [s,0 ] in dom [:fB,fF:] by A2, A26, ZFMISC_1:106;
A31: 1 - s is Point of I[01] by JORDAN5B:4;
[:fB,fF:] . s,1 = [(fB . s),(fF . 1)] by A2, A27, FUNCT_3:def 9
.= [(1 - s),1] by A24, A25, FUNCT_1:35 ;
then A32: ff . s,1 = f . (1 - s),1 by A28, FUNCT_1:23
.= Q . (1 - s) by A4, A31
.= (- Q) . s by A1, BORSUK_2:def 6 ;
[:fB,fF:] . s,0 = [(fB . s),(fF . 0 )] by A2, A29, FUNCT_3:def 9
.= [(1 - s),0 ] by A5, A24, FUNCT_1:35 ;
then ff . s,0 = f . (1 - s),0 by A30, FUNCT_1:23
.= P . (1 - s) by A4, A31
.= (- P) . s by A1, BORSUK_2:def 6 ;
hence ( ff . s,0 = (- P) . s & ff . s,1 = (- Q) . s ) by A32; :: thesis: verum
end;
hence for b1 being Element of the carrier of I[01] holds
( ff . b1,0 = (- P) . b1 & ff . b1,1 = (- Q) . b1 & ff . 0 ,b1 = b & ff . 1,b1 = a ) by A6; :: thesis: verum