let V, e be set ; for G being oriented finite Graph
for P, Q being oriented Chain of G
for W being Function of the carrier' of G,Real>=0
for v1, v2, v3 being Vertex of G st e in the carrier' of G & P is_shortestpath_of v1,v2,V,W & v1 <> v3 & Q = P ^ <*e*> & e orientedly_joins v2,v3 & v1 in V & ( for v4 being Vertex of G st v4 in V holds
for ee being set holds
( not ee in the carrier' of G or not ee orientedly_joins v4,v3 ) ) holds
Q is_shortestpath_of v1,v3,V \/ {v2},W
let G be oriented finite Graph; for P, Q being oriented Chain of G
for W being Function of the carrier' of G,Real>=0
for v1, v2, v3 being Vertex of G st e in the carrier' of G & P is_shortestpath_of v1,v2,V,W & v1 <> v3 & Q = P ^ <*e*> & e orientedly_joins v2,v3 & v1 in V & ( for v4 being Vertex of G st v4 in V holds
for ee being set holds
( not ee in the carrier' of G or not ee orientedly_joins v4,v3 ) ) holds
Q is_shortestpath_of v1,v3,V \/ {v2},W
let P, Q be oriented Chain of G; for W being Function of the carrier' of G,Real>=0
for v1, v2, v3 being Vertex of G st e in the carrier' of G & P is_shortestpath_of v1,v2,V,W & v1 <> v3 & Q = P ^ <*e*> & e orientedly_joins v2,v3 & v1 in V & ( for v4 being Vertex of G st v4 in V holds
for ee being set holds
( not ee in the carrier' of G or not ee orientedly_joins v4,v3 ) ) holds
Q is_shortestpath_of v1,v3,V \/ {v2},W
let W be Function of the carrier' of G,Real>=0; for v1, v2, v3 being Vertex of G st e in the carrier' of G & P is_shortestpath_of v1,v2,V,W & v1 <> v3 & Q = P ^ <*e*> & e orientedly_joins v2,v3 & v1 in V & ( for v4 being Vertex of G st v4 in V holds
for ee being set holds
( not ee in the carrier' of G or not ee orientedly_joins v4,v3 ) ) holds
Q is_shortestpath_of v1,v3,V \/ {v2},W
let v1, v2, v3 be Vertex of G; ( e in the carrier' of G & P is_shortestpath_of v1,v2,V,W & v1 <> v3 & Q = P ^ <*e*> & e orientedly_joins v2,v3 & v1 in V & ( for v4 being Vertex of G st v4 in V holds
for ee being set holds
( not ee in the carrier' of G or not ee orientedly_joins v4,v3 ) ) implies Q is_shortestpath_of v1,v3,V \/ {v2},W )
assume that
A1:
e in the carrier' of G
and
A2:
P is_shortestpath_of v1,v2,V,W
and
A3:
v1 <> v3
and
A4:
Q = P ^ <*e*>
and
A5:
e orientedly_joins v2,v3
and
A6:
v1 in V
and
A7:
for v4 being Vertex of G st v4 in V holds
for ee being set holds
( not ee in the carrier' of G or not ee orientedly_joins v4,v3 )
; Q is_shortestpath_of v1,v3,V \/ {v2},W
set Eg = the carrier' of G;
reconsider pe = <*e*> as FinSequence of the carrier' of G by A1, FINSEQ_1:74;
A8:
P is_orientedpath_of v1,v2,V
by A2, GRAPH_5:def 18;
then
P is_orientedpath_of v1,v2
by GRAPH_5:def 4;
then
P <> {}
by GRAPH_5:def 3;
then A9:
len P >= 1
by FINSEQ_1:20;
set V9 = V \/ {v2};
set FS = the Source of G;
set FT = the Target of G;
A10:
W is_weight>=0of G
by GRAPH_5:def 13;
A11:
now for S being oriented Chain of G st S is_orientedpath_of v1,v3,V \/ {v2} holds
cost (Q,W) <= cost (S,W)let S be
oriented Chain of
G;
( S is_orientedpath_of v1,v3,V \/ {v2} implies cost (Q,W) <= cost (S,W) )assume A12:
S is_orientedpath_of v1,
v3,
V \/ {v2}
;
cost (Q,W) <= cost (S,W)then consider s being
oriented Simple Chain of
G such that A13:
s is_shortestpath_of v1,
v3,
V \/ {v2},
W
by A10, GRAPH_5:62;
set Vs =
vertices s;
A14:
s is_orientedpath_of v1,
v3,
V \/ {v2}
by A13, GRAPH_5:def 18;
then A15:
s is_orientedpath_of v1,
v3
by GRAPH_5:def 4;
then A16:
the
Target of
G . (s . (len s)) = v3
by GRAPH_5:def 3;
A17:
(vertices s) \ {v3} c= V \/ {v2}
by A14, GRAPH_5:def 4;
s <> {}
by A15, GRAPH_5:def 3;
then A18:
len s >= 1
by FINSEQ_1:20;
then consider i being
Nat such that A19:
len s = 1
+ i
by NAT_1:10;
consider s1,
s2 being
FinSequence such that A20:
len s1 = i
and A21:
len s2 = 1
and A22:
s = s1 ^ s2
by A19, FINSEQ_2:22;
reconsider s1 =
s1,
s2 =
s2 as
oriented Simple Chain of
G by A22, GRAPH_5:14;
reconsider vx = the
Source of
G . (s2 . 1) as
Vertex of
G by A21, Lm3;
A23:
s2 . 1
= s . (len s)
by A19, A20, A21, A22, Lm2;
A24:
the
Source of
G . (s . 1) = v1
by A15, GRAPH_5:def 3;
A25:
s1 <> {}
then A27:
len s1 >= 1
by FINSEQ_1:20;
len s1 < len s
by A19, A20, NAT_1:13;
then A28: the
Source of
G . (s . (len s)) =
the
Target of
G . (s . (len s1))
by A19, A20, A27, GRAPH_1:def 15
.=
the
Target of
G . (s1 . (len s1))
by A22, A27, Lm1
;
A29:
now not vx <> v2
vx <> the
Target of
G . (s . (len s))
by A21, A22, A23, A27, A28, Th6;
then A30:
not
vx in {v3}
by A16, TARSKI:def 1;
vx in vertices s
by A18, A23, Lm4;
then
vx in (vertices s) \ {v3}
by A30, XBOOLE_0:def 5;
then A31:
(
vx in V or
vx in {v2} )
by A17, XBOOLE_0:def 3;
assume A32:
vx <> v2
;
contradiction
(
s2 . 1
orientedly_joins vx,
v3 &
s2 . 1
in the
carrier' of
G )
by A21, A23, A16, Th2, GRAPH_4:def 1;
hence
contradiction
by A7, A32, A31, TARSKI:def 1;
verum end;
len s2 = 1
by A21;
then
not the
Target of
G . (s . (len s)) in vertices s1
by A3, A22, A24, A16, A27, GRAPH_5:18;
then A33:
(vertices s1) \ {v3} = vertices s1
by A16, ZFMISC_1:57;
vertices s1 c= vertices (s1 ^ s2)
by GRAPH_5:26;
then
vertices s1 c= (vertices s) \ {v3}
by A22, A33, XBOOLE_1:33;
then
vertices s1 c= V \/ {v2}
by A17;
then
(vertices s1) \ {v2} c= (V \/ {v2}) \ {v2}
by XBOOLE_1:33;
then
(vertices s1) \ {v2} c= V \ {v2}
by XBOOLE_1:40;
then A34:
(vertices s1) \ {v2} c= V
by XBOOLE_1:1;
s2 /. 1
in the
carrier' of
G
by A1;
then A35:
s2 . 1
in the
carrier' of
G
by A21, FINSEQ_4:15;
( the
Source of
G . e = v2 & the
Target of
G . e = v3 )
by A5, GRAPH_4:def 1;
then
e = s2 . 1
by A1, A23, A16, A29, A35, GRAPH_1:def 7;
then
s2 = <*e*>
by A21, FINSEQ_1:40;
then A36:
cost (
Q,
W)
= (cost (P,W)) + (cost (s2,W))
by A4, A10, GRAPH_5:46, GRAPH_5:54;
the
Source of
G . (s1 . 1) = v1
by A22, A24, A27, Lm1;
then
s1 is_orientedpath_of v1,
v2
by A23, A25, A28, A29, GRAPH_5:def 3;
then
s1 is_orientedpath_of v1,
v2,
V
by A34, GRAPH_5:def 4;
then A37:
cost (
P,
W)
<= cost (
s1,
W)
by A2, GRAPH_5:def 18;
A38:
cost (
s,
W)
<= cost (
S,
W)
by A12, A13, GRAPH_5:def 18;
cost (
s,
W)
= (cost (s1,W)) + (cost (s2,W))
by A10, A22, GRAPH_5:46, GRAPH_5:54;
then
cost (
Q,
W)
<= cost (
s,
W)
by A37, A36, XREAL_1:7;
hence
cost (
Q,
W)
<= cost (
S,
W)
by A38, XXREAL_0:2;
verum end;
( len pe = 1 & pe . 1 = e )
by FINSEQ_1:40;
then
Q is_orientedpath_of v1,v3,V \/ {v2}
by A4, A5, A8, A9, GRAPH_5:34;
hence
Q is_shortestpath_of v1,v3,V \/ {v2},W
by A11, GRAPH_5:def 18; verum