P. 255 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 25401-25500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	clwwlkndivn 25401	The size of the set of closed walks (defined as words) of length n is divisible by n. (Contributed by Alexander van der Vekens, 17-Jun-2018.)
|- ( ( V USGrph E /\ V e. Fin /\ N e. Prime ) -> N || ( # ` ( ( V ClWWalksN E ) ` N ) ) )
Theorem	wlklenvp1 25402	The number of vertices of a walk (in an undirected graph) is the number of its edges plus 1. (Contributed by Alexander van der Vekens, 29-Jun-2018.)
|- ( F ( V Walks E ) P -> ( # ` P ) = ( ( # ` F ) + 1 ) )
Theorem	wlklenvclwlk 25403	The number of vertices in a walk equals the length of the walk after it is "closed" (i.e. enhanced by an edge from its last vertex to its first vertex). (Contributed by Alexander van der Vekens, 29-Jun-2018.)
|- ( ( W e. Word V /\ 1 <_ ( # ` W ) ) -> ( <. F , ( W ++ <" ( W ` 0 ) "> ) >. e. ( V Walks E ) -> ( # ` F ) = ( # ` W ) ) )
Theorem	clwlkfclwwlk2wrd 25404	The second component of a closed walk is a word over the "vertices". (Contributed by Alexander van der Vekens, 25-Jun-2018.)
|- A = ( 1st ` c )   &    |- B = ( 2nd ` c )   &    |- C = { c e. ( V ClWalks E ) | ( # ` A ) = N }   &    |- F = ( c e. C |-> ( B substr <. 0 , ( # ` A ) >. ) )   =>    |- ( c e. C -> B e. Word V )
Theorem	clwlkfclwwlk1hashn 25405*	The size of the first component of a closed walk. (Contributed by Alexander van der Vekens, 5-Jul-2018.)
|- A = ( 1st ` c )   &    |- B = ( 2nd ` c )   &    |- C = { c e. ( V ClWalks E ) | ( # ` A ) = N }   &    |- F = ( c e. C |-> ( B substr <. 0 , ( # ` A ) >. ) )   =>    |- ( W e. C -> ( # ` ( 1st ` W ) ) = N )
Theorem	clwlkfclwwlk1hash 25406*	The size of the first component of a closed walk is an integer in the range between 0 and the size of the second component. (Contributed by Alexander van der Vekens, 25-Jun-2018.)
|- A = ( 1st ` c )   &    |- B = ( 2nd ` c )   &    |- C = { c e. ( V ClWalks E ) | ( # ` A ) = N }   &    |- F = ( c e. C |-> ( B substr <. 0 , ( # ` A ) >. ) )   =>    |- ( c e. C -> ( # ` A ) e. ( 0 ... ( # ` B ) ) )
Theorem	clwlkfclwwlk2sswd 25407*	The size of a subword of the second component of a closed walk with length of the size of the second component. (Contributed by Alexander van der Vekens, 25-Jun-2018.)
|- A = ( 1st ` c )   &    |- B = ( 2nd ` c )   &    |- C = { c e. ( V ClWalks E ) | ( # ` A ) = N }   &    |- F = ( c e. C |-> ( B substr <. 0 , ( # ` A ) >. ) )   =>    |- ( c e. C -> ( # ` A ) = ( # ` ( B substr <. 0 , ( # ` A ) >. ) ) )
Theorem	clwlkfclwwlk 25408*	There is a function between the set of closed walks (defined as words) of length n and the set of closed walks of length n (in an undirected simple graph). (Contributed by Alexander van der Vekens, 25-Jun-2018.)
|- A = ( 1st ` c )   &    |- B = ( 2nd ` c )   &    |- C = { c e. ( V ClWalks E ) | ( # ` A ) = N }   &    |- F = ( c e. C |-> ( B substr <. 0 , ( # ` A ) >. ) )   =>    |- ( ( V USGrph E /\ V e. Fin /\ N e. Prime ) -> F : C --> ( ( V ClWWalksN E ) ` N ) )
Theorem	clwlkfoclwwlk 25409*	There is an onto function between the set of closed walks (defined as words) of length n and the set of closed walks of length n (in an undirected simple graph). (Contributed by Alexander van der Vekens, 30-Jun-2018.)
|- A = ( 1st ` c )   &    |- B = ( 2nd ` c )   &    |- C = { c e. ( V ClWalks E ) | ( # ` A ) = N }   &    |- F = ( c e. C |-> ( B substr <. 0 , ( # ` A ) >. ) )   =>    |- ( ( V USGrph E /\ V e. Fin /\ N e. Prime ) -> F : C -onto-> ( ( V ClWWalksN E ) ` N ) )
Theorem	clwlkf1clwwlklem1 25410*	Lemma 1 for clwlkf1clwwlklem 25413. (Contributed by Alexander van der Vekens, 5-Jul-2018.)
|- A = ( 1st ` c )   &    |- B = ( 2nd ` c )   &    |- C = { c e. ( V ClWalks E ) | ( # ` A ) = N }   &    |- F = ( c e. C |-> ( B substr <. 0 , ( # ` A ) >. ) )   =>    |- ( W e. C -> N <_ ( # ` ( 2nd ` W ) ) )
Theorem	clwlkf1clwwlklem2 25411*	Lemma 2 for clwlkf1clwwlklem 25413. (Contributed by Alexander van der Vekens, 5-Jul-2018.)
|- A = ( 1st ` c )   &    |- B = ( 2nd ` c )   &    |- C = { c e. ( V ClWalks E ) | ( # ` A ) = N }   &    |- F = ( c e. C |-> ( B substr <. 0 , ( # ` A ) >. ) )   =>    |- ( W e. C -> ( ( 2nd ` W ) ` 0 ) = ( ( 2nd ` W ) ` N ) )
Theorem	clwlkf1clwwlklem3 25412*	Lemma 3 for clwlkf1clwwlklem 25413. (Contributed by Alexander van der Vekens, 5-Jul-2018.)
|- A = ( 1st ` c )   &    |- B = ( 2nd ` c )   &    |- C = { c e. ( V ClWalks E ) | ( # ` A ) = N }   &    |- F = ( c e. C |-> ( B substr <. 0 , ( # ` A ) >. ) )   =>    |- ( W e. C -> ( 2nd ` W ) e. Word V )
Theorem	clwlkf1clwwlklem 25413*	Lemma for clwlkf1clwwlk 25414. (Contributed by Alexander van der Vekens, 5-Jul-2018.)
|- A = ( 1st ` c )   &    |- B = ( 2nd ` c )   &    |- C = { c e. ( V ClWalks E ) | ( # ` A ) = N }   &    |- F = ( c e. C |-> ( B substr <. 0 , ( # ` A ) >. ) )   =>    |- ( ( N e. NN /\ U e. C /\ W e. C ) -> ( ( ( 2nd ` U ) substr <. 0 , ( # ` ( 1st ` U ) ) >. ) = ( ( 2nd ` W ) substr <. 0 , ( # ` ( 1st ` W ) ) >. ) -> A. y e. ( 0 ... N ) ( ( 2nd ` U ) ` y ) = ( ( 2nd ` W ) ` y ) ) )
Theorem	clwlkf1clwwlk 25414*	There is a one-to-one function between the set of closed walks (defined as words) of length n and the set of closed walks of length n (in an undirected simple graph). (Contributed by Alexander van der Vekens, 5-Jul-2018.)
|- A = ( 1st ` c )   &    |- B = ( 2nd ` c )   &    |- C = { c e. ( V ClWalks E ) | ( # ` A ) = N }   &    |- F = ( c e. C |-> ( B substr <. 0 , ( # ` A ) >. ) )   =>    |- ( ( V USGrph E /\ V e. Fin /\ N e. Prime ) -> F : C -1-1-> ( ( V ClWWalksN E ) ` N ) )
Theorem	clwlkf1oclwwlk 25415*	There is a one-to-one onto function between the set of closed walks (defined as words) of length n and the set of closed walks of length n (in an undirected simple graph). (Contributed by Alexander van der Vekens, 5-Jul-2018.)
|- A = ( 1st ` c )   &    |- B = ( 2nd ` c )   &    |- C = { c e. ( V ClWalks E ) | ( # ` A ) = N }   &    |- F = ( c e. C |-> ( B substr <. 0 , ( # ` A ) >. ) )   =>    |- ( ( V USGrph E /\ V e. Fin /\ N e. Prime ) -> F : C -1-1-onto-> ( ( V ClWWalksN E ) ` N ) )
Theorem	clwlksizeeq 25416*	The size of the set of closed walks (defined as words) of length n corresponds to the size of the set of closed walks of length n (in an undirected simple graph). (Contributed by Alexander van der Vekens, 6-Jul-2018.)
|- ( ( V USGrph E /\ V e. Fin /\ N e. Prime ) -> ( # ` ( ( V ClWWalksN E ) ` N ) ) = ( # ` { c e. ( V ClWalks E ) | ( # ` ( 1st ` c ) ) = N } ) )
Theorem	clwlkndivn 25417*	The size of the set of closed walks of length n is divisible by n. This corresponds to statement 9 in [Huneke] p. 2: "It follows that, if p is a prime number, then the number of closed walks of length p is divisible by p". (Contributed by Alexander van der Vekens, 6-Jul-2018.)
|- ( ( V USGrph E /\ V e. Fin /\ N e. Prime ) -> N || ( # ` { c e. ( V ClWalks E ) | ( # ` ( 1st ` c ) ) = N } ) )
16.1.5.7  Walks/paths of length 2 as ordered triples
Syntax	c2wlkot 25418	Extend class notation with walks (of a graph) of length 2 as ordered triple.
class 2WalksOt
Syntax	c2wlkonot 25419	Extend class notation with walks between two vertices (within a graph) of length 2 as ordered triple.
class 2WalksOnOt
Syntax	c2spthot 25420	Extend class notation with paths (of a graph) of length 2 as ordered triple.
class 2SPathOnOt
Syntax	c2pthonot 25421	Extend class notation with simple paths between two vertices (within a graph) of length 2 as ordered triple.
class 2SPathOnOt
Definition	df-2wlkonot 25422*	Define the collection of walks of length 2 with particular endpoints as ordered triple (in a graph). (Contributed by Alexander van der Vekens, 15-Feb-2018.)
|- 2WalksOnOt = ( v e. _V , e e. _V |-> ( a e. v , b e. v |-> { t e. ( ( v X. v ) X. v ) | E. f E. p ( f ( a ( v WalkOn e ) b ) p /\ ( # ` f ) = 2 /\ ( ( 1st ` ( 1st ` t ) ) = a /\ ( 2nd ` ( 1st ` t ) ) = ( p ` 1 ) /\ ( 2nd ` t ) = b ) ) } ) )
Definition	df-2wlksot 25423*	Define the collection of all walks of length 2 as ordered triple (in a graph). (Contributed by Alexander van der Vekens, 15-Feb-2018.)
|- 2WalksOt = ( v e. _V , e e. _V |-> { t e. ( ( v X. v ) X. v ) | E. a e. v E. b e. v t e. ( a ( v 2WalksOnOt e ) b ) } )
Definition	df-2spthonot 25424*	Define the collection of simple paths of length 2 with particular endpoints as ordered triple (in a graph) . (Contributed by Alexander van der Vekens, 1-Mar-2018.)
|- 2SPathOnOt = ( v e. _V , e e. _V |-> ( a e. v , b e. v |-> { t e. ( ( v X. v ) X. v ) | E. f E. p ( f ( a ( v SPathOn e ) b ) p /\ ( # ` f ) = 2 /\ ( ( 1st ` ( 1st ` t ) ) = a /\ ( 2nd ` ( 1st ` t ) ) = ( p ` 1 ) /\ ( 2nd ` t ) = b ) ) } ) )
Definition	df-2spthsot 25425*	Define the collection of all simple paths of length 2 as ordered triple. (in a graph) (Contributed by Alexander van der Vekens, 1-Mar-2018.)
|- 2SPathOnOt = ( v e. _V , e e. _V |-> { t e. ( ( v X. v ) X. v ) | E. a e. v E. b e. v t e. ( a ( v 2SPathOnOt e ) b ) } )
Theorem	el2wlkonotlem 25426	Lemma for el2wlkonot 25433. (Contributed by Alexander van der Vekens, 15-Feb-2018.)
|- ( ( f ( V Walks E ) p /\ ( # ` f ) = 2 ) -> ( p ` 1 ) e. V )
Theorem	is2wlkonot 25427*	The set of walks of length 2 between two vertices (in a graph) as ordered triple. (Contributed by Alexander van der Vekens, 15-Feb-2018.)
|- ( ( V e. X /\ E e. Y ) -> ( V 2WalksOnOt E ) = ( a e. V , b e. V |-> { t e. ( ( V X. V ) X. V ) | E. f E. p ( f ( a ( V WalkOn E ) b ) p /\ ( # ` f ) = 2 /\ ( ( 1st ` ( 1st ` t ) ) = a /\ ( 2nd ` ( 1st ` t ) ) = ( p ` 1 ) /\ ( 2nd ` t ) = b ) ) } ) )
Theorem	is2spthonot 25428*	The set of simple paths of length 2 between two vertices (in a graph) as ordered triple. (Contributed by Alexander van der Vekens, 1-Mar-2018.)
|- ( ( V e. X /\ E e. Y ) -> ( V 2SPathOnOt E ) = ( a e. V , b e. V |-> { t e. ( ( V X. V ) X. V ) | E. f E. p ( f ( a ( V SPathOn E ) b ) p /\ ( # ` f ) = 2 /\ ( ( 1st ` ( 1st ` t ) ) = a /\ ( 2nd ` ( 1st ` t ) ) = ( p ` 1 ) /\ ( 2nd ` t ) = b ) ) } ) )
Theorem	2wlkonot 25429*	The set of walks of length 2 between two vertices (in a graph) as ordered triple. (Contributed by Alexander van der Vekens, 15-Feb-2018.)
|- ( ( ( V e. X /\ E e. Y ) /\ ( A e. V /\ B e. V ) ) -> ( A ( V 2WalksOnOt E ) B ) = { t e. ( ( V X. V ) X. V ) | E. f E. p ( f ( A ( V WalkOn E ) B ) p /\ ( # ` f ) = 2 /\ ( ( 1st ` ( 1st ` t ) ) = A /\ ( 2nd ` ( 1st ` t ) ) = ( p ` 1 ) /\ ( 2nd ` t ) = B ) ) } )
Theorem	2spthonot 25430*	The set of simple paths of length 2 between two vertices (in a graph) as ordered triple. (Contributed by Alexander van der Vekens, 1-Mar-2018.)
|- ( ( ( V e. X /\ E e. Y ) /\ ( A e. V /\ B e. V ) ) -> ( A ( V 2SPathOnOt E ) B ) = { t e. ( ( V X. V ) X. V ) | E. f E. p ( f ( A ( V SPathOn E ) B ) p /\ ( # ` f ) = 2 /\ ( ( 1st ` ( 1st ` t ) ) = A /\ ( 2nd ` ( 1st ` t ) ) = ( p ` 1 ) /\ ( 2nd ` t ) = B ) ) } )
Theorem	2wlksot 25431*	The set of walks of length 2 (in a graph) as ordered triple. (Contributed by Alexander van der Vekens, 21-Feb-2018.)
|- ( ( V e. X /\ E e. Y ) -> ( V 2WalksOt E ) = { t e. ( ( V X. V ) X. V ) | E. a e. V E. b e. V t e. ( a ( V 2WalksOnOt E ) b ) } )
Theorem	2spthsot 25432*	The set of simple paths of length 2 (in a graph) as ordered triple. (Contributed by Alexander van der Vekens, 28-Feb-2018.)
|- ( ( V e. X /\ E e. Y ) -> ( V 2SPathOnOt E ) = { t e. ( ( V X. V ) X. V ) | E. a e. V E. b e. V t e. ( a ( V 2SPathOnOt E ) b ) } )
Theorem	el2wlkonot 25433*	A walk of length 2 between two vertices (in a graph) as ordered triple. (Contributed by Alexander van der Vekens, 15-Feb-2018.)
|- ( ( ( V e. X /\ E e. Y ) /\ ( A e. V /\ C e. V ) ) -> ( T e. ( A ( V 2WalksOnOt E ) C ) <-> E. b e. V ( T = <. A , b , C >. /\ E. f E. p ( f ( V Walks E ) p /\ ( # ` f ) = 2 /\ ( A = ( p ` 0 ) /\ b = ( p ` 1 ) /\ C = ( p ` 2 ) ) ) ) ) )
Theorem	el2spthonot 25434*	A simple path of length 2 between two vertices (in a graph) as ordered triple. (Contributed by Alexander van der Vekens, 2-Mar-2018.)
|- ( ( ( V e. X /\ E e. Y ) /\ ( A e. V /\ C e. V ) ) -> ( T e. ( A ( V 2SPathOnOt E ) C ) <-> E. b e. V ( T = <. A , b , C >. /\ E. f E. p ( f ( V SPaths E ) p /\ ( # ` f ) = 2 /\ ( A = ( p ` 0 ) /\ b = ( p ` 1 ) /\ C = ( p ` 2 ) ) ) ) ) )
Theorem	el2spthonot0 25435*	A simple path of length 2 between two vertices (in a graph) as ordered triple. (Contributed by Alexander van der Vekens, 9-Mar-2018.)
|- ( ( ( V e. X /\ E e. Y ) /\ ( A e. V /\ C e. V ) ) -> ( T e. ( A ( V 2SPathOnOt E ) C ) <-> E. b e. V ( T = <. A , b , C >. /\ <. A , b , C >. e. ( A ( V 2SPathOnOt E ) C ) ) ) )
Theorem	el2wlkonotot0 25436*	A walk of length 2 between two vertices (in a graph) as ordered triple. (Contributed by Alexander van der Vekens, 15-Feb-2018.)
|- ( ( ( V e. X /\ E e. Y ) /\ ( R e. V /\ S e. V ) ) -> ( <. A , B , C >. e. ( R ( V 2WalksOnOt E ) S ) <-> ( A = R /\ C = S /\ E. f E. p ( f ( V Walks E ) p /\ ( # ` f ) = 2 /\ ( A = ( p ` 0 ) /\ B = ( p ` 1 ) /\ C = ( p ` 2 ) ) ) ) ) )
Theorem	el2wlkonotot 25437*	A walk of length 2 between two vertices (in a graph) as ordered triple. (Contributed by Alexander van der Vekens, 15-Feb-2018.)
|- ( ( ( V e. X /\ E e. Y ) /\ ( A e. V /\ C e. V ) ) -> ( <. A , B , C >. e. ( A ( V 2WalksOnOt E ) C ) <-> E. f E. p ( f ( V Walks E ) p /\ ( # ` f ) = 2 /\ ( A = ( p ` 0 ) /\ B = ( p ` 1 ) /\ C = ( p ` 2 ) ) ) ) )
Theorem	el2wlkonotot1 25438	A walk of length 2 between two vertices (in a graph) as ordered triple. (Contributed by Alexander van der Vekens, 8-Mar-2018.)
|- ( ( ( V e. X /\ E e. Y ) /\ ( R e. V /\ S e. V ) ) -> ( <. A , B , C >. e. ( R ( V 2WalksOnOt E ) S ) <-> ( A = R /\ C = S /\ <. A , B , C >. e. ( A ( V 2WalksOnOt E ) C ) ) ) )
Theorem	2wlkonot3v 25439	If an ordered triple represents a walk of length 2, its components are vertices. (Contributed by Alexander van der Vekens, 19-Feb-2018.)
|- ( T e. ( A ( V 2WalksOnOt E ) C ) -> ( ( V e. _V /\ E e. _V ) /\ ( A e. V /\ C e. V ) /\ T e. ( ( V X. V ) X. V ) ) )
Theorem	2spthonot3v 25440	If an ordered triple represents a simple path of length 2, its components are vertices. (Contributed by Alexander van der Vekens, 1-Mar-2018.)
|- ( T e. ( A ( V 2SPathOnOt E ) C ) -> ( ( V e. _V /\ E e. _V ) /\ ( A e. V /\ C e. V ) /\ T e. ( ( V X. V ) X. V ) ) )
Theorem	2wlkonotv 25441	If an ordered tripple represents a walk of length 2, its components are vertices. (Contributed by Alexander van der Vekens, 19-Feb-2018.)
|- ( <. A , B , C >. e. ( A ( V 2WalksOnOt E ) C ) -> ( ( V e. _V /\ E e. _V ) /\ ( A e. V /\ B e. V /\ C e. V ) ) )
Theorem	el2wlksoton 25442*	A walk of length 2 between two vertices (in a graph) as ordered triple. (Contributed by Alexander van der Vekens, 21-Feb-2018.)
|- ( ( V e. X /\ E e. Y ) -> ( T e. ( V 2WalksOt E ) <-> E. a e. V E. b e. V T e. ( a ( V 2WalksOnOt E ) b ) ) )
Theorem	el2spthsoton 25443*	A simple path of length 2 between two vertices (in a graph) as ordered triple. (Contributed by Alexander van der Vekens, 1-Mar-2018.)
|- ( ( V e. X /\ E e. Y ) -> ( T e. ( V 2SPathOnOt E ) <-> E. a e. V E. b e. V T e. ( a ( V 2SPathOnOt E ) b ) ) )
Theorem	el2wlksot 25444*	A walk of length 2 between two vertices (in a graph) as ordered triple. (Contributed by Alexander van der Vekens, 21-Feb-2018.)
|- ( ( V e. X /\ E e. Y ) -> ( T e. ( V 2WalksOt E ) <-> E. a e. V E. b e. V E. c e. V ( T = <. a , b , c >. /\ E. f E. p ( f ( V Walks E ) p /\ ( # ` f ) = 2 /\ ( a = ( p ` 0 ) /\ b = ( p ` 1 ) /\ c = ( p ` 2 ) ) ) ) ) )
Theorem	el2pthsot 25445*	A simple path of length 2 between two vertices (in a graph) as ordered triple. (Contributed by Alexander van der Vekens, 28-Feb-2018.)
|- ( ( V e. X /\ E e. Y ) -> ( T e. ( V 2SPathOnOt E ) <-> E. a e. V E. b e. V E. c e. V ( T = <. a , b , c >. /\ E. f E. p ( f ( V SPaths E ) p /\ ( # ` f ) = 2 /\ ( a = ( p ` 0 ) /\ b = ( p ` 1 ) /\ c = ( p ` 2 ) ) ) ) ) )
Theorem	el2wlksotot 25446*	A walk of length 2 between two vertices (in a graph) as ordered triple. (Contributed by Alexander van der Vekens, 26-Feb-2018.)
|- ( ( ( V e. X /\ E e. Y ) /\ ( A e. V /\ B e. V /\ C e. V ) ) -> ( <. A , B , C >. e. ( V 2WalksOt E ) <-> E. f E. p ( f ( V Walks E ) p /\ ( # ` f ) = 2 /\ ( A = ( p ` 0 ) /\ B = ( p ` 1 ) /\ C = ( p ` 2 ) ) ) ) )
Theorem	usg2wlkonot 25447	A walk of length 2 between two vertices as ordered triple in an undirected simple graph. This theorem would also hold for undirected multigraphs, but to proof this the cases A = B and/or B = C must be considered separately. (Contributed by Alexander van der Vekens, 18-Feb-2018.)
|- ( ( V USGrph E /\ ( A e. V /\ B e. V /\ C e. V ) ) -> ( <. A , B , C >. e. ( A ( V 2WalksOnOt E ) C ) <-> ( { A , B } e. ran E /\ { B , C } e. ran E ) ) )
Theorem	usg2wotspth 25448*	A walk of length 2 between two different vertices as ordered triple corresponds to a simple path of length 2 in an undirected simple graph. (Contributed by Alexander van der Vekens, 16-Feb-2018.)
|- ( ( V USGrph E /\ ( A e. V /\ B e. V /\ C e. V ) /\ A =/= C ) -> ( <. A , B , C >. e. ( A ( V 2WalksOnOt E ) C ) <-> E. f E. p ( f ( V SPaths E ) p /\ ( # ` f ) = 2 /\ ( A = ( p ` 0 ) /\ B = ( p ` 1 ) /\ C = ( p ` 2 ) ) ) ) )
Theorem	2pthwlkonot 25449	For two different vertices, a walk of length 2 between these vertices as ordered triple is a simple path of length 2 between these vertices as ordered triple in an undirected simple graph. (Contributed by Alexander van der Vekens, 2-Mar-2018.)
|- ( ( V USGrph E /\ ( A e. V /\ B e. V ) /\ A =/= B ) -> ( A ( V 2SPathOnOt E ) B ) = ( A ( V 2WalksOnOt E ) B ) )
Theorem	2wot2wont 25450*	The set of (simple) paths of length 2 (in a graph) is the set of (simple) paths of length 2 between any two different vertices. (Contributed by Alexander van der Vekens, 27-Feb-2018.)
|- ( ( V e. X /\ E e. Y ) -> ( V 2WalksOt E ) = U_ x e. V U_ y e. V ( x ( V 2WalksOnOt E ) y ) )
Theorem	2spontn0vne 25451	If the set of simple paths of length 2 between two vertices (in a graph) is not empty, the two vertices must be not equal. (Contributed by Alexander van der Vekens, 3-Mar-2018.)
|- ( ( X ( V 2SPathOnOt E ) Y ) =/= (/) -> X =/= Y )
Theorem	usg2spthonot 25452	A simple path of length 2 between two vertices as ordered triple corresponds to two adjacent edges in an undirected simple graph. (Contributed by Alexander van der Vekens, 8-Mar-2018.)
|- ( ( V USGrph E /\ ( A e. V /\ B e. V /\ C e. V ) ) -> ( <. A , B , C >. e. ( A ( V 2SPathOnOt E ) C ) <-> ( A =/= C /\ { A , B } e. ran E /\ { B , C } e. ran E ) ) )
Theorem	usg2spthonot0 25453	A simple path of length 2 between two vertices as ordered triple corresponds to two adjacent edges in an undirected simple graph. (Contributed by Alexander van der Vekens, 8-Mar-2018.)
|- ( ( V USGrph E /\ ( A e. V /\ B e. V /\ C e. V ) ) -> ( <. S , B , T >. e. ( A ( V 2SPathOnOt E ) C ) <-> ( ( S = A /\ T = C /\ A =/= C ) /\ ( { A , B } e. ran E /\ { B , C } e. ran E ) ) ) )
Theorem	usg2spthonot1 25454*	A simple path of length 2 between two vertices as ordered triple corresponds to two adjacent edges in an undirected simple graph. (Contributed by Alexander van der Vekens, 9-Mar-2018.)
|- ( ( V USGrph E /\ ( A e. V /\ C e. V ) ) -> ( T e. ( A ( V 2SPathOnOt E ) C ) <-> E. b e. V ( ( T = <. A , b , C >. /\ A =/= C ) /\ ( { A , b } e. ran E /\ { b , C } e. ran E ) ) ) )
Theorem	2spot2iun2spont 25455*	The set of simple paths of length 2 (in a graph) is the double union of the simple paths of length 2 between different vertices. (Contributed by Alexander van der Vekens, 3-Mar-2018.)
|- ( ( V e. _V /\ E e. _V ) -> ( V 2SPathOnOt E ) = U_ x e. V U_ y e. ( V \ { x } ) ( x ( V 2SPathOnOt E ) y ) )
Theorem	2spotfi 25456	In a finite graph, the set of simple paths of length 2 between two vertices (as ordered triples) is finite. (Contributed by Alexander van der Vekens, 4-Mar-2018.)
|- ( ( ( V e. Fin /\ E e. X ) /\ ( A e. V /\ B e. V ) ) -> ( A ( V 2SPathOnOt E ) B ) e. Fin )
16.1.6  Vertex degree
Syntax	cvdg 25457	Extend class notation with the vertex degree function.
class VDeg
Definition	df-vdgr 25458*	Define the vertex degree function (for an undirected multigraph). To be appropriate for multigraphs, we have to double-count those edges that contain u "twice" (i.e. self-loops), this being represented as a singleton as the edge's value. Since the degree of a vertex can be (positive) infinity (if the graph containing the vertex is not of finite size), the extended addition +e is used for the summation of the number of "ordinary" edges" and the number of "loops". (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Alexander van der Vekens, 20-Dec-2017.)
|- VDeg = ( v e. _V , e e. _V |-> ( u e. v |-> ( ( # ` { x e. dom e | u e. ( e ` x ) } ) +e ( # ` { x e. dom e | ( e ` x ) = { u } } ) ) ) )
Theorem	vdgrfval 25459*	The value of the vertex degree function. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Alexander van der Vekens, 20-Dec-2017.)
|- ( ( V e. W /\ E Fn A /\ A e. X ) -> ( V VDeg E ) = ( u e. V |-> ( ( # ` { x e. A | u e. ( E ` x ) } ) +e ( # ` { x e. A | ( E ` x ) = { u } } ) ) ) )
Theorem	vdgrval 25460*	The value of the vertex degree function. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Alexander van der Vekens, 20-Dec-2017.)
|- ( ( ( V e. W /\ E Fn A /\ A e. X ) /\ U e. V ) -> ( ( V VDeg E ) ` U ) = ( ( # ` { x e. A | U e. ( E ` x ) } ) +e ( # ` { x e. A | ( E ` x ) = { U } } ) ) )
Theorem	vdgrfival 25461*	The value of the vertex degree function (for graphs of finite size). (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Alexander van der Vekens, 21-Jan-2018.)
|- ( ( ( V e. W /\ E Fn A /\ A e. Fin ) /\ U e. V ) -> ( ( V VDeg E ) ` U ) = ( ( # ` { x e. A | U e. ( E ` x ) } ) + ( # ` { x e. A | ( E ` x ) = { U } } ) ) )
Theorem	vdgrf 25462	The vertex degree function is a function from vertices to nonnegative integers or plus infinity. (Contributed by Alexander van der Vekens, 20-Dec-2017.)
|- ( ( V e. W /\ E Fn A /\ A e. X ) -> ( V VDeg E ) : V --> ( NN0 u. { +oo } ) )
Theorem	vdgrfif 25463	The vertex degree function on graphs of finite size is a function from vertices to nonnegative integers. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Alexander van der Vekens, 20-Dec-2017.)
|- ( ( V e. W /\ E Fn A /\ A e. Fin ) -> ( V VDeg E ) : V --> NN0 )
Theorem	vdgr0 25464	The degree of a vertex in an empty graph is zero, because there are no edges. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Alexander van der Vekens, 20-Dec-2017.)
|- ( ( V e. W /\ U e. V ) -> ( ( V VDeg (/) ) ` U ) = 0 )
Theorem	vdgrun 25465	The degree of a vertex in the union of two graphs on the same vertex set is the sum of the degrees of the vertex in each graph. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Alexander van der Vekens, 21-Dec-2017.)
|- ( ph -> E Fn A )   &    |- ( ph -> F Fn B )   &    |- ( ph -> A e. X )   &    |- ( ph -> B e. Y )   &    |- ( ph -> ( A i^i B ) = (/) )   &    |- ( ph -> V UMGrph E )   &    |- ( ph -> V UMGrph F )   &    |- ( ph -> U e. V )   =>    |- ( ph -> ( ( V VDeg ( E u. F ) ) ` U ) = ( ( ( V VDeg E ) ` U ) +e ( ( V VDeg F ) ` U ) ) )
Theorem	vdgrfiun 25466	The degree of a vertex in the union of two graphs (of finite size) on the same vertex set is the sum of the degrees of the vertex in each graph. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Alexander van der Vekens, 21-Jan-2018.)
|- ( ph -> E Fn A )   &    |- ( ph -> F Fn B )   &    |- ( ph -> A e. Fin )   &    |- ( ph -> B e. Fin )   &    |- ( ph -> ( A i^i B ) = (/) )   &    |- ( ph -> V UMGrph E )   &    |- ( ph -> V UMGrph F )   &    |- ( ph -> U e. V )   =>    |- ( ph -> ( ( V VDeg ( E u. F ) ) ` U ) = ( ( ( V VDeg E ) ` U ) + ( ( V VDeg F ) ` U ) ) )
Theorem	vdgr1d 25467	The vertex degree of a one-edge graph, case 4: an edge from a vertex to itself contributes two to the vertex's degree. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Alexander van der Vekens, 22-Dec-2017.)
|- ( ph -> V e. _V )   &    |- ( ph -> A e. _V )   &    |- ( ph -> U e. V )   =>    |- ( ph -> ( ( V VDeg { <. A , { U } >. } ) ` U ) = 2 )
Theorem	vdgr1b 25468	The vertex degree of a one-edge graph, case 2: an edge from the given vertex to some other vertex contributes one to the vertex's degree. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Alexander van der Vekens, 22-Dec-2017.)
|- ( ph -> V e. _V )   &    |- ( ph -> A e. _V )   &    |- ( ph -> U e. V )   &    |- ( ph -> B e. V )   &    |- ( ph -> B =/= U )   =>    |- ( ph -> ( ( V VDeg { <. A , { U , B } >. } ) ` U ) = 1 )
Theorem	vdgr1c 25469	The vertex degree of a one-edge graph, case 3: an edge from some other vertex to the given vertex contributes one to the vertex's degree. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Alexander van der Vekens, 22-Dec-2017.)
|- ( ph -> V e. _V )   &    |- ( ph -> A e. _V )   &    |- ( ph -> U e. V )   &    |- ( ph -> B e. V )   &    |- ( ph -> B =/= U )   =>    |- ( ph -> ( ( V VDeg { <. A , { B , U } >. } ) ` U ) = 1 )
Theorem	vdgr1a 25470	The vertex degree of a one-edge graph, case 1: an edge between two vertices other than the given vertex contributes nothing to the vertex degree. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Alexander van der Vekens, 22-Dec-2017.)
|- ( ph -> V e. _V )   &    |- ( ph -> A e. _V )   &    |- ( ph -> U e. V )   &    |- ( ph -> B e. V )   &    |- ( ph -> B =/= U )   &    |- ( ph -> C e. V )   &    |- ( ph -> C =/= U )   =>    |- ( ph -> ( ( V VDeg { <. A , { B , C } >. } ) ` U ) = 0 )
Theorem	vdusgraval 25471*	The value of the vertex degree function for simple undirected graphs. (Contributed by Alexander van der Vekens, 20-Dec-2017.)
|- ( ( V USGrph E /\ U e. V ) -> ( ( V VDeg E ) ` U ) = ( # ` { x e. dom E | U e. ( E ` x ) } ) )
Theorem	vdusgra0nedg 25472*	If a vertex in a simple graph has degree 0, the vertex is not adjacent to another vertex via an edge. (Contributed by Alexander van der Vekens, 8-Dec-2017.)
|- ( ( V USGrph E /\ U e. V /\ E e. Fin ) -> ( ( ( V VDeg E ) ` U ) = 0 -> -. E. v e. V { U , v } e. ran E ) )
Theorem	vdgrnn0pnf 25473	The degree of a vertex is either a nonnegative integer or positive infinity. (Contributed by Alexander van der Vekens, 30-Dec-2017.)
|- ( ( V USGrph E /\ X e. V ) -> ( ( V VDeg E ) ` X ) e. ( NN0 u. { +oo } ) )
Theorem	usgfidegfi 25474*	In a finite graph, the degree of each vertex is finite. (Contributed by Alexander van der Vekens, 10-Mar-2018.)
|- ( ( V USGrph E /\ V e. Fin ) -> A. v e. V ( ( V VDeg E ) ` v ) e. NN0 )
Theorem	usgfiregdegfi 25475*	In a finite graph, the degree of each vertex is finite. (Contributed by Alexander van der Vekens, 6-Mar-2018.)
|- ( ( V USGrph E /\ V e. Fin /\ V =/= (/) ) -> ( A. v e. V ( ( V VDeg E ) ` v ) = K -> K e. NN0 ) )
Theorem	hashnbgravd 25476	The size of the set of the neighbors of a vertex is the vertex degree of this vertex. (Contributed by Alexander van der Vekens, 17-Dec-2017.)
|- ( ( V USGrph E /\ U e. V /\ E e. Fin ) -> ( # ` ( <. V , E >. Neighbors U ) ) = ( ( V VDeg E ) ` U ) )
Theorem	hashnbgravdg 25477	The size of the set of the neighbors of a vertex is the vertex degree of this vertex, analogous to hashnbgravd 25476. (Contributed by Alexander van der Vekens, 20-Dec-2017.)
|- ( ( V USGrph E /\ U e. V ) -> ( # ` ( <. V , E >. Neighbors U ) ) = ( ( V VDeg E ) ` U ) )
Theorem	nbhashnn0 25478	The number of the neighbors of a vertex in a finite undirected simple graph is a nonnegative integer. (Contributed by Alexander van der Vekens, 14-Jul-2018.)
|- ( ( V USGrph E /\ V e. Fin /\ N e. V ) -> ( # ` ( <. V , E >. Neighbors N ) ) e. NN0 )
Theorem	nbhashuvtx1 25479	If the number of the neighbors of a vertex in a finite graph is the number of vertices of the graph minus 1, each vertex except the first mentioned vertex is a neighbor of this vertex. (Contributed by Alexander van der Vekens, 14-Jul-2018.)
|- ( ( V USGrph E /\ V e. Fin /\ N e. V ) -> ( ( # ` ( <. V , E >. Neighbors N ) ) = ( ( # ` V ) - 1 ) -> ( ( M e. V /\ M =/= N ) -> M e. ( <. V , E >. Neighbors N ) ) ) )
Theorem	nbhashuvtx 25480	If the number of the neighbors of a vertex in a graph is the number of vertices of the graph minus 1, the vertex is universal. (Contributed by Alexander van der Vekens, 14-Jul-2018.)
|- ( ( V USGrph E /\ V e. Fin /\ N e. V ) -> ( ( # ` ( <. V , E >. Neighbors N ) ) = ( ( # ` V ) - 1 ) -> N e. ( V UnivVertex E ) ) )
Theorem	uvtxhashnb 25481	A universal vertex has n - 1 neighbors in a graph with n vertices, a biconditional version of uvtxnm1nbgra 25058. (Contributed by Alexander van der Vekens, 14-Jul-2018.)
|- ( ( V USGrph E /\ V e. Fin /\ N e. V ) -> ( N e. ( V UnivVertex E ) <-> ( # ` ( <. V , E >. Neighbors N ) ) = ( ( # ` V ) - 1 ) ) )
Theorem	usgravd0nedg 25482*	If a vertex in a simple graph has degree 0, the vertex is not adjacent to another vertex via an edge, analogous to vdusgra0nedg 25472. (Contributed by Alexander van der Vekens, 20-Dec-2017.)
|- ( ( V USGrph E /\ U e. V ) -> ( ( ( V VDeg E ) ` U ) = 0 -> -. E. v e. V { U , v } e. ran E ) )
Theorem	usgravd00 25483*	If every vertex in a simple graph has degree 0, there is no edge in the graph. (Contributed by Alexander van der Vekens, 12-Jul-2018.)
|- ( V USGrph E -> ( A. v e. V ( ( V VDeg E ) ` v ) = 0 -> E = (/) ) )
Theorem	usgrauvtxvdbi 25484	In a finite undirected simple graph with n vertices a vertex is universal if the vertex has degree n - 1. (Contributed by Alexander van der Vekens, 14-Jul-2018.)
|- ( ( V USGrph E /\ V e. Fin /\ K e. V ) -> ( K e. ( V UnivVertex E ) <-> ( ( V VDeg E ) ` K ) = ( ( # ` V ) - 1 ) ) )
Theorem	vdiscusgra 25485*	In a finite complete undirected simple graph with n vertices every vertex has degree n - 1. (Contributed by Alexander van der Vekens, 14-Jul-2018.)
|- ( ( V USGrph E /\ V e. Fin ) -> ( A. v e. V ( ( V VDeg E ) ` v ) = ( ( # ` V ) - 1 ) -> V ComplUSGrph E ) )
16.1.7  Regular graphs
16.1.7.1  Definition and basic properties
Syntax	crgra 25486	Extend class notation to include the class of all regular graphs.
class RegGrph
Syntax	crusgra 25487	Extend class notation to include the class of all regular undirected simple graphs.
class RegUSGrph
Definition	df-rgra 25488*	Define the class of k-regular "graphs". (Contributed by Alexander van der Vekens, 6-Jul-2018.)
|- RegGrph = { <. <. v , e >. , k >. | ( k e. NN0 /\ A. p e. v ( ( v VDeg e ) ` p ) = k ) }
Definition	df-rusgra 25489*	Define the class of k-regular undirected simple graphs. (Contributed by Alexander van der Vekens, 6-Jul-2018.)
|- RegUSGrph = { <. <. v , e >. , k >. | ( v USGrph e /\ <. v , e >. RegGrph k ) }
Theorem	isrgra 25490*	The property of being a k-regular graph. (Contributed by Alexander van der Vekens, 7-Jul-2018.)
|- ( ( V e. X /\ E e. Y /\ K e. Z ) -> ( <. V , E >. RegGrph K <-> ( K e. NN0 /\ A. p e. V ( ( V VDeg E ) ` p ) = K ) ) )
Theorem	isrusgra 25491*	The property of being a k-regular undirected simple graph. (Contributed by Alexander van der Vekens, 7-Jul-2018.)
|- ( ( V e. X /\ E e. Y /\ K e. Z ) -> ( <. V , E >. RegUSGrph K <-> ( V USGrph E /\ K e. NN0 /\ A. p e. V ( ( V VDeg E ) ` p ) = K ) ) )
Theorem	rgraprop 25492*	The properties of a k-regular graph. (Contributed by Alexander van der Vekens, 8-Jul-2018.)
|- ( <. V , E >. RegGrph K -> ( K e. NN0 /\ A. p e. V ( ( V VDeg E ) ` p ) = K ) )
Theorem	rusgraprop 25493*	The properties of a k-regular undirected simple graph. (Contributed by Alexander van der Vekens, 8-Jul-2018.)
|- ( <. V , E >. RegUSGrph K -> ( V USGrph E /\ K e. NN0 /\ A. p e. V ( ( V VDeg E ) ` p ) = K ) )
Theorem	rusgrargra 25494	A k-regular undirected simple graph is a k-regular graph. (Contributed by Alexander van der Vekens, 8-Jul-2018.)
|- ( <. V , E >. RegUSGrph K -> <. V , E >. RegGrph K )
Theorem	rusisusgra 25495	Any k-regular undirected simple graph is an undirected simple graph. (Contributed by Alexander van der Vekens, 8-Jul-2018.)
|- ( <. V , E >. RegUSGrph K -> V USGrph E )
Theorem	isrusgusrg 25496	A graph is a k-regular undirected simple graph iff it is an undirected simple graph and a k-regular graph. (Contributed by AV, 3-Jan-2020.)
|- ( ( V e. X /\ E e. Y /\ K e. Z ) -> ( <. V , E >. RegUSGrph K <-> ( V USGrph E /\ <. V , E >. RegGrph K ) ) )
Theorem	isrusgusrgcl 25497	A graph represented by a class is a k-regular undirected simple graph iff it is an undirected simple graph and a k-regular graph. (Contributed by AV, 2-Jan-2020.)
|- ( ( G e. ( X X. Y ) /\ K e. Z ) -> ( G RegUSGrph K <-> ( G e. USGrph /\ G RegGrph K ) ) )
Theorem	isrgrac 25498*	The property of being a k-regular graph represented by a class. (Contributed by AV, 3-Jan-2020.)
|- ( ( G e. ( X X. Y ) /\ K e. Z ) -> ( G RegGrph K <-> ( K e. NN0 /\ A. p e. ( 1st ` G ) ( ( VDeg ` G ) ` p ) = K ) ) )
Theorem	isrusgrac 25499*	The property of being a k-regular undirected simple graph represented by a class. (Contributed by AV, 3-Jan-2020.)
|- ( ( G e. ( X X. Y ) /\ K e. Z ) -> ( G RegUSGrph K <-> ( G e. USGrph /\ K e. NN0 /\ A. p e. ( 1st ` G ) ( ( VDeg ` G ) ` p ) = K ) ) )
Theorem	0egra0rgra 25500	A graph is 0-regular if it has no edges. (Contributed by Alexander van der Vekens, 8-Jul-2018.)
|- A. v <. v , (/) >. RegGrph 0