let G be finite nonnegative-weighted WGraph; for W being DPath of G
for x, y being set
for m, n being Element of NAT st W is_mincost_DPath_from x,y holds
W .cut m,n is_mincost_DPath_from (W .cut m,n) .first() ,(W .cut m,n) .last()
let W be DPath of G; for x, y being set
for m, n being Element of NAT st W is_mincost_DPath_from x,y holds
W .cut m,n is_mincost_DPath_from (W .cut m,n) .first() ,(W .cut m,n) .last()
let x, y be set ; for m, n being Element of NAT st W is_mincost_DPath_from x,y holds
W .cut m,n is_mincost_DPath_from (W .cut m,n) .first() ,(W .cut m,n) .last()
let m, n be Element of NAT ; ( W is_mincost_DPath_from x,y implies W .cut m,n is_mincost_DPath_from (W .cut m,n) .first() ,(W .cut m,n) .last() )
set WC = W .cut m,n;
A1:
W .cut m,n is_Walk_from (W .cut m,n) .first() ,(W .cut m,n) .last()
by GLIB_001:def 23;
assume A2:
W is_mincost_DPath_from x,y
; W .cut m,n is_mincost_DPath_from (W .cut m,n) .first() ,(W .cut m,n) .last()
then A3:
W is_Walk_from x,y
by Def2;
then A4:
( W . 1 = x & W . (len W) = y )
by GLIB_001:18;
now per cases
( ( not m is even & not n is even & m <= n & n <= len W ) or m is even or n is even or not m <= n or not n <= len W )
;
suppose A5:
( not
m is
even & not
n is
even &
m <= n &
n <= len W )
;
W .cut m,n is_mincost_DPath_from (W .cut m,n) .first() ,(W .cut m,n) .last() set W1 =
W .cut 1,
m;
set W3 =
W .cut n,
(len W);
A6:
1
<= n
by A5, HEYTING3:1;
then A7:
(W .cut 1,n) .append (W .cut n,(len W)) =
W .cut 1,
(len W)
by A5, GLIB_001:39, JORDAN12:3
.=
W
by GLIB_001:40
;
(W .cut 1,n) .last() =
W . n
by A5, A6, GLIB_001:38, JORDAN12:3
.=
(W .cut n,(len W)) .first()
by A5, GLIB_001:38
;
then A8:
W .cost() = ((W .cut 1,n) .cost() ) + ((W .cut n,(len W)) .cost() )
by A7, GLIB_003:31;
A9:
1
<= m
by A5, HEYTING3:1;
then A10:
(W .cut 1,m) .append (W .cut m,n) = W .cut 1,
n
by A5, GLIB_001:39, JORDAN12:3;
A11:
m <= len W
by A5, XXREAL_0:2;
then (W .cut 1,m) .last() =
W . m
by A5, A9, GLIB_001:38, JORDAN12:3
.=
(W .cut m,n) .first()
by A5, GLIB_001:38
;
then
(W .cut 1,n) .cost() = ((W .cut 1,m) .cost() ) + ((W .cut m,n) .cost() )
by A10, GLIB_003:31;
then A12:
W .cost() = ((W .cut m,n) .cost() ) + (((W .cut 1,m) .cost() ) + ((W .cut n,(len W)) .cost() ))
by A8;
A13:
W .cut n,
(len W) is_Walk_from W . n,
W . (len W)
by A5, GLIB_001:38;
A14:
W .cut 1,
m is_Walk_from W . 1,
W . m
by A5, A9, A11, GLIB_001:38, JORDAN12:3;
now assume
not
W .cut m,
n is_mincost_DPath_from (W .cut m,n) .first() ,
(W .cut m,n) .last()
;
contradictionthen consider W2 being
DPath of
G such that A15:
W2 is_Walk_from (W .cut m,n) .first() ,
(W .cut m,n) .last()
and A16:
W2 .cost() < (W .cut m,n) .cost()
by A1, Def2;
set WA =
(W .cut 1,m) .append W2;
set WB =
((W .cut 1,m) .append W2) .append (W .cut n,(len W));
consider WB2 being
DPath of
((W .cut 1,m) .append W2) .append (W .cut n,(len W));
A17:
(W .cut m,n) .last() = W . n
by A5, GLIB_001:38;
A18:
(W .cut m,n) .first() = W . m
by A5, GLIB_001:38;
then
(W .cut 1,m) .append W2 is_Walk_from W . 1,
W . n
by A14, A15, A17, GLIB_001:32;
then
((W .cut 1,m) .append W2) .append (W .cut n,(len W)) is_Walk_from x,
y
by A4, A13, GLIB_001:32;
then A19:
WB2 is_Walk_from x,
y
by GLIB_001:161;
W2 .first() = W . m
by A15, A18, GLIB_001:def 23;
then A20:
(W .cut 1,m) .last() = W2 .first()
by A5, A9, A11, GLIB_001:38, JORDAN12:3;
then A21:
((W .cut 1,m) .append W2) .cost() = ((W .cut 1,m) .cost() ) + (W2 .cost() )
by GLIB_003:31;
W2 .last() = W . n
by A15, A17, GLIB_001:def 23;
then (W .cut n,(len W)) .first() =
W2 .last()
by A5, GLIB_001:38
.=
((W .cut 1,m) .append W2) .last()
by A20, GLIB_001:31
;
then (((W .cut 1,m) .append W2) .append (W .cut n,(len W))) .cost() =
(((W .cut 1,m) .cost() ) + (W2 .cost() )) + ((W .cut n,(len W)) .cost() )
by A21, GLIB_003:31
.=
(W2 .cost() ) + (((W .cut 1,m) .cost() ) + ((W .cut n,(len W)) .cost() ))
;
then A22:
(((W .cut 1,m) .append W2) .append (W .cut n,(len W))) .cost() < W .cost()
by A12, A16, XREAL_1:10;
WB2 .cost() <= (((W .cut 1,m) .append W2) .append (W .cut n,(len W))) .cost()
by GLIB_003:37;
then
WB2 .cost() < W .cost()
by A22, XXREAL_0:2;
hence
contradiction
by A2, A19, Def2;
verum end; hence
W .cut m,
n is_mincost_DPath_from (W .cut m,n) .first() ,
(W .cut m,n) .last()
;
verum end; suppose
(
m is
even or
n is
even or not
m <= n or not
n <= len W )
;
W .cut m,n is_mincost_DPath_from (W .cut m,n) .first() ,(W .cut m,n) .last() then A23:
W .cut m,
n = W
by GLIB_001:def 11;
then
(W .cut m,n) .first() = x
by A3, GLIB_001:def 23;
hence
W .cut m,
n is_mincost_DPath_from (W .cut m,n) .first() ,
(W .cut m,n) .last()
by A2, A3, A23, GLIB_001:def 23;
verum end;
hence
W .cut m,n is_mincost_DPath_from (W .cut m,n) .first() ,(W .cut m,n) .last()
; verum