let G2, G3 be _Graph; for v, e, w being object
for G1 being addEdge of G3,v,e,w st not e in the_Edges_of G3 holds
( G2 is reverseEdgeDirections of G1,{e} iff G2 is addEdge of G3,w,e,v )
let v, e, w be object ; for G1 being addEdge of G3,v,e,w st not e in the_Edges_of G3 holds
( G2 is reverseEdgeDirections of G1,{e} iff G2 is addEdge of G3,w,e,v )
let G1 be addEdge of G3,v,e,w; ( not e in the_Edges_of G3 implies ( G2 is reverseEdgeDirections of G1,{e} iff G2 is addEdge of G3,w,e,v ) )
assume A1:
not e in the_Edges_of G3
; ( G2 is reverseEdgeDirections of G1,{e} iff G2 is addEdge of G3,w,e,v )
per cases
( ( v in the_Vertices_of G3 & w in the_Vertices_of G3 ) or not v in the_Vertices_of G3 or not w in the_Vertices_of G3 )
;
suppose A2:
(
v in the_Vertices_of G3 &
w in the_Vertices_of G3 )
;
( G2 is reverseEdgeDirections of G1,{e} iff G2 is addEdge of G3,w,e,v )then
the_Edges_of G1 = (the_Edges_of G3) \/ {e}
by A1, GLIB_006:def 11;
then A3:
{e} c= the_Edges_of G1
by XBOOLE_1:7;
(
dom (the_Source_of G1) = the_Edges_of G1 &
dom (the_Target_of G1) = the_Edges_of G1 )
by FUNCT_2:def 1;
then A4:
(
e in dom (the_Source_of G1) &
e in dom (the_Target_of G1) &
e is
set )
by A3, ZFMISC_1:31, TARSKI:1;
set S =
the_Source_of G3;
set T =
the_Target_of G3;
hereby ( G2 is addEdge of G3,w,e,v implies G2 is reverseEdgeDirections of G1,{e} )
assume A5:
G2 is
reverseEdgeDirections of
G1,
{e}
;
G2 is addEdge of G3,w,e,vthen A6:
the_Vertices_of G2 =
the_Vertices_of G1
by A3, GLIB_007:def 1
.=
the_Vertices_of G3
by A2, GLIB_006:102
;
now for e0, v0, w0 being object st e0 DJoins v0,w0,G3 holds
e0 DJoins v0,w0,G2let e0,
v0,
w0 be
object ;
( e0 DJoins v0,w0,G3 implies e0 DJoins v0,w0,G2 )assume A7:
e0 DJoins v0,
w0,
G3
;
e0 DJoins v0,w0,G2then
e0 in the_Edges_of G3
by GLIB_000:def 14;
then A8:
not
e0 in {e}
by A1, TARSKI:def 1;
(
v0 is
set &
w0 is
set )
by TARSKI:1;
then
e0 DJoins v0,
w0,
G1
by A7, GLIB_006:70;
hence
e0 DJoins v0,
w0,
G2
by A3, A5, A8, GLIB_007:8;
verum end; then A9:
G2 is
Supergraph of
G3
by A6, Th50;
A10:
the_Edges_of G2 =
the_Edges_of G1
by A3, A5, GLIB_007:def 1
.=
(the_Edges_of G3) \/ {e}
by A1, A2, GLIB_006:def 11
;
A11:
the_Source_of G2 =
(the_Source_of G1) +* ((the_Target_of G1) | {e})
by A5, A3, GLIB_007:def 1
.=
(the_Source_of G1) +* (e .--> ((the_Target_of G1) . e))
by A4, FUNCT_7:6
.=
((the_Source_of G3) +* (e .--> v)) +* (e .--> ((the_Target_of G1) . e))
by A1, A2, GLIB_006:def 11
.=
((the_Source_of G3) +* (e .--> v)) +* (e .--> (((the_Target_of G3) +* (e .--> w)) . e))
by A1, A2, GLIB_006:def 11
.=
((the_Source_of G3) +* (e .--> v)) +* (e .--> w)
by FUNCT_4:113
.=
(the_Source_of G3) +* (e .--> w)
by FUNCT_4:114
;
the_Target_of G2 =
(the_Target_of G1) +* ((the_Source_of G1) | {e})
by A5, A3, GLIB_007:def 1
.=
(the_Target_of G1) +* (e .--> ((the_Source_of G1) . e))
by A4, FUNCT_7:6
.=
((the_Target_of G3) +* (e .--> w)) +* (e .--> ((the_Source_of G1) . e))
by A1, A2, GLIB_006:def 11
.=
((the_Target_of G3) +* (e .--> w)) +* (e .--> (((the_Source_of G3) +* (e .--> v)) . e))
by A1, A2, GLIB_006:def 11
.=
((the_Target_of G3) +* (e .--> w)) +* (e .--> v)
by FUNCT_4:113
.=
(the_Target_of G3) +* (e .--> v)
by FUNCT_4:114
;
hence
G2 is
addEdge of
G3,
w,
e,
v
by A1, A2, A6, A9, A10, A11, GLIB_006:def 11;
verum
end; assume A12:
G2 is
addEdge of
G3,
w,
e,
v
;
G2 is reverseEdgeDirections of G1,{e}then A13:
the_Vertices_of G2 =
the_Vertices_of G3
by A2, GLIB_006:102
.=
the_Vertices_of G1
by A2, GLIB_006:102
;
A14:
the_Edges_of G2 =
(the_Edges_of G3) \/ {e}
by A1, A2, A12, GLIB_006:def 11
.=
the_Edges_of G1
by A1, A2, GLIB_006:def 11
;
A15:
the_Source_of G2 =
(the_Source_of G3) +* (e .--> w)
by A1, A2, A12, GLIB_006:def 11
.=
((the_Source_of G3) +* (e .--> v)) +* (e .--> w)
by FUNCT_4:114
.=
((the_Source_of G3) +* (e .--> v)) +* (e .--> (((the_Target_of G3) +* (e .--> w)) . e))
by FUNCT_4:113
.=
((the_Source_of G3) +* (e .--> v)) +* (e .--> ((the_Target_of G1) . e))
by A1, A2, GLIB_006:def 11
.=
(the_Source_of G1) +* (e .--> ((the_Target_of G1) . e))
by A1, A2, GLIB_006:def 11
.=
(the_Source_of G1) +* ((the_Target_of G1) | {e})
by A4, FUNCT_7:6
;
the_Target_of G2 =
(the_Target_of G3) +* (e .--> v)
by A1, A2, A12, GLIB_006:def 11
.=
((the_Target_of G3) +* (e .--> w)) +* (e .--> v)
by FUNCT_4:114
.=
((the_Target_of G3) +* (e .--> w)) +* (e .--> (((the_Source_of G3) +* (e .--> v)) . e))
by FUNCT_4:113
.=
((the_Target_of G3) +* (e .--> w)) +* (e .--> ((the_Source_of G1) . e))
by A1, A2, GLIB_006:def 11
.=
(the_Target_of G1) +* (e .--> ((the_Source_of G1) . e))
by A1, A2, GLIB_006:def 11
.=
(the_Target_of G1) +* ((the_Source_of G1) | {e})
by A4, FUNCT_7:6
;
hence
G2 is
reverseEdgeDirections of
G1,
{e}
by A3, A13, A14, A15, GLIB_007:def 1;
verum end; suppose A16:
( not
v in the_Vertices_of G3 or not
w in the_Vertices_of G3 )
;
( G2 is reverseEdgeDirections of G1,{e} iff G2 is addEdge of G3,w,e,v )then A17:
G1 == G3
by GLIB_006:def 11;
then
the_Edges_of G1 = the_Edges_of G3
by GLIB_000:def 34;
then A18:
not
{e} c= the_Edges_of G1
by A1, ZFMISC_1:31;
hereby ( G2 is addEdge of G3,w,e,v implies G2 is reverseEdgeDirections of G1,{e} )
assume
G2 is
reverseEdgeDirections of
G1,
{e}
;
G2 is addEdge of G3,w,e,vthen
G2 == G1
by A18, GLIB_007:def 1;
then A19:
G2 == G3
by A17, GLIB_000:85;
then
G2 is
Supergraph of
G3
by GLIB_006:59;
hence
G2 is
addEdge of
G3,
w,
e,
v
by A16, A19, GLIB_006:def 11;
verum
end; assume
G2 is
addEdge of
G3,
w,
e,
v
;
G2 is reverseEdgeDirections of G1,{e}then
G2 == G3
by A16, GLIB_006:def 11;
then
G2 == G1
by A17, GLIB_000:85;
hence
G2 is
reverseEdgeDirections of
G1,
{e}
by A18, GLIB_007:def 1;
verum end;