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