P. 297 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 29601-29700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	1hegrvtxdg1 29601	The vertex degree of a graph with one hyperedge, case 2: an edge from the given vertex to some other vertex contributes one to the vertex's degree. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Alexander van der Vekens, 22-Dec-2017.) (Revised by AV, 23-Feb-2021.)
⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ≠ 𝐶)    &   ⊢ (𝜑 → 𝐸 ∈ 𝒫 𝑉)    &   ⊢ (𝜑 → (iEdg‘𝐺) = {⟨𝐴, 𝐸⟩})    &   ⊢ (𝜑 → {𝐵, 𝐶} ⊆ 𝐸)    &   ⊢ (𝜑 → (Vtx‘𝐺) = 𝑉)    ⇒   ⊢ (𝜑 → ((VtxDeg‘𝐺)‘𝐵) = 1)
Theorem	1hegrvtxdg1r 29602	The vertex degree of a graph with one hyperedge, case 3: an edge from some other vertex to the given vertex contributes one to the vertex's degree. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Alexander van der Vekens, 22-Dec-2017.) (Revised by AV, 23-Feb-2021.)
⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ≠ 𝐶)    &   ⊢ (𝜑 → 𝐸 ∈ 𝒫 𝑉)    &   ⊢ (𝜑 → (iEdg‘𝐺) = {⟨𝐴, 𝐸⟩})    &   ⊢ (𝜑 → {𝐵, 𝐶} ⊆ 𝐸)    &   ⊢ (𝜑 → (Vtx‘𝐺) = 𝑉)    ⇒   ⊢ (𝜑 → ((VtxDeg‘𝐺)‘𝐶) = 1)
Theorem	1egrvtxdg1 29603	The vertex degree of a one-edge graph, case 2: an edge from the given vertex to some other vertex contributes one to the vertex's degree. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Alexander van der Vekens, 22-Dec-2017.) (Revised by AV, 21-Feb-2021.)
⊢ (𝜑 → (Vtx‘𝐺) = 𝑉)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ≠ 𝐶)    &   ⊢ (𝜑 → (iEdg‘𝐺) = {⟨𝐴, {𝐵, 𝐶}⟩})    ⇒   ⊢ (𝜑 → ((VtxDeg‘𝐺)‘𝐵) = 1)
Theorem	1egrvtxdg1r 29604	The vertex degree of a one-edge graph, case 3: an edge from some other vertex to the given vertex contributes one to the vertex's degree. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Alexander van der Vekens, 22-Dec-2017.) (Revised by AV, 21-Feb-2021.)
⊢ (𝜑 → (Vtx‘𝐺) = 𝑉)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ≠ 𝐶)    &   ⊢ (𝜑 → (iEdg‘𝐺) = {⟨𝐴, {𝐵, 𝐶}⟩})    ⇒   ⊢ (𝜑 → ((VtxDeg‘𝐺)‘𝐶) = 1)
Theorem	1egrvtxdg0 29605	The vertex degree of a one-edge graph, case 1: an edge between two vertices other than the given vertex contributes nothing to the vertex degree. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Alexander van der Vekens, 22-Dec-2017.) (Revised by AV, 21-Feb-2021.)
⊢ (𝜑 → (Vtx‘𝐺) = 𝑉)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ≠ 𝐶)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐶 ≠ 𝐷)    &   ⊢ (𝜑 → (iEdg‘𝐺) = {⟨𝐴, {𝐵, 𝐷}⟩})    ⇒   ⊢ (𝜑 → ((VtxDeg‘𝐺)‘𝐶) = 0)
Theorem	p1evtxdeqlem 29606	Lemma for p1evtxdeq 29607 and p1evtxdp1 29608. (Contributed by AV, 3-Mar-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ (𝜑 → Fun 𝐼)    &   ⊢ (𝜑 → (Vtx‘𝐹) = 𝑉)    &   ⊢ (𝜑 → (iEdg‘𝐹) = (𝐼 ∪ {⟨𝐾, 𝐸⟩}))    &   ⊢ (𝜑 → 𝐾 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐾 ∉ dom 𝐼)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑌)    ⇒   ⊢ (𝜑 → ((VtxDeg‘𝐹)‘𝑈) = (((VtxDeg‘𝐺)‘𝑈) +𝑒 ((VtxDeg‘⟨𝑉, {⟨𝐾, 𝐸⟩}⟩)‘𝑈)))
Theorem	p1evtxdeq 29607	If an edge 𝐸 which does not contain vertex 𝑈 is added to a graph 𝐺 (yielding a graph 𝐹), the degree of 𝑈 is the same in both graphs. (Contributed by AV, 2-Mar-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ (𝜑 → Fun 𝐼)    &   ⊢ (𝜑 → (Vtx‘𝐹) = 𝑉)    &   ⊢ (𝜑 → (iEdg‘𝐹) = (𝐼 ∪ {⟨𝐾, 𝐸⟩}))    &   ⊢ (𝜑 → 𝐾 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐾 ∉ dom 𝐼)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑌)    &   ⊢ (𝜑 → 𝑈 ∉ 𝐸)    ⇒   ⊢ (𝜑 → ((VtxDeg‘𝐹)‘𝑈) = ((VtxDeg‘𝐺)‘𝑈))
Theorem	p1evtxdp1 29608	If an edge 𝐸 (not being a loop) which contains vertex 𝑈 is added to a graph 𝐺 (yielding a graph 𝐹), the degree of 𝑈 is increased by 1. (Contributed by AV, 3-Mar-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ (𝜑 → Fun 𝐼)    &   ⊢ (𝜑 → (Vtx‘𝐹) = 𝑉)    &   ⊢ (𝜑 → (iEdg‘𝐹) = (𝐼 ∪ {⟨𝐾, 𝐸⟩}))    &   ⊢ (𝜑 → 𝐾 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐾 ∉ dom 𝐼)    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐸 ∈ 𝒫 𝑉)    &   ⊢ (𝜑 → 𝑈 ∈ 𝐸)    &   ⊢ (𝜑 → 2 ≤ (♯‘𝐸))    ⇒   ⊢ (𝜑 → ((VtxDeg‘𝐹)‘𝑈) = (((VtxDeg‘𝐺)‘𝑈) +𝑒 1))
Theorem	uspgrloopvtx 29609	The set of vertices in a graph (simple pseudograph) with one edge which is a loop (see uspgr1v1eop 29343). (Contributed by AV, 17-Dec-2020.)
⊢ 𝐺 = ⟨𝑉, {⟨𝐴, {𝑁}⟩}⟩    ⇒   ⊢ (𝑉 ∈ 𝑊 → (Vtx‘𝐺) = 𝑉)
Theorem	uspgrloopvtxel 29610	A vertex in a graph (simple pseudograph) with one edge which is a loop (see uspgr1v1eop 29343). (Contributed by AV, 17-Dec-2020.)
⊢ 𝐺 = ⟨𝑉, {⟨𝐴, {𝑁}⟩}⟩    ⇒   ⊢ ((𝑉 ∈ 𝑊 ∧ 𝑁 ∈ 𝑉) → 𝑁 ∈ (Vtx‘𝐺))
Theorem	uspgrloopiedg 29611	The set of edges in a graph (simple pseudograph) with one edge which is a loop (see uspgr1v1eop 29343) is a singleton of a singleton. (Contributed by AV, 21-Feb-2021.)
⊢ 𝐺 = ⟨𝑉, {⟨𝐴, {𝑁}⟩}⟩    ⇒   ⊢ ((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋) → (iEdg‘𝐺) = {⟨𝐴, {𝑁}⟩})
Theorem	uspgrloopedg 29612	The set of edges in a graph (simple pseudograph) with one edge which is a loop (see uspgr1v1eop 29343) is a singleton of a singleton. (Contributed by AV, 17-Dec-2020.)
⊢ 𝐺 = ⟨𝑉, {⟨𝐴, {𝑁}⟩}⟩    ⇒   ⊢ ((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋) → (Edg‘𝐺) = {{𝑁}})
Theorem	uspgrloopnb0 29613	In a graph (simple pseudograph) with one edge which is a loop (see uspgr1v1eop 29343), the vertex connected with itself by the loop has no neighbors. (Contributed by AV, 17-Dec-2020.) (Proof shortened by AV, 21-Feb-2021.)
⊢ 𝐺 = ⟨𝑉, {⟨𝐴, {𝑁}⟩}⟩    ⇒   ⊢ ((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ 𝑉) → (𝐺 NeighbVtx 𝑁) = ∅)
Theorem	uspgrloopvd2 29614	The vertex degree of a one-edge graph, case 4: an edge from a vertex to itself contributes two to the vertex's degree. I. e. in a graph (simple pseudograph) with one edge which is a loop (see uspgr1v1eop 29343), the vertex connected with itself by the loop has degree 2. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Alexander van der Vekens, 22-Dec-2017.) (Revised by AV, 17-Dec-2020.) (Proof shortened by AV, 21-Feb-2021.)
⊢ 𝐺 = ⟨𝑉, {⟨𝐴, {𝑁}⟩}⟩    ⇒   ⊢ ((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ 𝑉) → ((VtxDeg‘𝐺)‘𝑁) = 2)
Theorem	umgr2v2evtx 29615	The set of vertices in a multigraph with two edges connecting the same two vertices. (Contributed by AV, 17-Dec-2020.)
⊢ 𝐺 = ⟨𝑉, {⟨0, {𝐴, 𝐵}⟩, ⟨1, {𝐴, 𝐵}⟩}⟩    ⇒   ⊢ (𝑉 ∈ 𝑊 → (Vtx‘𝐺) = 𝑉)
Theorem	umgr2v2evtxel 29616	A vertex in a multigraph with two edges connecting the same two vertices. (Contributed by AV, 17-Dec-2020.)
⊢ 𝐺 = ⟨𝑉, {⟨0, {𝐴, 𝐵}⟩, ⟨1, {𝐴, 𝐵}⟩}⟩    ⇒   ⊢ ((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉) → 𝐴 ∈ (Vtx‘𝐺))
Theorem	umgr2v2eiedg 29617	The edge function in a multigraph with two edges connecting the same two vertices. (Contributed by AV, 17-Dec-2020.)
⊢ 𝐺 = ⟨𝑉, {⟨0, {𝐴, 𝐵}⟩, ⟨1, {𝐴, 𝐵}⟩}⟩    ⇒   ⊢ ((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (iEdg‘𝐺) = {⟨0, {𝐴, 𝐵}⟩, ⟨1, {𝐴, 𝐵}⟩})
Theorem	umgr2v2eedg 29618	The set of edges in a multigraph with two edges connecting the same two vertices. (Contributed by AV, 17-Dec-2020.)
⊢ 𝐺 = ⟨𝑉, {⟨0, {𝐴, 𝐵}⟩, ⟨1, {𝐴, 𝐵}⟩}⟩    ⇒   ⊢ ((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (Edg‘𝐺) = {{𝐴, 𝐵}})
Theorem	umgr2v2e 29619	A multigraph with two edges connecting the same two vertices. (Contributed by AV, 17-Dec-2020.)
⊢ 𝐺 = ⟨𝑉, {⟨0, {𝐴, 𝐵}⟩, ⟨1, {𝐴, 𝐵}⟩}⟩    ⇒   ⊢ (((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → 𝐺 ∈ UMGraph)
Theorem	umgr2v2enb1 29620	In a multigraph with two edges connecting the same two vertices, each of the vertices has one neighbor. (Contributed by AV, 18-Dec-2020.)
⊢ 𝐺 = ⟨𝑉, {⟨0, {𝐴, 𝐵}⟩, ⟨1, {𝐴, 𝐵}⟩}⟩    ⇒   ⊢ (((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → (𝐺 NeighbVtx 𝐴) = {𝐵})
Theorem	umgr2v2evd2 29621	In a multigraph with two edges connecting the same two vertices, each of the vertices has degree 2. (Contributed by AV, 18-Dec-2020.)
⊢ 𝐺 = ⟨𝑉, {⟨0, {𝐴, 𝐵}⟩, ⟨1, {𝐴, 𝐵}⟩}⟩    ⇒   ⊢ (((𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → ((VtxDeg‘𝐺)‘𝐴) = 2)
Theorem	hashnbusgrvd 29622	In a simple graph, the number of neighbors of a vertex is the degree of this vertex. This theorem does not hold for (simple) pseudographs, because a vertex connected with itself only by a loop has no neighbors, see uspgrloopnb0 29613, but degree 2, see uspgrloopvd2 29614. And it does not hold for multigraphs, because a vertex connected with only one other vertex by two edges has one neighbor, see umgr2v2enb1 29620, but also degree 2, see umgr2v2evd2 29621. (Contributed by Alexander van der Vekens, 17-Dec-2017.) (Revised by AV, 15-Dec-2020.) (Proof shortened by AV, 5-May-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉) → (♯‘(𝐺 NeighbVtx 𝑈)) = ((VtxDeg‘𝐺)‘𝑈))
Theorem	usgruvtxvdb 29623	In a finite simple graph with n vertices a vertex is universal iff the vertex has degree 𝑛 − 1. (Contributed by Alexander van der Vekens, 14-Jul-2018.) (Revised by AV, 17-Dec-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑈 ∈ 𝑉) → (𝑈 ∈ (UnivVtx‘𝐺) ↔ ((VtxDeg‘𝐺)‘𝑈) = ((♯‘𝑉) − 1)))
Theorem	vdiscusgrb 29624*	A finite simple graph with n vertices is complete iff every vertex has degree 𝑛 − 1. (Contributed by Alexander van der Vekens, 14-Jul-2018.) (Revised by AV, 22-Dec-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (𝐺 ∈ FinUSGraph → (𝐺 ∈ ComplUSGraph ↔ ∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = ((♯‘𝑉) − 1)))
Theorem	vdiscusgr 29625*	In a finite complete simple graph with n vertices every vertex has degree 𝑛 − 1. (Contributed by Alexander van der Vekens, 14-Jul-2018.) (Revised by AV, 17-Dec-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (𝐺 ∈ FinUSGraph → (∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = ((♯‘𝑉) − 1) → 𝐺 ∈ ComplUSGraph))
Theorem	vtxdusgradjvtx 29626*	The degree of a vertex in a simple graph is the number of vertices adjacent to this vertex. (Contributed by Alexander van der Vekens, 9-Jul-2018.) (Revised by AV, 23-Dec-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉) → ((VtxDeg‘𝐺)‘𝑈) = (♯‘{𝑣 ∈ 𝑉 ∣ {𝑈, 𝑣} ∈ 𝐸}))
Theorem	usgrvd0nedg 29627*	If a vertex in a simple graph has degree 0, the vertex is not adjacent to another vertex via an edge. (Contributed by Alexander van der Vekens, 20-Dec-2017.) (Revised by AV, 16-Dec-2020.) (Proof shortened by AV, 23-Dec-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉) → (((VtxDeg‘𝐺)‘𝑈) = 0 → ¬ ∃𝑣 ∈ 𝑉 {𝑈, 𝑣} ∈ 𝐸))
Theorem	uhgrvd00 29628*	If every vertex in a hypergraph has degree 0, there is no edge in the graph. (Contributed by Alexander van der Vekens, 12-Jul-2018.) (Revised by AV, 24-Dec-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (𝐺 ∈ UHGraph → (∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 0 → 𝐸 = ∅))
Theorem	usgrvd00 29629*	If every vertex in a simple graph has degree 0, there is no edge in the graph. (Contributed by Alexander van der Vekens, 12-Jul-2018.) (Revised by AV, 17-Dec-2020.) (Proof shortened by AV, 23-Dec-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (𝐺 ∈ USGraph → (∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 0 → 𝐸 = ∅))
Theorem	vdegp1ai 29630*	The induction step for a vertex degree calculation. If the degree of 𝑈 in the edge set 𝐸 is 𝑃, then adding {𝑋, 𝑌} to the edge set, where 𝑋 ≠ 𝑈 ≠ 𝑌, yields degree 𝑃 as well. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Mario Carneiro, 28-Feb-2016.) (Revised by AV, 3-Mar-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑈 ∈ 𝑉    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝐼 ∈ Word {𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (♯‘𝑥) ≤ 2}    &   ⊢ ((VtxDeg‘𝐺)‘𝑈) = 𝑃    &   ⊢ (Vtx‘𝐹) = 𝑉    &   ⊢ 𝑋 ∈ 𝑉    &   ⊢ 𝑋 ≠ 𝑈    &   ⊢ 𝑌 ∈ 𝑉    &   ⊢ 𝑌 ≠ 𝑈    &   ⊢ (iEdg‘𝐹) = (𝐼 ++ ⟨“{𝑋, 𝑌}”⟩)    ⇒   ⊢ ((VtxDeg‘𝐹)‘𝑈) = 𝑃
Theorem	vdegp1bi 29631*	The induction step for a vertex degree calculation, for example in the Königsberg graph. If the degree of 𝑈 in the edge set 𝐸 is 𝑃, then adding {𝑈, 𝑋} to the edge set, where 𝑋 ≠ 𝑈, yields degree 𝑃 + 1. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Mario Carneiro, 28-Feb-2016.) (Revised by AV, 3-Mar-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑈 ∈ 𝑉    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝐼 ∈ Word {𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (♯‘𝑥) ≤ 2}    &   ⊢ ((VtxDeg‘𝐺)‘𝑈) = 𝑃    &   ⊢ (Vtx‘𝐹) = 𝑉    &   ⊢ 𝑋 ∈ 𝑉    &   ⊢ 𝑋 ≠ 𝑈    &   ⊢ (iEdg‘𝐹) = (𝐼 ++ ⟨“{𝑈, 𝑋}”⟩)    ⇒   ⊢ ((VtxDeg‘𝐹)‘𝑈) = (𝑃 + 1)
Theorem	vdegp1ci 29632*	The induction step for a vertex degree calculation, for example in the Königsberg graph. If the degree of 𝑈 in the edge set 𝐸 is 𝑃, then adding {𝑋, 𝑈} to the edge set, where 𝑋 ≠ 𝑈, yields degree 𝑃 + 1. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Mario Carneiro, 28-Feb-2016.) (Revised by AV, 3-Mar-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑈 ∈ 𝑉    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝐼 ∈ Word {𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (♯‘𝑥) ≤ 2}    &   ⊢ ((VtxDeg‘𝐺)‘𝑈) = 𝑃    &   ⊢ (Vtx‘𝐹) = 𝑉    &   ⊢ 𝑋 ∈ 𝑉    &   ⊢ 𝑋 ≠ 𝑈    &   ⊢ (iEdg‘𝐹) = (𝐼 ++ ⟨“{𝑋, 𝑈}”⟩)    ⇒   ⊢ ((VtxDeg‘𝐹)‘𝑈) = (𝑃 + 1)
Theorem	vtxdginducedm1lem1 29633	Lemma 1 for vtxdginducedm1 29637: the edge function in the induced subgraph 𝑆 of a pseudograph 𝐺 obtained by removing one vertex 𝑁. (Contributed by AV, 16-Dec-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (iEdg‘𝐺)    &   ⊢ 𝐾 = (𝑉 ∖ {𝑁})    &   ⊢ 𝐼 = {𝑖 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑖)}    &   ⊢ 𝑃 = (𝐸 ↾ 𝐼)    &   ⊢ 𝑆 = ⟨𝐾, 𝑃⟩    ⇒   ⊢ (iEdg‘𝑆) = 𝑃
Theorem	vtxdginducedm1lem2 29634*	Lemma 2 for vtxdginducedm1 29637: the domain of the edge function in the induced subgraph 𝑆 of a pseudograph 𝐺 obtained by removing one vertex 𝑁. (Contributed by AV, 16-Dec-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (iEdg‘𝐺)    &   ⊢ 𝐾 = (𝑉 ∖ {𝑁})    &   ⊢ 𝐼 = {𝑖 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑖)}    &   ⊢ 𝑃 = (𝐸 ↾ 𝐼)    &   ⊢ 𝑆 = ⟨𝐾, 𝑃⟩    ⇒   ⊢ dom (iEdg‘𝑆) = 𝐼
Theorem	vtxdginducedm1lem3 29635*	Lemma 3 for vtxdginducedm1 29637: an edge in the induced subgraph 𝑆 of a pseudograph 𝐺 obtained by removing one vertex 𝑁. (Contributed by AV, 16-Dec-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (iEdg‘𝐺)    &   ⊢ 𝐾 = (𝑉 ∖ {𝑁})    &   ⊢ 𝐼 = {𝑖 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑖)}    &   ⊢ 𝑃 = (𝐸 ↾ 𝐼)    &   ⊢ 𝑆 = ⟨𝐾, 𝑃⟩    ⇒   ⊢ (𝐻 ∈ 𝐼 → ((iEdg‘𝑆)‘𝐻) = (𝐸‘𝐻))
Theorem	vtxdginducedm1lem4 29636*	Lemma 4 for vtxdginducedm1 29637. (Contributed by AV, 17-Dec-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (iEdg‘𝐺)    &   ⊢ 𝐾 = (𝑉 ∖ {𝑁})    &   ⊢ 𝐼 = {𝑖 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑖)}    &   ⊢ 𝑃 = (𝐸 ↾ 𝐼)    &   ⊢ 𝑆 = ⟨𝐾, 𝑃⟩    &   ⊢ 𝐽 = {𝑖 ∈ dom 𝐸 ∣ 𝑁 ∈ (𝐸‘𝑖)}    ⇒   ⊢ (𝑊 ∈ (𝑉 ∖ {𝑁}) → (♯‘{𝑘 ∈ 𝐽 ∣ (𝐸‘𝑘) = {𝑊}}) = 0)
Theorem	vtxdginducedm1 29637*	The degree of a vertex 𝑣 in the induced subgraph 𝑆 of a pseudograph 𝐺 obtained by removing one vertex 𝑁 plus the number of edges joining the vertex 𝑣 and the vertex 𝑁 is the degree of the vertex 𝑣 in the pseudograph 𝐺. (Contributed by AV, 17-Dec-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (iEdg‘𝐺)    &   ⊢ 𝐾 = (𝑉 ∖ {𝑁})    &   ⊢ 𝐼 = {𝑖 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑖)}    &   ⊢ 𝑃 = (𝐸 ↾ 𝐼)    &   ⊢ 𝑆 = ⟨𝐾, 𝑃⟩    &   ⊢ 𝐽 = {𝑖 ∈ dom 𝐸 ∣ 𝑁 ∈ (𝐸‘𝑖)}    ⇒   ⊢ ∀𝑣 ∈ (𝑉 ∖ {𝑁})((VtxDeg‘𝐺)‘𝑣) = (((VtxDeg‘𝑆)‘𝑣) +𝑒 (♯‘{𝑙 ∈ 𝐽 ∣ 𝑣 ∈ (𝐸‘𝑙)}))
Theorem	vtxdginducedm1fi 29638*	The degree of a vertex 𝑣 in the induced subgraph 𝑆 of a pseudograph 𝐺 of finite size obtained by removing one vertex 𝑁 plus the number of edges joining the vertex 𝑣 and the vertex 𝑁 is the degree of the vertex 𝑣 in the pseudograph 𝐺. (Contributed by AV, 18-Dec-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (iEdg‘𝐺)    &   ⊢ 𝐾 = (𝑉 ∖ {𝑁})    &   ⊢ 𝐼 = {𝑖 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑖)}    &   ⊢ 𝑃 = (𝐸 ↾ 𝐼)    &   ⊢ 𝑆 = ⟨𝐾, 𝑃⟩    &   ⊢ 𝐽 = {𝑖 ∈ dom 𝐸 ∣ 𝑁 ∈ (𝐸‘𝑖)}    ⇒   ⊢ (𝐸 ∈ Fin → ∀𝑣 ∈ (𝑉 ∖ {𝑁})((VtxDeg‘𝐺)‘𝑣) = (((VtxDeg‘𝑆)‘𝑣) + (♯‘{𝑙 ∈ 𝐽 ∣ 𝑣 ∈ (𝐸‘𝑙)})))
Theorem	finsumvtxdg2ssteplem1 29639*	Lemma for finsumvtxdg2sstep 29643. (Contributed by AV, 15-Dec-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (iEdg‘𝐺)    &   ⊢ 𝐾 = (𝑉 ∖ {𝑁})    &   ⊢ 𝐼 = {𝑖 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑖)}    &   ⊢ 𝑃 = (𝐸 ↾ 𝐼)    &   ⊢ 𝑆 = ⟨𝐾, 𝑃⟩    &   ⊢ 𝐽 = {𝑖 ∈ dom 𝐸 ∣ 𝑁 ∈ (𝐸‘𝑖)}    ⇒   ⊢ (((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ (𝑉 ∈ Fin ∧ 𝐸 ∈ Fin)) → (♯‘𝐸) = ((♯‘𝑃) + (♯‘𝐽)))
Theorem	finsumvtxdg2ssteplem2 29640*	Lemma for finsumvtxdg2sstep 29643. (Contributed by AV, 12-Dec-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (iEdg‘𝐺)    &   ⊢ 𝐾 = (𝑉 ∖ {𝑁})    &   ⊢ 𝐼 = {𝑖 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑖)}    &   ⊢ 𝑃 = (𝐸 ↾ 𝐼)    &   ⊢ 𝑆 = ⟨𝐾, 𝑃⟩    &   ⊢ 𝐽 = {𝑖 ∈ dom 𝐸 ∣ 𝑁 ∈ (𝐸‘𝑖)}    ⇒   ⊢ (((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ (𝑉 ∈ Fin ∧ 𝐸 ∈ Fin)) → ((VtxDeg‘𝐺)‘𝑁) = ((♯‘𝐽) + (♯‘{𝑖 ∈ dom 𝐸 ∣ (𝐸‘𝑖) = {𝑁}})))
Theorem	finsumvtxdg2ssteplem3 29641*	Lemma for finsumvtxdg2sstep 29643. (Contributed by AV, 19-Dec-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (iEdg‘𝐺)    &   ⊢ 𝐾 = (𝑉 ∖ {𝑁})    &   ⊢ 𝐼 = {𝑖 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑖)}    &   ⊢ 𝑃 = (𝐸 ↾ 𝐼)    &   ⊢ 𝑆 = ⟨𝐾, 𝑃⟩    &   ⊢ 𝐽 = {𝑖 ∈ dom 𝐸 ∣ 𝑁 ∈ (𝐸‘𝑖)}    ⇒   ⊢ (((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ (𝑉 ∈ Fin ∧ 𝐸 ∈ Fin)) → (Σ𝑣 ∈ (𝑉 ∖ {𝑁})(♯‘{𝑖 ∈ 𝐽 ∣ 𝑣 ∈ (𝐸‘𝑖)}) + (♯‘{𝑖 ∈ dom 𝐸 ∣ (𝐸‘𝑖) = {𝑁}})) = (♯‘𝐽))
Theorem	finsumvtxdg2ssteplem4 29642*	Lemma for finsumvtxdg2sstep 29643. (Contributed by AV, 12-Dec-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (iEdg‘𝐺)    &   ⊢ 𝐾 = (𝑉 ∖ {𝑁})    &   ⊢ 𝐼 = {𝑖 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑖)}    &   ⊢ 𝑃 = (𝐸 ↾ 𝐼)    &   ⊢ 𝑆 = ⟨𝐾, 𝑃⟩    &   ⊢ 𝐽 = {𝑖 ∈ dom 𝐸 ∣ 𝑁 ∈ (𝐸‘𝑖)}    ⇒   ⊢ ((((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ (𝑉 ∈ Fin ∧ 𝐸 ∈ Fin)) ∧ Σ𝑣 ∈ 𝐾 ((VtxDeg‘𝑆)‘𝑣) = (2 · (♯‘𝑃))) → (Σ𝑣 ∈ (𝑉 ∖ {𝑁})((VtxDeg‘𝐺)‘𝑣) + ((♯‘𝐽) + (♯‘{𝑖 ∈ dom 𝐸 ∣ (𝐸‘𝑖) = {𝑁}}))) = (2 · ((♯‘𝑃) + (♯‘𝐽))))
Theorem	finsumvtxdg2sstep 29643*	Induction step of finsumvtxdg2size 29644: In a finite pseudograph of finite size, the sum of the degrees of all vertices of the pseudograph is twice the size of the pseudograph if the sum of the degrees of all vertices of the subgraph of the pseudograph not containing one of the vertices is twice the size of the subgraph. (Contributed by AV, 19-Dec-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (iEdg‘𝐺)    &   ⊢ 𝐾 = (𝑉 ∖ {𝑁})    &   ⊢ 𝐼 = {𝑖 ∈ dom 𝐸 ∣ 𝑁 ∉ (𝐸‘𝑖)}    &   ⊢ 𝑃 = (𝐸 ↾ 𝐼)    &   ⊢ 𝑆 = ⟨𝐾, 𝑃⟩    ⇒   ⊢ (((𝐺 ∈ UPGraph ∧ 𝑁 ∈ 𝑉) ∧ (𝑉 ∈ Fin ∧ 𝐸 ∈ Fin)) → ((𝑃 ∈ Fin → Σ𝑣 ∈ 𝐾 ((VtxDeg‘𝑆)‘𝑣) = (2 · (♯‘𝑃))) → Σ𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = (2 · (♯‘𝐸))))
Theorem	finsumvtxdg2size 29644*	The sum of the degrees of all vertices of a finite pseudograph of finite size is twice the size of the pseudograph. See equation (1) in section I.1 in [Bollobas] p. 4. Here, the "proof" is simply the statement "Since each edge has two endvertices, the sum of the degrees is exactly twice the number of edges". The formal proof of this theorem (for pseudographs) is much more complicated, taking also the used auxiliary theorems into account. The proof for a (finite) simple graph (see fusgr1th 29645) would be shorter, but nevertheless still laborious. Although this theorem would hold also for infinite pseudographs and pseudographs of infinite size, the proof of this most general version (see theorem "sumvtxdg2size" below) would require many more auxiliary theorems (e.g., the extension of the sum Σ over an arbitrary set). I dedicate this theorem and its proof to Norman Megill, who deceased too early on December 9, 2021. This proof is an example for the rigor which was the main motivation for Norman Megill to invent and develop Metamath, see section 1.1.6 "Rigor" on page 19 of the Metamath book: "... it is usually assumed in mathematical literature that the person reading the proof is a mathematician familiar with the specialty being described, and that the missing steps are obvious to such a reader or at least the reader is capable of filling them in." I filled in the missing steps of Bollobas' proof as Norm would have liked it... (Contributed by Alexander van der Vekens, 19-Dec-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝐷 = (VtxDeg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UPGraph ∧ 𝑉 ∈ Fin ∧ 𝐼 ∈ Fin) → Σ𝑣 ∈ 𝑉 (𝐷‘𝑣) = (2 · (♯‘𝐼)))
Theorem	fusgr1th 29645*	The sum of the degrees of all vertices of a finite simple graph is twice the size of the graph. See equation (1) in section I.1 in [Bollobas] p. 4. Also known as the "First Theorem of Graph Theory" (see https://charlesreid1.com/wiki/First_Theorem_of_Graph_Theory). (Contributed by AV, 26-Dec-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝐷 = (VtxDeg‘𝐺)    ⇒   ⊢ (𝐺 ∈ FinUSGraph → Σ𝑣 ∈ 𝑉 (𝐷‘𝑣) = (2 · (♯‘𝐼)))
Theorem	finsumvtxdgeven 29646*	The sum of the degrees of all vertices of a finite pseudograph of finite size is even. See equation (2) in section I.1 in [Bollobas] p. 4, where it is also called the handshaking lemma. (Contributed by AV, 22-Dec-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝐷 = (VtxDeg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UPGraph ∧ 𝑉 ∈ Fin ∧ 𝐼 ∈ Fin) → 2 ∥ Σ𝑣 ∈ 𝑉 (𝐷‘𝑣))
Theorem	vtxdgoddnumeven 29647*	The number of vertices of odd degree is even in a finite pseudograph of finite size. Proposition 1.2.1 in [Diestel] p. 5. See also remark about equation (2) in section I.1 in [Bollobas] p. 4. (Contributed by AV, 22-Dec-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝐷 = (VtxDeg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UPGraph ∧ 𝑉 ∈ Fin ∧ 𝐼 ∈ Fin) → 2 ∥ (♯‘{𝑣 ∈ 𝑉 ∣ ¬ 2 ∥ (𝐷‘𝑣)}))
Theorem	fusgrvtxdgonume 29648*	The number of vertices of odd degree is even in a finite simple graph. Proposition 1.2.1 in [Diestel] p. 5. See also remark about equation (2) in section I.1 in [Bollobas] p. 4. (Contributed by AV, 27-Dec-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝐷 = (VtxDeg‘𝐺)    ⇒   ⊢ (𝐺 ∈ FinUSGraph → 2 ∥ (♯‘{𝑣 ∈ 𝑉 ∣ ¬ 2 ∥ (𝐷‘𝑣)}))
17.2.11  Regular graphs With df-rgr 29651 and df-rusgr 29652, k-regularity of a (simple) graph is defined as predicate RegGraph resp. RegUSGraph. Instead of defining a predicate, an alternative could have been to define a function that maps an extended nonnegative integer to the class of "graphs" in which every vertex has the extended nonnegative integer as degree: RegGraph = (𝑘 ∈ ℕ0* ↦ {𝑔 ∣ ∀𝑣 ∈ (Vtx‘𝑔)((VtxDeg‘𝑔)‘𝑣) = 𝑘}). This function, however, would not be defined at least for 𝑘 = 0 (see rgrx0nd 29688), because {𝑔 ∣ ∀𝑣 ∈ (Vtx‘𝑔)((VtxDeg‘𝑔)‘𝑣) = 0} is not a set (see rgrprcx 29686). It is expected that this function is not defined for every 𝑘 ∈ ℕ0* (how could this be proven?).
Syntax	crgr 29649	Extend class notation to include the class of all regular graphs.
class RegGraph
Syntax	crusgr 29650	Extend class notation to include the class of all regular simple graphs.
class RegUSGraph
Definition	df-rgr 29651*	Define the "k-regular" predicate, which is true for a "graph" being k-regular: read 𝐺 RegGraph 𝐾 as "𝐺 is 𝐾-regular" or "𝐺 is a 𝐾-regular graph". Note that 𝐾 is allowed to be positive infinity (𝐾 ∈ ℕ0*), as proposed by GL. (Contributed by Alexander van der Vekens, 6-Jul-2018.) (Revised by AV, 26-Dec-2020.)
⊢ RegGraph = {⟨𝑔, 𝑘⟩ ∣ (𝑘 ∈ ℕ0* ∧ ∀𝑣 ∈ (Vtx‘𝑔)((VtxDeg‘𝑔)‘𝑣) = 𝑘)}
Definition	df-rusgr 29652*	Define the "k-regular simple graph" predicate, which is true for a simple graph being k-regular: read 𝐺 RegUSGraph 𝐾 as 𝐺 is a 𝐾-regular simple graph. (Contributed by Alexander van der Vekens, 6-Jul-2018.) (Revised by AV, 18-Dec-2020.)
⊢ RegUSGraph = {⟨𝑔, 𝑘⟩ ∣ (𝑔 ∈ USGraph ∧ 𝑔 RegGraph 𝑘)}
Theorem	isrgr 29653*	The property of a class being a k-regular graph. (Contributed by Alexander van der Vekens, 7-Jul-2018.) (Revised by AV, 26-Dec-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐷 = (VtxDeg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ 𝑊 ∧ 𝐾 ∈ 𝑍) → (𝐺 RegGraph 𝐾 ↔ (𝐾 ∈ ℕ0* ∧ ∀𝑣 ∈ 𝑉 (𝐷‘𝑣) = 𝐾)))
Theorem	rgrprop 29654*	The properties of a k-regular graph. (Contributed by Alexander van der Vekens, 8-Jul-2018.) (Revised by AV, 26-Dec-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐷 = (VtxDeg‘𝐺)    ⇒   ⊢ (𝐺 RegGraph 𝐾 → (𝐾 ∈ ℕ0* ∧ ∀𝑣 ∈ 𝑉 (𝐷‘𝑣) = 𝐾))
Theorem	isrusgr 29655	The property of being a k-regular simple graph. (Contributed by Alexander van der Vekens, 7-Jul-2018.) (Revised by AV, 18-Dec-2020.)
⊢ ((𝐺 ∈ 𝑊 ∧ 𝐾 ∈ 𝑍) → (𝐺 RegUSGraph 𝐾 ↔ (𝐺 ∈ USGraph ∧ 𝐺 RegGraph 𝐾)))
Theorem	rusgrprop 29656	The properties of a k-regular simple graph. (Contributed by Alexander van der Vekens, 8-Jul-2018.) (Revised by AV, 18-Dec-2020.)
⊢ (𝐺 RegUSGraph 𝐾 → (𝐺 ∈ USGraph ∧ 𝐺 RegGraph 𝐾))
Theorem	rusgrrgr 29657	A k-regular simple graph is a k-regular graph. (Contributed by Alexander van der Vekens, 8-Jul-2018.) (Revised by AV, 18-Dec-2020.)
⊢ (𝐺 RegUSGraph 𝐾 → 𝐺 RegGraph 𝐾)
Theorem	rusgrusgr 29658	A k-regular simple graph is a simple graph. (Contributed by Alexander van der Vekens, 8-Jul-2018.) (Revised by AV, 18-Dec-2020.)
⊢ (𝐺 RegUSGraph 𝐾 → 𝐺 ∈ USGraph)
Theorem	finrusgrfusgr 29659	A finite regular simple graph is a finite simple graph. (Contributed by AV, 3-Jun-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝐺 RegUSGraph 𝐾 ∧ 𝑉 ∈ Fin) → 𝐺 ∈ FinUSGraph)
Theorem	isrusgr0 29660*	The property of being a k-regular simple graph. (Contributed by Alexander van der Vekens, 7-Jul-2018.) (Revised by AV, 26-Dec-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐷 = (VtxDeg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ 𝑊 ∧ 𝐾 ∈ 𝑍) → (𝐺 RegUSGraph 𝐾 ↔ (𝐺 ∈ USGraph ∧ 𝐾 ∈ ℕ0* ∧ ∀𝑣 ∈ 𝑉 (𝐷‘𝑣) = 𝐾)))
Theorem	rusgrprop0 29661*	The properties of a k-regular simple graph. (Contributed by Alexander van der Vekens, 8-Jul-2018.) (Revised by AV, 26-Dec-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐷 = (VtxDeg‘𝐺)    ⇒   ⊢ (𝐺 RegUSGraph 𝐾 → (𝐺 ∈ USGraph ∧ 𝐾 ∈ ℕ0* ∧ ∀𝑣 ∈ 𝑉 (𝐷‘𝑣) = 𝐾))
Theorem	usgreqdrusgr 29662*	If all vertices in a simple graph have the same degree, the graph is k-regular. (Contributed by AV, 26-Dec-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐷 = (VtxDeg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ USGraph ∧ 𝐾 ∈ ℕ0* ∧ ∀𝑣 ∈ 𝑉 (𝐷‘𝑣) = 𝐾) → 𝐺 RegUSGraph 𝐾)
Theorem	fusgrregdegfi 29663*	In a nonempty finite simple graph, the degree of each vertex is finite. (Contributed by Alexander van der Vekens, 6-Mar-2018.) (Revised by AV, 19-Dec-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐷 = (VtxDeg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅) → (∀𝑣 ∈ 𝑉 (𝐷‘𝑣) = 𝐾 → 𝐾 ∈ ℕ0))
Theorem	fusgrn0eqdrusgr 29664*	If all vertices in a nonempty finite simple graph have the same (finite) degree, the graph is k-regular. (Contributed by AV, 26-Dec-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐷 = (VtxDeg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅) → (∀𝑣 ∈ 𝑉 (𝐷‘𝑣) = 𝐾 → 𝐺 RegUSGraph 𝐾))
Theorem	frusgrnn0 29665	In a nonempty finite k-regular simple graph, the degree of each vertex is finite. (Contributed by AV, 7-May-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝐺 ∈ FinUSGraph ∧ 𝐺 RegUSGraph 𝐾 ∧ 𝑉 ≠ ∅) → 𝐾 ∈ ℕ0)
Theorem	0edg0rgr 29666	A graph is 0-regular if it has no edges. (Contributed by Alexander van der Vekens, 8-Jul-2018.) (Revised by AV, 26-Dec-2020.)
⊢ ((𝐺 ∈ 𝑊 ∧ (iEdg‘𝐺) = ∅) → 𝐺 RegGraph 0)
Theorem	uhgr0edg0rgr 29667	A hypergraph is 0-regular if it has no edges. (Contributed by AV, 19-Dec-2020.)
⊢ ((𝐺 ∈ UHGraph ∧ (Edg‘𝐺) = ∅) → 𝐺 RegGraph 0)
Theorem	uhgr0edg0rgrb 29668	A hypergraph is 0-regular iff it has no edges. (Contributed by Alexander van der Vekens, 12-Jul-2018.) (Revised by AV, 24-Dec-2020.)
⊢ (𝐺 ∈ UHGraph → (𝐺 RegGraph 0 ↔ (Edg‘𝐺) = ∅))
Theorem	usgr0edg0rusgr 29669	A simple graph is 0-regular iff it has no edges. (Contributed by Alexander van der Vekens, 12-Jul-2018.) (Revised by AV, 19-Dec-2020.) (Proof shortened by AV, 24-Dec-2020.)
⊢ (𝐺 ∈ USGraph → (𝐺 RegUSGraph 0 ↔ (Edg‘𝐺) = ∅))
Theorem	0vtxrgr 29670*	A null graph (with no vertices) is k-regular for every k. (Contributed by Alexander van der Vekens, 10-Jul-2018.) (Revised by AV, 26-Dec-2020.)
⊢ ((𝐺 ∈ 𝑊 ∧ (Vtx‘𝐺) = ∅) → ∀𝑘 ∈ ℕ0* 𝐺 RegGraph 𝑘)
Theorem	0vtxrusgr 29671*	A graph with no vertices and an empty edge function is a k-regular simple graph for every k. (Contributed by Alexander van der Vekens, 10-Jul-2018.) (Revised by AV, 26-Dec-2020.)
⊢ ((𝐺 ∈ 𝑊 ∧ (Vtx‘𝐺) = ∅ ∧ (iEdg‘𝐺) = ∅) → ∀𝑘 ∈ ℕ0* 𝐺 RegUSGraph 𝑘)
Theorem	0uhgrrusgr 29672*	The null graph as hypergraph is a k-regular simple graph for every k. (Contributed by Alexander van der Vekens, 10-Jul-2018.) (Revised by AV, 26-Dec-2020.)
⊢ ((𝐺 ∈ UHGraph ∧ (Vtx‘𝐺) = ∅) → ∀𝑘 ∈ ℕ0* 𝐺 RegUSGraph 𝑘)
Theorem	0grrusgr 29673	The null graph represented by an empty set is a k-regular simple graph for every k. (Contributed by AV, 26-Dec-2020.)
⊢ ∀𝑘 ∈ ℕ0* ∅ RegUSGraph 𝑘
Theorem	0grrgr 29674	The null graph represented by an empty set is k-regular for every k. (Contributed by AV, 26-Dec-2020.)
⊢ ∀𝑘 ∈ ℕ0* ∅ RegGraph 𝑘
Theorem	cusgrrusgr 29675	A complete simple graph with n vertices (at least one) is (n-1)-regular. (Contributed by Alexander van der Vekens, 10-Jul-2018.) (Revised by AV, 26-Dec-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝐺 ∈ ComplUSGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → 𝐺 RegUSGraph ((♯‘𝑉) − 1))
Theorem	cusgrm1rusgr 29676	A finite simple graph with n vertices is complete iff it is (n-1)-regular. Hint: If the definition of RegGraph was allowed for 𝑘 ∈ ℤ, then the assumption 𝑉 ≠ ∅ could be removed. (Contributed by Alexander van der Vekens, 14-Jul-2018.) (Revised by AV, 26-Dec-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅) → (𝐺 ∈ ComplUSGraph ↔ 𝐺 RegUSGraph ((♯‘𝑉) − 1)))
Theorem	rusgrpropnb 29677*	The properties of a k-regular simple graph expressed with neighbors. (Contributed by Alexander van der Vekens, 26-Jul-2018.) (Revised by AV, 26-Dec-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (𝐺 RegUSGraph 𝐾 → (𝐺 ∈ USGraph ∧ 𝐾 ∈ ℕ0* ∧ ∀𝑣 ∈ 𝑉 (♯‘(𝐺 NeighbVtx 𝑣)) = 𝐾))
Theorem	rusgrpropedg 29678*	The properties of a k-regular simple graph expressed with edges. (Contributed by AV, 23-Dec-2020.) (Revised by AV, 27-Dec-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (𝐺 RegUSGraph 𝐾 → (𝐺 ∈ USGraph ∧ 𝐾 ∈ ℕ0* ∧ ∀𝑣 ∈ 𝑉 (♯‘{𝑒 ∈ (Edg‘𝐺) ∣ 𝑣 ∈ 𝑒}) = 𝐾))
Theorem	rusgrpropadjvtx 29679*	The properties of a k-regular simple graph expressed with adjacent vertices. (Contributed by Alexander van der Vekens, 26-Jul-2018.) (Revised by AV, 27-Dec-2020.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (𝐺 RegUSGraph 𝐾 → (𝐺 ∈ USGraph ∧ 𝐾 ∈ ℕ0* ∧ ∀𝑣 ∈ 𝑉 (♯‘{𝑘 ∈ 𝑉 ∣ {𝑣, 𝑘} ∈ (Edg‘𝐺)}) = 𝐾))
Theorem	rusgrnumwrdl2 29680*	In a k-regular simple graph, the number of edges resp. walks of length 1 (represented as words of length 2) starting at a fixed vertex is k. (Contributed by Alexander van der Vekens, 28-Jul-2018.) (Revised by AV, 6-May-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝐺 RegUSGraph 𝐾 ∧ 𝑃 ∈ 𝑉) → (♯‘{𝑤 ∈ Word 𝑉 ∣ ((♯‘𝑤) = 2 ∧ (𝑤‘0) = 𝑃 ∧ {(𝑤‘0), (𝑤‘1)} ∈ (Edg‘𝐺))}) = 𝐾)
Theorem	rusgr1vtxlem 29681*	Lemma for rusgr1vtx 29682. (Contributed by AV, 27-Dec-2020.)
⊢ (((∀𝑣 ∈ 𝑉 (♯‘𝐴) = 𝐾 ∧ ∀𝑣 ∈ 𝑉 𝐴 = ∅) ∧ (𝑉 ∈ 𝑊 ∧ (♯‘𝑉) = 1)) → 𝐾 = 0)
Theorem	rusgr1vtx 29682	If a k-regular simple graph has only one vertex, then k must be 0. (Contributed by Alexander van der Vekens, 4-Sep-2018.) (Revised by AV, 27-Dec-2020.)
⊢ (((♯‘(Vtx‘𝐺)) = 1 ∧ 𝐺 RegUSGraph 𝐾) → 𝐾 = 0)
Theorem	rgrusgrprc 29683*	The class of 0-regular simple graphs is a proper class. (Contributed by AV, 27-Dec-2020.)
⊢ {𝑔 ∈ USGraph ∣ ∀𝑣 ∈ (Vtx‘𝑔)((VtxDeg‘𝑔)‘𝑣) = 0} ∉ V
Theorem	rusgrprc 29684	The class of 0-regular simple graphs is a proper class. (Contributed by AV, 27-Dec-2020.)
⊢ {𝑔 ∣ 𝑔 RegUSGraph 0} ∉ V
Theorem	rgrprc 29685	The class of 0-regular graphs is a proper class. (Contributed by AV, 27-Dec-2020.)
⊢ {𝑔 ∣ 𝑔 RegGraph 0} ∉ V
Theorem	rgrprcx 29686*	The class of 0-regular graphs is a proper class. (Contributed by AV, 27-Dec-2020.)
⊢ {𝑔 ∣ ∀𝑣 ∈ (Vtx‘𝑔)((VtxDeg‘𝑔)‘𝑣) = 0} ∉ V
Theorem	rgrx0ndm 29687*	0 is not in the domain of the potentially alternative definition of the sets of k-regular graphs for each extended nonnegative integer k. (Contributed by AV, 28-Dec-2020.)
⊢ 𝑅 = (𝑘 ∈ ℕ0* ↦ {𝑔 ∣ ∀𝑣 ∈ (Vtx‘𝑔)((VtxDeg‘𝑔)‘𝑣) = 𝑘})    ⇒   ⊢ 0 ∉ dom 𝑅
Theorem	rgrx0nd 29688*	The potentially alternatively defined k-regular graphs is not defined for k=0. (Contributed by AV, 28-Dec-2020.)
⊢ 𝑅 = (𝑘 ∈ ℕ0* ↦ {𝑔 ∣ ∀𝑣 ∈ (Vtx‘𝑔)((VtxDeg‘𝑔)‘𝑣) = 𝑘})    ⇒   ⊢ (𝑅‘0) = ∅
17.3  Walks, paths and cycles A "walk" in a graph is usually defined for simple graphs, multigraphs or even pseudographs as "alternating sequence of vertices and edges x0 , e1 , x1 , e2 , ... , e(l) , x(l) where e(i) = x(i-1)x(i), 0<i<=l.", see definition of [Bollobas] p. 4, or "A walk (of length k) in a graph is a nonempty alternating sequence v0 e0 v1 e1 ... e(k-1) vk of vertices and edges in G such that ei = { vi , vi+1 } for all i < k.", see definition of [Diestel] p. 10. Formalizing these definitions (mainly by representing the indexed vertices and edges by functions), a walk is represented by two mappings f from { 1 , ... , n } and p from { 0 , ... , n }, where f enumerates the (indices of the) edges (e is a third function enumerating the edges within the graph, not within the walk), and p enumerates the vertices, see df-wlks 29693. Hence a walk (of length n) is represented by the following sequence: p(0) e(f(1)) p(1) e(f(2)) ... p(n-1) e(f(n)) p(n). Alternatively, one could define a walk as a function 𝑤:(0...(2 · 𝑛))⟶((Edg‘𝐺) ∪ (Vtx‘𝐺)) such that for all 0 ≤ 𝑘 ≤ 𝑛, (𝑤‘(2 · 𝑘)) ∈ (Vtx‘𝐺) and for all 0 ≤ 𝑘 ≤ (𝑛 − 1), (𝑤‘((2 · 𝑘) + 1)) ∈ (Edg‘𝐺) and {(𝑤‘(2 · 𝑘)), (𝑤‘((2 · 𝑘) + 2))} ⊆ (𝑤‘((2 · 𝑘) + 1)). Based on our definition of Walks, the class of all walks, more restrictive constructs are defined: * Trails (df-trls 29784): A "walk is called a trail if all its edges are distinct.", see Definition of [Bollobas] p. 5, i.e., f(i) =/= f(j) if i =/= j. * Paths (df-pths 29807): A path is a walk whose vertices except the first and the last vertex are distinct, i.e., p(i) =/= p(j) if i < j, except possibly when i = 0 and j = n. * SPaths (simple paths, df-spths 29808): A simple path "is a walk with distinct vertices.", see Notation of [Bollobas] p. 5, i.e., p(i) =/= p(j) if i =/= j. * ClWalks (closed walks, df-clwlks 29864): A walk whose endvertices coincide is called a closed walk, i.e., p(0) = p(n). * Circuits (df-crcts 29879): "A trail whose endvertices coincide (a closed trail) is called a circuit." (see Definition of [Bollobas] p. 5), i.e., f(i) =/= f(j) if i =/= j and p(0) = p(n). Equivalently, a circuit is a closed walk with distinct edges. * Cycles (df-cycls 29880): A path whose endvertices coincide (a closed path) is called a cycle, i.e., p(i) =/= p(j) if i =/= j, except i = 0 and j = n, and p(0) = p(n). Equivalently, a cycle is a closed walk with distinct vertices. * EulerPaths (Eulerian paths, df-eupth 30293): An Eulerian path is "a trail containing all edges [of the graph]" (see definition in [Bollobas] p. 16), i.e., f(i) =/= f(j) if i =/= j and for all edges e(x) there is an 1 <= i <= n with e(x) = e(f(i)). Note, however, that an Eulerian path needs not be a path. * Eulerian circuit: An Eulerian circuit (called Euler tour in the definition in [Diestel] p. 22) is "a circuit in a graph containing all the edges" (see definition in [Bollobas] p. 16), i.e., f(i) =/= f(j) if i =/= j, p(0) = p(n) and for all edges e(x) there is an 1 <= i <= n with e(x) = e(f(i)). Hierarchy of all kinds of walks (apply ssriv 3926 and elopabran 5510 to the mentioned theorems to obtain the following subset relationships, as available for clwlkiswlk 29867, see clwlkwlk 29868 and clwlkswks 29869): * Trails are walks (trliswlk 29789): (Trails‘𝐺) ⊆ (Walks‘𝐺) * Paths are trails (pthistrl 29816): (Paths‘𝐺) ⊆ (Trails‘𝐺) * Simple paths are paths (spthispth 29817): (SPaths‘𝐺) ⊆ (Paths‘𝐺) * Closed walks are walks (clwlkiswlk 29867): (ClWalks‘𝐺) ⊆ (Walks‘𝐺) * Circuits are closed walks (crctisclwlk 29887): (Circuits‘𝐺) ⊆ (ClWalks‘𝐺) * Circuits are trails (crctistrl 29888): (Circuits‘𝐺) ⊆ (Trails‘𝐺) * Cycles are paths (cyclispth 29890): (Cycles‘𝐺) ⊆ (Paths‘𝐺) * Cycles are circuits (cycliscrct 29892): (Cycles‘𝐺) ⊆ (Circuits‘𝐺) * (Non-trivial) cycles are not simple paths (cyclnspth 29894): (𝐹 ≠ ∅ → (𝐹(Cycles‘𝐺)𝑃 → ¬ 𝐹(SPaths‘𝐺)𝑃)) * Eulerian paths are trails (eupthistrl 30306): (EulerPaths‘𝐺) ⊆ (Trails‘𝐺) Often, it is sufficient to refer to a walk by the natural sequence of its vertices, i.e., omitting its edges in its representation: p(0) p(1) ... p(n-1) p(n), see the corresponding remark in [Diestel] p. 6. The concept of a Word, see df-word 14474, is the appropriate way to define such a sequence (being finite and starting at index 0) of vertices. Therefore, it is used in definition df-wwlks 29923 for WWalks, and the representation of a walk as sequence of its vertices is called "walk as word". Only for simple pseudographs, however, the edges can be uniquely reconstructed from such a representation. In this case, the general definitions of walks and the definition of walks as words are equivalent, see wlkiswwlks 29969. In other cases, there could be more than one edge between two adjacent vertices in the walk (in a multigraph), or two adjacent vertices could be connected by two different hyperedges involving additional vertices (in a hypergraph). Based on this definition of WWalks, the class of all walks as word, more restrictive constructs are defined analogously to the general definition of a walk: * WWalksN (walks of length N as word, df-wwlksn 29924): n = N * WSPathsN (simple paths of length N as word, df-wspthsn 29926): p(i) =/= p(j) if i =/= j and n = N * ClWWalks (closed walks as word, df-clwwlk 30077): p(0) = p(n) * ClWWalksN (closed walks of length N as word, df-clwwlkn 30120): p(0) = p(n) and n = N Finally, there are a couple of definitions for (special) walks ⟨𝐹, 𝑃⟩ having fixed endpoints 𝐴 and 𝐵: * Walks with particular endpoints (df-wlkson 29694): 𝐹(𝐴(WalksOn‘𝐺)𝐵)𝑃 * Trails with particular endpoints (df-trlson 29785): 𝐹(𝐴(TrailsOn‘𝐺)𝐵)𝑃 * Paths with particular endpoints (df-pthson 29809): 𝐹(𝐴(PathsOn‘𝐺)𝐵)𝑃 * Simple paths with particular endpoints (df-spthson 29810): 𝐹(𝐴(SPathsOn‘𝐺)𝐵)𝑃 * Walks of a fixed length 𝑁 as words with particular endpoints (df-wwlksnon 29925): (𝐴(𝑁 WWalksNOn 𝐺)𝐵) * Simple paths of a fixed length 𝑁 as words with particular endpoints (df-wspthsnon 29927): (𝐴(𝑁 WSPathsNOn 𝐺)𝐵) * Closed Walks of a fixed length 𝑁 as words anchored at a particular vertex 𝐴 (df-wwlksnon 29925): (𝐴(ClWWalksNOn‘𝐺)𝑁)
17.3.1  Walks A "walk" within a graph is usually defined for simple graphs, multigraphs or even pseudographs as "alternating sequence of vertices and edges x0 , e1 , x1 , e2 , ... , e(l) , x(l) where e(i) = x(i-1)x(i), 0<i<=l.", see Definition of [Bollobas] p. 4. This definition requires the edges to connect two vertices at most (loops are also allowed: if e(i) is a loop, then x(i-1) = x(i)). For hypergraphs containing hyperedges (i.e. edges connecting more than two vertices), however, a more general definition is needed. Two approaches for a definition applicable for arbitrary hypergraphs are used in the literature: "walks on the vertex level" and "walks on the edge level" (see Aksoy, Joslyn, Marrero, Praggastis, Purvine: "Hypernetwork science via high-order hypergraph walks", June 2020, https://doi.org/10.1140/epjds/s13688-020-00231-0): "walks on the edge level": For a positive integer s, an s-walk of length k between hyperedges f and g is a sequence of hyperedges, f=e(0), e(1), ... , e(k)=g, where for j=1, ... , k, e(j-1) =/= e(j) and e(j-1) and e(j) have at least s vertices in common (according to Aksoy et al.). "walks on the vertex level": For a positive integer s, an s-walk of length k between vertices a and b is a sequence of vertices, a=v(0), v(1), ... , v(k)=b, where for j=1, ... , k, v(j-1) and v(j) are connected by at least s edges (analogous to Aksoy et al.). There are two imperfections for the definition for "walks on the edge level": one is that a walk of length 1 consists of two edges (or a walk of length 0 consists of one edge), whereas a walk of length 1 on the vertex level consists of two vertices and one edge (or a walk of length 0 consists of one vertex and no edge). The other is that edges, especially loops, can be traversed only once (and not repeatedly) because of the condition e(j-1) =/= e(j). The latter is avoided in the definition for EdgWalks, see df-ewlks 29692. To be compatible with the (usual) definition of walks for pseudographs, walks also suitable for arbitrary hypergraphs are defined "on the vertex level" in the following as Walks, see df-wlks 29693, restricting s to 1. wlk1ewlk 29733 shows that such a 1-walk "on the vertex level" induces a 1-walk "on the edge level".
Syntax	cewlks 29689	Extend class notation with s-walks "on the edge level" (of a hypergraph).
class EdgWalks
Syntax	cwlks 29690	Extend class notation with walks (i.e. 1-walks) (of a hypergraph).
class Walks
Syntax	cwlkson 29691	Extend class notation with walks between two vertices (within a graph).
class WalksOn
Definition	df-ewlks 29692*	Define the set of all s-walks of edges (in a hypergraph) corresponding to s-walks "on the edge level" discussed in Aksoy et al. For an extended nonnegative integer s, an s-walk is a sequence of hyperedges, e(0), e(1), ... , e(k), where e(j-1) and e(j) have at least s vertices in common (for j=1, ... , k). In contrast to the definition in Aksoy et al., 𝑠 = 0 (a 0-walk is an arbitrary sequence of hyperedges) and 𝑠 = +∞ (then the number of common vertices of two adjacent hyperedges must be infinite) are allowed. Furthermore, it is not forbidden that adjacent hyperedges are equal. (Contributed by AV, 4-Jan-2021.)
⊢ EdgWalks = (𝑔 ∈ V, 𝑠 ∈ ℕ0* ↦ {𝑓 ∣ [(iEdg‘𝑔) / 𝑖](𝑓 ∈ Word dom 𝑖 ∧ ∀𝑘 ∈ (1..^(♯‘𝑓))𝑠 ≤ (♯‘((𝑖‘(𝑓‘(𝑘 − 1))) ∩ (𝑖‘(𝑓‘𝑘)))))})
Definition	df-wlks 29693*	Define the set of all walks (in a hypergraph). Such walks correspond to the s-walks "on the vertex level" (with s = 1), and also to 1-walks "on the edge level" (see wlk1walk 29732) discussed in Aksoy et al. The predicate 𝐹(Walks‘𝐺)𝑃 can be read as "The pair ⟨𝐹, 𝑃⟩ represents a walk in a graph 𝐺", see also iswlk 29704. The condition {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))} ⊆ ((iEdg‘𝑔)‘(𝑓‘𝑘)) (hereinafter referred to as C) would not be sufficient, because the repetition of a vertex in a walk (i.e. (𝑝‘𝑘) = (𝑝‘(𝑘 + 1)) should be allowed only if there is a loop at (𝑝‘𝑘). Otherwise, C would be fulfilled by each edge containing (𝑝‘𝑘). According to the definition of [Bollobas] p. 4.: "A walk W in a graph is an alternating sequence of vertices and edges x0 , e1 , x1 , e2 , ... , e(l) , x(l) ...", a walk can be represented by two mappings f from { 1 , ... , n } and p from { 0 , ... , n }, where f enumerates the (indices of the) edges, and p enumerates the vertices. So the walk is 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 AV, 30-Dec-2020.)
⊢ Walks = (𝑔 ∈ V ↦ {⟨𝑓, 𝑝⟩ ∣ (𝑓 ∈ Word dom (iEdg‘𝑔) ∧ 𝑝:(0...(♯‘𝑓))⟶(Vtx‘𝑔) ∧ ∀𝑘 ∈ (0..^(♯‘𝑓))if-((𝑝‘𝑘) = (𝑝‘(𝑘 + 1)), ((iEdg‘𝑔)‘(𝑓‘𝑘)) = {(𝑝‘𝑘)}, {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))} ⊆ ((iEdg‘𝑔)‘(𝑓‘𝑘))))})
Definition	df-wlkson 29694*	Define the collection of walks with particular endpoints (in a hypergraph). The predicate 𝐹(𝐴(WalksOn‘𝐺)𝐵)𝑃 can be read as "The pair ⟨𝐹, 𝑃⟩ represents a walk from vertex 𝐴 to vertex 𝐵 in a graph 𝐺", see also iswlkon 29749. This corresponds to the "x0-x(l)-walks", see Definition in [Bollobas] p. 5. (Contributed by Alexander van der Vekens and Mario Carneiro, 4-Oct-2017.) (Revised by AV, 28-Dec-2020.)
⊢ WalksOn = (𝑔 ∈ V ↦ (𝑎 ∈ (Vtx‘𝑔), 𝑏 ∈ (Vtx‘𝑔) ↦ {⟨𝑓, 𝑝⟩ ∣ (𝑓(Walks‘𝑔)𝑝 ∧ (𝑝‘0) = 𝑎 ∧ (𝑝‘(♯‘𝑓)) = 𝑏)}))
Theorem	ewlksfval 29695*	The set of s-walks of edges (in a hypergraph). (Contributed by AV, 4-Jan-2021.)
⊢ 𝐼 = (iEdg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ 𝑊 ∧ 𝑆 ∈ ℕ0*) → (𝐺 EdgWalks 𝑆) = {𝑓 ∣ (𝑓 ∈ Word dom 𝐼 ∧ ∀𝑘 ∈ (1..^(♯‘𝑓))𝑆 ≤ (♯‘((𝐼‘(𝑓‘(𝑘 − 1))) ∩ (𝐼‘(𝑓‘𝑘)))))})
Theorem	isewlk 29696*	Conditions for a function (sequence of hyperedges) to be an s-walk of edges. (Contributed by AV, 4-Jan-2021.)
⊢ 𝐼 = (iEdg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ 𝑊 ∧ 𝑆 ∈ ℕ0* ∧ 𝐹 ∈ 𝑈) → (𝐹 ∈ (𝐺 EdgWalks 𝑆) ↔ (𝐹 ∈ Word dom 𝐼 ∧ ∀𝑘 ∈ (1..^(♯‘𝐹))𝑆 ≤ (♯‘((𝐼‘(𝐹‘(𝑘 − 1))) ∩ (𝐼‘(𝐹‘𝑘)))))))
Theorem	ewlkprop 29697*	Properties of an s-walk of edges. (Contributed by AV, 4-Jan-2021.)
⊢ 𝐼 = (iEdg‘𝐺)    ⇒   ⊢ (𝐹 ∈ (𝐺 EdgWalks 𝑆) → ((𝐺 ∈ V ∧ 𝑆 ∈ ℕ0*) ∧ 𝐹 ∈ Word dom 𝐼 ∧ ∀𝑘 ∈ (1..^(♯‘𝐹))𝑆 ≤ (♯‘((𝐼‘(𝐹‘(𝑘 − 1))) ∩ (𝐼‘(𝐹‘𝑘))))))
Theorem	ewlkinedg 29698	The intersection (common vertices) of two adjacent edges in an s-walk of edges. (Contributed by AV, 4-Jan-2021.)
⊢ 𝐼 = (iEdg‘𝐺)    ⇒   ⊢ ((𝐹 ∈ (𝐺 EdgWalks 𝑆) ∧ 𝐾 ∈ (1..^(♯‘𝐹))) → 𝑆 ≤ (♯‘((𝐼‘(𝐹‘(𝐾 − 1))) ∩ (𝐼‘(𝐹‘𝐾)))))
Theorem	ewlkle 29699	An s-walk of edges is also a t-walk of edges if 𝑡 ≤ 𝑠. (Contributed by AV, 4-Jan-2021.)
⊢ ((𝐹 ∈ (𝐺 EdgWalks 𝑆) ∧ 𝑇 ∈ ℕ0* ∧ 𝑇 ≤ 𝑆) → 𝐹 ∈ (𝐺 EdgWalks 𝑇))
Theorem	upgrewlkle2 29700	In a pseudograph, there is no s-walk of edges of length greater than 1 with s>2. (Contributed by AV, 4-Jan-2021.)
⊢ ((𝐺 ∈ UPGraph ∧ 𝐹 ∈ (𝐺 EdgWalks 𝑆) ∧ 1 < (♯‘𝐹)) → 𝑆 ≤ 2)