let G be Graph; ( G is connected iff for v1, v2 being Vertex of G st v1 <> v2 holds
ex c being Chain of G ex vs being FinSequence of the carrier of G st
( not c is empty & vs is_vertex_seq_of c & vs . 1 = v1 & vs . (len vs) = v2 ) )
set E = the carrier' of G;
set S = the Source of G;
set T = the Target of G;
thus
( G is connected implies for v1, v2 being Vertex of G st v1 <> v2 holds
ex c being Chain of G ex vs being FinSequence of the carrier of G st
( not c is empty & vs is_vertex_seq_of c & vs . 1 = v1 & vs . (len vs) = v2 ) )
( ( for v1, v2 being Vertex of G st v1 <> v2 holds
ex c being Chain of G ex vs being FinSequence of the carrier of G st
( not c is empty & vs is_vertex_seq_of c & vs . 1 = v1 & vs . (len vs) = v2 ) ) implies G is connected )proof
reconsider V = the
carrier of
G as non
empty set ;
assume A1:
G is
connected
;
for v1, v2 being Vertex of G st v1 <> v2 holds
ex c being Chain of G ex vs being FinSequence of the carrier of G st
( not c is empty & vs is_vertex_seq_of c & vs . 1 = v1 & vs . (len vs) = v2 )
let v1,
v2 be
Vertex of
G;
( v1 <> v2 implies ex c being Chain of G ex vs being FinSequence of the carrier of G st
( not c is empty & vs is_vertex_seq_of c & vs . 1 = v1 & vs . (len vs) = v2 ) )
set V1 =
{ v where v is Element of V : ( v = v1 or ex c being Chain of G ex vs being FinSequence of the carrier of G st
( not c is empty & vs is_vertex_seq_of c & vs . 1 = v1 & vs . (len vs) = v ) ) } ;
set V2 =
V \ { v where v is Element of V : ( v = v1 or ex c being Chain of G ex vs being FinSequence of the carrier of G st
( not c is empty & vs is_vertex_seq_of c & vs . 1 = v1 & vs . (len vs) = v ) ) } ;
v1 in { v where v is Element of V : ( v = v1 or ex c being Chain of G ex vs being FinSequence of the carrier of G st
( not c is empty & vs is_vertex_seq_of c & vs . 1 = v1 & vs . (len vs) = v ) ) }
;
then reconsider V1 =
{ v where v is Element of V : ( v = v1 or ex c being Chain of G ex vs being FinSequence of the carrier of G st
( not c is empty & vs is_vertex_seq_of c & vs . 1 = v1 & vs . (len vs) = v ) ) } as non
empty set ;
assume A2:
v1 <> v2
;
ex c being Chain of G ex vs being FinSequence of the carrier of G st
( not c is empty & vs is_vertex_seq_of c & vs . 1 = v1 & vs . (len vs) = v2 )
assume A3:
for
c being
Chain of
G for
vs being
FinSequence of the
carrier of
G holds
(
c is
empty or not
vs is_vertex_seq_of c or not
vs . 1
= v1 or not
vs . (len vs) = v2 )
;
contradiction
then reconsider V2 =
V \ { v where v is Element of V : ( v = v1 or ex c being Chain of G ex vs being FinSequence of the carrier of G st
( not c is empty & vs is_vertex_seq_of c & vs . 1 = v1 & vs . (len vs) = v ) ) } as non
empty set by XBOOLE_0:def 5;
defpred S1[
set ]
means ( $1
= v1 or ex
c being
Chain of
G ex
vs being
FinSequence of the
carrier of
G st
( not
c is
empty &
vs is_vertex_seq_of c &
vs . 1
= v1 &
vs . (len vs) = $1 ) );
A4:
{ v where v is Element of V : S1[v] } is
Subset of
V
from DOMAIN_1:sch 7();
defpred S2[
object ]
means ( the
Source of
G . $1
in V1 & the
Target of
G . $1
in V1 );
consider E1 being
set such that A5:
for
e being
object holds
(
e in E1 iff (
e in the
carrier' of
G &
S2[
e] ) )
from XBOOLE_0:sch 1();
A6:
dom the
Source of
G = the
carrier' of
G
by FUNCT_2:def 1;
set E2 = the
carrier' of
G \ E1;
A7:
dom ( the Source of G | ( the carrier' of G \ E1)) =
(dom the Source of G) /\ ( the carrier' of G \ E1)
by RELAT_1:61
.=
the
carrier' of
G \ E1
by A6, XBOOLE_1:28
;
A8:
rng the
Source of
G c= V
by RELAT_1:def 19;
rng ( the Source of G | ( the carrier' of G \ E1)) c= V2
proof
let v be
object ;
TARSKI:def 3 ( not v in rng ( the Source of G | ( the carrier' of G \ E1)) or v in V2 )
assume
v in rng ( the Source of G | ( the carrier' of G \ E1))
;
v in V2
then consider e being
object such that A9:
e in dom ( the Source of G | ( the carrier' of G \ E1))
and A10:
( the Source of G | ( the carrier' of G \ E1)) . e = v
by FUNCT_1:def 3;
reconsider e =
e as
Element of the
carrier' of
G by A7, A9;
A11:
( the Source of G | ( the carrier' of G \ E1)) . e = the
Source of
G . e
by A9, FUNCT_1:47;
A12:
not
e in E1
by A7, A9, XBOOLE_0:def 5;
per cases
( not e in the carrier' of G or not the Source of G . e in V1 or not the Target of G . e in V1 )
by A5, A12;
suppose A14:
not the
Target of
G . e in V1
;
v in V2reconsider Te = the
Target of
G . e as
Vertex of
G by A7, A9, FUNCT_2:5;
(
v in rng ( the Source of G | ( the carrier' of G \ E1)) &
rng ( the Source of G | ( the carrier' of G \ E1)) c= rng the
Source of
G )
by A9, A10, FUNCT_1:def 3, RELAT_1:70;
then A15:
v in rng the
Source of
G
;
assume
not
v in V2
;
contradictionthen
v in V1
by A8, A15, XBOOLE_0:def 5;
then consider v9 being
Vertex of
G such that A16:
v9 = v
and A17:
(
v9 = v1 or ex
c being
Chain of
G ex
vs being
FinSequence of the
carrier of
G st
( not
c is
empty &
vs is_vertex_seq_of c &
vs . 1
= v1 &
vs . (len vs) = v9 ) )
;
thus
contradiction
verumproof
per cases
( v9 = v1 or ex c being Chain of G ex vs being FinSequence of the carrier of G st
( not c is empty & vs is_vertex_seq_of c & vs . 1 = v1 & vs . (len vs) = v9 ) )
by A17;
suppose A18:
v9 = v1
;
contradictionend; suppose
ex
c being
Chain of
G ex
vs being
FinSequence of the
carrier of
G st
( not
c is
empty &
vs is_vertex_seq_of c &
vs . 1
= v1 &
vs . (len vs) = v9 )
;
contradictionthen consider c being
Chain of
G,
vs being
FinSequence of the
carrier of
G such that
not
c is
empty
and A20:
vs is_vertex_seq_of c
and A21:
vs . 1
= v1
and A22:
vs . (len vs) = v9
;
reconsider c9 =
c ^ <*e*> as
Chain of
G by A7, A9, A10, A11, A16, A20, A22, Th12;
ex
vs9 being
FinSequence of the
carrier of
G st
(
vs9 = vs ^' <*( the Source of G . e),( the Target of G . e)*> &
vs9 is_vertex_seq_of c9 &
vs9 . 1
= vs . 1 &
vs9 . (len vs9) = Te )
by A7, A9, A10, A11, A16, A20, A22, Th12;
hence
contradiction
by A14, A21;
verum end;
end; end;
end;
then reconsider S2 = the
Source of
G | ( the carrier' of G \ E1) as
Function of
( the carrier' of G \ E1),
V2 by A7, FUNCT_2:def 1, RELSET_1:4;
A23:
dom the
Target of
G = the
carrier' of
G
by FUNCT_2:def 1;
A24:
dom ( the Target of G | ( the carrier' of G \ E1)) =
(dom the Target of G) /\ ( the carrier' of G \ E1)
by RELAT_1:61
.=
the
carrier' of
G \ E1
by A23, XBOOLE_1:28
;
A25:
rng the
Target of
G c= V
by RELAT_1:def 19;
rng ( the Target of G | ( the carrier' of G \ E1)) c= V2
proof
let v be
object ;
TARSKI:def 3 ( not v in rng ( the Target of G | ( the carrier' of G \ E1)) or v in V2 )
assume
v in rng ( the Target of G | ( the carrier' of G \ E1))
;
v in V2
then consider e being
object such that A26:
e in dom ( the Target of G | ( the carrier' of G \ E1))
and A27:
( the Target of G | ( the carrier' of G \ E1)) . e = v
by FUNCT_1:def 3;
reconsider e =
e as
Element of the
carrier' of
G by A24, A26;
A28:
( the Target of G | ( the carrier' of G \ E1)) . e = the
Target of
G . e
by A26, FUNCT_1:47;
A29:
not
e in E1
by A24, A26, XBOOLE_0:def 5;
per cases
( not e in the carrier' of G or not the Target of G . e in V1 or not the Source of G . e in V1 )
by A5, A29;
suppose A31:
not the
Source of
G . e in V1
;
v in V2reconsider Se = the
Source of
G . e as
Vertex of
G by A24, A26, FUNCT_2:5;
(
v in rng ( the Target of G | ( the carrier' of G \ E1)) &
rng ( the Target of G | ( the carrier' of G \ E1)) c= rng the
Target of
G )
by A26, A27, FUNCT_1:def 3, RELAT_1:70;
then A32:
v in rng the
Target of
G
;
assume
not
v in V2
;
contradictionthen
v in V1
by A25, A32, XBOOLE_0:def 5;
then consider v9 being
Vertex of
G such that A33:
v9 = v
and A34:
(
v9 = v1 or ex
c being
Chain of
G ex
vs being
FinSequence of the
carrier of
G st
( not
c is
empty &
vs is_vertex_seq_of c &
vs . 1
= v1 &
vs . (len vs) = v9 ) )
;
thus
contradiction
verumproof
per cases
( v9 = v1 or ex c being Chain of G ex vs being FinSequence of the carrier of G st
( not c is empty & vs is_vertex_seq_of c & vs . 1 = v1 & vs . (len vs) = v9 ) )
by A34;
suppose A35:
v9 = v1
;
contradictionend; suppose
ex
c being
Chain of
G ex
vs being
FinSequence of the
carrier of
G st
( not
c is
empty &
vs is_vertex_seq_of c &
vs . 1
= v1 &
vs . (len vs) = v9 )
;
contradictionthen consider c being
Chain of
G,
vs being
FinSequence of the
carrier of
G such that
not
c is
empty
and A37:
vs is_vertex_seq_of c
and A38:
vs . 1
= v1
and A39:
vs . (len vs) = v9
;
reconsider c9 =
c ^ <*e*> as
Chain of
G by A24, A26, A27, A28, A33, A37, A39, Th13;
ex
vs9 being
FinSequence of the
carrier of
G st
(
vs9 = vs ^' <*( the Target of G . e),( the Source of G . e)*> &
vs9 is_vertex_seq_of c9 &
vs9 . 1
= vs . 1 &
vs9 . (len vs9) = Se )
by A24, A26, A27, A28, A33, A37, A39, Th13;
hence
contradiction
by A31, A38;
verum end;
end; end;
end;
then reconsider T2 = the
Target of
G | ( the carrier' of G \ E1) as
Function of
( the carrier' of G \ E1),
V2 by A24, FUNCT_2:def 1, RELSET_1:4;
A40:
E1 c= the
carrier' of
G
by A5;
A41:
dom ( the Target of G | E1) =
(dom the Target of G) /\ E1
by RELAT_1:61
.=
the
carrier' of
G /\ E1
by FUNCT_2:def 1
.=
E1
by A40, XBOOLE_1:28
;
rng ( the Target of G | E1) c= V1
then reconsider T1 = the
Target of
G | E1 as
Function of
E1,
V1 by A41, FUNCT_2:def 1, RELSET_1:4;
A44:
dom ( the Source of G | E1) =
(dom the Source of G) /\ E1
by RELAT_1:61
.=
the
carrier' of
G /\ E1
by FUNCT_2:def 1
.=
E1
by A40, XBOOLE_1:28
;
rng ( the Source of G | E1) c= V1
then reconsider S1 = the
Source of
G | E1 as
Function of
E1,
V1 by A44, FUNCT_2:def 1, RELSET_1:4;
reconsider G1 =
MultiGraphStruct(#
V1,
E1,
S1,
T1 #),
G2 =
MultiGraphStruct(#
V2,
( the carrier' of G \ E1),
S2,
T2 #) as
Graph ;
A47:
G is_sum_of G1,
G2
proof
reconsider MG =
MultiGraphStruct(# the
carrier of
G, the
carrier' of
G, the
Source of
G, the
Target of
G #) as
strict Graph ;
thus A48:
the
Target of
G1 tolerates the
Target of
G2
GRAPH_1:def 6 ( the Source of G1 tolerates the Source of G2 & MultiGraphStruct(# the carrier of G, the carrier' of G, the Source of G, the Target of G #) = G1 \/ G2 )
thus A51:
the
Source of
G1 tolerates the
Source of
G2
MultiGraphStruct(# the carrier of G, the carrier' of G, the Source of G, the Target of G #) = G1 \/ G2
A54:
( ( for
v being
set st
v in the
carrier' of
G1 holds
( the
Source of
MG . v = the
Source of
G1 . v & the
Target of
MG . v = the
Target of
G1 . v ) ) & ( for
v being
set st
v in the
carrier' of
G2 holds
( the
Source of
MG . v = the
Source of
G2 . v & the
Target of
MG . v = the
Target of
G2 . v ) ) )
by FUNCT_1:49;
( the
carrier of
MG = the
carrier of
G1 \/ the
carrier of
G2 & the
carrier' of
MG = the
carrier' of
G1 \/ the
carrier' of
G2 )
by A4, A40, XBOOLE_1:45;
hence
MultiGraphStruct(# the
carrier of
G, the
carrier' of
G, the
Source of
G, the
Target of
G #)
= G1 \/ G2
by A48, A51, A54, GRAPH_1:def 5;
verum
end;
V1 misses V2
by XBOOLE_1:79;
hence
contradiction
by A1, A47;
verum
end;
assume A55:
for v1, v2 being Vertex of G st v1 <> v2 holds
ex c being Chain of G ex vs being FinSequence of the carrier of G st
( not c is empty & vs is_vertex_seq_of c & vs . 1 = v1 & vs . (len vs) = v2 )
; G is connected
thus
G is connected
verumproof
given G1,
G2 being
Graph such that A56:
the
carrier of
G1 misses the
carrier of
G2
and A57:
G is_sum_of G1,
G2
;
GRAPH_1:def 10 contradiction
set v2 = the
Vertex of
G2;
set v1 = the
Vertex of
G1;
set V2 = the
carrier of
G2;
set V1 = the
carrier of
G1;
set T2 = the
Target of
G2;
set T1 = the
Target of
G1;
set S2 = the
Source of
G2;
set S1 = the
Source of
G1;
set E1 = the
carrier' of
G1;
A58:
MultiGraphStruct(# the
carrier of
G, the
carrier' of
G, the
Source of
G, the
Target of
G #)
= G1 \/ G2
by A57;
A59:
( the
Target of
G1 tolerates the
Target of
G2 & the
Source of
G1 tolerates the
Source of
G2 )
by A57;
then A60:
the
carrier' of
G = the
carrier' of
G1 \/ the
carrier' of
G2
by A58, GRAPH_1:def 5;
the
carrier of
MultiGraphStruct(# the
carrier of
G, the
carrier' of
G, the
Source of
G, the
Target of
G #)
= the
carrier of
G1 \/ the
carrier of
G2
by A59, A58, GRAPH_1:def 5;
then reconsider v19 = the
Vertex of
G1,
v29 = the
Vertex of
G2 as
Vertex of
G by XBOOLE_0:def 3;
A61:
the
carrier of
G1 /\ the
carrier of
G2 = {}
by A56;
then
the
Vertex of
G1 <> the
Vertex of
G2
by XBOOLE_0:def 4;
then consider c being
Chain of
G,
vs being
FinSequence of the
carrier of
G such that
not
c is
empty
and A62:
vs is_vertex_seq_of c
and A63:
vs . 1
= v19
and A64:
vs . (len vs) = v29
by A55;
defpred S1[
Nat]
means ( $1
in dom vs &
vs . $1 is
Vertex of
G2 );
A65:
len vs = (len c) + 1
by A62;
c is
FinSequence of the
carrier' of
G
by MSSCYC_1:def 1;
then A66:
rng c c= the
carrier' of
G
by FINSEQ_1:def 4;
1
<= (len c) + 1
by NAT_1:11;
then
len vs in dom vs
by A65, FINSEQ_3:25;
then A67:
ex
k being
Nat st
S1[
k]
by A64;
consider k being
Nat such that A68:
S1[
k]
and A69:
for
n being
Nat st
S1[
n] holds
k <= n
from NAT_1:sch 5(A67);
A70:
1
<= k
by A68, FINSEQ_3:25;
k <> 1
by A61, A63, A68, XBOOLE_0:def 4;
then
1
< k
by A70, XXREAL_0:1;
then
1
+ 1
<= k
by NAT_1:13;
then consider i being
Nat such that A71:
1
<= i
and A72:
i < k
and A73:
k = i + 1
by FINSEQ_6:127;
set e =
c . i;
A74:
k <= len vs
by A68, FINSEQ_3:25;
then A75:
i <= len c
by A65, A73, XREAL_1:6;
then
i in dom c
by A71, FINSEQ_3:25;
then A76:
c . i in rng c
by FUNCT_1:def 3;
i <= len vs
by A72, A74, XXREAL_0:2;
then A77:
i in dom vs
by A71, FINSEQ_3:25;
end;