let T be non empty TopSpace; for b, a being Point of T
for P being Path of b,a
for Q being constant Path of a,a st b,a are_connected holds
(- P) + P,Q are_homotopic
let b, a be Point of T; for P being Path of b,a
for Q being constant Path of a,a st b,a are_connected holds
(- P) + P,Q are_homotopic
set S = [:I[01] ,I[01] :];
let P be Path of b,a; for Q being constant Path of a,a st b,a are_connected holds
(- P) + P,Q are_homotopic
let Q be constant Path of a,a; ( b,a are_connected implies (- P) + P,Q are_homotopic )
assume A1:
b,a are_connected
; (- P) + P,Q are_homotopic
reconsider e2 = pr2 the carrier of I[01] ,the carrier of I[01] as continuous Function of [:I[01] ,I[01] :],I[01] by YELLOW12:40;
set gg = P * e2;
P is continuous
by A1, BORSUK_2:def 2;
then reconsider gg = P * e2 as continuous Function of [:I[01] ,I[01] :],T ;
set S2 = [:I[01] ,I[01] :] | IBB ;
reconsider g = gg | IBB as Function of ([:I[01] ,I[01] :] | IBB ),T by PRE_TOPC:30;
reconsider g = g as continuous Function of ([:I[01] ,I[01] :] | IBB ),T by TOPMETR:10;
A2:
for x being Point of ([:I[01] ,I[01] :] | IBB ) holds g . x = (- P) . (1 - (x `2 ))
proof
let x be
Point of
([:I[01] ,I[01] :] | IBB );
g . x = (- P) . (1 - (x `2 ))
x in the
carrier of
([:I[01] ,I[01] :] | IBB )
;
then A3:
x in IBB
by PRE_TOPC:29;
then A4:
x in the
carrier of
[:I[01] ,I[01] :]
;
then A5:
x in [:the carrier of I[01] ,the carrier of I[01] :]
by BORSUK_1:def 5;
then A6:
x = [(x `1 ),(x `2 )]
by MCART_1:23;
then A7:
x `2 in the
carrier of
I[01]
by A5, ZFMISC_1:106;
then A8:
1
- (x `2 ) in the
carrier of
I[01]
by JORDAN5B:4;
x `1 in the
carrier of
I[01]
by A5, A6, ZFMISC_1:106;
then A9:
e2 . (x `1 ),
(x `2 ) = x `2
by A7, FUNCT_3:def 6;
A10:
x in dom e2
by A4, FUNCT_2:def 1;
g . x =
gg . (x `1 ),
(x `2 )
by A3, A6, FUNCT_1:72
.=
P . (1 - (1 - (x `2 )))
by A6, A9, A10, FUNCT_1:23
.=
(- P) . (1 - (x `2 ))
by A1, A8, BORSUK_2:def 6
;
hence
g . x = (- P) . (1 - (x `2 ))
;
verum
end;
set S3 = [:I[01] ,I[01] :] | ICC ;
set S1 = [:I[01] ,I[01] :] | IAA ;
reconsider e1 = pr1 the carrier of I[01] ,the carrier of I[01] as continuous Function of [:I[01] ,I[01] :],I[01] by YELLOW12:39;
A11:
a,a are_connected
;
then reconsider PP = (- P) + P as continuous Path of a,a by BORSUK_2:def 2;
set ff = PP * e1;
reconsider f = (PP * e1) | IAA as Function of ([:I[01] ,I[01] :] | IAA ),T by PRE_TOPC:30;
reconsider f = f as continuous Function of ([:I[01] ,I[01] :] | IAA ),T by TOPMETR:10;
set S12 = [:I[01] ,I[01] :] | (IAA \/ IBB );
reconsider S12 = [:I[01] ,I[01] :] | (IAA \/ IBB ) as non empty SubSpace of [:I[01] ,I[01] :] ;
A12:
the carrier of S12 = IAA \/ IBB
by PRE_TOPC:29;
set hh = PP * e1;
reconsider h = (PP * e1) | ICC as Function of ([:I[01] ,I[01] :] | ICC ),T by PRE_TOPC:30;
reconsider h = h as continuous Function of ([:I[01] ,I[01] :] | ICC ),T by TOPMETR:10;
A13:
for x being Point of ([:I[01] ,I[01] :] | ICC ) holds h . x = P . ((2 * (x `1 )) - 1)
proof
let x be
Point of
([:I[01] ,I[01] :] | ICC );
h . x = P . ((2 * (x `1 )) - 1)
x in the
carrier of
([:I[01] ,I[01] :] | ICC )
;
then A14:
x in ICC
by PRE_TOPC:29;
then A15:
x `1 >= 1
/ 2
by Th68;
A16:
x in the
carrier of
[:I[01] ,I[01] :]
by A14;
then A17:
x in [:the carrier of I[01] ,the carrier of I[01] :]
by BORSUK_1:def 5;
then A18:
x = [(x `1 ),(x `2 )]
by MCART_1:23;
then A19:
x `1 in the
carrier of
I[01]
by A17, ZFMISC_1:106;
x `2 in the
carrier of
I[01]
by A17, A18, ZFMISC_1:106;
then A20:
e1 . (x `1 ),
(x `2 ) = x `1
by A19, FUNCT_3:def 5;
A21:
x in dom e1
by A16, FUNCT_2:def 1;
h . x =
(PP * e1) . x
by A14, FUNCT_1:72
.=
((- P) + P) . (e1 . (x `1 ),(x `2 ))
by A18, A21, FUNCT_1:23
.=
P . ((2 * (x `1 )) - 1)
by A1, A19, A20, A15, BORSUK_2:def 5
;
hence
h . x = P . ((2 * (x `1 )) - 1)
;
verum
end;
A22:
for x being Point of ([:I[01] ,I[01] :] | IAA ) holds f . x = (- P) . (2 * (x `1 ))
proof
let x be
Point of
([:I[01] ,I[01] :] | IAA );
f . x = (- P) . (2 * (x `1 ))
x in the
carrier of
([:I[01] ,I[01] :] | IAA )
;
then A23:
x in IAA
by PRE_TOPC:29;
then A24:
x `1 <= 1
/ 2
by Th67;
A25:
x in the
carrier of
[:I[01] ,I[01] :]
by A23;
then A26:
x in [:the carrier of I[01] ,the carrier of I[01] :]
by BORSUK_1:def 5;
then A27:
x = [(x `1 ),(x `2 )]
by MCART_1:23;
then A28:
x `1 in the
carrier of
I[01]
by A26, ZFMISC_1:106;
x `2 in the
carrier of
I[01]
by A26, A27, ZFMISC_1:106;
then A29:
e1 . (x `1 ),
(x `2 ) = x `1
by A28, FUNCT_3:def 5;
A30:
x in dom e1
by A25, FUNCT_2:def 1;
f . x =
(PP * e1) . x
by A23, FUNCT_1:72
.=
((- P) + P) . (e1 . x)
by A30, FUNCT_1:23
.=
(- P) . (2 * (x `1 ))
by A1, A27, A28, A29, A24, BORSUK_2:def 5
;
hence
f . x = (- P) . (2 * (x `1 ))
;
verum
end;
A31:
for p being set st p in ([#] ([:I[01] ,I[01] :] | IAA )) /\ ([#] ([:I[01] ,I[01] :] | IBB )) holds
f . p = g . p
proof
let p be
set ;
( p in ([#] ([:I[01] ,I[01] :] | IAA )) /\ ([#] ([:I[01] ,I[01] :] | IBB )) implies f . p = g . p )
assume
p in ([#] ([:I[01] ,I[01] :] | IAA )) /\ ([#] ([:I[01] ,I[01] :] | IBB ))
;
f . p = g . p
then A32:
p in ([#] ([:I[01] ,I[01] :] | IAA )) /\ IBB
by PRE_TOPC:def 10;
then A33:
p in IAA /\ IBB
by PRE_TOPC:def 10;
then consider r being
Point of
[:I[01] ,I[01] :] such that A34:
r = p
and A35:
r `2 = 1
- (2 * (r `1 ))
by Th65;
A36:
2
* (r `1 ) = 1
- (r `2 )
by A35;
p in IAA
by A33, XBOOLE_0:def 4;
then reconsider pp =
p as
Point of
([:I[01] ,I[01] :] | IAA ) by PRE_TOPC:29;
p in IBB
by A32, XBOOLE_0:def 4;
then A37:
pp is
Point of
([:I[01] ,I[01] :] | IBB )
by PRE_TOPC:29;
f . p =
(- P) . (2 * (pp `1 ))
by A22
.=
g . p
by A2, A34, A36, A37
;
hence
f . p = g . p
;
verum
end;
reconsider s12 = [#] S12, s3 = [#] ([:I[01] ,I[01] :] | ICC ) as Subset of [:I[01] ,I[01] :] by PRE_TOPC:def 10;
A38:
s3 = ICC
by PRE_TOPC:def 10;
A39:
( [:I[01] ,I[01] :] | IAA is SubSpace of S12 & [:I[01] ,I[01] :] | IBB is SubSpace of S12 )
by TOPMETR:29, XBOOLE_1:7;
A40:
[#] ([:I[01] ,I[01] :] | IBB ) = IBB
by PRE_TOPC:def 10;
A41:
[#] ([:I[01] ,I[01] :] | IAA ) = IAA
by PRE_TOPC:def 10;
then reconsider s1 = [#] ([:I[01] ,I[01] :] | IAA ), s2 = [#] ([:I[01] ,I[01] :] | IBB ) as Subset of S12 by A12, A40, XBOOLE_1:7;
A42:
s1 is closed
by A41, TOPS_2:34;
A43:
s2 is closed
by A40, TOPS_2:34;
([#] ([:I[01] ,I[01] :] | IAA )) \/ ([#] ([:I[01] ,I[01] :] | IBB )) = [#] S12
by A12, A40, PRE_TOPC:def 10;
then consider fg being Function of S12,T such that
A44:
fg = f +* g
and
A45:
fg is continuous
by A31, A39, A42, A43, JGRAPH_2:9;
A46:
[#] ([:I[01] ,I[01] :] | ICC ) = ICC
by PRE_TOPC:def 10;
A47:
for p being set st p in ([#] S12) /\ ([#] ([:I[01] ,I[01] :] | ICC )) holds
fg . p = h . p
proof
let p be
set ;
( p in ([#] S12) /\ ([#] ([:I[01] ,I[01] :] | ICC )) implies fg . p = h . p )
[(1 / 2),0 ] in IBB /\ ICC
by Th74, Th75, XBOOLE_0:def 4;
then A48:
{[(1 / 2),0 ]} c= IBB /\ ICC
by ZFMISC_1:37;
assume
p in ([#] S12) /\ ([#] ([:I[01] ,I[01] :] | ICC ))
;
fg . p = h . p
then
p in {[(1 / 2),0 ]} \/ (IBB /\ ICC )
by A12, A46, Th80, XBOOLE_1:23;
then A49:
p in IBB /\ ICC
by A48, XBOOLE_1:12;
then
p in ICC
by XBOOLE_0:def 4;
then reconsider pp =
p as
Point of
([:I[01] ,I[01] :] | ICC ) by PRE_TOPC:29;
A50:
ex
q being
Point of
[:I[01] ,I[01] :] st
(
q = p &
q `2 = (2 * (q `1 )) - 1 )
by A49, Th66;
pp `2 is
Point of
I[01]
by A49, Th31;
then A51:
1
- (pp `2 ) in the
carrier of
I[01]
by JORDAN5B:4;
A52:
p in IBB
by A49, XBOOLE_0:def 4;
then A53:
pp is
Point of
([:I[01] ,I[01] :] | IBB )
by PRE_TOPC:29;
p in the
carrier of
([:I[01] ,I[01] :] | IBB )
by A52, PRE_TOPC:29;
then
p in dom g
by FUNCT_2:def 1;
then fg . p =
g . p
by A44, FUNCT_4:14
.=
(- P) . (1 - (pp `2 ))
by A2, A53
.=
P . (1 - (1 - (pp `2 )))
by A1, A51, BORSUK_2:def 6
.=
h . p
by A13, A50
;
hence
fg . p = h . p
;
verum
end;
([#] S12) \/ ([#] ([:I[01] ,I[01] :] | ICC )) = [#] [:I[01] ,I[01] :]
by A12, A46, Th64, BORSUK_1:83, BORSUK_1:def 5;
then consider H being Function of [:I[01] ,I[01] :],T such that
A54:
H = fg +* h
and
A55:
H is continuous
by A12, A45, A47, A38, JGRAPH_2:9;
A56:
for s being Point of I[01] holds
( H . s,0 = ((- P) + P) . s & H . s,1 = Q . s )
proof
let s be
Point of
I[01] ;
( H . s,0 = ((- P) + P) . s & H . s,1 = Q . s )
thus
H . s,
0 = ((- P) + P) . s
H . s,1 = Q . sproof
A57:
[s,0 ] `1 = s
by MCART_1:7;
per cases
( s < 1 / 2 or s = 1 / 2 or s > 1 / 2 )
by XXREAL_0:1;
suppose A58:
s < 1
/ 2
;
H . s,0 = ((- P) + P) . sthen
not
[s,0 ] in IBB
by Th79;
then
not
[s,0 ] in the
carrier of
([:I[01] ,I[01] :] | IBB )
by PRE_TOPC:29;
then A59:
not
[s,0 ] in dom g
;
[s,0 ] in IAA
by A58, Th78;
then A60:
[s,0 ] in the
carrier of
([:I[01] ,I[01] :] | IAA )
by PRE_TOPC:29;
not
[s,0 ] in ICC
by A58, Th79;
then
not
[s,0 ] in the
carrier of
([:I[01] ,I[01] :] | ICC )
by PRE_TOPC:29;
then
not
[s,0 ] in dom h
;
then H . [s,0 ] =
fg . [s,0 ]
by A54, FUNCT_4:12
.=
f . [s,0 ]
by A44, A59, FUNCT_4:12
.=
(- P) . (2 * s)
by A22, A57, A60
.=
((- P) + P) . s
by A1, A58, BORSUK_2:def 5
;
hence
H . s,
0 = ((- P) + P) . s
;
verum end; suppose A61:
s = 1
/ 2
;
H . s,0 = ((- P) + P) . sthen A62:
[s,0 ] in the
carrier of
([:I[01] ,I[01] :] | ICC )
by Th74, PRE_TOPC:29;
then
[s,0 ] in dom h
by FUNCT_2:def 1;
then H . [s,0 ] =
h . [s,0 ]
by A54, FUNCT_4:14
.=
P . ((2 * s) - 1)
by A13, A57, A62
.=
b
by A1, A61, BORSUK_2:def 2
.=
(- P) . (2 * (1 / 2))
by A1, BORSUK_2:def 2
.=
((- P) + P) . s
by A1, A61, BORSUK_2:def 5
;
hence
H . s,
0 = ((- P) + P) . s
;
verum end; suppose A63:
s > 1
/ 2
;
H . s,0 = ((- P) + P) . sthen
[s,0 ] in ICC
by Th77;
then A64:
[s,0 ] in the
carrier of
([:I[01] ,I[01] :] | ICC )
by PRE_TOPC:29;
then
[s,0 ] in dom h
by FUNCT_2:def 1;
then H . [s,0 ] =
h . [s,0 ]
by A54, FUNCT_4:14
.=
P . ((2 * s) - 1)
by A13, A57, A64
.=
((- P) + P) . s
by A1, A63, BORSUK_2:def 5
;
hence
H . s,
0 = ((- P) + P) . s
;
verum end;
end;
thus
H . s,1
= Q . s
verumproof
A65:
[s,1] `2 = 1
by MCART_1:7;
A66:
[s,1] `1 = s
by MCART_1:7;
A67:
dom Q = the
carrier of
I[01]
by FUNCT_2:def 1;
then A68:
0 in dom Q
by BORSUK_1:86;
per cases
( s <> 1 or s = 1 )
;
suppose A69:
s <> 1
;
H . s,1 = Q . s
[s,1] in IBB
by Th73;
then A70:
[s,1] in the
carrier of
([:I[01] ,I[01] :] | IBB )
by PRE_TOPC:29;
then A71:
[s,1] in dom g
by FUNCT_2:def 1;
not
[s,1] in ICC
by A69, Th71;
then
not
[s,1] in the
carrier of
([:I[01] ,I[01] :] | ICC )
by PRE_TOPC:29;
then
not
[s,1] in dom h
;
then H . [s,1] =
fg . [s,1]
by A54, FUNCT_4:12
.=
g . [s,1]
by A44, A71, FUNCT_4:14
.=
(- P) . (1 - 1)
by A2, A65, A70
.=
a
by A1, BORSUK_2:def 2
.=
Q . 0
by A11, BORSUK_2:def 2
.=
Q . s
by A67, A68, FUNCT_1:def 16
;
hence
H . s,1
= Q . s
;
verum end; suppose A72:
s = 1
;
H . s,1 = Q . sthen A73:
[s,1] in the
carrier of
([:I[01] ,I[01] :] | ICC )
by Th74, PRE_TOPC:29;
then
[s,1] in dom h
by FUNCT_2:def 1;
then H . [s,1] =
h . [s,1]
by A54, FUNCT_4:14
.=
P . ((2 * s) - 1)
by A13, A66, A73
.=
a
by A1, A72, BORSUK_2:def 2
.=
Q . 0
by A11, BORSUK_2:def 2
.=
Q . s
by A67, A68, FUNCT_1:def 16
;
hence
H . s,1
= Q . s
;
verum end;
end;
end;
for t being Point of I[01] holds
( H . 0 ,t = a & H . 1,t = a )
proof
let t be
Point of
I[01] ;
( H . 0 ,t = a & H . 1,t = a )
thus
H . 0 ,
t = a
H . 1,t = aproof
0 in the
carrier of
I[01]
by BORSUK_1:86;
then reconsider x =
[0 ,t] as
Point of
[:I[01] ,I[01] :] by Lm1;
A74:
x `2 = t
by MCART_1:7;
x in IAA
by Th69;
then A75:
x is
Point of
([:I[01] ,I[01] :] | IAA )
by PRE_TOPC:29;
A76:
x `1 = 0
by MCART_1:7;
then
not
x in ICC
by Th68;
then
not
x in the
carrier of
([:I[01] ,I[01] :] | ICC )
by PRE_TOPC:29;
then A77:
not
[0 ,t] in dom h
;
per cases
( t <> 1 or t = 1 )
;
suppose
t <> 1
;
H . 0 ,t = athen
not
x in IBB
by Th70;
then
not
x in the
carrier of
([:I[01] ,I[01] :] | IBB )
by PRE_TOPC:29;
then
not
x in dom g
;
then fg . [0 ,t] =
f . [0 ,t]
by A44, FUNCT_4:12
.=
(- P) . (2 * (x `1 ))
by A22, A75
.=
a
by A1, A76, BORSUK_2:def 2
;
hence
H . 0 ,
t = a
by A54, A77, FUNCT_4:12;
verum end; suppose A78:
t = 1
;
H . 0 ,t = athen A79:
x in the
carrier of
([:I[01] ,I[01] :] | IBB )
by Th72, PRE_TOPC:29;
then
x in dom g
by FUNCT_2:def 1;
then fg . [0 ,t] =
g . [0 ,1]
by A44, A78, FUNCT_4:14
.=
(- P) . (1 - (x `2 ))
by A2, A78, A79
.=
a
by A1, A74, A78, BORSUK_2:def 2
;
hence
H . 0 ,
t = a
by A54, A77, FUNCT_4:12;
verum end;
end;
thus
H . 1,
t = a
verumproof
1
in the
carrier of
I[01]
by BORSUK_1:86;
then reconsider x =
[1,t] as
Point of
[:I[01] ,I[01] :] by Lm1;
A80:
x `1 = 1
by MCART_1:7;
x in ICC
by Th76;
then A81:
x in the
carrier of
([:I[01] ,I[01] :] | ICC )
by PRE_TOPC:29;
then A82:
[1,t] in dom h
by FUNCT_2:def 1;
h . [1,t] =
P . ((2 * (x `1 )) - 1)
by A13, A81
.=
a
by A1, A80, BORSUK_2:def 2
;
hence
H . 1,
t = a
by A54, A82, FUNCT_4:14;
verum
end;
end;
hence
(- P) + P,Q are_homotopic
by A55, A56, BORSUK_2:def 7; verum