let FT be non empty RelStr ; for g being FinSequence of FT
for A being Subset of FT
for x1, x2 being Element of FT st g is_minimum_path_in A,x1,x2 & FT is symmetric holds
g is inv_continuous
let g be FinSequence of FT; for A being Subset of FT
for x1, x2 being Element of FT st g is_minimum_path_in A,x1,x2 & FT is symmetric holds
g is inv_continuous
let A be Subset of FT; for x1, x2 being Element of FT st g is_minimum_path_in A,x1,x2 & FT is symmetric holds
g is inv_continuous
let x1, x2 be Element of FT; ( g is_minimum_path_in A,x1,x2 & FT is symmetric implies g is inv_continuous )
assume that
A1:
g is_minimum_path_in A,x1,x2
and
A2:
FT is symmetric
; g is inv_continuous
A3:
g . 1 = x1
by A1;
A4:
g . (len g) = x2
by A1;
A5:
g is continuous
by A1;
hence
1 <= len g
; FINTOPO6:def 9 for i, j being Nat
for y being Element of FT st 1 <= i & i <= len g & 1 <= j & j <= len g & y = g . i & i <> j & g . j in U_FT y & not i = j + 1 holds
j = i + 1
let i2, j2 be Nat; for y being Element of FT st 1 <= i2 & i2 <= len g & 1 <= j2 & j2 <= len g & y = g . i2 & i2 <> j2 & g . j2 in U_FT y & not i2 = j2 + 1 holds
j2 = i2 + 1
let y be Element of FT; ( 1 <= i2 & i2 <= len g & 1 <= j2 & j2 <= len g & y = g . i2 & i2 <> j2 & g . j2 in U_FT y & not i2 = j2 + 1 implies j2 = i2 + 1 )
assume that
A6:
1 <= i2
and
A7:
i2 <= len g
and
A8:
1 <= j2
and
A9:
j2 <= len g
and
A10:
y = g . i2
and
A11:
i2 <> j2
and
A12:
g . j2 in U_FT y
; ( i2 = j2 + 1 or j2 = i2 + 1 )
A13:
rng g c= A
by A1;
hereby verum
assume that A14:
i2 <> j2 + 1
and A15:
j2 <> i2 + 1
;
contradictionper cases
( i2 < j2 or j2 < i2 )
by A11, XXREAL_0:1;
suppose A16:
i2 < j2
;
contradictionset n1 =
j2 -' 1;
set n2 =
i2;
reconsider n1 =
j2 -' 1,
n2 =
i2 as
Element of
NAT by ORDINAL1:def 12;
i2 + 1
<= j2
by A16, NAT_1:13;
then
i2 + 1
< j2
by A15, XXREAL_0:1;
then
i2 < j2 - 1
by XREAL_1:20;
then A17:
n1 > n2
by A8, XREAL_1:233;
1
< j2
by A6, A16, XXREAL_0:2;
then
1
+ 1
<= j2
by NAT_1:13;
then
1
<= j2 - 1
by XREAL_1:19;
then A18:
1
<= n1
by A8, XREAL_1:233;
set k =
(len g) -' n1;
reconsider g2 =
(g | n2) ^ (g /^ n1) as
FinSequence of
FT ;
A19:
len (g | n2) = n2
by A7, FINSEQ_1:59;
A20:
j2 -' 1
<= j2
by NAT_D:35;
then A21:
n1 <= len g
by A9, XXREAL_0:2;
then A22:
len (g /^ n1) = (len g) - n1
by RFINSEQ:def 1;
A23:
(len g) - n1 >= 0
by A21, XREAL_1:48;
then A24:
(len g) -' n1 = (len g) - n1
by XREAL_0:def 2;
A25:
len g2 =
(len (g | n2)) + (len (g /^ n1))
by FINSEQ_1:22
.=
n2 + ((len g) - n1)
by A21, A19, RFINSEQ:def 1
;
A26:
g2 . 1 =
(g | n2) . 1
by A6, A19, FINSEQ_1:64
.=
x1
by A3, A6, FINSEQ_3:112
;
now contradictionper cases
( n1 < len g or n1 = len g )
by A21, XXREAL_0:1;
suppose
n1 < len g
;
contradictionthen
n1 + 1
<= len g
by NAT_1:13;
then A27:
(n1 + 1) - n1 <= (len g) - n1
by XREAL_1:13;
then A28:
0 + 1
<= n2 + ((len g) - n1)
by XREAL_1:7;
A29:
g2 is
continuous
proof
thus
len g2 >= 1
by A25, A28;
FINTOPO6:def 6 for i being Nat
for x1 being Element of FT st 1 <= i & i < len g2 & x1 = g2 . i holds
g2 . (i + 1) in U_FT x1
let i be
Nat;
for x1 being Element of FT st 1 <= i & i < len g2 & x1 = g2 . i holds
g2 . (i + 1) in U_FT x1let z1 be
Element of
FT;
( 1 <= i & i < len g2 & z1 = g2 . i implies g2 . (i + 1) in U_FT z1 )
assume that A30:
1
<= i
and A31:
i < len g2
and A32:
z1 = g2 . i
;
g2 . (i + 1) in U_FT z1
A33:
i + 1
<= len g2
by A31, NAT_1:13;
reconsider i =
i as
Element of
NAT by ORDINAL1:def 12;
1
< i + 1
by A30, NAT_1:13;
then
i + 1
in dom g2
by A33, FINSEQ_3:25;
then
g2 . (i + 1) = g2 /. (i + 1)
by PARTFUN1:def 6;
then reconsider z2 =
g2 . (i + 1) as
Element of
FT ;
per cases
( i < n2 or i >= n2 )
;
suppose A34:
i < n2
;
g2 . (i + 1) in U_FT z1then A35:
i + 1
<= n2
by NAT_1:13;
i + 1
<= len (g | n2)
by A19, A34, NAT_1:13;
then A36:
z2 =
(g | n2) . (i + 1)
by FINSEQ_1:64, NAT_1:12
.=
g . (i + 1)
by A35, FINSEQ_3:112
;
A37:
i < len g
by A7, A34, XXREAL_0:2;
z1 =
(g | n2) . i
by A19, A30, A32, A34, FINSEQ_1:64
.=
g . i
by A34, FINSEQ_3:112
;
hence
g2 . (i + 1) in U_FT z1
by A5, A30, A37, A36;
verum end; suppose A38:
i >= n2
;
g2 . (i + 1) in U_FT z1
i - n2 < (n2 + ((len g) - n1)) - n2
by A25, A31, XREAL_1:9;
then A39:
i -' n2 < (len g) - n1
by A38, XREAL_1:233;
then
i -' n2 < (len g) -' n1
by A9, A20, XREAL_1:233, XXREAL_0:2;
then
(i -' n2) + 1
<= (len g) -' n1
by NAT_1:13;
then A40:
(i -' n2) + 1
<= len (g /^ n1)
by A9, A20, A22, XREAL_1:233, XXREAL_0:2;
A41:
(len (g | n2)) + (i -' n2) =
n2 + (i - n2)
by A19, A38, XREAL_1:233
.=
i
;
A42:
(len (g | n2)) + ((i -' n2) + 1) =
((i - n2) + 1) + n2
by A19, A38, XREAL_1:233
.=
i + 1
;
1
<= (i -' n2) + 1
by NAT_1:12;
then A43:
(i -' n2) + 1
in dom (g /^ n1)
by A40, FINSEQ_3:25;
per cases
( i > n2 or i = n2 )
by A38, XXREAL_0:1;
suppose
i > n2
;
g2 . (i + 1) in U_FT z1then A44:
i - n2 > 0
by XREAL_1:50;
then
i -' n2 = i - n2
by XREAL_0:def 2;
then A45:
0 + 1
<= i -' n2
by A44, NAT_1:13;
then A46:
i -' n2 in dom (g /^ n1)
by A22, A39, FINSEQ_3:25;
A47:
z2 =
(g /^ n1) . ((i -' n2) + 1)
by A40, A42, FINSEQ_1:65, NAT_1:12
.=
g . (((i -' n2) + 1) + n1)
by A21, A43, RFINSEQ:def 1
.=
g . (((i -' n2) + n1) + 1)
;
A48:
( 1
<= (i -' n2) + n1 &
(i -' n2) + n1 < ((len g) - n1) + n1 )
by A18, A39, NAT_1:12, XREAL_1:6;
z1 =
(g /^ n1) . (i -' n2)
by A22, A32, A39, A41, A45, FINSEQ_1:65
.=
g . ((i -' n2) + n1)
by A21, A46, RFINSEQ:def 1
;
hence
g2 . (i + 1) in U_FT z1
by A5, A47, A48;
verum end; suppose A49:
i = n2
;
g2 . (i + 1) in U_FT z1then A50:
z1 =
(g | n2) . n2
by A19, A30, A32, FINSEQ_1:64
.=
y
by A10, FINSEQ_3:112
;
z2 =
(g /^ n1) . ((i -' n2) + 1)
by A40, A42, FINSEQ_1:65, NAT_1:12
.=
g . (((i -' n2) + 1) + n1)
by A21, A43, RFINSEQ:def 1
.=
g . (((i -' n2) + n1) + 1)
.=
g . ((0 + (j2 -' 1)) + 1)
by A49, XREAL_1:232
.=
g . ((j2 - 1) + 1)
by A8, XREAL_1:233
;
hence
g2 . (i + 1) in U_FT z1
by A12, A50;
verum end; end; end; end;
end; A51:
rng (g /^ n1) c= rng g
by FINSEQ_5:33;
(
rng g2 = (rng (g | n2)) \/ (rng (g /^ n1)) &
rng (g | n2) c= rng g )
by FINSEQ_1:31, FINSEQ_5:19;
then
rng g2 c= rng g
by A51, XBOOLE_1:8;
then A52:
rng g2 c= A
by A13;
A53:
((len g) -' n1) + n1 = len g
by A24;
A54:
(len g) -' n1 in dom (g /^ n1)
by A24, A22, A27, FINSEQ_3:25;
then g2 . ((len (g | n2)) + ((len g) -' n1)) =
(g /^ n1) . ((len g) -' n1)
by FINSEQ_1:def 7
.=
x2
by A4, A21, A54, A53, RFINSEQ:def 1
;
then
g2 . (len g2) = x2
by A19, A25, A23, XREAL_0:def 2;
then
len g <= len g2
by A1, A26, A52, A29;
then
(len g) - n2 <= (n2 + ((len g) - n1)) - n2
by A25, XREAL_1:13;
hence
contradiction
by A17, XREAL_1:10;
verum end; end; end; hence
contradiction
;
verum end; suppose A55:
j2 < i2
;
contradictionreconsider n1 =
i2 -' 1,
n2 =
j2 as
Element of
NAT by ORDINAL1:def 12;
j2 + 1
<= i2
by A55, NAT_1:13;
then
j2 + 1
< i2
by A14, XXREAL_0:1;
then
j2 < i2 - 1
by XREAL_1:20;
then A56:
n1 > n2
by A6, XREAL_1:233;
1
< i2
by A8, A55, XXREAL_0:2;
then
1
+ 1
<= i2
by NAT_1:13;
then
1
<= i2 - 1
by XREAL_1:19;
then A57:
1
<= n1
by A6, XREAL_1:233;
set k =
(len g) -' n1;
reconsider g2 =
(g | n2) ^ (g /^ n1) as
FinSequence of
FT ;
A58:
len (g | n2) = n2
by A9, FINSEQ_1:59;
A59:
i2 -' 1
<= i2
by NAT_D:35;
then A60:
n1 <= len g
by A7, XXREAL_0:2;
then A61:
len (g /^ n1) = (len g) - n1
by RFINSEQ:def 1;
A62:
(len g) - n1 >= 0
by A60, XREAL_1:48;
then A63:
(len g) -' n1 = (len g) - n1
by XREAL_0:def 2;
A64:
len g2 =
(len (g | n2)) + (len (g /^ n1))
by FINSEQ_1:22
.=
n2 + ((len g) - n1)
by A60, A58, RFINSEQ:def 1
;
A65:
g2 . 1 =
(g | n2) . 1
by A8, A58, FINSEQ_1:64
.=
x1
by A3, A8, FINSEQ_3:112
;
now contradictionper cases
( n1 < len g or n1 = len g )
by A60, XXREAL_0:1;
suppose
n1 < len g
;
contradictionthen
n1 + 1
<= len g
by NAT_1:13;
then A66:
(n1 + 1) - n1 <= (len g) - n1
by XREAL_1:13;
then A67:
0 + 1
<= n2 + ((len g) - n1)
by XREAL_1:7;
A68:
g2 is
continuous
proof
thus
len g2 >= 1
by A64, A67;
FINTOPO6:def 6 for i being Nat
for x1 being Element of FT st 1 <= i & i < len g2 & x1 = g2 . i holds
g2 . (i + 1) in U_FT x1
let i be
Nat;
for x1 being Element of FT st 1 <= i & i < len g2 & x1 = g2 . i holds
g2 . (i + 1) in U_FT x1let z1 be
Element of
FT;
( 1 <= i & i < len g2 & z1 = g2 . i implies g2 . (i + 1) in U_FT z1 )
assume that A69:
1
<= i
and A70:
i < len g2
and A71:
z1 = g2 . i
;
g2 . (i + 1) in U_FT z1
A72:
i + 1
<= len g2
by A70, NAT_1:13;
reconsider i =
i as
Element of
NAT by ORDINAL1:def 12;
1
< i + 1
by A69, NAT_1:13;
then
i + 1
in dom g2
by A72, FINSEQ_3:25;
then
g2 . (i + 1) = g2 /. (i + 1)
by PARTFUN1:def 6;
then reconsider z2 =
g2 . (i + 1) as
Element of
FT ;
per cases
( i < n2 or i >= n2 )
;
suppose A73:
i < n2
;
g2 . (i + 1) in U_FT z1then A74:
i + 1
<= n2
by NAT_1:13;
i + 1
<= len (g | n2)
by A58, A73, NAT_1:13;
then A75:
z2 =
(g | n2) . (i + 1)
by FINSEQ_1:64, NAT_1:12
.=
g . (i + 1)
by A74, FINSEQ_3:112
;
A76:
i < len g
by A9, A73, XXREAL_0:2;
z1 =
(g | n2) . i
by A58, A69, A71, A73, FINSEQ_1:64
.=
g . i
by A73, FINSEQ_3:112
;
hence
g2 . (i + 1) in U_FT z1
by A5, A69, A76, A75;
verum end; suppose A77:
i >= n2
;
g2 . (i + 1) in U_FT z1
i - n2 < (n2 + ((len g) - n1)) - n2
by A64, A70, XREAL_1:9;
then A78:
i -' n2 < (len g) - n1
by A77, XREAL_1:233;
then
i -' n2 < (len g) -' n1
by A7, A59, XREAL_1:233, XXREAL_0:2;
then
(i -' n2) + 1
<= (len g) -' n1
by NAT_1:13;
then A79:
(i -' n2) + 1
<= len (g /^ n1)
by A7, A59, A61, XREAL_1:233, XXREAL_0:2;
A80:
(len (g | n2)) + (i -' n2) =
n2 + (i - n2)
by A58, A77, XREAL_1:233
.=
i
;
A81:
(len (g | n2)) + ((i -' n2) + 1) =
((i - n2) + 1) + n2
by A58, A77, XREAL_1:233
.=
i + 1
;
1
<= (i -' n2) + 1
by NAT_1:12;
then A82:
(i -' n2) + 1
in dom (g /^ n1)
by A79, FINSEQ_3:25;
per cases
( i > n2 or i = n2 )
by A77, XXREAL_0:1;
suppose
i > n2
;
g2 . (i + 1) in U_FT z1then A83:
i - n2 > 0
by XREAL_1:50;
then
i -' n2 = i - n2
by XREAL_0:def 2;
then A84:
0 + 1
<= i -' n2
by A83, NAT_1:13;
then A85:
i -' n2 in dom (g /^ n1)
by A61, A78, FINSEQ_3:25;
A86:
z2 =
(g /^ n1) . ((i -' n2) + 1)
by A79, A81, FINSEQ_1:65, NAT_1:12
.=
g . (((i -' n2) + 1) + n1)
by A60, A82, RFINSEQ:def 1
.=
g . (((i -' n2) + n1) + 1)
;
A87:
( 1
<= (i -' n2) + n1 &
(i -' n2) + n1 < ((len g) - n1) + n1 )
by A57, A78, NAT_1:12, XREAL_1:6;
z1 =
(g /^ n1) . (i -' n2)
by A61, A71, A78, A80, A84, FINSEQ_1:65
.=
g . ((i -' n2) + n1)
by A60, A85, RFINSEQ:def 1
;
hence
g2 . (i + 1) in U_FT z1
by A5, A86, A87;
verum end; suppose A88:
i = n2
;
g2 . (i + 1) in U_FT z1then A89:
z1 =
(g | n2) . n2
by A58, A69, A71, FINSEQ_1:64
.=
g . j2
by FINSEQ_3:112
;
z2 =
(g /^ n1) . ((i -' n2) + 1)
by A79, A81, FINSEQ_1:65, NAT_1:12
.=
g . (((i -' n2) + 1) + n1)
by A60, A82, RFINSEQ:def 1
.=
g . (((i -' n2) + n1) + 1)
.=
g . ((0 + (i2 -' 1)) + 1)
by A88, XREAL_1:232
.=
g . ((i2 - 1) + 1)
by A6, XREAL_1:233
.=
y
by A10
;
hence
g2 . (i + 1) in U_FT z1
by A2, A12, A89;
verum end; end; end; end;
end; A90:
rng (g /^ n1) c= rng g
by FINSEQ_5:33;
(
rng g2 = (rng (g | n2)) \/ (rng (g /^ n1)) &
rng (g | n2) c= rng g )
by FINSEQ_1:31, FINSEQ_5:19;
then
rng g2 c= rng g
by A90, XBOOLE_1:8;
then A91:
rng g2 c= A
by A13;
A92:
((len g) -' n1) + n1 = len g
by A63;
A93:
(len g) -' n1 in dom (g /^ n1)
by A63, A61, A66, FINSEQ_3:25;
then g2 . ((len (g | n2)) + ((len g) -' n1)) =
(g /^ n1) . ((len g) -' n1)
by FINSEQ_1:def 7
.=
x2
by A4, A60, A93, A92, RFINSEQ:def 1
;
then
g2 . (len g2) = x2
by A58, A64, A62, XREAL_0:def 2;
then
len g <= len g2
by A1, A65, A91, A68;
then
(len g) - n2 <= (n2 + ((len g) - n1)) - n2
by A64, XREAL_1:13;
hence
contradiction
by A56, XREAL_1:10;
verum end; end; end; hence
contradiction
;
verum end; end;
end;