let T be non empty TopSpace; :: thesis: for c1, c2, c3, c4, c5, c6 being with_endpoints Curve of T st c1,c2 are_homotopic & dom c1 = dom c2 & c3,c4 are_homotopic & dom c3 = dom c4 & c5 = c1 + c3 & c6 = c2 + c4 & the_last_point_of c1 = the_first_point_of c3 & sup (dom c1) = inf (dom c3) holds
c5,c6 are_homotopic
let c1, c2, c3, c4, c5, c6 be with_endpoints Curve of T; :: thesis: ( c1,c2 are_homotopic & dom c1 = dom c2 & c3,c4 are_homotopic & dom c3 = dom c4 & c5 = c1 + c3 & c6 = c2 + c4 & the_last_point_of c1 = the_first_point_of c3 & sup (dom c1) = inf (dom c3) implies c5,c6 are_homotopic )
assume A1: ( c1,c2 are_homotopic & dom c1 = dom c2 ) ; :: thesis: ( not c3,c4 are_homotopic or not dom c3 = dom c4 or not c5 = c1 + c3 or not c6 = c2 + c4 or not the_last_point_of c1 = the_first_point_of c3 or not sup (dom c1) = inf (dom c3) or c5,c6 are_homotopic )
reconsider S1 = [.(inf (dom c1)),(sup (dom c1)).] as non empty Subset of R^1 by Th27, TOPMETR:17;
A2: dom c1 = S1 by Th27;
then consider H1 being Function of [:(R^1 | S1),I[01]:],T, a1, b1 being Point of T such that
A3: ( H1 is continuous & ( for t being Point of (R^1 | S1) holds
( H1 . (t,0) = c1 . t & H1 . (t,1) = c2 . t ) ) & ( for t being Point of I[01] holds
( H1 . ((inf S1),t) = a1 & H1 . ((sup S1),t) = b1 ) ) ) by A1, Th36;
assume A4: ( c3,c4 are_homotopic & dom c3 = dom c4 ) ; :: thesis: ( not c5 = c1 + c3 or not c6 = c2 + c4 or not the_last_point_of c1 = the_first_point_of c3 or not sup (dom c1) = inf (dom c3) or c5,c6 are_homotopic )
reconsider S2 = [.(inf (dom c3)),(sup (dom c3)).] as non empty Subset of R^1 by Th27, TOPMETR:17;
A5: dom c3 = S2 by Th27;
then consider H2 being Function of [:(R^1 | S2),I[01]:],T, a2, b2 being Point of T such that
A6: ( H2 is continuous & ( for t being Point of (R^1 | S2) holds
( H2 . (t,0) = c3 . t & H2 . (t,1) = c4 . t ) ) & ( for t being Point of I[01] holds
( H2 . ((inf S2),t) = a2 & H2 . ((sup S2),t) = b2 ) ) ) by A4, Th36;
assume A7: c5 = c1 + c3 ; :: thesis: ( not c6 = c2 + c4 or not the_last_point_of c1 = the_first_point_of c3 or not sup (dom c1) = inf (dom c3) or c5,c6 are_homotopic )
A8: c5 = c1 \/ c3
proof
per cases ( c1 \/ c3 is Curve of T or not c1 \/ c3 is Curve of T ) ;
suppose c1 \/ c3 is Curve of T ; :: thesis: c5 = c1 \/ c3
hence c5 = c1 \/ c3 by A7, Def12; :: thesis: verum
end;
suppose c1 \/ c3 is not Curve of T ; :: thesis: c5 = c1 \/ c3
hence c5 = c1 \/ c3 by A7, Def12; :: thesis: verum
end;
end;
end;
assume A9: c6 = c2 + c4 ; :: thesis: ( not the_last_point_of c1 = the_first_point_of c3 or not sup (dom c1) = inf (dom c3) or c5,c6 are_homotopic )
A10: c6 = c2 \/ c4
proof
per cases ( c2 \/ c4 is Curve of T or not c2 \/ c4 is Curve of T ) ;
suppose c2 \/ c4 is Curve of T ; :: thesis: c6 = c2 \/ c4
hence c6 = c2 \/ c4 by A9, Def12; :: thesis: verum
end;
suppose c2 \/ c4 is not Curve of T ; :: thesis: c6 = c2 \/ c4
hence c6 = c2 \/ c4 by A9, Def12; :: thesis: verum
end;
end;
end;
assume A11: the_last_point_of c1 = the_first_point_of c3 ; :: thesis: ( not sup (dom c1) = inf (dom c3) or c5,c6 are_homotopic )
assume A12: sup (dom c1) = inf (dom c3) ; :: thesis: c5,c6 are_homotopic
A13: dom c5 = (dom c1) \/ (dom c3) by A8, XTUPLE_0:23
.= dom c6 by A10, A1, A4, XTUPLE_0:23 ;
reconsider S3 = S1 \/ S2 as Subset of R^1 ;
A14: dom c5 = (dom c1) \/ (dom c3) by A8, XTUPLE_0:23
.= S3 by A5, Th27 ;
set T1 = [:(R^1 | S1),I[01]:];
set T2 = [:(R^1 | S2),I[01]:];
set T3 = [:(R^1 | S3),I[01]:];
A15: I[01] is SubSpace of I[01] by TSEP_1:2;
R^1 | S1 is SubSpace of R^1 | S3 by TOPMETR:4;
then A16: [:(R^1 | S1),I[01]:] is SubSpace of [:(R^1 | S3),I[01]:] by A15, BORSUK_3:21;
R^1 | S2 is SubSpace of R^1 | S3 by TOPMETR:4;
then A17: [:(R^1 | S2),I[01]:] is SubSpace of [:(R^1 | S3),I[01]:] by A15, BORSUK_3:21;
A18: ([#] (R^1 | S1)) \/ ([#] (R^1 | S2)) = S1 \/ ([#] (R^1 | S2)) by PRE_TOPC:def 5
.= S3 by PRE_TOPC:def 5
.= [#] (R^1 | S3) by PRE_TOPC:def 5 ;
A19: ([#] [:(R^1 | S1),I[01]:]) \/ ([#] [:(R^1 | S2),I[01]:]) = [:([#] (R^1 | S1)),([#] I[01]):] \/ ([#] [:(R^1 | S2),I[01]:]) by BORSUK_1:def 2
.= [:([#] (R^1 | S1)),([#] I[01]):] \/ [:([#] (R^1 | S2)),([#] I[01]):] by BORSUK_1:def 2
.= [:([#] (R^1 | S3)),([#] I[01]):] by A18, ZFMISC_1:97
.= [#] [:(R^1 | S3),I[01]:] by BORSUK_1:def 2 ;
A20: inf (dom c1) <= sup (dom c1) by XXREAL_2:40;
R^1 | S1 = Closed-Interval-TSpace ((inf (dom c1)),(sup (dom c1))) by A20, TOPMETR:19;
then A21: R^1 | S1 is compact by A20, HEINE:4;
A22: inf (dom c3) <= sup (dom c3) by XXREAL_2:40;
R^1 | S2 = Closed-Interval-TSpace ((inf (dom c3)),(sup (dom c3))) by A22, TOPMETR:19;
then A23: R^1 | S2 is compact by A22, HEINE:4;
[:(R^1 | S3),I[01]:] is SubSpace of [:R^1,I[01]:] by A15, BORSUK_3:21;
then A24: [:(R^1 | S3),I[01]:] is T_2 by TOPMETR:2;
for p being set st p in ([#] [:(R^1 | S1),I[01]:]) /\ ([#] [:(R^1 | S2),I[01]:]) holds
H1 . p = H2 . p
proof
let p be set ; :: thesis: ( p in ([#] [:(R^1 | S1),I[01]:]) /\ ([#] [:(R^1 | S2),I[01]:]) implies H1 . p = H2 . p )
assume A25: p in ([#] [:(R^1 | S1),I[01]:]) /\ ([#] [:(R^1 | S2),I[01]:]) ; :: thesis: H1 . p = H2 . p
A26: ([#] [:(R^1 | S1),I[01]:]) /\ ([#] [:(R^1 | S2),I[01]:]) = [:([#] (R^1 | S1)),([#] I[01]):] /\ ([#] [:(R^1 | S2),I[01]:]) by BORSUK_1:def 2
.= [:([#] (R^1 | S1)),([#] I[01]):] /\ [:([#] (R^1 | S2)),([#] I[01]):] by BORSUK_1:def 2
.= [:(([#] (R^1 | S1)) /\ ([#] (R^1 | S2))),([#] I[01]):] by ZFMISC_1:99 ;
A27: ([#] (R^1 | S1)) /\ ([#] (R^1 | S2)) = S1 /\ ([#] (R^1 | S2)) by PRE_TOPC:def 5
.= S1 /\ S2 by PRE_TOPC:def 5 ;
A28: S1 /\ S2 = {(sup (dom c1))} by A22, A20, A12, XXREAL_1:418;
then consider x, y being object such that
A29: ( x in {(sup (dom c1))} & y in [#] I[01] & p = [x,y] ) by A25, A27, A26, ZFMISC_1:def 2;
reconsider y = y as Point of I[01] by A29;
A30: x = sup S1 by A2, A29, TARSKI:def 1;
A31: x = inf S2 by A5, A12, A29, TARSKI:def 1;
A32: 0 in [#] I[01] by BORSUK_1:40, XXREAL_1:1;
A33: sup S1 in [#] (R^1 | S1) by A30, A27, A28, A29, XBOOLE_0:def 4;
thus H1 . p = H1 . ((sup S1),y) by A29, A30, BINOP_1:def 1
.= b1 by A3
.= H1 . ((sup S1),0) by A3, A32
.= the_last_point_of c1 by A2, A3, A33
.= H2 . ((inf S2),0) by A6, A31, A27, A28, A29, A11, A5
.= a2 by A32, A6
.= H2 . ((inf S2),y) by A6
.= H2 . p by A29, A30, A2, A5, A12, BINOP_1:def 1 ; :: thesis: verum
end;
then consider H3 being Function of [:(R^1 | S3),I[01]:],T such that
A34: ( H3 = H1 +* H2 & H3 is continuous ) by A16, A17, A19, A21, A23, A24, A3, A6, BORSUK_2:1;
A35: for t being Point of (R^1 | S3) holds
( H3 . (t,0) = c5 . t & H3 . (t,1) = c6 . t )
proof
let t be Point of (R^1 | S3); :: thesis: ( H3 . (t,0) = c5 . t & H3 . (t,1) = c6 . t )
A36: 0 in [#] I[01] by BORSUK_1:40, XXREAL_1:1;
then [t,0] in [:([#] (R^1 | S3)),([#] I[01]):] by ZFMISC_1:def 2;
then [t,0] in [#] [:(R^1 | S3),I[01]:] ;
then [t,0] in dom H3 by FUNCT_2:def 1;
then A37: [t,0] in (dom H1) \/ (dom H2) by A34, FUNCT_4:def 1;
A38: 1 in [#] I[01] by BORSUK_1:40, XXREAL_1:1;
then [t,1] in [:([#] (R^1 | S3)),([#] I[01]):] by ZFMISC_1:def 2;
then [t,1] in [#] [:(R^1 | S3),I[01]:] ;
then [t,1] in dom H3 by FUNCT_2:def 1;
then A39: [t,1] in (dom H1) \/ (dom H2) by A34, FUNCT_4:def 1;
per cases ( [t,0] in dom H2 or not [t,0] in dom H2 ) ;
suppose A40: [t,0] in dom H2 ; :: thesis: ( H3 . (t,0) = c5 . t & H3 . (t,1) = c6 . t )
then [t,0] in [#] [:(R^1 | S2),I[01]:] ;
then [t,0] in [:([#] (R^1 | S2)),([#] I[01]):] by BORSUK_1:def 2;
then A41: t in [#] (R^1 | S2) by ZFMISC_1:87;
then A42: t in dom c3 by A5, PRE_TOPC:def 5;
then t in (dom c1) \/ (dom c3) by XBOOLE_0:def 3;
then A43: t in dom c5 by A8, XTUPLE_0:23;
[t,(c3 . t)] in c3 by A42, FUNCT_1:1;
then A44: [t,(c3 . t)] in c5 by A8, XBOOLE_0:def 3;
thus H3 . (t,0) = H3 . [t,0] by BINOP_1:def 1
.= H2 . [t,0] by A37, A40, A34, FUNCT_4:def 1
.= H2 . (t,0) by BINOP_1:def 1
.= c3 . t by A6, A41
.= c5 . t by A44, A43, FUNCT_1:def 2 ; :: thesis: H3 . (t,1) = c6 . t
[t,1] in [:([#] (R^1 | S2)),([#] I[01]):] by A41, A38, ZFMISC_1:def 2;
then [t,1] in [#] [:(R^1 | S2),I[01]:] ;
then A45: [t,1] in dom H2 by FUNCT_2:def 1;
t in (dom c2) \/ (dom c4) by A42, A4, XBOOLE_0:def 3;
then A46: t in dom c6 by A10, XTUPLE_0:23;
[t,(c4 . t)] in c4 by A42, A4, FUNCT_1:1;
then A47: [t,(c4 . t)] in c6 by A10, XBOOLE_0:def 3;
thus H3 . (t,1) = H3 . [t,1] by BINOP_1:def 1
.= H2 . [t,1] by A39, A45, A34, FUNCT_4:def 1
.= H2 . (t,1) by BINOP_1:def 1
.= c4 . t by A6, A41
.= c6 . t by A47, A46, FUNCT_1:def 2 ; :: thesis: verum
end;
suppose A48: not [t,0] in dom H2 ; :: thesis: ( H3 . (t,0) = c5 . t & H3 . (t,1) = c6 . t )
( [t,0] in dom H1 or [t,0] in dom H2 ) by A37, XBOOLE_0:def 3;
then [t,0] in [#] [:(R^1 | S1),I[01]:] by A48;
then [t,0] in [:([#] (R^1 | S1)),([#] I[01]):] by BORSUK_1:def 2;
then A49: t in [#] (R^1 | S1) by ZFMISC_1:87;
then A50: t in dom c1 by A2, PRE_TOPC:def 5;
then t in (dom c1) \/ (dom c3) by XBOOLE_0:def 3;
then A51: t in dom c5 by A8, XTUPLE_0:23;
[t,(c1 . t)] in c1 by A50, FUNCT_1:1;
then A52: [t,(c1 . t)] in c5 by A8, XBOOLE_0:def 3;
thus H3 . (t,0) = H3 . [t,0] by BINOP_1:def 1
.= H1 . [t,0] by A48, A37, A34, FUNCT_4:def 1
.= H1 . (t,0) by BINOP_1:def 1
.= c1 . t by A3, A49
.= c5 . t by A52, A51, FUNCT_1:def 2 ; :: thesis: H3 . (t,1) = c6 . t
t in (dom c2) \/ (dom c4) by A50, A1, XBOOLE_0:def 3;
then A53: t in dom c6 by A10, XTUPLE_0:23;
[t,(c2 . t)] in c2 by A50, A1, FUNCT_1:1;
then A54: [t,(c2 . t)] in c6 by A10, XBOOLE_0:def 3;
A55: not [t,1] in dom H2 thus H3 . (t,1) = H3 . [t,1] by BINOP_1:def 1
.= H1 . [t,1] by A55, A39, A34, FUNCT_4:def 1
.= H1 . (t,1) by BINOP_1:def 1
.= c2 . t by A3, A49
.= c6 . t by A54, A53, FUNCT_1:def 2 ; :: thesis: verum
end;
end;
end;
for t being Point of I[01] holds
( H3 . ((inf S3),t) = a1 & H3 . ((sup S3),t) = b2 )
proof
let t be Point of I[01]; :: thesis: ( H3 . ((inf S3),t) = a1 & H3 . ((sup S3),t) = b2 )
A56: inf S1 = inf (dom c1) by Th27
.= inf [.(inf (dom c1)),(sup (dom c3)).] by A22, A20, A12, XXREAL_0:2, XXREAL_2:25
.= inf S3 by A22, A20, A12, XXREAL_1:165 ;
inf S1 in S1 by A2, A20, XXREAL_1:1;
then inf S1 in [#] (R^1 | S1) by PRE_TOPC:def 5;
then [(inf S1),t] in [:([#] (R^1 | S1)),([#] I[01]):] by ZFMISC_1:def 2;
then [(inf S1),t] in [#] [:(R^1 | S1),I[01]:] ;
then [(inf S1),t] in dom H1 by FUNCT_2:def 1;
then A57: [(inf S3),t] in (dom H1) \/ (dom H2) by A56, XBOOLE_0:def 3;
thus H3 . ((inf S3),t) = a1 :: thesis: H3 . ((sup S3),t) = b2
proof
per cases ( [(inf S3),t] in dom H2 or not [(inf S3),t] in dom H2 ) ;
suppose A58: [(inf S3),t] in dom H2 ; :: thesis: H3 . ((inf S3),t) = a1
then [(inf S3),t] in [#] [:(R^1 | S2),I[01]:] ;
then [(inf S3),t] in [:([#] (R^1 | S2)),([#] I[01]):] by BORSUK_1:def 2;
then inf S3 in [#] (R^1 | S2) by ZFMISC_1:87;
then inf S3 in S2 by PRE_TOPC:def 5;
then ( inf (dom c3) <= inf S1 & inf S1 <= sup (dom c3) ) by A56, XXREAL_1:1;
then A59: inf (dom c3) <= inf (dom c1) by Th27;
A60: inf (dom c3) = inf (dom c1) by A59, A12, A20, XXREAL_0:1;
A61: inf S2 = inf (dom c3) by Th27
.= inf S1 by A60, Th27 ;
A62: inf S1 = inf (dom c1) by Th27
.= inf (dom c3) by A59, A12, A20, XXREAL_0:1
.= sup S1 by A12, Th27 ;
A63: 0 in [#] I[01] by BORSUK_1:40, XXREAL_1:1;
sup (dom c1) = sup S1 by Th27;
then sup S1 in S1 by A20, XXREAL_1:1;
then A64: sup S1 in [#] (R^1 | S1) by PRE_TOPC:def 5;
inf (dom c3) = inf S2 by Th27;
then inf S2 in S2 by A22, XXREAL_1:1;
then A65: inf S2 in [#] (R^1 | S2) by PRE_TOPC:def 5;
A66: sup S1 = sup (dom c1) by Th27;
A67: inf S2 = inf (dom c3) by Th27;
A68: a1 = H1 . ((inf S1),0) by A3, A63
.= the_last_point_of c1 by A66, A62, A64, A3
.= H2 . ((inf S2),0) by A65, A6, A67, A11
.= a2 by A6, A63 ;
H3 . ((inf S3),t) = H3 . [(inf S3),t] by BINOP_1:def 1
.= H2 . [(inf S3),t] by A57, A58, A34, FUNCT_4:def 1
.= H2 . ((inf S2),t) by A56, A61, BINOP_1:def 1
.= a1 by A6, A68 ;
hence H3 . ((inf S3),t) = a1 ; :: thesis: verum
end;
suppose A69: not [(inf S3),t] in dom H2 ; :: thesis: H3 . ((inf S3),t) = a1
H3 . ((inf S3),t) = H3 . [(inf S3),t] by BINOP_1:def 1
.= H1 . [(inf S3),t] by A57, A69, A34, FUNCT_4:def 1
.= H1 . ((inf S3),t) by BINOP_1:def 1
.= a1 by A56, A3 ;
hence H3 . ((inf S3),t) = a1 ; :: thesis: verum
end;
end;
end;
A70: sup S2 = sup (dom c3) by Th27
.= sup [.(inf (dom c1)),(sup (dom c3)).] by A22, A20, A12, XXREAL_0:2, XXREAL_2:29
.= sup S3 by A22, A20, A12, XXREAL_1:165 ;
sup S2 in S2 by A5, A22, XXREAL_1:1;
then sup S2 in [#] (R^1 | S2) by PRE_TOPC:def 5;
then [(sup S2),t] in [:([#] (R^1 | S2)),([#] I[01]):] by ZFMISC_1:def 2;
then A71: [(sup S2),t] in [#] [:(R^1 | S2),I[01]:] ;
then [(sup S2),t] in dom H2 by FUNCT_2:def 1;
then A72: [(sup S3),t] in (dom H1) \/ (dom H2) by A70, XBOOLE_0:def 3;
A73: [(sup S3),t] in dom H2 by A71, A70, FUNCT_2:def 1;
H3 . ((sup S3),t) = H3 . [(sup S3),t] by BINOP_1:def 1
.= H2 . [(sup S3),t] by A72, A73, A34, FUNCT_4:def 1
.= H2 . ((sup S2),t) by A70, BINOP_1:def 1
.= b2 by A6 ;
hence H3 . ((sup S3),t) = b2 ; :: thesis: verum
end;
hence c5,c6 are_homotopic by A13, A14, A35, A34, Th36; :: thesis: verum