let G1, G2 be _Graph; for F being PGraphMapping of G1,G2 st F is isomorphism holds
( ( G1 is acyclic implies G2 is acyclic ) & ( G2 is acyclic implies G1 is acyclic ) & ( G1 is chordal implies G2 is chordal ) & ( G2 is chordal implies G1 is chordal ) & ( G1 is connected implies G2 is connected ) & ( G2 is connected implies G1 is connected ) )
let F be PGraphMapping of G1,G2; ( F is isomorphism implies ( ( G1 is acyclic implies G2 is acyclic ) & ( G2 is acyclic implies G1 is acyclic ) & ( G1 is chordal implies G2 is chordal ) & ( G2 is chordal implies G1 is chordal ) & ( G1 is connected implies G2 is connected ) & ( G2 is connected implies G1 is connected ) ) )
assume A1:
F is isomorphism
; ( ( G1 is acyclic implies G2 is acyclic ) & ( G2 is acyclic implies G1 is acyclic ) & ( G1 is chordal implies G2 is chordal ) & ( G2 is chordal implies G1 is chordal ) & ( G1 is connected implies G2 is connected ) & ( G2 is connected implies G1 is connected ) )
then reconsider F = F as non empty one-to-one PGraphMapping of G1,G2 ;
A2:
( F " is isomorphism & F " is semi-continuous )
by A1, Th75;
hence
( G1 is acyclic iff G2 is acyclic )
by A1, Th139; ( ( G1 is chordal implies G2 is chordal ) & ( G2 is chordal implies G1 is chordal ) & ( G1 is connected implies G2 is connected ) & ( G2 is connected implies G1 is connected ) )
A3:
F is semi-continuous
;
hereby ( ( G2 is chordal implies G1 is chordal ) & ( G1 is connected implies G2 is connected ) & ( G2 is connected implies G1 is connected ) )
assume A4:
G1 is
chordal
;
G2 is chordal now for P being Walk of G2 st P .length() > 3 & P is Cycle-like holds
P is chordal let P be
Walk of
G2;
( P .length() > 3 & P is Cycle-like implies P is chordal )assume A5:
(
P .length() > 3 &
P is
Cycle-like )
;
P is chordal now ex m, n being odd Nat st
( m + 2 < n & n <= len P & P . m <> P . n & ex e being object st e Joins P . m,P . n,G2 & ( for f being object st f in P .edges() holds
not f Joins P . m,P . n,G2 ) )reconsider C =
P as
F -valued Walk of
G2 by A1, Th122;
A6:
(F " C) .length() > 3
by A5, Th125;
F " C is
Cycle-like
by A5, Th138;
then
F " C is
chordal
by A4, A6, CHORD:def 11;
then consider m,
n being
odd Nat such that A7:
(
m + 2
< n &
n <= len (F " C) &
(F " C) . m <> (F " C) . n )
and A8:
ex
e being
object st
e Joins (F " C) . m,
(F " C) . n,
G1
and A9:
for
f being
object st
f in (F " C) .edges() holds
not
f Joins (F " C) . m,
(F " C) . n,
G1
by CHORD:def 10;
take m =
m;
ex n being odd Nat st
( m + 2 < n & n <= len P & P . m <> P . n & ex e being object st e Joins P . m,P . n,G2 & ( for f being object st f in P .edges() holds
not f Joins P . m,P . n,G2 ) )take n =
n;
( m + 2 < n & n <= len P & P . m <> P . n & ex e being object st e Joins P . m,P . n,G2 & ( for f being object st f in P .edges() holds
not f Joins P . m,P . n,G2 ) )thus A10:
(
m + 2
< n &
n <= len P )
by A7, Th125;
( P . m <> P . n & ex e being object st e Joins P . m,P . n,G2 & ( for f being object st f in P .edges() holds
not f Joins P . m,P . n,G2 ) )A11:
n is
odd Element of
NAT
by ORDINAL1:def 12;
then A12:
(F " C) . n = ((F ") _V) . (C . n)
by A10, Th129;
(m + 2) - 2
<= n - 0
by A10, XREAL_1:13;
then A13:
m <= len P
by A10, XXREAL_0:2;
A14:
m is
odd Element of
NAT
by ORDINAL1:def 12;
then A15:
(F " C) . m = ((F ") _V) . (C . m)
by A13, Th129;
hence
P . m <> P . n
by A7, A12;
( ex e being object st e Joins P . m,P . n,G2 & ( for f being object st f in P .edges() holds
not f Joins P . m,P . n,G2 ) )
(
P . m in the_Vertices_of G2 &
P . n in the_Vertices_of G2 )
by A10, A11, A13, A14, GLIB_001:7;
then A16:
(
P . m in dom ((F ") _V) &
P . n in dom ((F ") _V) )
by A2, Def11;
thus
ex
e being
object st
e Joins P . m,
P . n,
G2
for f being object st f in P .edges() holds
not f Joins P . m,P . n,G2proof
consider e0 being
object such that A17:
e0 Joins (F " C) . m,
(F " C) . n,
G1
by A8;
e0 in the_Edges_of G1
by A17, GLIB_000:def 13;
then
e0 in rng ((F ") _E)
by A2, Def12;
then consider e being
object such that A18:
(
e in dom ((F ") _E) &
((F ") _E) . e = e0 )
by FUNCT_1:def 3;
take
e
;
e Joins P . m,P . n,G2
((F ") _E) . e Joins ((F ") _V) . (C . m),
((F ") _V) . (C . n),
G1
by A12, A15, A17, A18;
hence
e Joins P . m,
P . n,
G2
by A2, A16, A18;
verum
end; let f be
object ;
( f in P .edges() implies not f Joins P . m,P . n,G2 )assume A19:
f in P .edges()
;
not f Joins P . m,P . n,G2then
f in the_Edges_of G2
;
then A20:
f in dom ((F ") _E)
by A2, Def11;
then
((F ") _E) . f in ((F ") _E) .: (P .edges())
by A19, FUNCT_1:def 6;
then A21:
((F ") _E) . f in (F " C) .edges()
by Th136;
thus
not
f Joins P . m,
P . n,
G2
by A9, A12, A15, A16, A20, A21, Th4;
verum end; hence
P is
chordal
by CHORD:def 10;
verum end; hence
G2 is
chordal
by CHORD:def 11;
verum
end;
hereby ( G1 is connected iff G2 is connected )
assume A22:
G2 is
chordal
;
G1 is chordal now for P being Walk of G1 st P .length() > 3 & P is Cycle-like holds
P is chordal let P be
Walk of
G1;
( P .length() > 3 & P is Cycle-like implies P is chordal )assume A23:
(
P .length() > 3 &
P is
Cycle-like )
;
P is chordal now ex m, n being odd Nat st
( m + 2 < n & n <= len P & P . m <> P . n & ex e being object st e Joins P . m,P . n,G1 & ( for f being object st f in P .edges() holds
not f Joins P . m,P . n,G1 ) )reconsider C =
P as
F -defined Walk of
G1 by A1, Th121;
A24:
(F .: C) .length() > 3
by A23, Th125;
F .: C is
Cycle-like
by A23, Th138;
then
F .: C is
chordal
by A22, A24, CHORD:def 11;
then consider m,
n being
odd Nat such that A25:
(
m + 2
< n &
n <= len (F .: C) &
(F .: C) . m <> (F .: C) . n )
and A26:
ex
e being
object st
e Joins (F .: C) . m,
(F .: C) . n,
G2
and A27:
for
f being
object st
f in (F .: C) .edges() holds
not
f Joins (F .: C) . m,
(F .: C) . n,
G2
by CHORD:def 10;
take m =
m;
ex n being odd Nat st
( m + 2 < n & n <= len P & P . m <> P . n & ex e being object st e Joins P . m,P . n,G1 & ( for f being object st f in P .edges() holds
not f Joins P . m,P . n,G1 ) )take n =
n;
( m + 2 < n & n <= len P & P . m <> P . n & ex e being object st e Joins P . m,P . n,G1 & ( for f being object st f in P .edges() holds
not f Joins P . m,P . n,G1 ) )thus A28:
(
m + 2
< n &
n <= len P )
by A25, Th125;
( P . m <> P . n & ex e being object st e Joins P . m,P . n,G1 & ( for f being object st f in P .edges() holds
not f Joins P . m,P . n,G1 ) )A29:
n is
odd Element of
NAT
by ORDINAL1:def 12;
then A30:
(F .: C) . n = (F _V) . (C . n)
by A28, Th129;
(m + 2) - 2
<= n - 0
by A28, XREAL_1:13;
then A31:
m <= len P
by A28, XXREAL_0:2;
A32:
m is
odd Element of
NAT
by ORDINAL1:def 12;
then A33:
(F .: C) . m = (F _V) . (C . m)
by A31, Th129;
hence
P . m <> P . n
by A25, A30;
( ex e being object st e Joins P . m,P . n,G1 & ( for f being object st f in P .edges() holds
not f Joins P . m,P . n,G1 ) )
(
P . m in the_Vertices_of G1 &
P . n in the_Vertices_of G1 )
by A28, A29, A31, A32, GLIB_001:7;
then A34:
(
P . m in dom (F _V) &
P . n in dom (F _V) )
by A1, Def11;
thus
ex
e being
object st
e Joins P . m,
P . n,
G1
for f being object st f in P .edges() holds
not f Joins P . m,P . n,G1proof
consider e0 being
object such that A35:
e0 Joins (F .: C) . m,
(F .: C) . n,
G2
by A26;
e0 in the_Edges_of G2
by A35, GLIB_000:def 13;
then
e0 in rng (F _E)
by A1, Def12;
then consider e being
object such that A36:
(
e in dom (F _E) &
(F _E) . e = e0 )
by FUNCT_1:def 3;
take
e
;
e Joins P . m,P . n,G1
(F _E) . e Joins (F _V) . (C . m),
(F _V) . (C . n),
G2
by A30, A33, A35, A36;
hence
e Joins P . m,
P . n,
G1
by A3, A34, A36;
verum
end; let f be
object ;
( f in P .edges() implies not f Joins P . m,P . n,G1 )assume A37:
f in P .edges()
;
not f Joins P . m,P . n,G1then
f in the_Edges_of G1
;
then A38:
f in dom (F _E)
by A1, Def11;
then
(F _E) . f in (F _E) .: (P .edges())
by A37, FUNCT_1:def 6;
then A39:
(F _E) . f in (F .: C) .edges()
by Th136;
thus
not
f Joins P . m,
P . n,
G1
by A27, A30, A33, A34, A38, A39, Th4;
verum end; hence
P is
chordal
by CHORD:def 10;
verum end; hence
G1 is
chordal
by CHORD:def 11;
verum
end;
hereby ( G2 is connected implies G1 is connected )
assume A40:
G1 is
connected
;
G2 is connected
for
u,
v being
Vertex of
G2 ex
W2 being
Walk of
G2 st
W2 is_Walk_from u,
v
proof
let u2,
v2 be
Vertex of
G2;
ex W2 being Walk of G2 st W2 is_Walk_from u2,v2
reconsider u1 =
((F ") _V) . u2,
v1 =
((F ") _V) . v2 as
Vertex of
G1 by A1, Th79;
consider W1 being
Walk of
G1 such that A41:
W1 is_Walk_from u1,
v1
by A40, GLIB_002:def 1;
reconsider W1 =
W1 as
F -defined Walk of
G1 by A1, Th121;
take
F .: W1
;
F .: W1 is_Walk_from u2,v2
F " is
total
by A2;
then
(
u2 in dom ((F _V) ") &
v2 in dom ((F _V) ") )
;
then A42:
(
u2 in rng (F _V) &
v2 in rng (F _V) )
by FUNCT_1:33;
F .: W1 is_Walk_from (F _V) . (((F _V) ") . u2),
(F _V) . v1
by A41, Th132;
then
F .: W1 is_Walk_from u2,
(F _V) . (((F _V) ") . v2)
by A42, FUNCT_1:35;
hence
F .: W1 is_Walk_from u2,
v2
by A42, FUNCT_1:35;
verum
end; hence
G2 is
connected
by GLIB_002:def 1;
verum
end;
assume A43:
G2 is connected
; G1 is connected
for u, v being Vertex of G1 ex W1 being Walk of G1 st W1 is_Walk_from u,v
proof
let u1,
v1 be
Vertex of
G1;
ex W1 being Walk of G1 st W1 is_Walk_from u1,v1
reconsider u2 =
(F _V) . u1,
v2 =
(F _V) . v1 as
Vertex of
G2 by A1, Th34;
consider W2 being
Walk of
G2 such that A44:
W2 is_Walk_from u2,
v2
by A43, GLIB_002:def 1;
reconsider W2 =
W2 as
F -valued Walk of
G2 by A1, Th122;
take
F " W2
;
F " W2 is_Walk_from u1,v1
A45:
F is
total
by A1;
F " W2 is_Walk_from ((F _V) ") . ((F _V) . u1),
((F ") _V) . v2
by A44, Th132;
then
F " W2 is_Walk_from u1,
((F _V) ") . ((F _V) . v1)
by A45, FUNCT_1:34;
hence
F " W2 is_Walk_from u1,
v1
by A45, FUNCT_1:34;
verum
end;
hence
G1 is connected
by GLIB_002:def 1; verum