let T be non empty TopSpace; for a, b 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 a, b 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:9;
reconsider g = g as continuous Function of ([:I[01],I[01]:] | IBB),T by TOPMETR:7;
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:8;
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 2;
then A6:
x = [(x `1),(x `2)]
by MCART_1:21;
then A7:
x `2 in the
carrier of
I[01]
by A5, ZFMISC_1:87;
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:87;
then A9:
e2 . (
(x `1),
(x `2))
= x `2
by A7, FUNCT_3:def 5;
A10:
x in dom e2
by A4, FUNCT_2:def 1;
g . x =
gg . (
(x `1),
(x `2))
by A3, A6, FUNCT_1:49
.=
P . (1 - (1 - (x `2)))
by A6, A9, A10, FUNCT_1:13
.=
(- 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:9;
reconsider f = f as continuous Function of ([:I[01],I[01]:] | IAA),T by TOPMETR:7;
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:8;
set hh = PP * e1;
reconsider h = (PP * e1) | ICC as Function of ([:I[01],I[01]:] | ICC),T by PRE_TOPC:9;
reconsider h = h as continuous Function of ([:I[01],I[01]:] | ICC),T by TOPMETR:7;
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:8;
then A15:
x `1 >= 1
/ 2
by Th60;
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 2;
then A18:
x = [(x `1),(x `2)]
by MCART_1:21;
then A19:
x `1 in the
carrier of
I[01]
by A17, ZFMISC_1:87;
x `2 in the
carrier of
I[01]
by A17, A18, ZFMISC_1:87;
then A20:
e1 . (
(x `1),
(x `2))
= x `1
by A19, FUNCT_3:def 4;
A21:
x in dom e1
by A16, FUNCT_2:def 1;
h . x =
(PP * e1) . x
by A14, FUNCT_1:49
.=
((- P) + P) . (e1 . ((x `1),(x `2)))
by A18, A21, FUNCT_1:13
.=
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:8;
then A24:
x `1 <= 1
/ 2
by Th59;
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 2;
then A27:
x = [(x `1),(x `2)]
by MCART_1:21;
then A28:
x `1 in the
carrier of
I[01]
by A26, ZFMISC_1:87;
x `2 in the
carrier of
I[01]
by A26, A27, ZFMISC_1:87;
then A29:
e1 . (
(x `1),
(x `2))
= x `1
by A28, FUNCT_3:def 4;
A30:
x in dom e1
by A25, FUNCT_2:def 1;
f . x =
(PP * e1) . x
by A23, FUNCT_1:49
.=
((- P) + P) . (e1 . x)
by A30, FUNCT_1:13
.=
(- 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 object st p in ([#] ([:I[01],I[01]:] | IAA)) /\ ([#] ([:I[01],I[01]:] | IBB)) holds
f . p = g . p
proof
let p be
object ;
( 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 5;
then A33:
p in IAA /\ IBB
by PRE_TOPC:def 5;
then consider r being
Point of
[:I[01],I[01]:] such that A34:
r = p
and A35:
r `2 = 1
- (2 * (r `1))
by Th57;
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:8;
p in IBB
by A32, XBOOLE_0:def 4;
then A37:
pp is
Point of
([:I[01],I[01]:] | IBB)
by PRE_TOPC:8;
f . p =
(- P) . (2 * (pp `1))
by A22
.=
g . p
by A2, A34, A36, A37
;
hence
f . p = g . p
;
verum
end;
reconsider s3 = [#] ([:I[01],I[01]:] | ICC) as Subset of [:I[01],I[01]:] by PRE_TOPC:def 5;
A38:
s3 = ICC
by PRE_TOPC:def 5;
A39:
( [:I[01],I[01]:] | IAA is SubSpace of S12 & [:I[01],I[01]:] | IBB is SubSpace of S12 )
by TOPMETR:22, XBOOLE_1:7;
A40:
[#] ([:I[01],I[01]:] | IBB) = IBB
by PRE_TOPC:def 5;
A41:
[#] ([:I[01],I[01]:] | IAA) = IAA
by PRE_TOPC:def 5;
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:26;
A43:
s2 is closed
by A40, TOPS_2:26;
([#] ([:I[01],I[01]:] | IAA)) \/ ([#] ([:I[01],I[01]:] | IBB)) = [#] S12
by A12, A40, PRE_TOPC:def 5;
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:1;
A46:
[#] ([:I[01],I[01]:] | ICC) = ICC
by PRE_TOPC:def 5;
A47:
for p being object st p in ([#] S12) /\ ([#] ([:I[01],I[01]:] | ICC)) holds
fg . p = h . p
proof
let p be
object ;
( p in ([#] S12) /\ ([#] ([:I[01],I[01]:] | ICC)) implies fg . p = h . p )
[(1 / 2),0] in IBB /\ ICC
by Th66, Th67, XBOOLE_0:def 4;
then A48:
{[(1 / 2),0]} c= IBB /\ ICC
by ZFMISC_1:31;
assume
p in ([#] S12) /\ ([#] ([:I[01],I[01]:] | ICC))
;
fg . p = h . p
then
p in {[(1 / 2),0]} \/ (IBB /\ ICC)
by A12, A46, Th72, 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:8;
A50:
ex
q being
Point of
[:I[01],I[01]:] st
(
q = p &
q `2 = (2 * (q `1)) - 1 )
by A49, Th58;
pp `2 is
Point of
I[01]
by A49, Th27;
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:8;
p in the
carrier of
([:I[01],I[01]:] | IBB)
by A52, PRE_TOPC:8;
then
p in dom g
by FUNCT_2:def 1;
then fg . p =
g . p
by A44, FUNCT_4:13
.=
(- 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, Th56, BORSUK_1:40, BORSUK_1:def 2;
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:1;
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
;
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 Th71;
then
not
[s,0] in the
carrier of
([:I[01],I[01]:] | IBB)
by PRE_TOPC:8;
then A59:
not
[s,0] in dom g
;
[s,0] in IAA
by A58, Th70;
then A60:
[s,0] in the
carrier of
([:I[01],I[01]:] | IAA)
by PRE_TOPC:8;
not
[s,0] in ICC
by A58, Th71;
then
not
[s,0] in the
carrier of
([:I[01],I[01]:] | ICC)
by PRE_TOPC:8;
then
not
[s,0] in dom h
;
then H . [s,0] =
fg . [s,0]
by A54, FUNCT_4:11
.=
f . [s,0]
by A44, A59, FUNCT_4:11
.=
(- 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 Th66, PRE_TOPC:8;
then
[s,0] in dom h
by FUNCT_2:def 1;
then H . [s,0] =
h . [s,0]
by A54, FUNCT_4:13
.=
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 Th69;
then A64:
[s,0] in the
carrier of
([:I[01],I[01]:] | ICC)
by PRE_TOPC:8;
then
[s,0] in dom h
by FUNCT_2:def 1;
then H . [s,0] =
h . [s,0]
by A54, FUNCT_4:13
.=
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
;
A66:
[s,1] `1 = s
;
A67:
dom Q = the
carrier of
I[01]
by FUNCT_2:def 1;
then A68:
0 in dom Q
by BORSUK_1:43;
per cases
( s <> 1 or s = 1 )
;
suppose A69:
s <> 1
;
H . (s,1) = Q . s
[s,1] in IBB
by Th65;
then A70:
[s,1] in the
carrier of
([:I[01],I[01]:] | IBB)
by PRE_TOPC:8;
then A71:
[s,1] in dom g
by FUNCT_2:def 1;
not
[s,1] in ICC
by A69, Th63;
then
not
[s,1] in the
carrier of
([:I[01],I[01]:] | ICC)
by PRE_TOPC:8;
then
not
[s,1] in dom h
;
then H . [s,1] =
fg . [s,1]
by A54, FUNCT_4:11
.=
g . [s,1]
by A44, A71, FUNCT_4:13
.=
(- 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 10
;
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 Th66, PRE_TOPC:8;
then
[s,1] in dom h
by FUNCT_2:def 1;
then H . [s,1] =
h . [s,1]
by A54, FUNCT_4:13
.=
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 10
;
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:43;
then reconsider x =
[0,t] as
Point of
[:I[01],I[01]:] by Lm1;
x in IAA
by Th61;
then A74:
x is
Point of
([:I[01],I[01]:] | IAA)
by PRE_TOPC:8;
x `1 = 0
;
then
not
x in ICC
by Th60;
then
not
x in the
carrier of
([:I[01],I[01]:] | ICC)
by PRE_TOPC:8;
then A75:
not
[0,t] in dom h
;
per cases
( t <> 1 or t = 1 )
;
suppose A76:
t = 1
;
H . (0,t) = athen A77:
x in the
carrier of
([:I[01],I[01]:] | IBB)
by Th64, PRE_TOPC:8;
then
x in dom g
by FUNCT_2:def 1;
then fg . [0,t] =
g . [0,1]
by A44, A76, FUNCT_4:13
.=
(- P) . (1 - (x `2))
by A2, A76, A77
.=
a
by A1, A76, BORSUK_2:def 2
;
hence
H . (
0,
t)
= a
by A54, A75, FUNCT_4:11;
verum end;
end;
thus
H . (1,
t)
= a
verumproof
1
in the
carrier of
I[01]
by BORSUK_1:43;
then reconsider x =
[1,t] as
Point of
[:I[01],I[01]:] by Lm1;
x in ICC
by Th68;
then A78:
x in the
carrier of
([:I[01],I[01]:] | ICC)
by PRE_TOPC:8;
then A79:
[1,t] in dom h
by FUNCT_2:def 1;
h . [1,t] =
P . ((2 * (x `1)) - 1)
by A13, A78
.=
a
by A1, BORSUK_2:def 2
;
hence
H . (1,
t)
= a
by A54, A79, FUNCT_4:13;
verum
end;
end;
hence
(- P) + P,Q are_homotopic
by A55, A56; verum