P. 399 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 39801-39900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	umgr1wlknloop 39801*	In a multigraph, each walk has no loops! (Contributed by Alexander van der Vekens, 7-Nov-2017.) (Revised by AV, 3-Jan-2021.)
|- ( ( G e. UMGraph /\ F (1Walks ` G ) P ) -> A. k e. ( 0..^ ( # ` F ) ) ( P ` k ) =/= ( P ` ( k + 1 ) ) )
Theorem	wlkRes 39802*	Restrictions of walks (i.e. special kinds of walks, for example paths - see pthsfval 39851) are sets. (Contributed by Alexander van der Vekens, 1-Nov-2017.) (Revised by AV, 30-Dec-2020.) (Proof shortened by AV, 15-Jan-2021.)
|- ( f ( W ` G ) p -> f (1Walks ` G ) p )   =>    |- { <. f , p >. | ( f ( W ` G ) p /\ ph ) } e. _V
Theorem	wlkson 39803*	The set of walks between two vertices. (Contributed by Alexander van der Vekens, 12-Dec-2017.) (Revised by AV, 30-Dec-2020.) (Proof shortened by AV, 15-Jan-2021.)
|- V = (Vtx ` G )   =>    |- ( ( G e. W /\ A e. V /\ B e. V ) -> ( A (WalksOn ` G ) B ) = { <. f , p >. | ( f (1Walks ` G ) p /\ ( p ` 0 ) = A /\ ( p ` ( # ` f ) ) = B ) } )
Theorem	iswlkOn 39804	Properties of a pair of functions to be a walk between two given vertices (in an undirected graph). (Contributed by Alexander van der Vekens, 2-Nov-2017.) (Revised by AV, 31-Dec-2020.) (Proof shortened by AV, 31-Jan-2021.)
|- V = (Vtx ` G )   =>    |- ( ( ( G e. W /\ A e. V /\ B e. V ) /\ ( F e. U /\ P e. Z ) ) -> ( F ( A (WalksOn ` G ) B ) P <-> ( F (1Walks ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) ) )
Theorem	wlkOnprop 39805	Properties of a walk between two vertices. (Contributed by Alexander van der Vekens, 12-Dec-2017.) (Revised by AV, 31-Dec-2020.) (Proof shortened by AV, 16-Jan-2021.)
|- V = (Vtx ` G )   =>    |- ( F ( A (WalksOn ` G ) B ) P -> ( ( G e. _V /\ A e. V /\ B e. V ) /\ ( F e. _V /\ P e. _V ) /\ ( F (1Walks ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) ) )
Theorem	1wlkepvtx 39806	The endpoints of a walk are vertices. (Contributed by AV, 31-Jan-2021.)
|- V = (Vtx ` G )   =>    |- ( F (1Walks ` G ) P -> ( ( P ` 0 ) e. V /\ ( P ` ( # ` F ) ) e. V ) )
Theorem	wlkOniswlk 39807	A walk between two vertices is a walk. (Contributed by Alexander van der Vekens, 12-Dec-2017.) (Revised by AV, 2-Jan-2021.)
|- ( F ( A (WalksOn ` G ) B ) P -> F (1Walks ` G ) P )
Theorem	wlkOnwlk 39808	A walk is a walk between its endpoints. (Contributed by Alexander van der Vekens, 2-Nov-2017.) (Revised by AV, 2-Jan-2021.) (Proof shortened by AV, 31-Jan-2021.)
|- ( F (1Walks ` G ) P -> F ( ( P ` 0 ) (WalksOn ` G ) ( P ` ( # ` F ) ) ) P )
Theorem	wlkOnwlk1l 39809	A walk is a walk from its first vertex to its last vertex. (Contributed by AV, 7-Feb-2021.)
|- ( ph -> G e. W )   &    |- ( ph -> F (1Walks ` G ) P )   =>    |- ( ph -> F ( ( P ` 0 ) (WalksOn ` G ) ( lastS ` P ) ) P )
Theorem	2Wlklem 39810*	Lemma for upgr2wlk 39811 and 2wlklemA 25340. Identical with is2wlk 25351. (Contributed by Alexander van der Vekens, 1-Feb-2018.)
|- ( A. k e. { 0 , 1 } ( E ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } <-> ( ( E ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( E ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) )
Theorem	upgr2wlk 39811	Properties of a pair of functions to be a walk of length 2 in a pseudograph. Note that the vertices need not to be distinct and the edges can be loops or multiedges. (Contributed by Alexander van der Vekens, 16-Feb-2018.) (Revised by AV, 3-Jan-2021.)
|- V = (Vtx ` G )   &    |- I = (iEdg ` G )   =>    |- ( ( G e. UPGraph /\ ( F e. W /\ P e. Z ) ) -> ( ( F (1Walks ` G ) P /\ ( # ` F ) = 2 ) <-> ( F : ( 0..^ 2 ) --> dom I /\ P : ( 0 ... 2 ) --> V /\ ( ( I ` ( F ` 0 ) ) = { ( P ` 0 ) , ( P ` 1 ) } /\ ( I ` ( F ` 1 ) ) = { ( P ` 1 ) , ( P ` 2 ) } ) ) ) )
Theorem	red1wlklem 39812	Lemma for red1wlk 39813. (Contributed by Alexander van der Vekens, 1-Nov-2017.) (Revised by AV, 29-Jan-2021.)
|- ( ( F e. Word S /\ 1 <_ ( # ` F ) /\ P : ( 0 ... ( # ` F ) ) --> V ) -> ( P |` ( 0..^ ( # ` F ) ) ) : ( 0 ... ( # ` ( F |` ( 0..^ ( ( # ` F ) - 1 ) ) ) ) ) --> V )
Theorem	red1wlk 39813	A 1-walk ending at the last but one vertex of the walk is a 1-walk. (Contributed by Alexander van der Vekens, 1-Nov-2017.) (Revised by AV, 29-Jan-2021.)
|- ( ( F (1Walks ` G ) P /\ 1 <_ ( # ` F ) ) -> ( F |` ( 0..^ ( ( # ` F ) - 1 ) ) ) (1Walks ` G ) ( P |` ( 0..^ ( # ` F ) ) ) )
21.33.8.14  Walks for loop-free graphs For a hypergraph, the property to be "loop-free" is expressed by I : dom I --> { x e. ~P V | 2 <_ ( # ` x ) } with I = (iEdg ` G ).
Theorem	umgrislfupgrlem 39814	Lemma for umgrislfupgr 39815 and usgrislfuspgr 39816. (Contributed by AV, 27-Jan-2021.)
|- ( { x e. ( ~P V \ { (/) } ) | ( # ` x ) <_ 2 } i^i { x e. ~P V | 2 <_ ( # ` x ) } ) = { x e. ( ~P V \ { (/) } ) | ( # ` x ) = 2 }
Theorem	umgrislfupgr 39815*	A multigraph is a loop-free pseudograph. (Contributed by AV, 27-Jan-2021.)
|- V = (Vtx ` G )   &    |- I = (iEdg ` G )   =>    |- ( G e. UMGraph <-> ( G e. UPGraph /\ I : dom I --> { x e. ~P V | 2 <_ ( # ` x ) } ) )
Theorem	usgrislfuspgr 39816*	A simple graph is a loop-free simple pseudograph. (Contributed by AV, 27-Jan-2021.)
|- V = (Vtx ` G )   &    |- I = (iEdg ` G )   =>    |- ( G e. USGraph <-> ( G e. USPGraph /\ I : dom I --> { x e. ~P V | 2 <_ ( # ` x ) } ) )
Theorem	1wlkvtxeledg 39817*	Each pair of adjacent vertices in a 1-walk is a subset of an edge. (Contributed by AV, 28-Jan-2021.)
|- I = (iEdg ` G )   =>    |- ( F (1Walks ` G ) P -> A. k e. ( 0..^ ( # ` F ) ) { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) )
Theorem	lfgrwlkprop 39818*	Two adjacent vertices in a 1-walk are different in a loop-free graph. (Contributed by AV, 28-Jan-2021.)
|- I = (iEdg ` G )   =>    |- ( ( F (1Walks ` G ) P /\ I : dom I --> { x e. ~P V | 2 <_ ( # ` x ) } ) -> A. k e. ( 0..^ ( # ` F ) ) ( P ` k ) =/= ( P ` ( k + 1 ) ) )
Theorem	lfgriswlk 39819*	Conditions for a pair of functions to be a 1-walk in a loop-free graph. (Contributed by AV, 28-Jan-2021.)
|- I = (iEdg ` G )   &    |- V = (Vtx ` G )   =>    |- ( ( G e. W /\ I : dom I --> { x e. ~P V | 2 <_ ( # ` x ) } ) -> ( F (1Walks ` G ) P <-> ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. k e. ( 0..^ ( # ` F ) ) ( ( P ` k ) =/= ( P ` ( k + 1 ) ) /\ { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) ) ) )
Theorem	lfgr1wlknloop 39820*	In a loop-free graph, each walk has no loops! (Contributed by AV, 2-Feb-2021.)
|- I = (iEdg ` G )   &    |- V = (Vtx ` G )   =>    |- ( ( I : dom I --> { x e. ~P V | 2 <_ ( # ` x ) } /\ F (1Walks ` G ) P ) -> A. k e. ( 0..^ ( # ` F ) ) ( P ` k ) =/= ( P ` ( k + 1 ) ) )
Theorem	1wlkdlem1 39821*	Lemma 1 for 1wlkd 39825. (Contributed by AV, 7-Feb-2021.)
|- ( ph -> P e. Word _V )   &    |- ( ph -> F e. Word _V )   &    |- ( ph -> ( # ` P ) = ( ( # ` F ) + 1 ) )   &    |- ( ph -> A. k e. ( 0 ... ( # ` F ) ) ( P ` k ) e. V )   =>    |- ( ph -> P : ( 0 ... ( # ` F ) ) --> V )
Theorem	1wlkdlem2 39822*	Lemma 2 for 1wlkd 39825. (Contributed by AV, 7-Feb-2021.)
|- ( ph -> P e. Word _V )   &    |- ( ph -> F e. Word _V )   &    |- ( ph -> ( # ` P ) = ( ( # ` F ) + 1 ) )   &    |- ( ph -> A. k e. ( 0..^ ( # ` F ) ) { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) )   =>    |- ( ph -> ( ( ( # ` F ) e. NN -> ( P ` ( # ` F ) ) e. ( I ` ( F ` ( ( # ` F ) - 1 ) ) ) ) /\ A. k e. ( 0..^ ( # ` F ) ) ( P ` k ) e. ( I ` ( F ` k ) ) ) )
Theorem	1wlkdlem3 39823*	Lemma 3 for 1wlkd 39825. (Contributed by Alexander van der Vekens, 10-Nov-2017.) (Revised by AV, 7-Feb-2021.)
|- ( ph -> P e. Word _V )   &    |- ( ph -> F e. Word _V )   &    |- ( ph -> ( # ` P ) = ( ( # ` F ) + 1 ) )   &    |- ( ph -> A. k e. ( 0..^ ( # ` F ) ) { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) )   =>    |- ( ph -> F e. Word dom I )
Theorem	1wlkdlem4 39824*	Lemma 4 for 1wlkd 39825. (Contributed by Alexander van der Vekens, 1-Feb-2018.) (Revised by AV, 23-Jan-2021.)
|- ( ph -> P e. Word _V )   &    |- ( ph -> F e. Word _V )   &    |- ( ph -> ( # ` P ) = ( ( # ` F ) + 1 ) )   &    |- ( ph -> A. k e. ( 0..^ ( # ` F ) ) { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) )   &    |- ( ph -> A. k e. ( 0..^ ( # ` F ) ) ( P ` k ) =/= ( P ` ( k + 1 ) ) )   =>    |- ( ph -> A. k e. ( 0..^ ( # ` F ) )if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( I ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) )
Theorem	1wlkd 39825*	Two words representing a walk in a graph. (Contributed by AV, 7-Feb-2021.)
|- ( ph -> P e. Word _V )   &    |- ( ph -> F e. Word _V )   &    |- ( ph -> ( # ` P ) = ( ( # ` F ) + 1 ) )   &    |- ( ph -> A. k e. ( 0..^ ( # ` F ) ) { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) )   &    |- ( ph -> A. k e. ( 0..^ ( # ` F ) ) ( P ` k ) =/= ( P ` ( k + 1 ) ) )   &    |- ( ph -> G e. W )   &    |- V = (Vtx ` G )   &    |- I = (iEdg ` G )   &    |- ( ph -> A. k e. ( 0 ... ( # ` F ) ) ( P ` k ) e. V )   =>    |- ( ph -> F (1Walks ` G ) P )
21.33.8.15  Trails
Syntax	ctrls 39826	Extend class notation with trails (within a graph).
class TrailS
Syntax	ctrlson 39827	Extend class notation with tails between two vertices (within a graph).
class TrailsOn
Definition	df-trls 39828*	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 (1Walks ` g ) p /\ Fun `' f ) } )
Definition	df-trlson 39829*	Define the collection of trails with particular endpoints (in an undirected graph). (Contributed by Alexander van der Vekens and Mario Carneiro, 4-Oct-2017.) (Revised by AV, 28-Dec-2020.)
|- TrailsOn = ( g e. _V |-> ( a e. (Vtx ` g ) , b e. (Vtx ` g ) |-> { <. f , p >. | ( f ( a (WalksOn ` g ) b ) p /\ f (TrailS ` g ) p ) } ) )
Theorem	trlsfval 39830*	The set of trails (in an undirected graph). (Contributed by Alexander van der Vekens, 20-Oct-2017.) (Revised by AV, 28-Dec-2020.) (Proof shortened by AV, 31-Jan-2021.)
|- ( G e. W -> (TrailS ` G ) = { <. f , p >. | ( f (1Walks ` G ) p /\ Fun `' f ) } )
Theorem	isTrl 39831	Conditions for a pair of functions to be a trail (in an undirected graph). (Contributed by Alexander van der Vekens, 20-Oct-2017.) (Revised by AV, 28-Dec-2020.) (Proof shortened by AV, 31-Jan-2021.)
|- ( ( G e. W /\ F e. U /\ P e. Z ) -> ( F (TrailS ` G ) P <-> ( F (1Walks ` G ) P /\ Fun `' F ) ) )
Theorem	upgrtrls 39832*	The set of trails in a pseudograph, definition of walks expanded. (Contributed by Alexander van der Vekens, 20-Oct-2017.) (Revised by AV, 7-Jan-2021.)
|- V = (Vtx ` G )   &    |- I = (iEdg ` G )   =>    |- ( G e. UPGraph -> (TrailS ` G ) = { <. f , p >. | ( ( f e. Word dom I /\ Fun `' f ) /\ p : ( 0 ... ( # ` f ) ) --> V /\ A. k e. ( 0..^ ( # ` f ) ) ( I ` ( f ` k ) ) = { ( p ` k ) , ( p ` ( k + 1 ) ) } ) } )
Theorem	upgristrl 39833*	Properties of a pair of functions to be a trail in a pseudograph, definition of walks expanded. (Contributed by Alexander van der Vekens, 20-Oct-2017.) (Revised by AV, 7-Jan-2021.)
|- V = (Vtx ` G )   &    |- I = (iEdg ` G )   =>    |- ( ( G e. UPGraph /\ F e. U /\ P e. Z ) -> ( F (TrailS ` G ) P <-> ( ( F e. Word dom I /\ Fun `' F ) /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. k e. ( 0..^ ( # ` F ) ) ( I ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) ) )
Theorem	upgrf1istrl 39834*	Properties of a pair of a one-to-one function into the set of indices of edges and a function into the set of vertices to be a trail in a pseudograph. (Contributed by Alexander van der Vekens, 20-Oct-2017.) (Revised by AV, 7-Jan-2021.)
|- V = (Vtx ` G )   &    |- I = (iEdg ` G )   =>    |- ( ( G e. UPGraph /\ F e. U /\ P e. Z ) -> ( F (TrailS ` G ) P <-> ( F : ( 0..^ ( # ` F ) ) -1-1-> dom I /\ P : ( 0 ... ( # ` F ) ) --> V /\ A. k e. ( 0..^ ( # ` F ) ) ( I ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } ) ) )
Theorem	trlis1wlk 39835	A trail is a walk. (Contributed by Alexander van der Vekens, 20-Oct-2017.) (Revised by AV, 7-Jan-2021.)
|- ( F (TrailS ` G ) P -> F (1Walks ` G ) P )
Theorem	1wlksonproplem 39836*	Lemma for theorems for properties of walks between two vertices, e.g. trlsonprop 39839. (Contributed by AV, 16-Jan-2021.)
|- V = (Vtx ` G )   &    |- ( ( ( G e. _V /\ A e. V /\ B e. V ) /\ ( F e. _V /\ P e. _V ) ) -> ( F ( A ( W ` G ) B ) P <-> ( F ( A ( O ` G ) B ) P /\ F ( Q ` G ) P ) ) )   &    |- W = ( g e. _V |-> ( a e. (Vtx ` g ) , b e. (Vtx ` g ) |-> { <. f , p >. | ( f ( a ( O ` g ) b ) p /\ f ( Q ` g ) p ) } ) )   &    |- ( ( ( G e. _V /\ A e. V /\ B e. V ) /\ f ( Q ` G ) p ) -> f (1Walks ` G ) p )   =>    |- ( F ( A ( W ` G ) B ) P -> ( ( G e. _V /\ A e. V /\ B e. V ) /\ ( F e. _V /\ P e. _V ) /\ ( F ( A ( O ` G ) B ) P /\ F ( Q ` G ) P ) ) )
Theorem	trlsonfval 39837*	The set of trails between two vertices. (Contributed by Alexander van der Vekens, 4-Nov-2017.) (Revised by AV, 7-Jan-2021.) (Proof shortened by AV, 15-Jan-2021.)
|- V = (Vtx ` G )   =>    |- ( ( G e. W /\ A e. V /\ B e. V ) -> ( A (TrailsOn ` G ) B ) = { <. f , p >. | ( f ( A (WalksOn ` G ) B ) p /\ f (TrailS ` G ) p ) } )
Theorem	istrlson 39838	Properties of a pair of functions to be a trail between two given vertices. (Contributed by Alexander van der Vekens, 3-Nov-2017.) (Revised by AV, 7-Jan-2021.)
|- V = (Vtx ` G )   =>    |- ( ( ( G e. W /\ A e. V /\ B e. V ) /\ ( F e. U /\ P e. Z ) ) -> ( F ( A (TrailsOn ` G ) B ) P <-> ( F ( A (WalksOn ` G ) B ) P /\ F (TrailS ` G ) P ) ) )
Theorem	trlsonprop 39839	Properties of a trail between two vertices. (Contributed by Alexander van der Vekens, 5-Nov-2017.) (Revised by AV, 7-Jan-2021.) (Proof shortened by AV, 16-Jan-2021.)
|- V = (Vtx ` G )   =>    |- ( F ( A (TrailsOn ` G ) B ) P -> ( ( G e. _V /\ A e. V /\ B e. V ) /\ ( F e. _V /\ P e. _V ) /\ ( F ( A (WalksOn ` G ) B ) P /\ F (TrailS ` G ) P ) ) )
Theorem	trlsonistrl 39840	A trail between two vertices is a trail. (Contributed by Alexander van der Vekens, 12-Dec-2017.) (Revised by AV, 7-Jan-2021.)
|- ( F ( A (TrailsOn ` G ) B ) P -> F (TrailS ` G ) P )
Theorem	trlsonwlkon 39841	A trail between two vertices is a walk between these vertices. (Contributed by Alexander van der Vekens, 5-Nov-2017.) (Revised by AV, 7-Jan-2021.)
|- ( F ( A (TrailsOn ` G ) B ) P -> F ( A (WalksOn ` G ) B ) P )
Theorem	trlOntrl 39842	A trail is a trail between its endpoints. (Contributed by AV, 31-Jan-2021.)
|- ( F (TrailS ` G ) P -> F ( ( P ` 0 ) (TrailsOn ` G ) ( P ` ( # ` F ) ) ) P )
21.33.8.16  Paths
Syntax	cpths 39843	Extend class notation with paths (of a graph).
class PathS
Syntax	cspths 39844	Extend class notation with simple paths (of a graph).
class SPathS
Syntax	cpthson 39845	Extend class notation with paths between two vertices (within a graph).
class PathsOn
Syntax	cspthson 39846	Extend class notation with simple paths between two vertices (within a graph).
class SPathsOn
Definition	df-pths 39847*	Define the set of all paths (in an undirected graph). According to Wikipedia ("Path (graph theory)", https://en.wikipedia.org/wiki/Path_(graph_theory), 3-Oct-2017): "A path is a trail in which all vertices (except possibly the first and last) are distinct. ... use the term simple path to refer to a path which contains no repeated vertices." According to Bollobas: "... a path is a walk with distinct vertices.", see Notation of [Bollobas] p. 5. (A walk with distinct vertices is actually a simple path, see wlkdvspth 25394). Therefore, a path can be represented by an injective mapping f from { 1 , ... , n } and a mapping p from { 0 , ... , n }, which is injective restricted to the set { 1 , ... , n }, where f enumerates the (indices of the) different edges, and p enumerates the vertices. So the path 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, 9-Jan-2021.)
|- PathS = ( g e. _V |-> { <. f , p >. | ( f (TrailS ` g ) p /\ Fun `' ( p |` ( 1..^ ( # ` f ) ) ) /\ ( ( p " { 0 , ( # ` f ) } ) i^i ( p " ( 1..^ ( # ` f ) ) ) ) = (/) ) } )
Definition	df-spths 39848*	Define the set of all simple paths (in an undirected graph). According to Wikipedia ("Path (graph theory)", https://en.wikipedia.org/wiki/Path_(graph_theory), 3-Oct-2017): "A path is a trail in which all vertices (except possibly the first and last) are distinct. ... use the term simple path to refer to a path which contains no repeated vertices." Therefore, a simple path can be represented by an injective mapping f from { 1 , ... , n } and an injective mapping p from { 0 , ... , n }, where f enumerates the (indices of the) different edges, and p enumerates the vertices. So the simple path 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, 20-Oct-2017.) (Revised by AV, 9-Jan-2021.)
|- SPathS = ( g e. _V |-> { <. f , p >. | ( f (TrailS ` g ) p /\ Fun `' p ) } )
Definition	df-pthson 39849*	Define the collection of paths with particular endpoints (in an undirected graph). (Contributed by Alexander van der Vekens and Mario Carneiro, 4-Oct-2017.) (Revised by AV, 9-Jan-2021.)
|- PathsOn = ( g e. _V |-> ( a e. (Vtx ` g ) , b e. (Vtx ` g ) |-> { <. f , p >. | ( f ( a (TrailsOn ` g ) b ) p /\ f (PathS ` g ) p ) } ) )
Definition	df-spthson 39850*	Define the collection of simple paths with particular endpoints (in an undirected graph). (Contributed by Alexander van der Vekens, 1-Mar-2018.) (Revised by AV, 9-Jan-2021.)
|- SPathsOn = ( g e. _V |-> ( a e. (Vtx ` g ) , b e. (Vtx ` g ) |-> { <. f , p >. | ( f ( a (TrailsOn ` g ) b ) p /\ f (SPathS ` g ) p ) } ) )
Theorem	pthsfval 39851*	The set of paths (in an undirected graph). (Contributed by Alexander van der Vekens, 20-Oct-2017.) (Revised by AV, 9-Jan-2021.) (Proof shortened by AV, 31-Jan-2021.)
|- ( G e. W -> (PathS ` G ) = { <. f , p >. | ( f (TrailS ` G ) p /\ Fun `' ( p |` ( 1..^ ( # ` f ) ) ) /\ ( ( p " { 0 , ( # ` f ) } ) i^i ( p " ( 1..^ ( # ` f ) ) ) ) = (/) ) } )
Theorem	spthsfval 39852*	The set of simple paths (in an undirected graph). (Contributed by Alexander van der Vekens, 21-Oct-2017.) (Revised by AV, 9-Jan-2021.) (Proof shortened by AV, 31-Jan-2021.)
|- ( G e. W -> (SPathS ` G ) = { <. f , p >. | ( f (TrailS ` G ) p /\ Fun `' p ) } )
Theorem	isPth 39853	Conditions for a pair of functions to be a path (in an undirected graph). (Contributed by Alexander van der Vekens, 21-Oct-2017.) (Revised by AV, 9-Jan-2021.) (Proof shortened by AV, 31-Jan-2021.)
|- ( ( G e. W /\ F e. U /\ P e. Z ) -> ( F (PathS ` G ) P <-> ( F (TrailS ` G ) P /\ Fun `' ( P |` ( 1..^ ( # ` F ) ) ) /\ ( ( P " { 0 , ( # ` F ) } ) i^i ( P " ( 1..^ ( # ` F ) ) ) ) = (/) ) ) )
Theorem	issPth 39854	Conditions for a pair of functions to be a simple path (in an undirected graph). (Contributed by Alexander van der Vekens, 21-Oct-2017.) (Revised by AV, 9-Jan-2021.) (Proof shortened by AV, 31-Jan-2021.)
|- ( ( G e. W /\ F e. U /\ P e. Z ) -> ( F (SPathS ` G ) P <-> ( F (TrailS ` G ) P /\ Fun `' P ) ) )
Theorem	PthisTrl 39855	A path is a trail (in an undirected graph). (Contributed by Alexander van der Vekens, 21-Oct-2017.) (Revised by AV, 9-Jan-2021.)
|- ( F (PathS ` G ) P -> F (TrailS ` G ) P )
Theorem	sPthisPth 39856	A simple path is a path (in an undirected graph). (Contributed by Alexander van der Vekens, 21-Oct-2017.) (Revised by AV, 9-Jan-2021.)
|- ( F (SPathS ` G ) P -> F (PathS ` G ) P )
Theorem	pthis1wlk 39857	A path is a 1-walk (in an undirected graph). (Contributed by AV, 6-Feb-2021.)
|- ( F (PathS ` G ) P -> F (1Walks ` G ) P )
Theorem	pthdivtx 39858	The inner vertices of a path are distinct from all other vertices. (Contributed by AV, 5-Feb-2021.)
|- ( ( F (PathS ` G ) P /\ ( I e. ( 1..^ ( # ` F ) ) /\ J e. ( 0 ... ( # ` F ) ) /\ I =/= J ) ) -> ( P ` I ) =/= ( P ` J ) )
Theorem	pthdadjvtx 39859	The adjacent vertices of a path of length at least 2 are distinct. (Contributed by AV, 5-Feb-2021.)
|- ( ( F (PathS ` G ) P /\ 1 < ( # ` F ) /\ I e. ( 0..^ ( # ` F ) ) ) -> ( P ` I ) =/= ( P ` ( I + 1 ) ) )
Theorem	2pthnloop 39860*	A path of length at least 2 does not contain a loop. In contrast, a path of length 1 can contain/be a loop, see lppthon 39962. (Contributed by AV, 6-Feb-2021.)
|- I = (iEdg ` G )   =>    |- ( ( F (PathS ` G ) P /\ 1 < ( # ` F ) ) -> A. i e. ( 0..^ ( # ` F ) ) 2 <_ ( # ` ( I ` ( F ` i ) ) ) )
Theorem	upgr2pthnlp 39861*	A path of length at least 2 in a pseudograph does not contain a loop. (Contributed by AV, 6-Feb-2021.)
|- I = (iEdg ` G )   =>    |- ( ( G e. UPGraph /\ F (PathS ` G ) P /\ 1 < ( # ` F ) ) -> A. i e. ( 0..^ ( # ` F ) ) ( # ` ( I ` ( F ` i ) ) ) = 2 )
Theorem	spthdep 39862	A simple path (at least of length 1) has different start and end points (in an undirected graph). (Contributed by AV, 31-Jan-2021.)
|- ( ( F (SPathS ` G ) P /\ ( # ` F ) =/= 0 ) -> ( P ` 0 ) =/= ( P ` ( # ` F ) ) )
Theorem	pthdepissPth 39863	A path with different start and end points is a simple path (in an undirected graph). (Contributed by Alexander van der Vekens, 31-Oct-2017.) (Revised by AV, 12-Jan-2021.)
|- ( ( F (PathS ` G ) P /\ ( P ` 0 ) =/= ( P ` ( # ` F ) ) ) -> F (SPathS ` G ) P )
Theorem	upgrwlkdvdelem 39864*	Lemma for upgrwlkdvde 39865. Formerly wlkdvspthlem 25393. (Contributed by Alexander van der Vekens, 27-Oct-2017.) (Proof shortened by AV, 17-Jan-2021.)
|- ( ( P : ( 0 ... ( # ` F ) ) -1-1-> V /\ F e. Word dom I ) -> ( A. k e. ( 0..^ ( # ` F ) ) ( I ` ( F ` k ) ) = { ( P ` k ) , ( P ` ( k + 1 ) ) } -> Fun `' F ) )
Theorem	upgrwlkdvde 39865	In a pseudograph, all edges of a walk consisting of different vertices are different. Notice that this theorem would not hold for arbitrary hypergraphs, see the counterexample given in the comment of upgrspths1wlk 39866. (Contributed by AV, 17-Jan-2021.)
|- ( ( G e. UPGraph /\ F (1Walks ` G ) P /\ Fun `' P ) -> Fun `' F )
Theorem	upgrspths1wlk 39866*	The set of simple paths in a pseudograph, expressed as walk. Notice that this theorem would not hold for arbitrary hypergraphs, since a walk with distinct vertices does not need to be a trail: let E = { p0, p1, p2 } be a hyperedge, then ( p0, e, p1, e, p2 ) is walk with distinct vertices, but not with distinct edges. Therefore, E is not a trail and, by definition, also no path. (Contributed by AV, 11-Jan-2021.) (Proof shortened by AV, 17-Jan-2021.)
|- ( G e. UPGraph -> (SPathS ` G ) = { <. f , p >. | ( f (1Walks ` G ) p /\ Fun `' p ) } )
Theorem	upgrwlkdvspth 39867	A walk consisting of different vertices is a simple path. Formerly wlkdvspth 25394. Notice that this theorem would not hold for arbitrary hypergraphs, see the counterexample given in the comment of upgrspths1wlk 39866. (Contributed by Alexander van der Vekens, 27-Oct-2017.) (Revised by AV, 17-Jan-2021.)
|- ( ( G e. UPGraph /\ F (1Walks ` G ) P /\ Fun `' P ) -> F (SPathS ` G ) P )
Theorem	pthsonfval 39868*	The set of paths between two vertices (in an undirected graph). (Contributed by Alexander van der Vekens, 8-Nov-2017.) (Revised by AV, 16-Jan-2021.)
|- V = (Vtx ` G )   =>    |- ( ( G e. W /\ A e. V /\ B e. V ) -> ( A (PathsOn ` G ) B ) = { <. f , p >. | ( f ( A (TrailsOn ` G ) B ) p /\ f (PathS ` G ) p ) } )
Theorem	spthson 39869*	The set of simple paths between two vertices (in an undirected graph). (Contributed by Alexander van der Vekens, 1-Mar-2018.) (Revised by AV, 16-Jan-2021.)
|- V = (Vtx ` G )   =>    |- ( ( G e. W /\ A e. V /\ B e. V ) -> ( A (SPathsOn ` G ) B ) = { <. f , p >. | ( f ( A (TrailsOn ` G ) B ) p /\ f (SPathS ` G ) p ) } )
Theorem	ispthson 39870	Properties of a pair of functions to be a path between two given vertices. (Contributed by Alexander van der Vekens, 8-Nov-2017.) (Revised by AV, 16-Jan-2021.)
|- V = (Vtx ` G )   =>    |- ( ( ( G e. W /\ A e. V /\ B e. V ) /\ ( F e. U /\ P e. Z ) ) -> ( F ( A (PathsOn ` G ) B ) P <-> ( F ( A (TrailsOn ` G ) B ) P /\ F (PathS ` G ) P ) ) )
Theorem	isspthson 39871	Properties of a pair of functions to be a simple path between two given vertices. (Contributed by Alexander van der Vekens, 1-Mar-2018.) (Revised by AV, 16-Jan-2021.)
|- V = (Vtx ` G )   =>    |- ( ( ( G e. W /\ A e. V /\ B e. V ) /\ ( F e. U /\ P e. Z ) ) -> ( F ( A (SPathsOn ` G ) B ) P <-> ( F ( A (TrailsOn ` G ) B ) P /\ F (SPathS ` G ) P ) ) )
Theorem	pthsonprop 39872	Properties of a path between two vertices. (Contributed by Alexander van der Vekens, 12-Dec-2017.) (Revised by AV, 16-Jan-2021.)
|- V = (Vtx ` G )   =>    |- ( F ( A (PathsOn ` G ) B ) P -> ( ( G e. _V /\ A e. V /\ B e. V ) /\ ( F e. _V /\ P e. _V ) /\ ( F ( A (TrailsOn ` G ) B ) P /\ F (PathS ` G ) P ) ) )
Theorem	spthonprop 39873	Properties of a simple path between two vertices. (Contributed by Alexander van der Vekens, 1-Mar-2018.) (Revised by AV, 16-Jan-2021.)
|- V = (Vtx ` G )   =>    |- ( F ( A (SPathsOn ` G ) B ) P -> ( ( G e. _V /\ A e. V /\ B e. V ) /\ ( F e. _V /\ P e. _V ) /\ ( F ( A (TrailsOn ` G ) B ) P /\ F (SPathS ` G ) P ) ) )
Theorem	pthonispth-av 39874	A path between two vertices is a path. (Contributed by Alexander van der Vekens, 12-Dec-2017.) (Revised by AV, 17-Jan-2021.)
|- ( F ( A (PathsOn ` G ) B ) P -> F (PathS ` G ) P )
Theorem	pthontrlon 39875	A path between two vertices is a trail between these vertices. (Contributed by AV, 24-Jan-2021.)
|- ( F ( A (PathsOn ` G ) B ) P -> F ( A (TrailsOn ` G ) B ) P )
Theorem	pthOnpth 39876	A path is a path between its endpoints. (Contributed by AV, 31-Jan-2021.)
|- ( F (PathS ` G ) P -> F ( ( P ` 0 ) (PathsOn ` G ) ( P ` ( # ` F ) ) ) P )
Theorem	isspthonpth-av 39877	A pair of functions is a simple path between two given vertices iff it is a simple path starting and ending at the two vertices. (Contributed by Alexander van der Vekens, 9-Mar-2018.) (Revised by AV, 17-Jan-2021.)
|- V = (Vtx ` G )   =>    |- ( ( ( G e. W /\ A e. V /\ B e. V ) /\ ( F e. W /\ P e. Z ) ) -> ( F ( A (SPathsOn ` G ) B ) P <-> ( F (SPathS ` G ) P /\ ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) ) )
Theorem	spthonisspth-av 39878	A simple path between to vertices is a simple path. (Contributed by Alexander van der Vekens, 2-Mar-2018.) (Revised by AV, 18-Jan-2021.)
|- ( F ( A (SPathsOn ` G ) B ) P -> F (SPathS ` G ) P )
Theorem	spthonpthon 39879	A simple path between two vertices is a path between these vertices. (Contributed by AV, 24-Jan-2021.)
|- ( F ( A (SPathsOn ` G ) B ) P -> F ( A (PathsOn ` G ) B ) P )
Theorem	spthonepeq-av 39880	The endpoints of a simple path between two vertices are equal iff the path is of length 0. (Contributed by Alexander van der Vekens, 1-Mar-2018.) (Revised by AV, 18-Jan-2021.)
|- ( F ( A (SPathsOn ` G ) B ) P -> ( A = B <-> ( # ` F ) = 0 ) )
Theorem	uhgr1wlkspthlem1 39881	Lemma 1 for uhgr1wlkspth 39883. (Contributed by AV, 25-Jan-2021.)
|- ( ( F (1Walks ` G ) P /\ ( # ` F ) = 1 ) -> Fun `' F )
Theorem	uhgr1wlkspthlem2 39882	Lemma 2 for uhgr1wlkspth 39883. (Contributed by AV, 25-Jan-2021.)
|- ( ( F (1Walks ` G ) P /\ ( ( # ` F ) = 1 /\ A =/= B ) /\ ( ( P ` 0 ) = A /\ ( P ` ( # ` F ) ) = B ) ) -> Fun `' P )
Theorem	uhgr1wlkspth 39883	Any walk of length 1 between two different vertices is a simple path. (Contributed by AV, 25-Jan-2021.)
|- V = (Vtx ` G )   &    |- E = (Edg ` G )   =>    |- ( ( G e. W /\ ( # ` F ) = 1 /\ A =/= B ) -> ( F ( A (WalksOn ` G ) B ) P <-> F ( A (SPathsOn ` G ) B ) P ) )
Theorem	usgr2wlkneq 39884	The vertices and edges are pairwise different in a walk of length 2 in a simple graph. (Contributed by Alexander van der Vekens, 2-Mar-2018.) (Revised by AV, 26-Jan-2021.)
|- ( ( ( G e. USGraph /\ F (1Walks ` G ) P ) /\ ( ( # ` F ) = 2 /\ ( P ` 0 ) =/= ( P ` ( # ` F ) ) ) ) -> ( ( ( P ` 0 ) =/= ( P ` 1 ) /\ ( P ` 0 ) =/= ( P ` 2 ) /\ ( P ` 1 ) =/= ( P ` 2 ) ) /\ ( F ` 0 ) =/= ( F ` 1 ) ) )
Theorem	usgr2wlkspthlem1 39885	Lemma 1 for usgr2wlkspth 39887. (Contributed by Alexander van der Vekens, 2-Mar-2018.) (Revised by AV, 26-Jan-2021.)
|- ( ( F (1Walks ` G ) P /\ ( G e. USGraph /\ ( # ` F ) = 2 /\ ( P ` 0 ) =/= ( P ` ( # ` F ) ) ) ) -> Fun `' F )
Theorem	usgr2wlkspthlem2 39886	Lemma 2 for usgr2wlkspth 39887. (Contributed by Alexander van der Vekens, 2-Mar-2018.) (Revised by AV, 27-Jan-2021.)
|- ( ( F (1Walks ` G ) P /\ ( G e. USGraph /\ ( # ` F ) = 2 /\ ( P ` 0 ) =/= ( P ` ( # ` F ) ) ) ) -> Fun `' P )
Theorem	usgr2wlkspth 39887	In a simple graph, any walk of length 2 between two different vertices is a simple path. (Contributed by Alexander van der Vekens, 2-Mar-2018.) (Revised by AV, 27-Jan-2021.)
|- ( ( G e. USGraph /\ ( # ` F ) = 2 /\ A =/= B ) -> ( F ( A (WalksOn ` G ) B ) P <-> F ( A (SPathsOn ` G ) B ) P ) )
Theorem	pthdlem1 39888*	Lemma 1 for pthd 39891. (Contributed by Alexander van der Vekens, 13-Nov-2017.) (Revised by AV, 9-Feb-2021.)
|- ( ph -> P e. Word _V )   &    |- R = ( ( # ` P ) - 1 )   &    |- ( ph -> A. i e. ( 0..^ ( # ` P ) ) A. j e. ( 1..^ R ) ( i =/= j -> ( P ` i ) =/= ( P ` j ) ) )   =>    |- ( ph -> Fun `' ( P |` ( 1..^ R ) ) )
Theorem	pthdlem2lem 39889*	Lemma for pthdlem2 39890. (Contributed by AV, 10-Feb-2021.)
|- ( ph -> P e. Word _V )   &    |- R = ( ( # ` P ) - 1 )   &    |- ( ph -> A. i e. ( 0..^ ( # ` P ) ) A. j e. ( 1..^ R ) ( i =/= j -> ( P ` i ) =/= ( P ` j ) ) )   =>    |- ( ( ph /\ ( # ` P ) e. NN /\ ( I = 0 \/ I = R ) ) -> ( P ` I ) e/ ( P " ( 1..^ R ) ) )
Theorem	pthdlem2 39890*	Lemma 2 for pthd 39891. (Contributed by Alexander van der Vekens, 11-Nov-2017.) (Revised by AV, 10-Feb-2021.)
|- ( ph -> P e. Word _V )   &    |- R = ( ( # ` P ) - 1 )   &    |- ( ph -> A. i e. ( 0..^ ( # ` P ) ) A. j e. ( 1..^ R ) ( i =/= j -> ( P ` i ) =/= ( P ` j ) ) )   =>    |- ( ph -> ( ( P " { 0 , R } ) i^i ( P " ( 1..^ R ) ) ) = (/) )
Theorem	pthd 39891*	Two words representing a trail which also represent a path in a graph. (Contributed by AV, 10-Feb-2021.)
|- ( ph -> P e. Word _V )   &    |- R = ( ( # ` P ) - 1 )   &    |- ( ph -> A. i e. ( 0..^ ( # ` P ) ) A. j e. ( 1..^ R ) ( i =/= j -> ( P ` i ) =/= ( P ` j ) ) )   &    |- ( # ` F ) = R   &    |- ( ph -> F (TrailS ` G ) P )   =>    |- ( ph -> F (PathS ` G ) P )
21.33.8.17  Closed walks
Syntax	cclwlks 39892	Extend class notation with closed walks (of a graph).
class ClWalkS
Definition	df-clwlks 39893*	Define the set of all closed walks (in an undirected graph). According to definition 4 in [Huneke] p. 2: "A walk of length n on (a graph) G is an ordered sequence v0 , v1 , ... v(n) of vertices such that v(i) and v(i+1) are neighbors (i.e are connected by an edge). We say the walk is closed if v(n) = v0". According to the definition of a walk as two mappings f from { 0 , ... , ( n - 1 ) } and p from { 0 , ... , n }, where f enumerates the (indices of the) edges, and p enumerates the vertices, a closed walk is represented by the following sequence: p(0) e(f(0)) p(1) e(f(1)) ... p(n-1) e(f(n-1)) p(n)=p(0). Notice that by this definition, a single vertex is a closed walk of length 0, see also 0clwlk 25549! (Contributed by Alexander van der Vekens, 12-Mar-2018.) (Revised by AV, 16-Feb-2021.)
|- ClWalkS = ( g e. _V |-> { <. f , p >. | ( f (1Walks ` g ) p /\ ( p ` 0 ) = ( p ` ( # ` f ) ) ) } )
Theorem	clwlkS 39894*	The set of closed walks (in an undirected graph). (Contributed by Alexander van der Vekens, 15-Mar-2018.) (Revised by AV, 16-Feb-2021.)
|- ( G e. X -> (ClWalkS ` G ) = { <. f , p >. | ( f (1Walks ` G ) p /\ ( p ` 0 ) = ( p ` ( # ` f ) ) ) } )
Theorem	isclWlk 39895	Properties of a pair of functions to be a closed walk (in an undirected graph) in terms of walks. (Contributed by Alexander van der Vekens, 15-Mar-2018.) (Revised by AV, 16-Feb-2021.)
|- ( ( G e. X /\ F e. Y /\ P e. Z ) -> ( F (ClWalkS ` G ) P <-> ( F (1Walks ` G ) P /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) ) )
Theorem	isclWlkb 39896	Generalisation of isclwlk 25540: A pair of functions represents a closed walk iff it represents a walk in which the first vertex is equal to the last vertex. (Contributed by Alexander van der Vekens, 24-Jun-2018.) (Revised by AV, 16-Feb-2021.)
|- ( F (ClWalkS ` G ) P <-> ( F (1Walks ` G ) P /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) )
Theorem	clwlkis1wlk 39897	A closed walk is a walk (in an undirected graph). (Contributed by Alexander van der Vekens, 15-Mar-2018.) (Revised by AV, 16-Feb-2021.)
|- ( F (ClWalkS ` G ) P -> F (1Walks ` G ) P )
Theorem	clwlk1wlk 39898	Closed walks are walks (in an undirected graph). (Contributed by Alexander van der Vekens, 23-Jun-2018.) (Revised by AV, 16-Feb-2021.)
|- ( W e. (ClWalkS ` G ) -> W e. (1Walks ` G ) )
Theorem	clwlks1wlks 39899	Closed walks are walks (in an undirected graph). (Contributed by Alexander van der Vekens, 25-Aug-2018.) (Revised by AV, 16-Feb-2021.)
|- (ClWalkS ` G ) C_ (1Walks ` G )
Theorem	isclWlke 39900*	Properties of a pair of functions to be a closed walk (in an undirected graph). (Contributed by Alexander van der Vekens, 24-Jun-2018.) (Revised by AV, 16-Feb-2021.)
|- V = (Vtx ` G )   &    |- I = (iEdg ` G )   =>    |- ( G e. X -> ( F (ClWalkS ` G ) P <-> ( ( F e. Word dom I /\ P : ( 0 ... ( # ` F ) ) --> V ) /\ ( A. k e. ( 0..^ ( # ` F ) )if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( I ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( I ` ( F ` k ) ) ) /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) ) ) )