let V be set ; :: thesis: for W being Function
for G being finite Graph
for P being oriented Chain of G
for v1, v2 being Element of the carrier of G st P is_orientedpath_of v1,v2,V & W is_weight>=0of G holds
ex q being oriented Simple Chain of G st q is_shortestpath_of v1,v2,V,W
let W be Function; :: thesis: for G being finite Graph
for P being oriented Chain of G
for v1, v2 being Element of the carrier of G st P is_orientedpath_of v1,v2,V & W is_weight>=0of G holds
ex q being oriented Simple Chain of G st q is_shortestpath_of v1,v2,V,W
let G be finite Graph; :: thesis: for P being oriented Chain of G
for v1, v2 being Element of the carrier of G st P is_orientedpath_of v1,v2,V & W is_weight>=0of G holds
ex q being oriented Simple Chain of G st q is_shortestpath_of v1,v2,V,W
let P be oriented Chain of G; :: thesis: for v1, v2 being Element of the carrier of G st P is_orientedpath_of v1,v2,V & W is_weight>=0of G holds
ex q being oriented Simple Chain of G st q is_shortestpath_of v1,v2,V,W
let v1, v2 be Element of the carrier of G; :: thesis: ( P is_orientedpath_of v1,v2,V & W is_weight>=0of G implies ex q being oriented Simple Chain of G st q is_shortestpath_of v1,v2,V,W )
assume A1:
( P is_orientedpath_of v1,v2,V & W is_weight>=0of G )
; :: thesis: ex q being oriented Simple Chain of G st q is_shortestpath_of v1,v2,V,W
then
AcyclicPaths v1,v2,V <> {}
by Th48;
then consider r being FinSequence of the carrier' of G such that
A2:
( r in AcyclicPaths v1,v2,V & ( for s being FinSequence of the carrier' of G st s in AcyclicPaths v1,v2,V holds
cost r,W <= cost s,W ) )
by Th57;
consider t being oriented Simple Chain of G such that
A3:
( r = t & t is_acyclicpath_of v1,v2,V )
by A2;
take
t
; :: thesis: t is_shortestpath_of v1,v2,V,W
thus
t is_orientedpath_of v1,v2,V
by A3, Def7; :: according to GRAPH_5:def 18 :: thesis: for q being oriented Chain of G st q is_orientedpath_of v1,v2,V holds
cost t,W <= cost q,W
hereby :: thesis: verum
let s be
oriented Chain of
G;
:: thesis: ( s is_orientedpath_of v1,v2,V implies cost t,W <= cost s,W )assume A4:
s is_orientedpath_of v1,
v2,
V
;
:: thesis: cost t,W <= cost s,Wthen
AcyclicPaths s <> {}
by Th48;
then consider x being
Element of the
carrier' of
G * such that A5:
x in AcyclicPaths s
by SUBSET_1:10;
A6:
cost x,
W <= cost s,
W
by A1, A5, Th60;
AcyclicPaths s c= AcyclicPaths v1,
v2,
V
by A4, Th45;
then
cost r,
W <= cost x,
W
by A2, A5;
hence
cost t,
W <= cost s,
W
by A3, A6, XXREAL_0:2;
:: thesis: verum
end;