let G1 be _Graph; :: thesis: for v being Vertex of G1
for G2 being removeVertex of G1,v st v is endvertex holds
G1 .numComponents() = G2 .numComponents()
let v be Vertex of G1; :: thesis: for G2 being removeVertex of G1,v st v is endvertex holds
G1 .numComponents() = G2 .numComponents()
let G2 be removeVertex of G1,v; :: thesis: ( v is endvertex implies G1 .numComponents() = G2 .numComponents() )
assume A1: v is endvertex ; :: thesis: G1 .numComponents() = G2 .numComponents()
then A2: not G1 is _trivial by Th16;
ex f being Function st
( f is one-to-one & dom f = G1 .componentSet() & rng f = G2 .componentSet() )
proof
reconsider C = G1 .componentSet() as a_partition of the_Vertices_of G1 by Th23;
set V = EqClass (v,C);
set f = (id C) +* ((EqClass (v,C)),((EqClass (v,C)) \ {v}));
take (id C) +* ((EqClass (v,C)),((EqClass (v,C)) \ {v})) ; :: thesis: ( (id C) +* ((EqClass (v,C)),((EqClass (v,C)) \ {v})) is one-to-one & dom ((id C) +* ((EqClass (v,C)),((EqClass (v,C)) \ {v}))) = G1 .componentSet() & rng ((id C) +* ((EqClass (v,C)),((EqClass (v,C)) \ {v}))) = G2 .componentSet() )
for x1, x2 being object st x1 in dom ((id C) +* ((EqClass (v,C)),((EqClass (v,C)) \ {v}))) & x2 in dom ((id C) +* ((EqClass (v,C)),((EqClass (v,C)) \ {v}))) & ((id C) +* ((EqClass (v,C)),((EqClass (v,C)) \ {v}))) . x1 = ((id C) +* ((EqClass (v,C)),((EqClass (v,C)) \ {v}))) . x2 holds
x1 = x2
proof
let x1, x2 be object ; :: thesis: ( x1 in dom ((id C) +* ((EqClass (v,C)),((EqClass (v,C)) \ {v}))) & x2 in dom ((id C) +* ((EqClass (v,C)),((EqClass (v,C)) \ {v}))) & ((id C) +* ((EqClass (v,C)),((EqClass (v,C)) \ {v}))) . x1 = ((id C) +* ((EqClass (v,C)),((EqClass (v,C)) \ {v}))) . x2 implies x1 = x2 )
assume A3: ( x1 in dom ((id C) +* ((EqClass (v,C)),((EqClass (v,C)) \ {v}))) & x2 in dom ((id C) +* ((EqClass (v,C)),((EqClass (v,C)) \ {v}))) & ((id C) +* ((EqClass (v,C)),((EqClass (v,C)) \ {v}))) . x1 = ((id C) +* ((EqClass (v,C)),((EqClass (v,C)) \ {v}))) . x2 ) ; :: thesis: x1 = x2
then A4: ( x1 in dom (id C) & x2 in dom (id C) ) by FUNCT_7:30;
A5: not (EqClass (v,C)) \ {v} in C
per cases ( ( x1 <> EqClass (v,C) & x2 <> EqClass (v,C) ) or ( x1 = EqClass (v,C) & x2 <> EqClass (v,C) ) or ( x1 <> EqClass (v,C) & x2 = EqClass (v,C) ) or ( x1 = EqClass (v,C) & x2 = EqClass (v,C) ) ) ;
suppose ( x1 <> EqClass (v,C) & x2 <> EqClass (v,C) ) ; :: thesis: x1 = x2
then ( ((id C) +* ((EqClass (v,C)),((EqClass (v,C)) \ {v}))) . x1 = (id C) . x1 & ((id C) +* ((EqClass (v,C)),((EqClass (v,C)) \ {v}))) . x2 = (id C) . x2 ) by FUNCT_7:32;
then ( ((id C) +* ((EqClass (v,C)),((EqClass (v,C)) \ {v}))) . x1 = x1 & ((id C) +* ((EqClass (v,C)),((EqClass (v,C)) \ {v}))) . x2 = x2 ) by A4, FUNCT_1:18;
hence x1 = x2 by A3; :: thesis: verum
end;
suppose ( x1 = EqClass (v,C) & x2 <> EqClass (v,C) ) ; :: thesis: x1 = x2
then ( ((id C) +* ((EqClass (v,C)),((EqClass (v,C)) \ {v}))) . x1 = (EqClass (v,C)) \ {v} & ((id C) +* ((EqClass (v,C)),((EqClass (v,C)) \ {v}))) . x2 = (id C) . x2 ) by A4, FUNCT_7:31, FUNCT_7:32;
hence x1 = x2 by A5, A3, A4, FUNCT_1:18; :: thesis: verum
end;
suppose ( x1 <> EqClass (v,C) & x2 = EqClass (v,C) ) ; :: thesis: x1 = x2
then ( ((id C) +* ((EqClass (v,C)),((EqClass (v,C)) \ {v}))) . x2 = (EqClass (v,C)) \ {v} & ((id C) +* ((EqClass (v,C)),((EqClass (v,C)) \ {v}))) . x1 = (id C) . x1 ) by A4, FUNCT_7:31, FUNCT_7:32;
hence x1 = x2 by A5, A3, A4, FUNCT_1:18; :: thesis: verum
end;
suppose ( x1 = EqClass (v,C) & x2 = EqClass (v,C) ) ; :: thesis: x1 = x2
hence x1 = x2 ; :: thesis: verum
end;
end;
end;
hence (id C) +* ((EqClass (v,C)),((EqClass (v,C)) \ {v})) is one-to-one by FUNCT_1:def 4; :: thesis: ( dom ((id C) +* ((EqClass (v,C)),((EqClass (v,C)) \ {v}))) = G1 .componentSet() & rng ((id C) +* ((EqClass (v,C)),((EqClass (v,C)) \ {v}))) = G2 .componentSet() )
thus A10: dom ((id C) +* ((EqClass (v,C)),((EqClass (v,C)) \ {v}))) = dom (id C) by FUNCT_7:30
.= G1 .componentSet() ; :: thesis: rng ((id C) +* ((EqClass (v,C)),((EqClass (v,C)) \ {v}))) = G2 .componentSet()
for y being object holds
( y in rng ((id C) +* ((EqClass (v,C)),((EqClass (v,C)) \ {v}))) iff y in G2 .componentSet() )
proof
let y be object ; :: thesis: ( y in rng ((id C) +* ((EqClass (v,C)),((EqClass (v,C)) \ {v}))) iff y in G2 .componentSet() )
hereby :: thesis: ( y in G2 .componentSet() implies y in rng ((id C) +* ((EqClass (v,C)),((EqClass (v,C)) \ {v}))) )
assume y in rng ((id C) +* ((EqClass (v,C)),((EqClass (v,C)) \ {v}))) ; :: thesis: y in G2 .componentSet()
then consider x being object such that
A11: ( x in dom ((id C) +* ((EqClass (v,C)),((EqClass (v,C)) \ {v}))) & y = ((id C) +* ((EqClass (v,C)),((EqClass (v,C)) \ {v}))) . x ) by FUNCT_1:def 3;
reconsider x = x as set by TARSKI:1;
per cases ( x = EqClass (v,C) or x <> EqClass (v,C) ) ;
suppose A12: x = EqClass (v,C) ; :: thesis: y in G2 .componentSet()
EqClass (v,C) in dom (id C) by EQREL_1:def 6;
then A13: y = (EqClass (v,C)) \ {v} by A11, A12, FUNCT_7:31;
ex w being Vertex of G2 st (EqClass (v,C)) \ {v} = G2 .reachableFrom w
proof
consider e being object such that
A14: ( v .edgesInOut() = {e} & not e Joins v,v,G1 ) by A1, GLIB_000:def 51;
set w = v .adj e;
A15: e in v .edgesInOut() by A14, TARSKI:def 1;
then A16: v <> v .adj e by A14, GLIB_000:67;
A17: the_Vertices_of G2 = (the_Vertices_of G1) \ {v} by A2, GLIB_000:47;
( v in G1 .reachableFrom v & e Joins v,v .adj e,G1 ) by A15, GLIB_000:67, GLIB_002:9;
then A18: v .adj e in G1 .reachableFrom v by GLIB_002:10;
not v .adj e in {v} by A16, TARSKI:def 1;
then reconsider w0 = v .adj e as Vertex of G2 by A17, XBOOLE_0:def 5;
take w0 ; :: thesis: (EqClass (v,C)) \ {v} = G2 .reachableFrom w0
thus (EqClass (v,C)) \ {v} = (G1 .reachableFrom v) \ {v} by Th24
.= (G1 .reachableFrom (v .adj e)) \ {v} by A18, GLIB_002:12
.= G2 .reachableFrom w0 by A1, A18, Th25 ; :: thesis: verum
end;
hence y in G2 .componentSet() by A13, GLIB_002:def 8; :: thesis: verum
end;
suppose A19: x <> EqClass (v,C) ; :: thesis: y in G2 .componentSet()
consider w being Vertex of G1 such that
A20: x = G1 .reachableFrom w by A10, A11, GLIB_002:def 8;
A21: ( x in C & EqClass (v,C) in C ) by A10, A11, EQREL_1:def 6;
x misses EqClass (v,C) by A19, A21, EQREL_1:def 4;
then A22: x misses G1 .reachableFrom v by Th24;
G1 .reachableFrom w <> G1 .reachableFrom v by A20, A22, XBOOLE_1:66;
then A23: not w in G1 .reachableFrom v by GLIB_002:12;
then A24: v <> w by GLIB_002:9;
A25: the_Vertices_of G2 = (the_Vertices_of G1) \ {v} by A2, GLIB_000:47;
not w in {v} by A24, TARSKI:def 1;
then reconsider w0 = w as Vertex of G2 by A25, XBOOLE_0:def 5;
G1 .reachableFrom w = G2 .reachableFrom w0 by A2, A23, Th26;
then A26: x in G2 .componentSet() by A20, GLIB_002:def 8;
x = (id C) . x by A10, A11, FUNCT_1:18
.= y by A11, A19, FUNCT_7:32 ;
hence y in G2 .componentSet() by A26; :: thesis: verum
end;
end;
end;
assume y in G2 .componentSet() ; :: thesis: y in rng ((id C) +* ((EqClass (v,C)),((EqClass (v,C)) \ {v})))
then consider w0 being Vertex of G2 such that
A27: y = G2 .reachableFrom w0 by GLIB_002:def 8;
the_Vertices_of G2 c= the_Vertices_of G1 ;
then reconsider w = w0 as Vertex of G1 by TARSKI:def 3;
ex x being object st
( x in dom ((id C) +* ((EqClass (v,C)),((EqClass (v,C)) \ {v}))) & y = ((id C) +* ((EqClass (v,C)),((EqClass (v,C)) \ {v}))) . x )
proof
per cases ( w in G1 .reachableFrom v or not w in G1 .reachableFrom v ) ;
suppose A28: w in G1 .reachableFrom v ; :: thesis: ex x being object st
( x in dom ((id C) +* ((EqClass (v,C)),((EqClass (v,C)) \ {v}))) & y = ((id C) +* ((EqClass (v,C)),((EqClass (v,C)) \ {v}))) . x )
then G2 .reachableFrom w0 = (G1 .reachableFrom w) \ {v} by A1, Th25;
then y = (G1 .reachableFrom v) \ {v} by A27, A28, GLIB_002:12;
then A29: y = (EqClass (v,C)) \ {v} by Th24;
take EqClass (v,C) ; :: thesis: ( EqClass (v,C) in dom ((id C) +* ((EqClass (v,C)),((EqClass (v,C)) \ {v}))) & y = ((id C) +* ((EqClass (v,C)),((EqClass (v,C)) \ {v}))) . (EqClass (v,C)) )
EqClass (v,C) = G1 .reachableFrom v by Th24;
then A30: EqClass (v,C) in C by GLIB_002:def 8;
hence EqClass (v,C) in dom ((id C) +* ((EqClass (v,C)),((EqClass (v,C)) \ {v}))) by A10; :: thesis: y = ((id C) +* ((EqClass (v,C)),((EqClass (v,C)) \ {v}))) . (EqClass (v,C))
EqClass (v,C) in dom (id C) by A30;
hence y = ((id C) +* ((EqClass (v,C)),((EqClass (v,C)) \ {v}))) . (EqClass (v,C)) by A29, FUNCT_7:31; :: thesis: verum
end;
suppose A31: not w in G1 .reachableFrom v ; :: thesis: ex x being object st
( x in dom ((id C) +* ((EqClass (v,C)),((EqClass (v,C)) \ {v}))) & y = ((id C) +* ((EqClass (v,C)),((EqClass (v,C)) \ {v}))) . x )
then A32: G2 .reachableFrom w0 = G1 .reachableFrom w by A2, Th26;
set x = G1 .reachableFrom w;
take G1 .reachableFrom w ; :: thesis: ( G1 .reachableFrom w in dom ((id C) +* ((EqClass (v,C)),((EqClass (v,C)) \ {v}))) & y = ((id C) +* ((EqClass (v,C)),((EqClass (v,C)) \ {v}))) . (G1 .reachableFrom w) )
A33: G1 .reachableFrom w in G1 .componentSet() by GLIB_002:def 8;
hence G1 .reachableFrom w in dom ((id C) +* ((EqClass (v,C)),((EqClass (v,C)) \ {v}))) by A10; :: thesis: y = ((id C) +* ((EqClass (v,C)),((EqClass (v,C)) \ {v}))) . (G1 .reachableFrom w)
G1 .reachableFrom w <> EqClass (v,C) then ((id C) +* ((EqClass (v,C)),((EqClass (v,C)) \ {v}))) . (G1 .reachableFrom w) = (id C) . (G1 .reachableFrom w) by FUNCT_7:32
.= G1 .reachableFrom w by A33, FUNCT_1:18 ;
hence y = ((id C) +* ((EqClass (v,C)),((EqClass (v,C)) \ {v}))) . (G1 .reachableFrom w) by A27, A32; :: thesis: verum
end;
end;
end;
hence y in rng ((id C) +* ((EqClass (v,C)),((EqClass (v,C)) \ {v}))) by FUNCT_1:def 3; :: thesis: verum
end;
hence rng ((id C) +* ((EqClass (v,C)),((EqClass (v,C)) \ {v}))) = G2 .componentSet() by TARSKI:2; :: thesis: verum
end;
then card (G1 .componentSet()) = card (G2 .componentSet()) by WELLORD2:def 4, CARD_1:5;
then G1 .numComponents() = card (G2 .componentSet()) by GLIB_002:def 9;
hence G1 .numComponents() = G2 .numComponents() by GLIB_002:def 9; :: thesis: verum