P. 169 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 16801-16900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	trlreslem 16801	Lemma for trlres 16802. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Mario Carneiro, 3-May-2015.) (Revised by AV, 6-Mar-2021.) Hypothesis revised using the prefix operation. (Revised by AV, 30-Nov-2022.)
|- V = (Vtx ` G )   &    |- I = (iEdg ` G )   &    |- ( ph -> F (Trails ` G ) P )   &    |- ( ph -> N e. ( 0..^ (♯ ` F ) ) )   &    |- H = ( F prefix N )   =>    |- ( ph -> H : ( 0..^ (♯ ` H ) ) -1-1-onto-> dom ( I |` ( F " ( 0..^ N ) ) ) )
Theorem	trlres 16802	The restriction <. H , Q >. of a trail <. F , P >. to an initial segment of the trail (of length N) forms a trail on the subgraph S consisting of the edges in the initial segment. (Contributed by AV, 6-Mar-2021.) Hypothesis revised using the prefix operation. (Revised by AV, 30-Nov-2022.)
|- V = (Vtx ` G )   &    |- I = (iEdg ` G )   &    |- ( ph -> F (Trails ` G ) P )   &    |- ( ph -> N e. ( 0..^ (♯ ` F ) ) )   &    |- H = ( F prefix N )   &    |- ( ph -> (Vtx ` S ) = V )   &    |- ( ph -> (iEdg ` S ) = ( I |` ( F " ( 0..^ N ) ) ) )   &    |- Q = ( P |` ( 0 ... N ) )   =>    |- ( ph -> H (Trails ` S ) Q )
12.3.3  Closed walks as words
12.3.3.1  Closed walks as words
Syntax	cclwwlk 16803	Extend class notation with closed walks (in an undirected graph) as word over the set of vertices.
class ClWWalks
Definition	df-clwwlk 16804*	Define the set of all closed walks (in an undirected graph) as words over the set of vertices. Such a word corresponds to the sequence p(0) p(1) ... p(n-1) of the vertices in a closed walk p(0) e(f(1)) p(1) e(f(2)) ... p(n-1) e(f(n)) p(n)=p(0) as defined elsewhere. Notice that the word does not contain the terminating vertex p(n) of the walk, because it is always equal to the first vertex of the closed walk. (Contributed by Alexander van der Vekens, 20-Mar-2018.) (Revised by AV, 24-Apr-2021.)
|- ClWWalks = ( g e. _V |-> { w e. Word (Vtx ` g ) | ( w =/= (/) /\ A. i e. ( 0..^ ( (♯ ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. (Edg ` g ) /\ { (lastS ` w ) , ( w ` 0 ) } e. (Edg ` g ) ) } )
Theorem	clwwlkg 16805*	The set of closed walks (in an undirected graph) as words over the set of vertices. (Contributed by Alexander van der Vekens, 20-Mar-2018.) (Revised by AV, 24-Apr-2021.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   =>    |- ( G e. W -> (ClWWalks ` G ) = { w e. Word V | ( w =/= (/) /\ A. i e. ( 0..^ ( (♯ ` w ) - 1 ) ) { ( w ` i ) , ( w ` ( i + 1 ) ) } e. E /\ { (lastS ` w ) , ( w ` 0 ) } e. E ) } )
Theorem	isclwwlk 16806*	Properties of a word to represent a closed walk (in an undirected graph). (Contributed by Alexander van der Vekens, 20-Mar-2018.) (Revised by AV, 24-Apr-2021.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   =>    |- ( W e. (ClWWalks ` G ) <-> ( ( W e. Word V /\ W =/= (/) ) /\ A. i e. ( 0..^ ( (♯ ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { (lastS ` W ) , ( W ` 0 ) } e. E ) )
Theorem	clwwlkbp 16807	Basic properties of a closed walk (in an undirected graph) as word. (Contributed by Alexander van der Vekens, 15-Mar-2018.) (Revised by AV, 24-Apr-2021.)
|- V = (Vtx ` G )   =>    |- ( W e. (ClWWalks ` G ) -> ( G e. _V /\ W e. Word V /\ W =/= (/) ) )
Theorem	clwwlkgt0 16808	There is no empty closed walk (i.e. a closed walk without any edge) represented by a word of vertices. (Contributed by Alexander van der Vekens, 15-Sep-2018.) (Revised by AV, 24-Apr-2021.)
|- ( W e. (ClWWalks ` G ) -> 0 < (♯ ` W ) )
Theorem	clwwlksswrd 16809	Closed walks (represented by words) are words. (Contributed by Alexander van der Vekens, 25-Mar-2018.) (Revised by AV, 25-Apr-2021.)
|- (ClWWalks ` G ) C_ Word (Vtx ` G )
Theorem	clwwlkex 16810	Existence of the set of closed walks (represented by words). (Contributed by Jim Kingdon, 21-Feb-2026.)
|- ( G e. V -> (ClWWalks ` G ) e. _V )
Theorem	clwwlk1loop 16811	A closed walk of length 1 is a loop. (Contributed by AV, 24-Apr-2021.)
|- ( ( W e. (ClWWalks ` G ) /\ (♯ ` W ) = 1 ) -> { ( W ` 0 ) , ( W ` 0 ) } e. (Edg ` G ) )
Theorem	clwwlkccatlem 16812*	Lemma for clwwlkccat 16813: index j is shifted up by (♯ ` A ), and the case i = ( (♯ ` A ) - 1 ) is covered by the "bridge" { (lastS ` A ) , ( B ` 0 ) } = { (lastS ` A ) , ( A ` 0 ) } e. (Edg ` G ). (Contributed by AV, 23-Apr-2022.)
|- ( ( ( ( A e. Word (Vtx ` G ) /\ A =/= (/) ) /\ A. i e. ( 0..^ ( (♯ ` A ) - 1 ) ) { ( A ` i ) , ( A ` ( i + 1 ) ) } e. (Edg ` G ) /\ { (lastS ` A ) , ( A ` 0 ) } e. (Edg ` G ) ) /\ ( ( B e. Word (Vtx ` G ) /\ B =/= (/) ) /\ A. j e. ( 0..^ ( (♯ ` B ) - 1 ) ) { ( B ` j ) , ( B ` ( j + 1 ) ) } e. (Edg ` G ) /\ { (lastS ` B ) , ( B ` 0 ) } e. (Edg ` G ) ) /\ ( A ` 0 ) = ( B ` 0 ) ) -> A. i e. ( 0..^ ( (♯ ` ( A ++ B ) ) - 1 ) ) { ( ( A ++ B ) ` i ) , ( ( A ++ B ) ` ( i + 1 ) ) } e. (Edg ` G ) )
Theorem	clwwlkccat 16813	The concatenation of two words representing closed walks anchored at the same vertex represents a closed walk. The resulting walk is a "double loop", starting at the common vertex, coming back to the common vertex by the first walk, following the second walk and finally coming back to the common vertex again. (Contributed by AV, 23-Apr-2022.)
|- ( ( A e. (ClWWalks ` G ) /\ B e. (ClWWalks ` G ) /\ ( A ` 0 ) = ( B ` 0 ) ) -> ( A ++ B ) e. (ClWWalks ` G ) )
Theorem	umgrclwwlkge2 16814	A closed walk in a multigraph has a length of at least 2 (because it cannot have a loop). (Contributed by Alexander van der Vekens, 16-Sep-2018.) (Revised by AV, 24-Apr-2021.)
|- ( G e. UMGraph -> ( P e. (ClWWalks ` G ) -> 2 <_ (♯ ` P ) ) )
12.3.3.2  Closed walks of a fixed length as words
Syntax	cclwwlkn 16815	Extend class notation with closed walks (in an undirected graph) of a fixed length as word over the set of vertices.
class ClWWalksN
Definition	df-clwwlkn 16816*	Define the set of all closed walks of a fixed length n as words over the set of vertices in a graph g. If 0 < n, such a word corresponds to the sequence p(0) p(1) ... p(n-1) of the vertices in a closed walk p(0) e(f(1)) p(1) e(f(2)) ... p(n-1) e(f(n)) p(n)=p(0) . For n = 0, the set is empty, see clwwlkn0 16820. (Contributed by Alexander van der Vekens, 20-Mar-2018.) (Revised by AV, 24-Apr-2021.) (Revised by AV, 22-Mar-2022.)
|- ClWWalksN = ( n e. NN0 , g e. _V |-> { w e. (ClWWalks ` g ) | (♯ ` w ) = n } )
Theorem	clwwlkng 16817*	The set of closed walks of a fixed length N as words over the set of vertices in a graph G. (Contributed by Alexander van der Vekens, 20-Mar-2018.) (Revised by AV, 24-Apr-2021.) (Revised by AV, 22-Mar-2022.)
|- ( ( N e. NN0 /\ G e. V ) -> ( N ClWWalksN G ) = { w e. (ClWWalks ` G ) | (♯ ` w ) = N } )
Theorem	isclwwlkng 16818	A word over the set of vertices representing a closed walk of a fixed length. (Contributed by Alexander van der Vekens, 15-Mar-2018.) (Revised by AV, 24-Apr-2021.) (Revised by AV, 22-Mar-2022.)
|- ( N e. NN0 -> ( W e. ( N ClWWalksN G ) <-> ( W e. (ClWWalks ` G ) /\ (♯ ` W ) = N ) ) )
Theorem	isclwwlkni 16819	A word over the set of vertices representing a closed walk of a fixed length. (Contributed by Jim Kingdon, 22-Feb-2026.)
|- ( W e. ( N ClWWalksN G ) -> ( W e. (ClWWalks ` G ) /\ (♯ ` W ) = N ) )
Theorem	clwwlkn0 16820	There is no closed walk of length 0 (i.e. a closed walk without any edge) represented by a word of vertices. (Contributed by Alexander van der Vekens, 15-Sep-2018.) (Revised by AV, 24-Apr-2021.)
|- ( 0 ClWWalksN G ) = (/)
Theorem	clwwlkclwwlkn 16821	A closed walk of a fixed length as word is a closed walk (in an undirected graph) as word. (Contributed by Alexander van der Vekens, 15-Mar-2018.) (Revised by AV, 24-Apr-2021.) (Proof shortened by AV, 22-Mar-2022.)
|- ( W e. ( N ClWWalksN G ) -> W e. (ClWWalks ` G ) )
Theorem	clwwlksclwwlkn 16822	The closed walks of a fixed length as words are closed walks (in an undirected graph) as words. (Contributed by Alexander van der Vekens, 15-Mar-2018.) (Revised by AV, 12-Apr-2021.)
|- ( N ClWWalksN G ) C_ (ClWWalks ` G )
Theorem	clwwlknlen 16823	The length of a word representing a closed walk of a fixed length is this fixed length. (Contributed by AV, 22-Mar-2022.)
|- ( W e. ( N ClWWalksN G ) -> (♯ ` W ) = N )
Theorem	clwwlknnn 16824	The length of a closed walk of a fixed length as word is a positive integer. (Contributed by AV, 22-Mar-2022.)
|- ( W e. ( N ClWWalksN G ) -> N e. NN )
Theorem	isclwwlkn 16825	A word over the set of vertices representing a closed walk of a fixed length. (Contributed by Alexander van der Vekens, 15-Mar-2018.) (Revised by AV, 24-Apr-2021.) (Revised by AV, 22-Mar-2022.)
|- ( W e. ( N ClWWalksN G ) <-> ( W e. (ClWWalks ` G ) /\ (♯ ` W ) = N ) )
Theorem	clwwlknwrd 16826	A closed walk of a fixed length as word is a word over the vertices. (Contributed by AV, 30-Apr-2021.)
|- V = (Vtx ` G )   =>    |- ( W e. ( N ClWWalksN G ) -> W e. Word V )
Theorem	clwwlknbp 16827	Basic properties of a closed walk of a fixed length as word. (Contributed by AV, 30-Apr-2021.) (Proof shortened by AV, 22-Mar-2022.)
|- V = (Vtx ` G )   =>    |- ( W e. ( N ClWWalksN G ) -> ( W e. Word V /\ (♯ ` W ) = N ) )
Theorem	isclwwlknx 16828*	Characterization of a word representing a closed walk of a fixed length, definition of ClWWalks expanded. (Contributed by AV, 25-Apr-2021.) (Proof shortened by AV, 22-Mar-2022.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   =>    |- ( N e. NN -> ( W e. ( N ClWWalksN G ) <-> ( ( W e. Word V /\ A. i e. ( 0..^ ( (♯ ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { (lastS ` W ) , ( W ` 0 ) } e. E ) /\ (♯ ` W ) = N ) ) )
Theorem	clwwlknp 16829*	Properties of a set being a closed walk (represented by a word). (Contributed by Alexander van der Vekens, 17-Jun-2018.) (Revised by AV, 24-Apr-2021.) (Proof shortened by AV, 23-Mar-2022.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   =>    |- ( W e. ( N ClWWalksN G ) -> ( ( W e. Word V /\ (♯ ` W ) = N ) /\ A. i e. ( 0..^ ( N - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { (lastS ` W ) , ( W ` 0 ) } e. E ) )
Theorem	clwwlkn1 16830	A closed walk of length 1 represented as word is a word consisting of 1 symbol representing a vertex connected to itself by (at least) one edge, that is, a loop. (Contributed by AV, 24-Apr-2021.) (Revised by AV, 11-Feb-2022.)
|- ( W e. ( 1 ClWWalksN G ) <-> ( (♯ ` W ) = 1 /\ W e. Word (Vtx ` G ) /\ { ( W ` 0 ) } e. (Edg ` G ) ) )
Theorem	loopclwwlkn1b 16831	The singleton word consisting of a vertex V represents a closed walk of length 1 iff there is a loop at vertex V. (Contributed by AV, 11-Feb-2022.)
|- ( V e. (Vtx ` G ) -> ( { V } e. (Edg ` G ) <-> <" V "> e. ( 1 ClWWalksN G ) ) )
Theorem	clwwlkn1loopb 16832*	A word represents a closed walk of length 1 iff this word is a singleton word consisting of a vertex with an attached loop. (Contributed by AV, 11-Feb-2022.)
|- ( W e. ( 1 ClWWalksN G ) <-> E. v e. (Vtx ` G ) ( W = <" v "> /\ { v } e. (Edg ` G ) ) )
Theorem	clwwlkn2 16833	A closed walk of length 2 represented as word is a word consisting of 2 symbols representing (not necessarily different) vertices connected by (at least) one edge. (Contributed by Alexander van der Vekens, 19-Sep-2018.) (Revised by AV, 25-Apr-2021.)
|- ( W e. ( 2 ClWWalksN G ) <-> ( (♯ ` W ) = 2 /\ W e. Word (Vtx ` G ) /\ { ( W ` 0 ) , ( W ` 1 ) } e. (Edg ` G ) ) )
Theorem	clwwlkext2edg 16834	If a word concatenated with a vertex represents a closed walk (in a graph), there is an edge between this vertex and the last vertex of the word, and between this vertex and the first vertex of the word. (Contributed by Alexander van der Vekens, 3-Oct-2018.) (Revised by AV, 27-Apr-2021.) (Proof shortened by AV, 22-Mar-2022.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   =>    |- ( ( ( W e. Word V /\ Z e. V /\ N e. ( ZZ>= ` 2 ) ) /\ ( W ++ <" Z "> ) e. ( N ClWWalksN G ) ) -> ( { (lastS ` W ) , Z } e. E /\ { Z , ( W ` 0 ) } e. E ) )
Theorem	clwwlknccat 16835	The concatenation of two words representing closed walks anchored at the same vertex represents a closed walk with a length which is the sum of the lengths of the two walks. The resulting walk is a "double loop", starting at the common vertex, coming back to the common vertex by the first walk, following the second walk and finally coming back to the common vertex again. (Contributed by AV, 24-Apr-2022.)
|- ( ( A e. ( M ClWWalksN G ) /\ B e. ( N ClWWalksN G ) /\ ( A ` 0 ) = ( B ` 0 ) ) -> ( A ++ B ) e. ( ( M + N ) ClWWalksN G ) )
Theorem	umgr2cwwk2dif 16836	If a word represents a closed walk of length at least 2 in a multigraph, the first two symbols of the word must be different. (Contributed by Alexander van der Vekens, 17-Jun-2018.) (Revised by AV, 30-Apr-2021.)
|- ( ( G e. UMGraph /\ N e. ( ZZ>= ` 2 ) /\ W e. ( N ClWWalksN G ) ) -> ( W ` 1 ) =/= ( W ` 0 ) )
Theorem	umgr2cwwkdifex 16837*	If a word represents a closed walk of length at least 2 in a undirected simple graph, there must be a symbol different from the first symbol of the word. (Contributed by Alexander van der Vekens, 17-Jun-2018.) (Revised by AV, 30-Apr-2021.)
|- ( ( G e. UMGraph /\ N e. ( ZZ>= ` 2 ) /\ W e. ( N ClWWalksN G ) ) -> E. i e. ( 0..^ N ) ( W ` i ) =/= ( W ` 0 ) )
12.3.3.3  Closed walks on a vertex of a fixed length as words
Syntax	cclwwlknon 16838	Extend class notation with closed walks (in an undirected graph) anchored at a fixed vertex and of a fixed length as word over the set of vertices.
class ClWWalksNOn
Definition	df-clwwlknon 16839*	Define the set of all closed walks a graph g, anchored at a fixed vertex v (i.e., a walk starting and ending at the fixed vertex v, also called "a closed walk on vertex v") and having a fixed length n as words over the set of vertices. Such a word corresponds to the sequence v=p(0) p(1) ... p(n-1) of the vertices in a closed walk p(0) e(f(1)) p(1) e(f(2)) ... p(n-1) e(f(n)) p(n)=p(0)=v . The set ( ( v (ClWWalksNOn ` g ) n ) corresponds to the set of "walks from v to v of length n" in a statement of [Huneke] p. 2. (Contributed by AV, 24-Feb-2022.)
|- ClWWalksNOn = ( g e. _V |-> ( v e. (Vtx ` g ) , n e. NN0 |-> { w e. ( n ClWWalksN g ) | ( w ` 0 ) = v } ) )
Theorem	clwwlknonmpo 16840*	(ClWWalksNOn ` G ) is an operator mapping a vertex v and a nonnegative integer n to the set of closed walks on v of length n as words over the set of vertices in a graph G. (Contributed by AV, 25-Feb-2022.) (Proof shortened by AV, 2-Mar-2024.)
|- (ClWWalksNOn ` G ) = ( v e. (Vtx ` G ) , n e. NN0 |-> { w e. ( n ClWWalksN G ) | ( w ` 0 ) = v } )
Theorem	clwwlknon 16841*	The set of closed walks on vertex X of length N in a graph G as words over the set of vertices. (Contributed by Alexander van der Vekens, 14-Sep-2018.) (Revised by AV, 28-May-2021.) (Revised by AV, 24-Mar-2022.)
|- ( X (ClWWalksNOn ` G ) N ) = { w e. ( N ClWWalksN G ) | ( w ` 0 ) = X }
Theorem	isclwwlknon 16842	A word over the set of vertices representing a closed walk on vertex X of length N in a graph G. (Contributed by AV, 25-Feb-2022.) (Revised by AV, 24-Mar-2022.)
|- ( W e. ( X (ClWWalksNOn ` G ) N ) <-> ( W e. ( N ClWWalksN G ) /\ ( W ` 0 ) = X ) )
Theorem	clwwlk0on0 16843	There is no word over the set of vertices representing a closed walk on vertex X of length 0 in a graph G. (Contributed by AV, 17-Feb-2022.) (Revised by AV, 25-Feb-2022.)
|- ( X (ClWWalksNOn ` G ) 0 ) = (/)
Theorem	clwwlknonel 16844*	Characterization of a word over the set of vertices representing a closed walk on vertex X of (nonzero) length N in a graph G. This theorem would not hold for N = 0 if W = X = (/). (Contributed by Alexander van der Vekens, 20-Sep-2018.) (Revised by AV, 28-May-2021.) (Revised by AV, 24-Mar-2022.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   =>    |- ( N =/= 0 -> ( W e. ( X (ClWWalksNOn ` G ) N ) <-> ( ( W e. Word V /\ A. i e. ( 0..^ ( (♯ ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { (lastS ` W ) , ( W ` 0 ) } e. E ) /\ (♯ ` W ) = N /\ ( W ` 0 ) = X ) ) )
Theorem	clwwlknonccat 16845	The concatenation of two words representing closed walks on a vertex X represents a closed walk on vertex X. The resulting walk is a "double loop", starting at vertex X, coming back to X by the first walk, following the second walk and finally coming back to X again. (Contributed by AV, 24-Apr-2022.)
|- ( ( A e. ( X (ClWWalksNOn ` G ) M ) /\ B e. ( X (ClWWalksNOn ` G ) N ) ) -> ( A ++ B ) e. ( X (ClWWalksNOn ` G ) ( M + N ) ) )
Theorem	clwwlknon2 16846*	The set of closed walks on vertex X of length 2 in a graph G as words over the set of vertices. (Contributed by AV, 5-Mar-2022.) (Revised by AV, 25-Mar-2022.)
|- C = (ClWWalksNOn ` G )   =>    |- ( X C 2 ) = { w e. ( 2 ClWWalksN G ) | ( w ` 0 ) = X }
Theorem	clwwlknon2x 16847*	The set of closed walks on vertex X of length 2 in a graph G as words over the set of vertices, definition of ClWWalksN expanded. (Contributed by Alexander van der Vekens, 19-Sep-2018.) (Revised by AV, 25-Mar-2022.)
|- C = (ClWWalksNOn ` G )   &    |- V = (Vtx ` G )   &    |- E = (Edg ` G )   =>    |- ( X C 2 ) = { w e. Word V | ( (♯ ` w ) = 2 /\ { ( w ` 0 ) , ( w ` 1 ) } e. E /\ ( w ` 0 ) = X ) }
Theorem	s2elclwwlknon2 16848	Sufficient conditions of a doubleton word to represent a closed walk on vertex X of length 2. (Contributed by AV, 11-May-2022.)
|- C = (ClWWalksNOn ` G )   &    |- V = (Vtx ` G )   &    |- E = (Edg ` G )   =>    |- ( ( X e. V /\ Y e. V /\ { X , Y } e. E ) -> <" X Y "> e. ( X C 2 ) )
Theorem	clwwlknonex2lem1 16849	Lemma 1 for clwwlknonex2 16851: Transformation of a special half-open integer range into a union of a smaller half-open integer range and an unordered pair. This Lemma would not hold for N = 2, i.e., (♯ ` W ) = 0, because ( 0..^ ( ( (♯ ` W ) + 2 ) - 1 ) ) = ( 0..^ ( ( 0 + 2 ) - 1 ) ) = ( 0..^ 1 ) = { 0 } =/= { -u 1 , 0 } = ( (/) u. { -u 1 , 0 } ) = ( ( 0..^ ( 0 - 1 ) ) u. { ( 0 - 1 ) , 0 } ) = ( ( 0..^ ( (♯ ` W ) - 1 ) ) u. { ( (♯ ` W ) - 1 ) , (♯ ` W ) } ). (Contributed by AV, 22-Sep-2018.) (Revised by AV, 26-Jan-2022.)
|- ( ( N e. ( ZZ>= ` 3 ) /\ (♯ ` W ) = ( N - 2 ) ) -> ( 0..^ ( ( (♯ ` W ) + 2 ) - 1 ) ) = ( ( 0..^ ( (♯ ` W ) - 1 ) ) u. { ( (♯ ` W ) - 1 ) , (♯ ` W ) } ) )
Theorem	clwwlknonex2lem2 16850*	Lemma 2 for clwwlknonex2 16851: Transformation of a walk and two edges into a walk extended by two vertices/edges. (Contributed by AV, 22-Sep-2018.) (Revised by AV, 27-Jan-2022.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   =>    |- ( ( ( ( X e. V /\ Y e. V /\ N e. ( ZZ>= ` 3 ) ) /\ ( ( W e. Word V /\ A. i e. ( 0..^ ( (♯ ` W ) - 1 ) ) { ( W ` i ) , ( W ` ( i + 1 ) ) } e. E /\ { (lastS ` W ) , ( W ` 0 ) } e. E ) /\ (♯ ` W ) = ( N - 2 ) /\ ( W ` 0 ) = X ) ) /\ { X , Y } e. E ) -> A. i e. ( ( 0..^ ( (♯ ` W ) - 1 ) ) u. { ( (♯ ` W ) - 1 ) , (♯ ` W ) } ) { ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` i ) , ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` ( i + 1 ) ) } e. E )
Theorem	clwwlknonex2 16851	Extending a closed walk W on vertex X by an additional edge (forth and back) results in a closed walk. (Contributed by AV, 22-Sep-2018.) (Revised by AV, 25-Feb-2022.) (Proof shortened by AV, 28-Mar-2022.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   =>    |- ( ( ( X e. V /\ Y e. V /\ N e. ( ZZ>= ` 3 ) ) /\ { X , Y } e. E /\ W e. ( X (ClWWalksNOn ` G ) ( N - 2 ) ) ) -> ( ( W ++ <" X "> ) ++ <" Y "> ) e. ( N ClWWalksN G ) )
Theorem	clwwlknonex2e 16852	Extending a closed walk W on vertex X by an additional edge (forth and back) results in a closed walk on vertex X. (Contributed by AV, 17-Apr-2022.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   =>    |- ( ( ( X e. V /\ Y e. V /\ N e. ( ZZ>= ` 3 ) ) /\ { X , Y } e. E /\ W e. ( X (ClWWalksNOn ` G ) ( N - 2 ) ) ) -> ( ( W ++ <" X "> ) ++ <" Y "> ) e. ( X (ClWWalksNOn ` G ) N ) )
Theorem	clwwlknun 16853*	The set of closed walks of fixed length N in a simple graph G is the union of the closed walks of the fixed length N on each of the vertices of graph G. (Contributed by Alexander van der Vekens, 7-Oct-2018.) (Revised by AV, 28-May-2021.) (Revised by AV, 3-Mar-2022.) (Proof shortened by AV, 28-Mar-2022.)
|- V = (Vtx ` G )   =>    |- ( G e. USGraph -> ( N ClWWalksN G ) = U_ x e. V ( x (ClWWalksNOn ` G ) N ) )
12.4  Eulerian paths and the Konigsberg Bridge problem
12.4.1  Eulerian paths According to Wikipedia ("Eulerian path", 9-Mar-2021, https://en.wikipedia.org/wiki/Eulerian_path): "In graph theory, an Eulerian trail (or Eulerian path) is a trail in a finite graph that visits every edge exactly once (allowing for revisiting vertices). Similarly, an Eulerian circuit or Eulerian cycle is an Eulerian trail that starts and ends on the same vertex. ... The term Eulerian graph has two common meanings in graph theory. One meaning is a graph with an Eulerian circuit, and the other is a graph with every vertex of even degree. These definitions coincide for connected graphs. ... A graph that has an Eulerian trail but not an Eulerian circuit is called semi-Eulerian."
Syntax	ceupth 16854	Extend class notation with Eulerian paths.
class EulerPaths
Definition	df-eupth 16855*	Define the set of all Eulerian paths on an arbitrary graph. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by AV, 18-Feb-2021.)
|- EulerPaths = ( g e. _V |-> { <. f , p >. | ( f (Trails ` g ) p /\ f : ( 0..^ (♯ ` f ) ) -onto-> dom (iEdg ` g ) ) } )
Theorem	releupth 16856	The set (EulerPaths ` G ) of all Eulerian paths on G is a set of pairs by our definition of an Eulerian path, and so is a relation. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by AV, 18-Feb-2021.)
|- Rel (EulerPaths ` G )
Theorem	eupthsg 16857*	The Eulerian paths on the graph G. (Contributed by AV, 18-Feb-2021.) (Revised by AV, 29-Oct-2021.)
|- I = (iEdg ` G )   =>    |- ( G e. V -> (EulerPaths ` G ) = { <. f , p >. | ( f (Trails ` G ) p /\ f : ( 0..^ (♯ ` f ) ) -onto-> dom I ) } )
Theorem	eupthv 16858	The classes involved in a Eulerian path are sets. (Contributed by Jim Kingdon, 13-Mar-2026.)
|- ( F (EulerPaths ` G ) P -> ( G e. _V /\ F e. _V /\ P e. _V ) )
Theorem	iseupth 16859	The property " <. F , P >. is an Eulerian path on the graph G". An Eulerian path is defined as bijection F from the edges to a set 0 ... ( N - 1 ) and a function P : ( 0 ... N ) --> V into the vertices such that for each 0 <_ k < N, F ( k ) is an edge from P ( k ) to P ( k + 1 ). (Since the edges are undirected and there are possibly many edges between any two given vertices, we need to list both the edges and the vertices of the path separately.) (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Mario Carneiro, 3-May-2015.) (Revised by AV, 18-Feb-2021.) (Revised by AV, 30-Oct-2021.)
|- I = (iEdg ` G )   =>    |- ( F (EulerPaths ` G ) P <-> ( F (Trails ` G ) P /\ F : ( 0..^ (♯ ` F ) ) -onto-> dom I ) )
Theorem	iseupthf1o 16860	The property " <. F , P >. is an Eulerian path on the graph G". An Eulerian path is defined as bijection F from the edges to a set 0 ... ( N - 1 ) and a function P : ( 0 ... N ) --> V into the vertices such that for each 0 <_ k < N, F ( k ) is an edge from P ( k ) to P ( k + 1 ). (Since the edges are undirected and there are possibly many edges between any two given vertices, we need to list both the edges and the vertices of the path separately.) (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Mario Carneiro, 3-May-2015.) (Revised by AV, 18-Feb-2021.) (Revised by AV, 30-Oct-2021.)
|- I = (iEdg ` G )   =>    |- ( F (EulerPaths ` G ) P <-> ( F (Walks ` G ) P /\ F : ( 0..^ (♯ ` F ) ) -1-1-onto-> dom I ) )
Theorem	eupthi 16861	Properties of an Eulerian path. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by AV, 18-Feb-2021.) (Proof shortened by AV, 30-Oct-2021.)
|- I = (iEdg ` G )   =>    |- ( F (EulerPaths ` G ) P -> ( F (Walks ` G ) P /\ F : ( 0..^ (♯ ` F ) ) -1-1-onto-> dom I ) )
Theorem	eupthf1o 16862	The F function in an Eulerian path is a bijection from a half-open range of nonnegative integers to the set of edges. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by AV, 18-Feb-2021.)
|- I = (iEdg ` G )   =>    |- ( F (EulerPaths ` G ) P -> F : ( 0..^ (♯ ` F ) ) -1-1-onto-> dom I )
Theorem	eupthfi 16863	Any graph with an Eulerian path is of finite size, i.e. with a finite number of edges. (Contributed by Mario Carneiro, 7-Apr-2015.) (Revised by AV, 18-Feb-2021.)
|- I = (iEdg ` G )   =>    |- ( F (EulerPaths ` G ) P -> dom I e. Fin )
Theorem	eupthseg 16864	The N-th edge in an eulerian path is the edge having P ( N ) and P ( N + 1 ) as endpoints . (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by AV, 18-Feb-2021.)
|- I = (iEdg ` G )   =>    |- ( ( F (EulerPaths ` G ) P /\ N e. ( 0..^ (♯ ` F ) ) ) -> { ( P ` N ) , ( P ` ( N + 1 ) ) } C_ ( I ` ( F ` N ) ) )
Theorem	eupthcl 16865	An Eulerian path has length ♯ ( F ), which is an integer. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by AV, 18-Feb-2021.)
|- ( F (EulerPaths ` G ) P -> (♯ ` F ) e. NN0 )
Theorem	eupthistrl 16866	An Eulerian path is a trail. (Contributed by Alexander van der Vekens, 24-Nov-2017.) (Revised by AV, 18-Feb-2021.)
|- ( F (EulerPaths ` G ) P -> F (Trails ` G ) P )
Theorem	eupthiswlk 16867	An Eulerian path is a walk. (Contributed by AV, 6-Apr-2021.)
|- ( F (EulerPaths ` G ) P -> F (Walks ` G ) P )
Theorem	eupthpf 16868	The P function in an Eulerian path is a function from a finite sequence of nonnegative integers to the vertices. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by AV, 18-Feb-2021.)
|- ( F (EulerPaths ` G ) P -> P : ( 0 ... (♯ ` F ) ) --> (Vtx ` G ) )
Theorem	eupthres 16869	The restriction <. H , Q >. of an Eulerian path <. F , P >. to an initial segment of the path (of length N) forms an Eulerian path on the subgraph S consisting of the edges in the initial segment. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Mario Carneiro, 3-May-2015.) (Revised by AV, 6-Mar-2021.) Hypothesis revised using the prefix operation. (Revised by AV, 30-Nov-2022.)
|- V = (Vtx ` G )   &    |- I = (iEdg ` G )   &    |- ( ph -> F (EulerPaths ` G ) P )   &    |- ( ph -> N e. ( 0..^ (♯ ` F ) ) )   &    |- ( ph -> (iEdg ` S ) = ( I |` ( F " ( 0..^ N ) ) ) )   &    |- H = ( F prefix N )   &    |- Q = ( P |` ( 0 ... N ) )   &    |- (Vtx ` S ) = V   =>    |- ( ph -> H (EulerPaths ` S ) Q )
Theorem	eupth2lem1 16870	Lemma for eupth2 . (Contributed by Mario Carneiro, 8-Apr-2015.)
|- ( U e. V -> ( U e. if ( A = B , (/) , { A , B } ) <-> ( A =/= B /\ ( U = A \/ U = B ) ) ) )
Theorem	eupth2lem2dc 16871	Lemma for eupth2 . (Contributed by Mario Carneiro, 8-Apr-2015.)
|- ( ph -> B e. X )   &    |- ( ph -> DECID A = B )   &    |- ( ph -> B =/= C )   &    |- ( ph -> B = U )   =>    |- ( ph -> ( -. U e. if ( A = B , (/) , { A , B } ) <-> U e. if ( A = C , (/) , { A , C } ) ) )
Theorem	trlsegvdeglem1 16872	Lemma for trlsegvdeg . (Contributed by AV, 20-Feb-2021.)
|- V = (Vtx ` G )   &    |- I = (iEdg ` G )   &    |- ( ph -> Fun I )   &    |- ( ph -> N e. ( 0..^ (♯ ` F ) ) )   &    |- ( ph -> U e. V )   &    |- ( ph -> F (Trails ` G ) P )   =>    |- ( ph -> ( ( P ` N ) e. V /\ ( P ` ( N + 1 ) ) e. V ) )
Theorem	trlsegvdeglem2 16873	Lemma for trlsegvdeg . (Contributed by AV, 20-Feb-2021.)
|- V = (Vtx ` G )   &    |- I = (iEdg ` G )   &    |- ( ph -> Fun I )   &    |- ( ph -> N e. ( 0..^ (♯ ` F ) ) )   &    |- ( ph -> U e. V )   &    |- ( ph -> F (Trails ` G ) P )   &    |- ( ph -> (Vtx ` X ) = V )   &    |- ( ph -> (Vtx ` Y ) = V )   &    |- ( ph -> (Vtx ` Z ) = V )   &    |- ( ph -> (iEdg ` X ) = ( I |` ( F " ( 0..^ N ) ) ) )   &    |- ( ph -> (iEdg ` Y ) = { <. ( F ` N ) , ( I ` ( F ` N ) ) >. } )   &    |- ( ph -> (iEdg ` Z ) = ( I |` ( F " ( 0 ... N ) ) ) )   =>    |- ( ph -> Fun (iEdg ` X ) )
Theorem	trlsegvdeglem3 16874	Lemma for trlsegvdeg . (Contributed by AV, 20-Feb-2021.)
|- V = (Vtx ` G )   &    |- I = (iEdg ` G )   &    |- ( ph -> Fun I )   &    |- ( ph -> N e. ( 0..^ (♯ ` F ) ) )   &    |- ( ph -> U e. V )   &    |- ( ph -> F (Trails ` G ) P )   &    |- ( ph -> (Vtx ` X ) = V )   &    |- ( ph -> (Vtx ` Y ) = V )   &    |- ( ph -> (Vtx ` Z ) = V )   &    |- ( ph -> (iEdg ` X ) = ( I |` ( F " ( 0..^ N ) ) ) )   &    |- ( ph -> (iEdg ` Y ) = { <. ( F ` N ) , ( I ` ( F ` N ) ) >. } )   &    |- ( ph -> (iEdg ` Z ) = ( I |` ( F " ( 0 ... N ) ) ) )   =>    |- ( ph -> Fun (iEdg ` Y ) )
Theorem	trlsegvdeglem4 16875	Lemma for trlsegvdeg . (Contributed by AV, 21-Feb-2021.)
|- V = (Vtx ` G )   &    |- I = (iEdg ` G )   &    |- ( ph -> Fun I )   &    |- ( ph -> N e. ( 0..^ (♯ ` F ) ) )   &    |- ( ph -> U e. V )   &    |- ( ph -> F (Trails ` G ) P )   &    |- ( ph -> (Vtx ` X ) = V )   &    |- ( ph -> (Vtx ` Y ) = V )   &    |- ( ph -> (Vtx ` Z ) = V )   &    |- ( ph -> (iEdg ` X ) = ( I |` ( F " ( 0..^ N ) ) ) )   &    |- ( ph -> (iEdg ` Y ) = { <. ( F ` N ) , ( I ` ( F ` N ) ) >. } )   &    |- ( ph -> (iEdg ` Z ) = ( I |` ( F " ( 0 ... N ) ) ) )   =>    |- ( ph -> dom (iEdg ` X ) = ( ( F " ( 0..^ N ) ) i^i dom I ) )
Theorem	trlsegvdeglem5 16876	Lemma for trlsegvdeg . (Contributed by AV, 21-Feb-2021.)
|- V = (Vtx ` G )   &    |- I = (iEdg ` G )   &    |- ( ph -> Fun I )   &    |- ( ph -> N e. ( 0..^ (♯ ` F ) ) )   &    |- ( ph -> U e. V )   &    |- ( ph -> F (Trails ` G ) P )   &    |- ( ph -> (Vtx ` X ) = V )   &    |- ( ph -> (Vtx ` Y ) = V )   &    |- ( ph -> (Vtx ` Z ) = V )   &    |- ( ph -> (iEdg ` X ) = ( I |` ( F " ( 0..^ N ) ) ) )   &    |- ( ph -> (iEdg ` Y ) = { <. ( F ` N ) , ( I ` ( F ` N ) ) >. } )   &    |- ( ph -> (iEdg ` Z ) = ( I |` ( F " ( 0 ... N ) ) ) )   =>    |- ( ph -> dom (iEdg ` Y ) = { ( F ` N ) } )
Theorem	trlsegvdeglem6 16877	Lemma for trlsegvdeg . (Contributed by AV, 21-Feb-2021.)
|- V = (Vtx ` G )   &    |- I = (iEdg ` G )   &    |- ( ph -> Fun I )   &    |- ( ph -> N e. ( 0..^ (♯ ` F ) ) )   &    |- ( ph -> U e. V )   &    |- ( ph -> F (Trails ` G ) P )   &    |- ( ph -> (Vtx ` X ) = V )   &    |- ( ph -> (Vtx ` Y ) = V )   &    |- ( ph -> (Vtx ` Z ) = V )   &    |- ( ph -> (iEdg ` X ) = ( I |` ( F " ( 0..^ N ) ) ) )   &    |- ( ph -> (iEdg ` Y ) = { <. ( F ` N ) , ( I ` ( F ` N ) ) >. } )   &    |- ( ph -> (iEdg ` Z ) = ( I |` ( F " ( 0 ... N ) ) ) )   =>    |- ( ph -> dom (iEdg ` X ) e. Fin )
Theorem	trlsegvdeglem7 16878	Lemma for trlsegvdeg . (Contributed by AV, 21-Feb-2021.)
|- V = (Vtx ` G )   &    |- I = (iEdg ` G )   &    |- ( ph -> Fun I )   &    |- ( ph -> N e. ( 0..^ (♯ ` F ) ) )   &    |- ( ph -> U e. V )   &    |- ( ph -> F (Trails ` G ) P )   &    |- ( ph -> (Vtx ` X ) = V )   &    |- ( ph -> (Vtx ` Y ) = V )   &    |- ( ph -> (Vtx ` Z ) = V )   &    |- ( ph -> (iEdg ` X ) = ( I |` ( F " ( 0..^ N ) ) ) )   &    |- ( ph -> (iEdg ` Y ) = { <. ( F ` N ) , ( I ` ( F ` N ) ) >. } )   &    |- ( ph -> (iEdg ` Z ) = ( I |` ( F " ( 0 ... N ) ) ) )   =>    |- ( ph -> dom (iEdg ` Y ) e. Fin )
Theorem	trlsegvdegfi 16879	The effect on vertex degree of adding one edge to a trail. In the following, a subgraph induced by a segment of a trail is called a "subtrail": For any subtrail Z of a trail <. F , P >. in a pseudograph G which is composed of subtrails X and Y, where Y consists of a single edge, the vertex degree of any vertex U within Z is the sum of the vertex degree of U within X and the vertex degree of U within Y. Note that this theorem would not hold for arbitrary walks (if the last edge was identical with a previous edge, the degree of the vertices incident with this edge would not be increased because of this edge). (Contributed by Mario Carneiro, 8-Apr-2015.) (Revised by AV, 20-Feb-2021.)
|- V = (Vtx ` G )   &    |- I = (iEdg ` G )   &    |- ( ph -> Fun I )   &    |- ( ph -> N e. ( 0..^ (♯ ` F ) ) )   &    |- ( ph -> U e. V )   &    |- ( ph -> F (Trails ` G ) P )   &    |- ( ph -> (Vtx ` X ) = V )   &    |- ( ph -> (Vtx ` Y ) = V )   &    |- ( ph -> (Vtx ` Z ) = V )   &    |- ( ph -> (iEdg ` X ) = ( I |` ( F " ( 0..^ N ) ) ) )   &    |- ( ph -> (iEdg ` Y ) = { <. ( F ` N ) , ( I ` ( F ` N ) ) >. } )   &    |- ( ph -> (iEdg ` Z ) = ( I |` ( F " ( 0 ... N ) ) ) )   &    |- ( ph -> G e. UPGraph )   &    |- ( ph -> V e. Fin )   =>    |- ( ph -> ( (VtxDeg ` Z ) ` U ) = ( ( (VtxDeg ` X ) ` U ) + ( (VtxDeg ` Y ) ` U ) ) )
Theorem	eupth2lem3lem1fi 16880	Lemma for eupth2lem3fi 16888. (Contributed by AV, 21-Feb-2021.)
|- V = (Vtx ` G )   &    |- I = (iEdg ` G )   &    |- ( ph -> Fun I )   &    |- ( ph -> N e. ( 0..^ (♯ ` F ) ) )   &    |- ( ph -> U e. V )   &    |- ( ph -> F (Trails ` G ) P )   &    |- ( ph -> (Vtx ` X ) = V )   &    |- ( ph -> (Vtx ` Y ) = V )   &    |- ( ph -> (Vtx ` Z ) = V )   &    |- ( ph -> (iEdg ` X ) = ( I |` ( F " ( 0..^ N ) ) ) )   &    |- ( ph -> (iEdg ` Y ) = { <. ( F ` N ) , ( I ` ( F ` N ) ) >. } )   &    |- ( ph -> (iEdg ` Z ) = ( I |` ( F " ( 0 ... N ) ) ) )   &    |- ( ph -> G e. UPGraph )   &    |- ( ph -> V e. Fin )   =>    |- ( ph -> ( (VtxDeg ` X ) ` U ) e. NN0 )
Theorem	eupth2lem3lem2fi 16881	Lemma for eupth2lem3fi 16888. (Contributed by AV, 21-Feb-2021.)
|- V = (Vtx ` G )   &    |- I = (iEdg ` G )   &    |- ( ph -> Fun I )   &    |- ( ph -> N e. ( 0..^ (♯ ` F ) ) )   &    |- ( ph -> U e. V )   &    |- ( ph -> F (Trails ` G ) P )   &    |- ( ph -> (Vtx ` X ) = V )   &    |- ( ph -> (Vtx ` Y ) = V )   &    |- ( ph -> (Vtx ` Z ) = V )   &    |- ( ph -> (iEdg ` X ) = ( I |` ( F " ( 0..^ N ) ) ) )   &    |- ( ph -> (iEdg ` Y ) = { <. ( F ` N ) , ( I ` ( F ` N ) ) >. } )   &    |- ( ph -> (iEdg ` Z ) = ( I |` ( F " ( 0 ... N ) ) ) )   &    |- ( ph -> G e. UPGraph )   &    |- ( ph -> V e. Fin )   =>    |- ( ph -> ( (VtxDeg ` Y ) ` U ) e. NN0 )
Theorem	eupth2lem3lem3fi 16882*	Lemma for eupth2lem3fi 16888. If a loop { ( P ` N ) , ( P ` ( N + 1 ) ) } is added to a trail, the degree of the vertices with odd degree remains odd (regarding the subgraphs induced by the involved trails). (Contributed by Mario Carneiro, 8-Apr-2015.) (Revised by AV, 21-Feb-2021.)
|- V = (Vtx ` G )   &    |- I = (iEdg ` G )   &    |- ( ph -> Fun I )   &    |- ( ph -> N e. ( 0..^ (♯ ` F ) ) )   &    |- ( ph -> U e. V )   &    |- ( ph -> F (Trails ` G ) P )   &    |- ( ph -> (Vtx ` X ) = V )   &    |- ( ph -> (Vtx ` Y ) = V )   &    |- ( ph -> (Vtx ` Z ) = V )   &    |- ( ph -> (iEdg ` X ) = ( I |` ( F " ( 0..^ N ) ) ) )   &    |- ( ph -> (iEdg ` Y ) = { <. ( F ` N ) , ( I ` ( F ` N ) ) >. } )   &    |- ( ph -> (iEdg ` Z ) = ( I |` ( F " ( 0 ... N ) ) ) )   &    |- ( ph -> G e. UPGraph )   &    |- ( ph -> V e. Fin )   &    |- ( ph -> { x e. V | -. 2 || ( (VtxDeg ` X ) ` x ) } = if ( ( P ` 0 ) = ( P ` N ) , (/) , { ( P ` 0 ) , ( P ` N ) } ) )   &    |- ( ph -> if- ( ( P ` N ) = ( P ` ( N + 1 ) ) , ( I ` ( F ` N ) ) = { ( P ` N ) } , { ( P ` N ) , ( P ` ( N + 1 ) ) } C_ ( I ` ( F ` N ) ) ) )   =>    |- ( ( ph /\ ( P ` N ) = ( P ` ( N + 1 ) ) ) -> ( -. 2 || ( ( (VtxDeg ` X ) ` U ) + ( (VtxDeg ` Y ) ` U ) ) <-> U e. if ( ( P ` 0 ) = ( P ` ( N + 1 ) ) , (/) , { ( P ` 0 ) , ( P ` ( N + 1 ) ) } ) ) )
Theorem	eupth2lem3lem6fi 16883*	If an edge (not a loop) is added to a trail, the degree of vertices not being end vertices of this edge remains odd if it was odd before (regarding the subgraphs induced by the involved trails). Remark: This seems to be not valid for hyperedges joining more vertices than ( P ` 0 ) and ( P ` N ): if there is a third vertex in the edge, and this vertex is already contained in the trail, then the degree of this vertex could be affected by this edge! (Contributed by Mario Carneiro, 8-Apr-2015.) (Revised by AV, 25-Feb-2021.)
|- V = (Vtx ` G )   &    |- I = (iEdg ` G )   &    |- ( ph -> Fun I )   &    |- ( ph -> N e. ( 0..^ (♯ ` F ) ) )   &    |- ( ph -> U e. V )   &    |- ( ph -> F (Trails ` G ) P )   &    |- ( ph -> (Vtx ` X ) = V )   &    |- ( ph -> (Vtx ` Y ) = V )   &    |- ( ph -> (Vtx ` Z ) = V )   &    |- ( ph -> (iEdg ` X ) = ( I |` ( F " ( 0..^ N ) ) ) )   &    |- ( ph -> (iEdg ` Y ) = { <. ( F ` N ) , ( I ` ( F ` N ) ) >. } )   &    |- ( ph -> (iEdg ` Z ) = ( I |` ( F " ( 0 ... N ) ) ) )   &    |- ( ph -> G e. UPGraph )   &    |- ( ph -> V e. Fin )   &    |- ( ph -> { x e. V | -. 2 || ( (VtxDeg ` X ) ` x ) } = if ( ( P ` 0 ) = ( P ` N ) , (/) , { ( P ` 0 ) , ( P ` N ) } ) )   &    |- ( ph -> ( I ` ( F ` N ) ) = { ( P ` N ) , ( P ` ( N + 1 ) ) } )   =>    |- ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) /\ ( U =/= ( P ` N ) /\ U =/= ( P ` ( N + 1 ) ) ) ) -> ( -. 2 || ( ( (VtxDeg ` X ) ` U ) + ( (VtxDeg ` Y ) ` U ) ) <-> U e. if ( ( P ` 0 ) = ( P ` ( N + 1 ) ) , (/) , { ( P ` 0 ) , ( P ` ( N + 1 ) ) } ) ) )
Theorem	eupth2lem3lem5 16884	Lemma for eupth2fi 16891. (Contributed by AV, 25-Feb-2021.)
|- V = (Vtx ` G )   &    |- I = (iEdg ` G )   &    |- ( ph -> Fun I )   &    |- ( ph -> N e. ( 0..^ (♯ ` F ) ) )   &    |- ( ph -> U e. V )   &    |- ( ph -> F (Trails ` G ) P )   &    |- ( ph -> (Vtx ` X ) = V )   &    |- ( ph -> (Vtx ` Y ) = V )   &    |- ( ph -> (Vtx ` Z ) = V )   &    |- ( ph -> (iEdg ` X ) = ( I |` ( F " ( 0..^ N ) ) ) )   &    |- ( ph -> (iEdg ` Y ) = { <. ( F ` N ) , ( I ` ( F ` N ) ) >. } )   &    |- ( ph -> (iEdg ` Z ) = ( I |` ( F " ( 0 ... N ) ) ) )   &    |- ( ph -> { x e. V | -. 2 || ( (VtxDeg ` X ) ` x ) } = if ( ( P ` 0 ) = ( P ` N ) , (/) , { ( P ` 0 ) , ( P ` N ) } ) )   &    |- ( ph -> ( I ` ( F ` N ) ) = { ( P ` N ) , ( P ` ( N + 1 ) ) } )   =>    |- ( ph -> ( I ` ( F ` N ) ) e. ~P V )
Theorem	eupth2lem3lem4fi 16885*	Lemma for eupth2lem3fi 16888. If an edge (not a loop) is added to a trail, the degree of the end vertices of this edge remains odd if it was odd before (regarding the subgraphs induced by the involved trails). (Contributed by Mario Carneiro, 8-Apr-2015.) (Revised by AV, 25-Feb-2021.)
|- V = (Vtx ` G )   &    |- I = (iEdg ` G )   &    |- ( ph -> Fun I )   &    |- ( ph -> N e. ( 0..^ (♯ ` F ) ) )   &    |- ( ph -> U e. V )   &    |- ( ph -> F (Trails ` G ) P )   &    |- ( ph -> (Vtx ` X ) = V )   &    |- ( ph -> (Vtx ` Y ) = V )   &    |- ( ph -> (Vtx ` Z ) = V )   &    |- ( ph -> (iEdg ` X ) = ( I |` ( F " ( 0..^ N ) ) ) )   &    |- ( ph -> (iEdg ` Y ) = { <. ( F ` N ) , ( I ` ( F ` N ) ) >. } )   &    |- ( ph -> (iEdg ` Z ) = ( I |` ( F " ( 0 ... N ) ) ) )   &    |- ( ph -> G e. UMGraph )   &    |- ( ph -> V e. Fin )   &    |- ( ph -> { x e. V | -. 2 || ( (VtxDeg ` X ) ` x ) } = if ( ( P ` 0 ) = ( P ` N ) , (/) , { ( P ` 0 ) , ( P ` N ) } ) )   &    |- ( ph -> if- ( ( P ` N ) = ( P ` ( N + 1 ) ) , ( I ` ( F ` N ) ) = { ( P ` N ) } , { ( P ` N ) , ( P ` ( N + 1 ) ) } C_ ( I ` ( F ` N ) ) ) )   &    |- ( ph -> ( I ` ( F ` N ) ) e. ~P V )   =>    |- ( ( ph /\ ( P ` N ) =/= ( P ` ( N + 1 ) ) /\ ( U = ( P ` N ) \/ U = ( P ` ( N + 1 ) ) ) ) -> ( -. 2 || ( ( (VtxDeg ` X ) ` U ) + ( (VtxDeg ` Y ) ` U ) ) <-> U e. if ( ( P ` 0 ) = ( P ` ( N + 1 ) ) , (/) , { ( P ` 0 ) , ( P ` ( N + 1 ) ) } ) ) )
Theorem	eupth2lem3lem7fi 16886*	Lemma for eupth2lem3fi 16888: Combining trlsegvdegfi 16879, eupth2lem3lem3fi 16882, eupth2lem3lem4fi 16885 and eupth2lem3lem6fi 16883. (Contributed by Mario Carneiro, 8-Apr-2015.) (Revised by AV, 27-Feb-2021.)
|- V = (Vtx ` G )   &    |- I = (iEdg ` G )   &    |- ( ph -> Fun I )   &    |- ( ph -> N e. ( 0..^ (♯ ` F ) ) )   &    |- ( ph -> U e. V )   &    |- ( ph -> F (Trails ` G ) P )   &    |- ( ph -> (Vtx ` X ) = V )   &    |- ( ph -> (Vtx ` Y ) = V )   &    |- ( ph -> (Vtx ` Z ) = V )   &    |- ( ph -> (iEdg ` X ) = ( I |` ( F " ( 0..^ N ) ) ) )   &    |- ( ph -> (iEdg ` Y ) = { <. ( F ` N ) , ( I ` ( F ` N ) ) >. } )   &    |- ( ph -> (iEdg ` Z ) = ( I |` ( F " ( 0 ... N ) ) ) )   &    |- ( ph -> G e. UMGraph )   &    |- ( ph -> V e. Fin )   &    |- ( ph -> { x e. V | -. 2 || ( (VtxDeg ` X ) ` x ) } = if ( ( P ` 0 ) = ( P ` N ) , (/) , { ( P ` 0 ) , ( P ` N ) } ) )   &    |- ( ph -> ( I ` ( F ` N ) ) = { ( P ` N ) , ( P ` ( N + 1 ) ) } )   =>    |- ( ph -> ( -. 2 || ( (VtxDeg ` Z ) ` U ) <-> U e. if ( ( P ` 0 ) = ( P ` ( N + 1 ) ) , (/) , { ( P ` 0 ) , ( P ` ( N + 1 ) ) } ) ) )
Theorem	eupthvdres 16887	The vertex degree remains the same for all vertices if the edges are restricted to the edges of an Eulerian path. (Contributed by Mario Carneiro, 8-Apr-2015.) (Revised by AV, 26-Feb-2021.)
|- V = (Vtx ` G )   &    |- I = (iEdg ` G )   &    |- ( ph -> G e. W )   &    |- ( ph -> Fun I )   &    |- ( ph -> F (EulerPaths ` G ) P )   &    |- H = <. V , ( I |` ( F " ( 0..^ (♯ ` F ) ) ) ) >.   =>    |- ( ph -> (VtxDeg ` H ) = (VtxDeg ` G ) )
Theorem	eupth2lem3fi 16888*	Lemma for eupth2fi 16891. (Contributed by Mario Carneiro, 8-Apr-2015.) (Revised by AV, 26-Feb-2021.)
|- V = (Vtx ` G )   &    |- I = (iEdg ` G )   &    |- ( ph -> G e. UMGraph )   &    |- ( ph -> Fun I )   &    |- ( ph -> F (EulerPaths ` G ) P )   &    |- ( ph -> V e. Fin )   &    |- H = <. V , ( I |` ( F " ( 0..^ N ) ) ) >.   &    |- X = <. V , ( I |` ( F " ( 0..^ ( N + 1 ) ) ) ) >.   &    |- ( ph -> N e. NN0 )   &    |- ( ph -> ( N + 1 ) <_ (♯ ` F ) )   &    |- ( ph -> U e. V )   &    |- ( ph -> { x e. V | -. 2 || ( (VtxDeg ` H ) ` x ) } = if ( ( P ` 0 ) = ( P ` N ) , (/) , { ( P ` 0 ) , ( P ` N ) } ) )   =>    |- ( ph -> ( -. 2 || ( (VtxDeg ` X ) ` U ) <-> U e. if ( ( P ` 0 ) = ( P ` ( N + 1 ) ) , (/) , { ( P ` 0 ) , ( P ` ( N + 1 ) ) } ) ) )
Theorem	eupth2lembfi 16889*	Lemma for eupth2fi 16891 (induction basis): There are no vertices of odd degree in an Eulerian path of length 0, having no edge and identical endpoints (the single vertex of the Eulerian path). (Contributed by Mario Carneiro, 8-Apr-2015.) (Revised by AV, 26-Feb-2021.)
|- V = (Vtx ` G )   &    |- I = (iEdg ` G )   &    |- ( ph -> G e. UMGraph )   &    |- ( ph -> Fun I )   &    |- ( ph -> F (EulerPaths ` G ) P )   &    |- ( ph -> V e. Fin )   =>    |- ( ph -> { x e. V | -. 2 || ( (VtxDeg ` <. V , ( I |` ( F " ( 0..^ 0 ) ) ) >. ) ` x ) } = (/) )
Theorem	eupth2lemsfi 16890*	Lemma for eupth2fi 16891 (induction step): The only vertices of odd degree in a graph with an Eulerian path are the endpoints, and then only if the endpoints are distinct, if the Eulerian path shortened by one edge has this property. (Contributed by Mario Carneiro, 8-Apr-2015.) (Revised by AV, 26-Feb-2021.)
|- V = (Vtx ` G )   &    |- I = (iEdg ` G )   &    |- ( ph -> G e. UMGraph )   &    |- ( ph -> Fun I )   &    |- ( ph -> F (EulerPaths ` G ) P )   &    |- ( ph -> V e. Fin )   =>    |- ( ( ph /\ n e. NN0 ) -> ( ( n <_ (♯ ` F ) -> { x e. V | -. 2 || ( (VtxDeg ` <. V , ( I |` ( F " ( 0..^ n ) ) ) >. ) ` x ) } = if ( ( P ` 0 ) = ( P ` n ) , (/) , { ( P ` 0 ) , ( P ` n ) } ) ) -> ( ( n + 1 ) <_ (♯ ` F ) -> { x e. V | -. 2 || ( (VtxDeg ` <. V , ( I |` ( F " ( 0..^ ( n + 1 ) ) ) ) >. ) ` x ) } = if ( ( P ` 0 ) = ( P ` ( n + 1 ) ) , (/) , { ( P ` 0 ) , ( P ` ( n + 1 ) ) } ) ) ) )
Theorem	eupth2fi 16891*	The only vertices of odd degree in a graph with an Eulerian path are the endpoints, and then only if the endpoints are distinct. (Contributed by Mario Carneiro, 8-Apr-2015.) (Revised by AV, 26-Feb-2021.)
|- V = (Vtx ` G )   &    |- I = (iEdg ` G )   &    |- ( ph -> G e. UMGraph )   &    |- ( ph -> Fun I )   &    |- ( ph -> F (EulerPaths ` G ) P )   &    |- ( ph -> V e. Fin )   =>    |- ( ph -> { x e. V | -. 2 || ( (VtxDeg ` G ) ` x ) } = if ( ( P ` 0 ) = ( P ` (♯ ` F ) ) , (/) , { ( P ` 0 ) , ( P ` (♯ ` F ) ) } ) )
Theorem	eulerpathprum 16892*	A graph with an Eulerian path has either zero or two vertices of odd degree. (Contributed by Mario Carneiro, 7-Apr-2015.) (Revised by AV, 26-Feb-2021.)
|- V = (Vtx ` G )   =>    |- ( ( G e. UMGraph /\ F (EulerPaths ` G ) P /\ V e. Fin ) -> (♯ ` { x e. V | -. 2 || ( (VtxDeg ` G ) ` x ) } ) e. { 0 , 2 } )
Theorem	eulerpathum 16893*	A multigraph with an Eulerian path has either zero or two vertices of odd degree. (Contributed by Mario Carneiro, 7-Apr-2015.) (Revised by AV, 26-Feb-2021.)
|- V = (Vtx ` G )   =>    |- ( ( G e. UMGraph /\ E. j j e. (EulerPaths ` G ) /\ V e. Fin ) -> (♯ ` { x e. V | -. 2 || ( (VtxDeg ` G ) ` x ) } ) e. { 0 , 2 } )
12.4.2  The Königsberg Bridge problem According to Wikipedia ("Seven Bridges of Königsberg", 9-Mar-2021, https://en.wikipedia.org/wiki/Seven_Bridges_of_Koenigsberg): "The Seven Bridges of Königsberg is a historically notable problem in mathematics. Its negative resolution by Leonhard Euler in 1736 laid the foundations of graph theory and prefigured the idea of topology. The city of Königsberg in [East] Prussia (now Kaliningrad, Russia) was set on both sides of the Pregel River, and included two large islands - Kneiphof and Lomse - which were connected to each other, or to the two mainland portions of the city, by seven bridges. The problem was to devise a walk through the city that would cross each of those bridges once and only once.". Euler proved that the problem has no solution by applying Euler's theorem to the Königsberg graph, which is obtained by replacing each land mass with an abstract "vertex" or node, and each bridge with an abstract connection, an "edge", which connects two land masses/vertices. The Königsberg graph G is a multigraph consisting of 4 vertices and 7 edges, represented by the following ordered pair: G = <. ( 0 ... 3 ) , <" { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } { 2 , 3 } { 2 , 3 } "> >., see konigsbergumgr 16899. konigsberg 16905 shows that the Königsberg graph has no Eulerian path, thus the Königsberg Bridge problem has no solution.
Theorem	konigsbergvtx 16894	The set of vertices of the Königsberg graph G. (Contributed by AV, 28-Feb-2021.)
|- V = ( 0 ... 3 )   &    |- E = <" { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } { 2 , 3 } { 2 , 3 } ">   &    |- G = <. V , E >.   =>    |- (Vtx ` G ) = ( 0 ... 3 )
Theorem	konigsbergiedg 16895	The indexed edges of the Königsberg graph G. (Contributed by AV, 28-Feb-2021.)
|- V = ( 0 ... 3 )   &    |- E = <" { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } { 2 , 3 } { 2 , 3 } ">   &    |- G = <. V , E >.   =>    |- (iEdg ` G ) = <" { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } { 2 , 3 } { 2 , 3 } ">
Theorem	konigsbergiedgwen 16896*	The indexed edges of the Königsberg graph G is a word over the pairs of vertices. (Contributed by AV, 28-Feb-2021.)
|- V = ( 0 ... 3 )   &    |- E = <" { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } { 2 , 3 } { 2 , 3 } ">   &    |- G = <. V , E >.   =>    |- E e. Word { x e. ~P V | x ~~ 2o }
Theorem	konigsbergssiedgwpren 16897*	Each subset of the indexed edges of the Königsberg graph G is a word over the pairs of vertices. (Contributed by AV, 28-Feb-2021.)
|- V = ( 0 ... 3 )   &    |- E = <" { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } { 2 , 3 } { 2 , 3 } ">   &    |- G = <. V , E >.   =>    |- ( ( A e. Word _V /\ B e. Word _V /\ E = ( A ++ B ) ) -> A e. Word { x e. ~P V | x ~~ 2o } )
Theorem	konigsbergssiedgwen 16898*	Each subset of the indexed edges of the Königsberg graph G is a word over the pairs of vertices. (Contributed by AV, 28-Feb-2021.)
|- V = ( 0 ... 3 )   &    |- E = <" { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } { 2 , 3 } { 2 , 3 } ">   &    |- G = <. V , E >.   =>    |- ( ( A e. Word _V /\ B e. Word _V /\ E = ( A ++ B ) ) -> A e. Word { x e. ~P V | ( x ~~ 1o \/ x ~~ 2o ) } )
Theorem	konigsbergumgr 16899	The Königsberg graph G is a multigraph. (Contributed by AV, 28-Feb-2021.) (Revised by AV, 9-Mar-2021.)
|- V = ( 0 ... 3 )   &    |- E = <" { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } { 2 , 3 } { 2 , 3 } ">   &    |- G = <. V , E >.   =>    |- G e. UMGraph
Theorem	konigsberglem1 16900	Lemma 1 for konigsberg 16905: Vertex 0 has degree three. (Contributed by Mario Carneiro, 11-Mar-2015.) (Revised by Mario Carneiro, 28-Feb-2016.) (Revised by AV, 4-Mar-2021.)
|- V = ( 0 ... 3 )   &    |- E = <" { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } { 2 , 3 } { 2 , 3 } ">   &    |- G = <. V , E >.   =>    |- ( (VtxDeg ` G ) ` 0 ) = 3