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: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;
x `1 in the
carrier of
I[01]
by A5, A6, ZFMISC_1:106;
then A8:
e2 . (x `1 ),
(x `2 ) = x `2
by A7, FUNCT_3:def 6;
A9:
x in dom e2
by A4, FUNCT_2:def 1;
g . x =
gg . x
by A3, FUNCT_1:72
.=
(- P) . (e2 . x)
by A9, FUNCT_1:23
.=
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: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] :] ;
A11:
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;
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:29;
then A14:
x `1 >= 1
/ 2
by Th68;
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 5;
then A17:
x = [(x `1 ),(x `2 )]
by MCART_1:23;
then A18:
x `1 in the
carrier of
I[01]
by A16, ZFMISC_1:106;
x `2 in the
carrier of
I[01]
by A16, A17, ZFMISC_1:106;
then A19:
e1 . (x `1 ),
(x `2 ) = x `1
by A18, FUNCT_3:def 5;
A20:
x in dom e1
by A15, FUNCT_2:def 1;
h . x =
(PP * e1) . x
by A13, FUNCT_1:72
.=
(P + (- P)) . (e1 . x)
by A20, FUNCT_1:23
.=
(- 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:29;
then A23:
x `1 <= 1
/ 2
by Th67;
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 5;
then A26:
x = [(x `1 ),(x `2 )]
by MCART_1:23;
then A27:
x `1 in the
carrier of
I[01]
by A25, ZFMISC_1:106;
x `2 in the
carrier of
I[01]
by A25, A26, ZFMISC_1:106;
then A28:
e1 . (x `1 ),
(x `2 ) = x `1
by A27, FUNCT_3:def 5;
A29:
x in dom e1
by A24, FUNCT_2:def 1;
f . x =
(PP * e1) . x
by A22, FUNCT_1:72
.=
(P + (- P)) . (e1 . x)
by A29, FUNCT_1:23
.=
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 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 A31:
p in ([#] ([:I[01] ,I[01] :] | IAA )) /\ IBB
by PRE_TOPC:def 10;
then A32:
p in IAA /\ IBB
by PRE_TOPC:def 10;
then consider r being
Point of
[:I[01] ,I[01] :] such that A33:
r = p
and A34:
r `2 = 1
- (2 * (r `1 ))
by Th65;
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:29;
p in IBB
by A31, XBOOLE_0:def 4;
then A36:
pp is
Point of
([:I[01] ,I[01] :] | IBB )
by PRE_TOPC:29;
f . p =
P . (2 * (pp `1 ))
by A21
.=
g . p
by A2, A33, A35, A36
;
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;
A37:
s3 = ICC
by PRE_TOPC:def 10;
A38:
( [:I[01] ,I[01] :] | IAA is SubSpace of S12 & [:I[01] ,I[01] :] | IBB is SubSpace of S12 )
by TOPMETR:29, XBOOLE_1:7;
A39:
[#] ([:I[01] ,I[01] :] | IBB ) = IBB
by PRE_TOPC:def 10;
A40:
[#] ([: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 A11, A39, XBOOLE_1:7;
A41:
s1 is closed
by A40, TOPS_2:34;
A42:
s2 is closed
by A39, TOPS_2:34;
([#] ([:I[01] ,I[01] :] | IAA )) \/ ([#] ([:I[01] ,I[01] :] | IBB )) = [#] S12
by A11, A39, PRE_TOPC:def 10;
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:9;
A45:
[#] ([:I[01] ,I[01] :] | ICC ) = ICC
by PRE_TOPC:def 10;
A46:
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 A47:
{[(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 A11, A45, Th80, 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:29;
A49:
p in IBB
by A48, XBOOLE_0:def 4;
then A50:
pp is
Point of
([:I[01] ,I[01] :] | IBB )
by PRE_TOPC:29;
A51:
ex
q being
Point of
[:I[01] ,I[01] :] st
(
q = p &
q `2 = (2 * (q `1 )) - 1 )
by A48, Th66;
then A52:
(2 * (pp `1 )) - 1 is
Point of
I[01]
by Th31;
p in the
carrier of
([:I[01] ,I[01] :] | IBB )
by A49, PRE_TOPC:29;
then
p in dom g
by FUNCT_2:def 1;
then fg . p =
g . p
by A43, FUNCT_4:14
.=
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 10
.=
[#] [:I[01] ,I[01] :]
by Th64, BORSUK_1:83, BORSUK_1:def 5
;
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:9;
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
by MCART_1:7;
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 Th79;
then
not
[s,0 ] in the
carrier of
([:I[01] ,I[01] :] | IBB )
by PRE_TOPC:29;
then A58:
not
[s,0 ] in dom g
;
[s,0 ] in IAA
by A57, Th78;
then A59:
[s,0 ] in the
carrier of
([:I[01] ,I[01] :] | IAA )
by PRE_TOPC:29;
not
[s,0 ] in ICC
by A57, 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 A53, FUNCT_4:12
.=
f . [s,0 ]
by A43, A58, FUNCT_4:12
.=
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 Th74, PRE_TOPC:29;
then
[s,0 ] in dom h
by FUNCT_2:def 1;
then H . [s,0 ] =
h . [s,0 ]
by A53, FUNCT_4:14
.=
(- 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 Th77;
then A63:
[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 A53, FUNCT_4:14
.=
(- 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
by MCART_1:7;
A65:
[s,1] `1 = s
by MCART_1:7;
A66:
dom Q = the
carrier of
I[01]
by FUNCT_2:def 1;
then A67:
0 in dom Q
by BORSUK_1:86;
per cases
( s <> 1 or s = 1 )
;
suppose A68:
s <> 1
;
H . s,1 = Q . s
[s,1] in IBB
by Th73;
then A69:
[s,1] in the
carrier of
([:I[01] ,I[01] :] | IBB )
by PRE_TOPC:29;
then A70:
[s,1] in dom g
by FUNCT_2:def 1;
not
[s,1] in ICC
by A68, 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 A53, FUNCT_4:12
.=
g . [s,1]
by A43, A70, FUNCT_4:14
.=
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 16
;
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 Th74, PRE_TOPC:29;
then
[s,1] in dom h
by FUNCT_2:def 1;
then H . [s,1] =
h . [s,1]
by A53, FUNCT_4:14
.=
(- 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 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;
A73:
x `2 = t
by MCART_1:7;
x in IAA
by Th69;
then A74:
x is
Point of
([:I[01] ,I[01] :] | IAA )
by PRE_TOPC:29;
A75:
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 A76:
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 A43, FUNCT_4:12
.=
P . (2 * (x `1 ))
by A21, A74
.=
a
by A1, A75, BORSUK_2:def 2
;
hence
H . 0 ,
t = a
by A53, A76, FUNCT_4:12;
verum end; suppose A77:
t = 1
;
H . 0 ,t = athen A78:
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 A43, A77, FUNCT_4:14
.=
P . (1 - (x `2 ))
by A2, A77, A78
.=
a
by A1, A73, A77, BORSUK_2:def 2
;
hence
H . 0 ,
t = a
by A53, A76, 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;
A79:
x `1 = 1
by MCART_1:7;
x in ICC
by Th76;
then A80:
x in the
carrier of
([:I[01] ,I[01] :] | ICC )
by PRE_TOPC:29;
then A81:
[1,t] in dom h
by FUNCT_2:def 1;
h . [1,t] =
(- P) . ((2 * (x `1 )) - 1)
by A12, A80
.=
a
by A1, A79, BORSUK_2:def 2
;
hence
H . 1,
t = a
by A53, A81, FUNCT_4:14;
verum
end;
end;
hence
P + (- P),Q are_homotopic
by A54, A55, BORSUK_2:def 7; verum