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:20, TREAL_1:8;
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 ) ) ) ;
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 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:43;
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:20;
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:7
.= 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:43;
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] ;
reconsider tt = t as Real ;
A13: dom fB = the carrier of I[01] by FUNCT_2:def 1;
then A14: 0 in dom fB by BORSUK_1:43;
A15: dom [:fB,fF:] = [:(dom fB),(dom fF):] by FUNCT_3:def 8;
then A16: [0,t] in dom [:fB,fF:] by A14, ZFMISC_1:87;
A17: 1 in dom fB by A13, BORSUK_1:43;
then A18: [1,t] in dom [:fB,fF:] by A15, ZFMISC_1:87;
[:fB,fF:] . (1,t) = [(fB . 1),(fF . t)] by A12, A17, FUNCT_3:def 8
.= [0,tt] by A11, FUNCT_1:18 ;
then A19: ff . (1,t) = f . (0,t) by A18, FUNCT_1:13
.= a by A4 ;
[:fB,fF:] . (0,t) = [(fB . 0),(fF . t)] by A12, A14, FUNCT_3:def 8
.= [1,tt] by A10, FUNCT_1:18 ;
then ff . (0,t) = f . (1,t) by A16, FUNCT_1:13
.= b by A4 ;
hence ( ff . (0,t) = b & ff . (1,t) = a ) by A19; :: thesis: verum
end;
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 )
A20: 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 A21: t = t9 ; :: thesis: fB . t = 1 - t9
reconsider ee = t as Point of (Closed-Interval-TSpace (0,1)) by TOPMETR:20;
A22: ( (0,1) (#) = 1 & (#) (0,1) = 0 ) by TREAL_1:def 1, TREAL_1:def 2;
fB . t = fB . ee
.= ((0 - 1) * t9) + 1 by A21, A22, TREAL_1:7
.= 1 - (1 * t9) ;
hence fB . t = 1 - t9 ; :: thesis: verum
end;
A23: fB . s = 1 - s by A20;
A24: 1 is Point of I[01] by BORSUK_1:43;
A25: dom [:fB,fF:] = [:(dom fB),(dom fF):] by FUNCT_3:def 8;
A26: 1 in dom fF by BORSUK_1:43;
then A27: [s,1] in dom [:fB,fF:] by A2, A25, ZFMISC_1:87;
A28: 0 in dom fF by BORSUK_1:43;
then A29: [s,0] in dom [:fB,fF:] by A2, A25, ZFMISC_1:87;
A30: 1 - s is Point of I[01] by JORDAN5B:4;
[:fB,fF:] . (s,1) = [(fB . s),(fF . 1)] by A2, A26, FUNCT_3:def 8
.= [(1 - s),1] by A23, A24, FUNCT_1:18 ;
then A31: ff . (s,1) = f . ((1 - s),1) by A27, FUNCT_1:13
.= Q . (1 - s) by A4, A30
.= (- Q) . s by A1, BORSUK_2:def 6 ;
[:fB,fF:] . (s,0) = [(fB . s),(fF . 0)] by A2, A28, FUNCT_3:def 8
.= [(1 - s),0] by A5, A23, FUNCT_1:18 ;
then ff . (s,0) = f . ((1 - s),0) by A29, FUNCT_1:13
.= P . (1 - s) by A4, A30
.= (- P) . s by A1, BORSUK_2:def 6 ;
hence ( ff . (s,0) = (- P) . s & ff . (s,1) = (- Q) . s ) by A31; :: 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