let T be non empty TopSpace; for a, b, c being Point of T
for P1, P2 being Path of a,b
for Q1, Q2 being Path of b,c st a,b are_connected & b,c are_connected & P1,P2 are_homotopic & Q1,Q2 are_homotopic holds
P1 + Q1,P2 + Q2 are_homotopic
let a, b, c be Point of T; for P1, P2 being Path of a,b
for Q1, Q2 being Path of b,c st a,b are_connected & b,c are_connected & P1,P2 are_homotopic & Q1,Q2 are_homotopic holds
P1 + Q1,P2 + Q2 are_homotopic
set BB = [:I[01],I[01]:];
reconsider R1 = L[01] (0,(1 / 2),0,1) as continuous Function of (Closed-Interval-TSpace (0,(1 / 2))),I[01] by Th38, TOPMETR:20;
let P1, P2 be Path of a,b; for Q1, Q2 being Path of b,c st a,b are_connected & b,c are_connected & P1,P2 are_homotopic & Q1,Q2 are_homotopic holds
P1 + Q1,P2 + Q2 are_homotopic
let Q1, Q2 be Path of b,c; ( a,b are_connected & b,c are_connected & P1,P2 are_homotopic & Q1,Q2 are_homotopic implies P1 + Q1,P2 + Q2 are_homotopic )
assume that
A1:
( a,b are_connected & b,c are_connected )
and
A2:
P1,P2 are_homotopic
and
A3:
Q1,Q2 are_homotopic
; P1 + Q1,P2 + Q2 are_homotopic
reconsider R2 = L[01] ((1 / 2),1,0,1) as continuous Function of (Closed-Interval-TSpace ((1 / 2),1)),I[01] by Th38, TOPMETR:20;
A4:
1 is Point of I[01]
by BORSUK_1:43;
A5:
0 is Point of I[01]
by BORSUK_1:43;
then reconsider A01 = [.0,1.] as non empty Subset of I[01] by A4, BORSUK_4:24;
A6:
1 / 2 is Point of I[01]
by BORSUK_1:43;
then reconsider B01 = [.0,(1 / 2).] as non empty Subset of I[01] by A5, BORSUK_4:24;
reconsider N2 = [:[.(1 / 2),1.],[.0,1.]:] as non empty compact Subset of [:I[01],I[01]:] by A5, A4, A6, Th13;
reconsider N1 = [:[.0,(1 / 2).],[.0,1.]:] as non empty compact Subset of [:I[01],I[01]:] by A5, A4, A6, Th13;
set T1 = [:I[01],I[01]:] | N1;
set T2 = [:I[01],I[01]:] | N2;
A01 = [#] I[01]
by BORSUK_1:40;
then A7:
I[01] = I[01] | A01
by TSEP_1:93;
set f1 = [:R1,(id I[01]):];
set g1 = [:R2,(id I[01]):];
reconsider f1 = [:R1,(id I[01]):] as continuous Function of [:(Closed-Interval-TSpace (0,(1 / 2))),I[01]:],[:I[01],I[01]:] ;
reconsider g1 = [:R2,(id I[01]):] as continuous Function of [:(Closed-Interval-TSpace ((1 / 2),1)),I[01]:],[:I[01],I[01]:] ;
A8: dom g1 =
the carrier of [:(Closed-Interval-TSpace ((1 / 2),1)),I[01]:]
by FUNCT_2:def 1
.=
[: the carrier of (Closed-Interval-TSpace ((1 / 2),1)), the carrier of I[01]:]
by BORSUK_1:def 2
;
reconsider B02 = [.(1 / 2),1.] as non empty Subset of I[01] by A4, A6, BORSUK_4:24;
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) = P1 . s & f . (s,1) = P2 . s & ( for t being Point of I[01] holds
( f . (0,t) = a & f . (1,t) = b ) ) )
by A2, BORSUK_2:def 7;
Closed-Interval-TSpace (0,(1 / 2)) = I[01] | B01
by TOPMETR:24;
then
[:I[01],I[01]:] | N1 = [:(Closed-Interval-TSpace (0,(1 / 2))),I[01]:]
by A7, BORSUK_3:22;
then reconsider K1 = f * f1 as continuous Function of ([:I[01],I[01]:] | N1),T by A9;
consider g being Function of [:I[01],I[01]:],T such that
A11:
g is continuous
and
A12:
for s being Point of I[01] holds
( g . (s,0) = Q1 . s & g . (s,1) = Q2 . s & ( for t being Point of I[01] holds
( g . (0,t) = b & g . (1,t) = c ) ) )
by A3, BORSUK_2:def 7;
Closed-Interval-TSpace ((1 / 2),1) = I[01] | B02
by TOPMETR:24;
then
[:I[01],I[01]:] | N2 = [:(Closed-Interval-TSpace ((1 / 2),1)),I[01]:]
by A7, BORSUK_3:22;
then reconsider K2 = g * g1 as continuous Function of ([:I[01],I[01]:] | N2),T by A11;
A13: dom K2 =
the carrier of [:(Closed-Interval-TSpace ((1 / 2),1)),I[01]:]
by FUNCT_2:def 1
.=
[: the carrier of (Closed-Interval-TSpace ((1 / 2),1)), the carrier of I[01]:]
by BORSUK_1:def 2
;
A14:
for p being set st p in ([#] ([:I[01],I[01]:] | N1)) /\ ([#] ([:I[01],I[01]:] | N2)) holds
K1 . p = K2 . p
proof
A15:
R2 . (1 / 2) = 0
by Th37;
let p be
set ;
( p in ([#] ([:I[01],I[01]:] | N1)) /\ ([#] ([:I[01],I[01]:] | N2)) implies K1 . p = K2 . p )
A16:
R1 . (1 / 2) = 1
by Th37;
assume
p in ([#] ([:I[01],I[01]:] | N1)) /\ ([#] ([:I[01],I[01]:] | N2))
;
K1 . p = K2 . p
then
p in [:{(1 / 2)},[.0,1.]:]
by Th33;
then consider x,
y being
set such that A17:
x in {(1 / 2)}
and A18:
y in [.0,1.]
and A19:
p = [x,y]
by ZFMISC_1:def 2;
A20:
y in the
carrier of
I[01]
by A18, TOPMETR:18, TOPMETR:20;
reconsider y =
y as
Point of
I[01] by A18, TOPMETR:18, TOPMETR:20;
A21:
y in dom (id I[01])
by A20, FUNCT_2:def 1;
A22:
x = 1
/ 2
by A17, TARSKI:def 1;
then
x in [.(1 / 2),1.]
by XXREAL_1:1;
then A23:
x in the
carrier of
(Closed-Interval-TSpace ((1 / 2),1))
by TOPMETR:18;
then
p in [: the carrier of (Closed-Interval-TSpace ((1 / 2),1)), the carrier of I[01]:]
by A19, A20, ZFMISC_1:87;
then
p in the
carrier of
[:(Closed-Interval-TSpace ((1 / 2),1)),I[01]:]
by BORSUK_1:def 2;
then A24:
p in dom g1
by FUNCT_2:def 1;
x in [.0,(1 / 2).]
by A22, XXREAL_1:1;
then A25:
x in the
carrier of
(Closed-Interval-TSpace (0,(1 / 2)))
by TOPMETR:18;
then
x in dom R1
by FUNCT_2:def 1;
then A26:
[x,y] in [:(dom R1),(dom (id I[01])):]
by A21, ZFMISC_1:87;
x in dom R2
by A23, FUNCT_2:def 1;
then A27:
[x,y] in [:(dom R2),(dom (id I[01])):]
by A21, ZFMISC_1:87;
p in [: the carrier of (Closed-Interval-TSpace (0,(1 / 2))), the carrier of I[01]:]
by A19, A20, A25, ZFMISC_1:87;
then
p in the
carrier of
[:(Closed-Interval-TSpace (0,(1 / 2))),I[01]:]
by BORSUK_1:def 2;
then
p in dom f1
by FUNCT_2:def 1;
then K1 . p =
f . (f1 . (x,y))
by A19, FUNCT_1:13
.=
f . (
(R1 . x),
((id I[01]) . y))
by A26, FUNCT_3:65
.=
b
by A10, A22, A16
.=
g . (
(R2 . x),
((id I[01]) . y))
by A12, A22, A15
.=
g . (g1 . (x,y))
by A27, FUNCT_3:65
.=
K2 . p
by A19, A24, FUNCT_1:13
;
hence
K1 . p = K2 . p
;
verum
end;
([#] ([:I[01],I[01]:] | N1)) \/ ([#] ([:I[01],I[01]:] | N2)) = [#] [:I[01],I[01]:]
by Th32;
then consider h being Function of [:I[01],I[01]:],T such that
A28:
h = K1 +* K2
and
A29:
h is continuous
by A14, BORSUK_2:1;
A30: dom f1 =
the carrier of [:(Closed-Interval-TSpace (0,(1 / 2))),I[01]:]
by FUNCT_2:def 1
.=
[: the carrier of (Closed-Interval-TSpace (0,(1 / 2))), the carrier of I[01]:]
by BORSUK_1:def 2
;
A31:
for s being Point of I[01] holds
( h . (s,0) = (P1 + Q1) . s & h . (s,1) = (P2 + Q2) . s )
proof
let s be
Point of
I[01];
( h . (s,0) = (P1 + Q1) . s & h . (s,1) = (P2 + Q2) . s )
A32:
h . (
s,1)
= (P2 + Q2) . s
proof
per cases
( s < 1 / 2 or s >= 1 / 2 )
;
suppose A33:
s < 1
/ 2
;
h . (s,1) = (P2 + Q2) . sthen A34:
2
* s is
Point of
I[01]
by Th6;
A35:
1
in the
carrier of
I[01]
by BORSUK_1:43;
then A36:
1
in dom (id I[01])
by FUNCT_2:def 1;
A37:
s >= 0
by BORSUK_1:43;
then A38:
R1 . s =
(((1 - 0) / ((1 / 2) - 0)) * (s - 0)) + 0
by A33, Th39
.=
2
* s
;
s in [.0,(1 / 2).]
by A33, A37, XXREAL_1:1;
then A39:
s in the
carrier of
(Closed-Interval-TSpace (0,(1 / 2)))
by TOPMETR:18;
then A40:
[s,1] in dom f1
by A30, A35, ZFMISC_1:87;
s in dom R1
by A39, FUNCT_2:def 1;
then A41:
[s,1] in [:(dom R1),(dom (id I[01])):]
by A36, ZFMISC_1:87;
not
s in [.(1 / 2),1.]
by A33, XXREAL_1:1;
then
not
s in the
carrier of
(Closed-Interval-TSpace ((1 / 2),1))
by TOPMETR:18;
then
not
[s,1] in dom K2
by A13, ZFMISC_1:87;
then h . (
s,1) =
K1 . (
s,1)
by A28, FUNCT_4:11
.=
f . (f1 . (s,1))
by A40, FUNCT_1:13
.=
f . (
(R1 . s),
((id I[01]) . 1))
by A41, FUNCT_3:65
.=
f . (
(2 * s),1)
by A4, A38, FUNCT_1:18
.=
P2 . (2 * s)
by A10, A34
;
hence
h . (
s,1)
= (P2 + Q2) . s
by A1, A33, BORSUK_2:def 5;
verum end; suppose A42:
s >= 1
/ 2
;
h . (s,1) = (P2 + Q2) . sA43:
s <= 1
by BORSUK_1:43;
then A44:
R2 . s =
(((1 - 0) / (1 - (1 / 2))) * (s - (1 / 2))) + 0
by A42, Th39
.=
(2 * s) - 1
;
A45:
(2 * s) - 1 is
Point of
I[01]
by A42, Th7;
A46:
1
in the
carrier of
I[01]
by BORSUK_1:43;
then A47:
1
in dom (id I[01])
by FUNCT_2:def 1;
s in [.(1 / 2),1.]
by A42, A43, XXREAL_1:1;
then A48:
s in the
carrier of
(Closed-Interval-TSpace ((1 / 2),1))
by TOPMETR:18;
then A49:
[s,1] in dom g1
by A8, A46, ZFMISC_1:87;
s in dom R2
by A48, FUNCT_2:def 1;
then A50:
[s,1] in [:(dom R2),(dom (id I[01])):]
by A47, ZFMISC_1:87;
[s,1] in dom K2
by A13, A48, A46, ZFMISC_1:87;
then h . (
s,1) =
K2 . (
s,1)
by A28, FUNCT_4:13
.=
g . (g1 . (s,1))
by A49, FUNCT_1:13
.=
g . (
(R2 . s),
((id I[01]) . 1))
by A50, FUNCT_3:65
.=
g . (
((2 * s) - 1),1)
by A4, A44, FUNCT_1:18
.=
Q2 . ((2 * s) - 1)
by A12, A45
;
hence
h . (
s,1)
= (P2 + Q2) . s
by A1, A42, BORSUK_2:def 5;
verum end;
end;
h . (
s,
0)
= (P1 + Q1) . s
proof
per cases
( s < 1 / 2 or s >= 1 / 2 )
;
suppose A51:
s < 1
/ 2
;
h . (s,0) = (P1 + Q1) . sthen A52:
2
* s is
Point of
I[01]
by Th6;
A53:
0 in the
carrier of
I[01]
by BORSUK_1:43;
then A54:
0 in dom (id I[01])
by FUNCT_2:def 1;
A55:
s >= 0
by BORSUK_1:43;
then A56:
R1 . s =
(((1 - 0) / ((1 / 2) - 0)) * (s - 0)) + 0
by A51, Th39
.=
2
* s
;
s in [.0,(1 / 2).]
by A51, A55, XXREAL_1:1;
then A57:
s in the
carrier of
(Closed-Interval-TSpace (0,(1 / 2)))
by TOPMETR:18;
then A58:
[s,0] in dom f1
by A30, A53, ZFMISC_1:87;
s in dom R1
by A57, FUNCT_2:def 1;
then A59:
[s,0] in [:(dom R1),(dom (id I[01])):]
by A54, ZFMISC_1:87;
not
s in [.(1 / 2),1.]
by A51, XXREAL_1:1;
then
not
s in the
carrier of
(Closed-Interval-TSpace ((1 / 2),1))
by TOPMETR:18;
then
not
[s,0] in dom K2
by A13, ZFMISC_1:87;
then h . (
s,
0) =
K1 . (
s,
0)
by A28, FUNCT_4:11
.=
f . (f1 . (s,0))
by A58, FUNCT_1:13
.=
f . (
(R1 . s),
((id I[01]) . 0))
by A59, FUNCT_3:65
.=
f . (
(2 * s),
0)
by A5, A56, FUNCT_1:18
.=
P1 . (2 * s)
by A10, A52
;
hence
h . (
s,
0)
= (P1 + Q1) . s
by A1, A51, BORSUK_2:def 5;
verum end; suppose A60:
s >= 1
/ 2
;
h . (s,0) = (P1 + Q1) . sA61:
s <= 1
by BORSUK_1:43;
then A62:
R2 . s =
(((1 - 0) / (1 - (1 / 2))) * (s - (1 / 2))) + 0
by A60, Th39
.=
(2 * s) - 1
;
A63:
(2 * s) - 1 is
Point of
I[01]
by A60, Th7;
A64:
0 in the
carrier of
I[01]
by BORSUK_1:43;
then A65:
0 in dom (id I[01])
by FUNCT_2:def 1;
s in [.(1 / 2),1.]
by A60, A61, XXREAL_1:1;
then A66:
s in the
carrier of
(Closed-Interval-TSpace ((1 / 2),1))
by TOPMETR:18;
then A67:
[s,0] in dom g1
by A8, A64, ZFMISC_1:87;
s in dom R2
by A66, FUNCT_2:def 1;
then A68:
[s,0] in [:(dom R2),(dom (id I[01])):]
by A65, ZFMISC_1:87;
[s,0] in dom K2
by A13, A66, A64, ZFMISC_1:87;
then h . (
s,
0) =
K2 . (
s,
0)
by A28, FUNCT_4:13
.=
g . (g1 . (s,0))
by A67, FUNCT_1:13
.=
g . (
(R2 . s),
((id I[01]) . 0))
by A68, FUNCT_3:65
.=
g . (
((2 * s) - 1),
0)
by A5, A62, FUNCT_1:18
.=
Q1 . ((2 * s) - 1)
by A12, A63
;
hence
h . (
s,
0)
= (P1 + Q1) . s
by A1, A60, BORSUK_2:def 5;
verum end;
end;
hence
(
h . (
s,
0)
= (P1 + Q1) . s &
h . (
s,1)
= (P2 + Q2) . s )
by A32;
verum
end;
take
h
; BORSUK_2:def 7 ( h is continuous & ( for b1 being Element of the carrier of I[01] holds
( h . (b1,0) = (P1 + Q1) . b1 & h . (b1,1) = (P2 + Q2) . b1 & h . (0,b1) = a & h . (1,b1) = c ) ) )
for t being Point of I[01] holds
( h . (0,t) = a & h . (1,t) = c )
proof
let t be
Point of
I[01];
( h . (0,t) = a & h . (1,t) = c )
A69:
dom K2 =
the
carrier of
[:(Closed-Interval-TSpace ((1 / 2),1)),I[01]:]
by FUNCT_2:def 1
.=
[: the carrier of (Closed-Interval-TSpace ((1 / 2),1)), the carrier of I[01]:]
by BORSUK_1:def 2
;
t in the
carrier of
I[01]
;
then A70:
t in dom (id I[01])
by FUNCT_2:def 1;
0 in [.0,(1 / 2).]
by XXREAL_1:1;
then A71:
0 in the
carrier of
(Closed-Interval-TSpace (0,(1 / 2)))
by TOPMETR:18;
then A72:
[0,t] in dom f1
by A30, ZFMISC_1:87;
0 in dom R1
by A71, FUNCT_2:def 1;
then A73:
[0,t] in [:(dom R1),(dom (id I[01])):]
by A70, ZFMISC_1:87;
not
0 in [.(1 / 2),1.]
by XXREAL_1:1;
then
not
0 in the
carrier of
(Closed-Interval-TSpace ((1 / 2),1))
by TOPMETR:18;
then
not
[0,t] in dom K2
by A69, ZFMISC_1:87;
hence h . (
0,
t) =
K1 . (
0,
t)
by A28, FUNCT_4:11
.=
f . (f1 . (0,t))
by A72, FUNCT_1:13
.=
f . (
(R1 . 0),
((id I[01]) . t))
by A73, FUNCT_3:65
.=
f . (
(R1 . 0),
t)
by FUNCT_1:18
.=
f . (
0,
t)
by Th37
.=
a
by A10
;
h . (1,t) = c
t in the
carrier of
I[01]
;
then A74:
t in dom (id I[01])
by FUNCT_2:def 1;
1
in [.(1 / 2),1.]
by XXREAL_1:1;
then A75:
1
in the
carrier of
(Closed-Interval-TSpace ((1 / 2),1))
by TOPMETR:18;
then
1
in dom R2
by FUNCT_2:def 1;
then A76:
[1,t] in [:(dom R2),(dom (id I[01])):]
by A74, ZFMISC_1:87;
1
in [.(1 / 2),1.]
by XXREAL_1:1;
then
1
in the
carrier of
(Closed-Interval-TSpace ((1 / 2),1))
by TOPMETR:18;
then A77:
[1,t] in dom g1
by A8, ZFMISC_1:87;
[1,t] in dom K2
by A69, A75, ZFMISC_1:87;
then h . (1,
t) =
K2 . (1,
t)
by A28, FUNCT_4:13
.=
g . (g1 . (1,t))
by A77, FUNCT_1:13
.=
g . (
(R2 . 1),
((id I[01]) . t))
by A76, FUNCT_3:65
.=
g . (
(R2 . 1),
t)
by FUNCT_1:18
.=
g . (1,
t)
by Th37
.=
c
by A12
;
hence
h . (1,
t)
= c
;
verum
end;
hence
( h is continuous & ( for b1 being Element of the carrier of I[01] holds
( h . (b1,0) = (P1 + Q1) . b1 & h . (b1,1) = (P2 + Q2) . b1 & h . (0,b1) = a & h . (1,b1) = c ) ) )
by A29, A31; verum