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