P. 166 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 16501-16600   *Has distinct variable group(s)

Type	Label	Description
Statement
12.3.2  Trails
Syntax	ctrls 16501	Extend class notation with trails (within a graph).
class Trails
Definition	df-trls 16502*	Define the set of all Trails (in an undirected graph). According to Wikipedia ("Path (graph theory)", https://en.wikipedia.org/wiki/Path_(graph_theory), 3-Oct-2017): "A trail is a walk in which all edges are distinct. According to Bollobas: "... walk is called a trail if all its edges are distinct.", see Definition of [Bollobas] p. 5. Therefore, a trail can be represented by an injective mapping f from { 1 , ... , n } and a mapping p from { 0 , ... , n }, where f enumerates the (indices of the) different edges, and p enumerates the vertices. So the trail is also represented by the following sequence: p(0) e(f(1)) p(1) e(f(2)) ... p(n-1) e(f(n)) p(n). (Contributed by Alexander van der Vekens and Mario Carneiro, 4-Oct-2017.) (Revised by AV, 28-Dec-2020.)
|- Trails = ( g e. _V |-> { <. f , p >. | ( f (Walks ` g ) p /\ Fun `' f ) } )
Theorem	reltrls 16503	The set (Trails ` G ) of all trails on G is a set of pairs by our definition of a trail, and so is a relation. (Contributed by AV, 29-Oct-2021.)
|- Rel (Trails ` G )
Theorem	trlsfvalg 16504*	The set of trails (in an undirected graph). (Contributed by Alexander van der Vekens, 20-Oct-2017.) (Revised by AV, 28-Dec-2020.) (Revised by AV, 29-Oct-2021.)
|- ( G e. V -> (Trails ` G ) = { <. f , p >. | ( f (Walks ` G ) p /\ Fun `' f ) } )
Theorem	trlsv 16505	The classes involved in a trail are sets. (Contributed by Jim Kingdon, 7-Feb-2026.)
|- ( F (Trails ` G ) P -> ( G e. _V /\ F e. _V /\ P e. _V ) )
Theorem	istrl 16506	Conditions for a pair of classes/functions to be a trail (in an undirected graph). (Contributed by Alexander van der Vekens, 20-Oct-2017.) (Revised by AV, 28-Dec-2020.) (Revised by AV, 29-Oct-2021.)
|- ( F (Trails ` G ) P <-> ( F (Walks ` G ) P /\ Fun `' F ) )
Theorem	trliswlk 16507	A trail is a walk. (Contributed by Alexander van der Vekens, 20-Oct-2017.) (Revised by AV, 7-Jan-2021.) (Proof shortened by AV, 29-Oct-2021.)
|- ( F (Trails ` G ) P -> F (Walks ` G ) P )
Theorem	trlsex 16508	The class of trails on a graph is a set. (Contributed by Jim Kingdon, 14-Mar-2026.)
|- ( G e. V -> (Trails ` G ) e. _V )
Theorem	trlf1 16509	The enumeration F of a trail <. F , P >. is injective. (Contributed by AV, 20-Feb-2021.) (Proof shortened by AV, 29-Oct-2021.)
|- I = (iEdg ` G )   =>    |- ( F (Trails ` G ) P -> F : ( 0..^ (♯ ` F ) ) -1-1-> dom I )
Theorem	trlreslem 16510	Lemma for trlres 16511. (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 16511	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 16512	Extend class notation with closed walks (in an undirected graph) as word over the set of vertices.
class ClWWalks
Definition	df-clwwlk 16513*	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 16514*	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 16515*	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 16516	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 16517	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 16518	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 16519	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 16520	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 16521*	Lemma for clwwlkccat 16522: 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 16522	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 16523	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 16524	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 16525*	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 16529. (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 16526*	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 16527	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 16528	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 16529	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 16530	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 16531	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 16532	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 16533	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 16534	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 16535	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 16536	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 16537*	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 16538*	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 16539	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 16540	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 16541*	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 16542	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 16543	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 16544	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 16545	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 16546*	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 16547	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 16548*	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 16549*	(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 16550*	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 16551	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 16552	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 16553*	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 16554	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 16555*	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 16556*	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 16557	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 16558	Lemma 1 for clwwlknonex2 16560: 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 16559*	Lemma 2 for clwwlknonex2 16560: 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 16560	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 16561	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 16562*	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 16563	Extend class notation with Eulerian paths.
class EulerPaths
Definition	df-eupth 16564*	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 16565	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 16566*	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 16567	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 16568	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 16569	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 16570	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 16571	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 16572	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 16573	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 16574	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 16575	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 16576	An Eulerian path is a walk. (Contributed by AV, 6-Apr-2021.)
|- ( F (EulerPaths ` G ) P -> F (Walks ` G ) P )
Theorem	eupthpf 16577	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 16578	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 16579	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 16580	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 16581	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 16582	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 16583	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 16584	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 16585	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 16586	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 16587	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 16588	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 16589	Lemma for eupth2lem3fi 16597. (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 16590	Lemma for eupth2lem3fi 16597. (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 16591*	Lemma for eupth2lem3fi 16597. 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 16592*	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 16593	Lemma for eupth2fi 16600. (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 16594*	Lemma for eupth2lem3fi 16597. 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 16595*	Lemma for eupth2lem3fi 16597: Combining trlsegvdegfi 16588, eupth2lem3lem3fi 16591, eupth2lem3lem4fi 16594 and eupth2lem3lem6fi 16592. (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 16596	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 16597*	Lemma for eupth2fi 16600. (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 16598*	Lemma for eupth2fi 16600 (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 16599*	Lemma for eupth2fi 16600 (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 16600*	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 ) ) } ) )