P. 304 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 30301-30400   *Has distinct variable group(s)

Type	Label	Description
Statement
17.5.3  Theorems according to Mertzios and Unger
Theorem	2pthfrgrrn 30301*	Between any two (different) vertices in a friendship graph is a 2-path (path of length 2), see Proposition 1(b) of [MertziosUnger] p. 153 : "A friendship graph G ..., as well as the distance between any two nodes in G is at most two". (Contributed by Alexander van der Vekens, 15-Nov-2017.) (Revised by AV, 1-Apr-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (𝐺 ∈ FriendGraph → ∀𝑎 ∈ 𝑉 ∀𝑐 ∈ (𝑉 ∖ {𝑎})∃𝑏 ∈ 𝑉 ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸))
Theorem	2pthfrgrrn2 30302*	Between any two (different) vertices in a friendship graph is a 2-path (path of length 2), see Proposition 1(b) of [MertziosUnger] p. 153 : "A friendship graph G ..., as well as the distance between any two nodes in G is at most two". (Contributed by Alexander van der Vekens, 16-Nov-2017.) (Revised by AV, 1-Apr-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (𝐺 ∈ FriendGraph → ∀𝑎 ∈ 𝑉 ∀𝑐 ∈ (𝑉 ∖ {𝑎})∃𝑏 ∈ 𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ (𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐)))
Theorem	2pthfrgr 30303*	Between any two (different) vertices in a friendship graph, tere is a 2-path (simple path of length 2), see Proposition 1(b) of [MertziosUnger] p. 153 : "A friendship graph G ..., as well as the distance between any two nodes in G is at most two". (Contributed by Alexander van der Vekens, 6-Dec-2017.) (Revised by AV, 1-Apr-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (𝐺 ∈ FriendGraph → ∀𝑎 ∈ 𝑉 ∀𝑏 ∈ (𝑉 ∖ {𝑎})∃𝑓∃𝑝(𝑓(𝑎(SPathsOn‘𝐺)𝑏)𝑝 ∧ (♯‘𝑓) = 2))
Theorem	3cyclfrgrrn1 30304*	Every vertex in a friendship graph (with more than 1 vertex) is part of a 3-cycle. (Contributed by Alexander van der Vekens, 16-Nov-2017.) (Revised by AV, 2-Apr-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ FriendGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ 𝐴 ≠ 𝐶) → ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ({𝐴, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝐴} ∈ 𝐸))
Theorem	3cyclfrgrrn 30305*	Every vertex in a friendship graph (with more than 1 vertex) is part of a 3-cycle. (Contributed by Alexander van der Vekens, 16-Nov-2017.) (Revised by AV, 2-Apr-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ FriendGraph ∧ 1 < (♯‘𝑉)) → ∀𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸))
Theorem	3cyclfrgrrn2 30306*	Every vertex in a friendship graph (with more than 1 vertex) is part of a 3-cycle. (Contributed by Alexander van der Vekens, 10-Dec-2017.) (Revised by AV, 2-Apr-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ FriendGraph ∧ 1 < (♯‘𝑉)) → ∀𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (𝑏 ≠ 𝑐 ∧ ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸)))
Theorem	3cyclfrgr 30307*	Every vertex in a friendship graph (with more than 1 vertex) is part of a 3-cycle. (Contributed by Alexander van der Vekens, 19-Nov-2017.) (Revised by AV, 2-Apr-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝐺 ∈ FriendGraph ∧ 1 < (♯‘𝑉)) → ∀𝑣 ∈ 𝑉 ∃𝑓∃𝑝(𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 3 ∧ (𝑝‘0) = 𝑣))
Theorem	4cycl2v2nb 30308	In a (maybe degenerate) 4-cycle, two vertice have two (maybe not different) common neighbors. (Contributed by Alexander van der Vekens, 19-Nov-2017.) (Revised by AV, 2-Apr-2021.)
⊢ ((({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸) ∧ ({𝐶, 𝐷} ∈ 𝐸 ∧ {𝐷, 𝐴} ∈ 𝐸)) → ({{𝐴, 𝐵}, {𝐵, 𝐶}} ⊆ 𝐸 ∧ {{𝐴, 𝐷}, {𝐷, 𝐶}} ⊆ 𝐸))
Theorem	4cycl2vnunb 30309*	In a 4-cycle, two distinct vertices have not a unique common neighbor. (Contributed by Alexander van der Vekens, 19-Nov-2017.) (Revised by AV, 2-Apr-2021.)
⊢ ((({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸) ∧ ({𝐶, 𝐷} ∈ 𝐸 ∧ {𝐷, 𝐴} ∈ 𝐸) ∧ (𝐵 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ∧ 𝐵 ≠ 𝐷)) → ¬ ∃!𝑥 ∈ 𝑉 {{𝐴, 𝑥}, {𝑥, 𝐶}} ⊆ 𝐸)
Theorem	n4cyclfrgr 30310	There is no 4-cycle in a friendship graph, see Proposition 1(a) of [MertziosUnger] p. 153 : "A friendship graph G contains no C4 as a subgraph ...". (Contributed by Alexander van der Vekens, 19-Nov-2017.) (Revised by AV, 2-Apr-2021.)
⊢ ((𝐺 ∈ FriendGraph ∧ 𝐹(Cycles‘𝐺)𝑃) → (♯‘𝐹) ≠ 4)
Theorem	4cyclusnfrgr 30311	A graph with a 4-cycle is not a friendhip graph. (Contributed by Alexander van der Vekens, 19-Dec-2017.) (Revised by AV, 2-Apr-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ USGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ∧ 𝐴 ≠ 𝐶) ∧ (𝐵 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ∧ 𝐵 ≠ 𝐷)) → ((({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸) ∧ ({𝐶, 𝐷} ∈ 𝐸 ∧ {𝐷, 𝐴} ∈ 𝐸)) → 𝐺 ∉ FriendGraph ))
Theorem	frgrnbnb 30312	If two neighbors 𝑈 and 𝑊 of a vertex 𝑋 have a common neighbor 𝐴 in a friendship graph, then this common neighbor 𝐴 must be the vertex 𝑋. (Contributed by Alexander van der Vekens, 19-Dec-2017.) (Revised by AV, 2-Apr-2021.) (Proof shortened by AV, 13-Feb-2022.)
⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝐷 = (𝐺 NeighbVtx 𝑋)    ⇒   ⊢ ((𝐺 ∈ FriendGraph ∧ (𝑈 ∈ 𝐷 ∧ 𝑊 ∈ 𝐷) ∧ 𝑈 ≠ 𝑊) → (({𝑈, 𝐴} ∈ 𝐸 ∧ {𝑊, 𝐴} ∈ 𝐸) → 𝐴 = 𝑋))
Theorem	frgrconngr 30313	A friendship graph is connected, see remark 1 in [MertziosUnger] p. 153 (after Proposition 1): "An arbitrary friendship graph has to be connected, ... ". (Contributed by Alexander van der Vekens, 6-Dec-2017.) (Revised by AV, 1-Apr-2021.)
⊢ (𝐺 ∈ FriendGraph → 𝐺 ∈ ConnGraph)
Theorem	vdgn0frgrv2 30314	A vertex in a friendship graph with more than one vertex cannot have degree 0. (Contributed by Alexander van der Vekens, 9-Dec-2017.) (Revised by AV, 4-Apr-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝐺 ∈ FriendGraph ∧ 𝑁 ∈ 𝑉) → (1 < (♯‘𝑉) → ((VtxDeg‘𝐺)‘𝑁) ≠ 0))
Theorem	vdgn1frgrv2 30315	Any vertex in a friendship graph does not have degree 1, see remark 2 in [MertziosUnger] p. 153 (after Proposition 1): "... no node v of it [a friendship graph] may have deg(v) = 1.". (Contributed by Alexander van der Vekens, 10-Dec-2017.) (Revised by AV, 4-Apr-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝐺 ∈ FriendGraph ∧ 𝑁 ∈ 𝑉) → (1 < (♯‘𝑉) → ((VtxDeg‘𝐺)‘𝑁) ≠ 1))
Theorem	vdgn1frgrv3 30316*	Any vertex in a friendship graph does not have degree 1, see remark 2 in [MertziosUnger] p. 153 (after Proposition 1): "... no node v of it [a friendship graph] may have deg(v) = 1.". (Contributed by Alexander van der Vekens, 4-Sep-2018.) (Revised by AV, 4-Apr-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝐺 ∈ FriendGraph ∧ 1 < (♯‘𝑉)) → ∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) ≠ 1)
Theorem	vdgfrgrgt2 30317	Any vertex in a friendship graph (with more than one vertex - then, actually, the graph must have at least three vertices, because otherwise, it would not be a friendship graph) has at least degree 2, see remark 3 in [MertziosUnger] p. 153 (after Proposition 1): "It follows that deg(v) >= 2 for every node v of a friendship graph". (Contributed by Alexander van der Vekens, 21-Dec-2017.) (Revised by AV, 5-Apr-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝐺 ∈ FriendGraph ∧ 𝑁 ∈ 𝑉) → (1 < (♯‘𝑉) → 2 ≤ ((VtxDeg‘𝐺)‘𝑁)))
17.5.4  Huneke's Proof of the Friendship Theorem In this section, the friendship theorem friendship 30418 is proven by formalizing Huneke's proof, see [Huneke] pp. 1-2. The three claims (see frgrncvvdeq 30328, frgrregorufr 30344 and frrusgrord0 30359) and additional statements (numbered in the order of their occurrence in the paper) in Huneke's proof are cited in the corresponding theorems.
Theorem	frgrncvvdeqlem1 30318	Lemma 1 for frgrncvvdeq 30328. (Contributed by Alexander van der Vekens, 23-Dec-2017.) (Revised by AV, 8-May-2021.) (Proof shortened by AV, 12-Feb-2022.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝐷 = (𝐺 NeighbVtx 𝑋)    &   ⊢ 𝑁 = (𝐺 NeighbVtx 𝑌)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ≠ 𝑌)    &   ⊢ (𝜑 → 𝑌 ∉ 𝐷)    &   ⊢ (𝜑 → 𝐺 ∈ FriendGraph )    &   ⊢ 𝐴 = (𝑥 ∈ 𝐷 ↦ (℩𝑦 ∈ 𝑁 {𝑥, 𝑦} ∈ 𝐸))    ⇒   ⊢ (𝜑 → 𝑋 ∉ 𝑁)
Theorem	frgrncvvdeqlem2 30319*	Lemma 2 for frgrncvvdeq 30328. In a friendship graph, for each neighbor of a vertex there is exactly one neighbor of another vertex so that there is an edge between these two neighbors. (Contributed by Alexander van der Vekens, 22-Dec-2017.) (Revised by AV, 10-May-2021.) (Proof shortened by AV, 12-Feb-2022.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝐷 = (𝐺 NeighbVtx 𝑋)    &   ⊢ 𝑁 = (𝐺 NeighbVtx 𝑌)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ≠ 𝑌)    &   ⊢ (𝜑 → 𝑌 ∉ 𝐷)    &   ⊢ (𝜑 → 𝐺 ∈ FriendGraph )    &   ⊢ 𝐴 = (𝑥 ∈ 𝐷 ↦ (℩𝑦 ∈ 𝑁 {𝑥, 𝑦} ∈ 𝐸))    ⇒   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → ∃!𝑦 ∈ 𝑁 {𝑥, 𝑦} ∈ 𝐸)
Theorem	frgrncvvdeqlem3 30320*	Lemma 3 for frgrncvvdeq 30328. The unique neighbor of a vertex (expressed by a restricted iota) is the intersection of the corresponding neighborhoods. (Contributed by Alexander van der Vekens, 18-Dec-2017.) (Revised by AV, 10-May-2021.) (Proof shortened by AV, 12-Feb-2022.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝐷 = (𝐺 NeighbVtx 𝑋)    &   ⊢ 𝑁 = (𝐺 NeighbVtx 𝑌)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ≠ 𝑌)    &   ⊢ (𝜑 → 𝑌 ∉ 𝐷)    &   ⊢ (𝜑 → 𝐺 ∈ FriendGraph )    &   ⊢ 𝐴 = (𝑥 ∈ 𝐷 ↦ (℩𝑦 ∈ 𝑁 {𝑥, 𝑦} ∈ 𝐸))    ⇒   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → {(℩𝑦 ∈ 𝑁 {𝑥, 𝑦} ∈ 𝐸)} = ((𝐺 NeighbVtx 𝑥) ∩ 𝑁))
Theorem	frgrncvvdeqlem4 30321*	Lemma 4 for frgrncvvdeq 30328. The mapping of neighbors to neighbors is a function. (Contributed by Alexander van der Vekens, 22-Dec-2017.) (Revised by AV, 10-May-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝐷 = (𝐺 NeighbVtx 𝑋)    &   ⊢ 𝑁 = (𝐺 NeighbVtx 𝑌)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ≠ 𝑌)    &   ⊢ (𝜑 → 𝑌 ∉ 𝐷)    &   ⊢ (𝜑 → 𝐺 ∈ FriendGraph )    &   ⊢ 𝐴 = (𝑥 ∈ 𝐷 ↦ (℩𝑦 ∈ 𝑁 {𝑥, 𝑦} ∈ 𝐸))    ⇒   ⊢ (𝜑 → 𝐴:𝐷⟶𝑁)
Theorem	frgrncvvdeqlem5 30322*	Lemma 5 for frgrncvvdeq 30328. The mapping of neighbors to neighbors applied on a vertex is the intersection of the corresponding neighborhoods. (Contributed by Alexander van der Vekens, 23-Dec-2017.) (Revised by AV, 10-May-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝐷 = (𝐺 NeighbVtx 𝑋)    &   ⊢ 𝑁 = (𝐺 NeighbVtx 𝑌)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ≠ 𝑌)    &   ⊢ (𝜑 → 𝑌 ∉ 𝐷)    &   ⊢ (𝜑 → 𝐺 ∈ FriendGraph )    &   ⊢ 𝐴 = (𝑥 ∈ 𝐷 ↦ (℩𝑦 ∈ 𝑁 {𝑥, 𝑦} ∈ 𝐸))    ⇒   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → {(𝐴‘𝑥)} = ((𝐺 NeighbVtx 𝑥) ∩ 𝑁))
Theorem	frgrncvvdeqlem6 30323*	Lemma 6 for frgrncvvdeq 30328. (Contributed by Alexander van der Vekens, 23-Dec-2017.) (Revised by AV, 10-May-2021.) (Proof shortened by AV, 30-Dec-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝐷 = (𝐺 NeighbVtx 𝑋)    &   ⊢ 𝑁 = (𝐺 NeighbVtx 𝑌)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ≠ 𝑌)    &   ⊢ (𝜑 → 𝑌 ∉ 𝐷)    &   ⊢ (𝜑 → 𝐺 ∈ FriendGraph )    &   ⊢ 𝐴 = (𝑥 ∈ 𝐷 ↦ (℩𝑦 ∈ 𝑁 {𝑥, 𝑦} ∈ 𝐸))    ⇒   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → {𝑥, (𝐴‘𝑥)} ∈ 𝐸)
Theorem	frgrncvvdeqlem7 30324*	Lemma 7 for frgrncvvdeq 30328. This corresponds to statement 1 in [Huneke] p. 1: "This common neighbor cannot be x, as x and y are not adjacent.". This is only an observation, which is not required to proof the friendship theorem. (Contributed by Alexander van der Vekens, 23-Dec-2017.) (Revised by AV, 10-May-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝐷 = (𝐺 NeighbVtx 𝑋)    &   ⊢ 𝑁 = (𝐺 NeighbVtx 𝑌)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ≠ 𝑌)    &   ⊢ (𝜑 → 𝑌 ∉ 𝐷)    &   ⊢ (𝜑 → 𝐺 ∈ FriendGraph )    &   ⊢ 𝐴 = (𝑥 ∈ 𝐷 ↦ (℩𝑦 ∈ 𝑁 {𝑥, 𝑦} ∈ 𝐸))    ⇒   ⊢ (𝜑 → ∀𝑥 ∈ 𝐷 (𝐴‘𝑥) ≠ 𝑋)
Theorem	frgrncvvdeqlem8 30325*	Lemma 8 for frgrncvvdeq 30328. This corresponds to statement 2 in [Huneke] p. 1: "The map is one-to-one since z in N(x) is uniquely determined as the common neighbor of x and a(x)". (Contributed by Alexander van der Vekens, 23-Dec-2017.) (Revised by AV, 10-May-2021.) (Revised by AV, 30-Dec-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝐷 = (𝐺 NeighbVtx 𝑋)    &   ⊢ 𝑁 = (𝐺 NeighbVtx 𝑌)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ≠ 𝑌)    &   ⊢ (𝜑 → 𝑌 ∉ 𝐷)    &   ⊢ (𝜑 → 𝐺 ∈ FriendGraph )    &   ⊢ 𝐴 = (𝑥 ∈ 𝐷 ↦ (℩𝑦 ∈ 𝑁 {𝑥, 𝑦} ∈ 𝐸))    ⇒   ⊢ (𝜑 → 𝐴:𝐷–1-1→𝑁)
Theorem	frgrncvvdeqlem9 30326*	Lemma 9 for frgrncvvdeq 30328. This corresponds to statement 3 in [Huneke] p. 1: "By symmetry the map is onto". (Contributed by Alexander van der Vekens, 24-Dec-2017.) (Revised by AV, 10-May-2021.) (Proof shortened by AV, 12-Feb-2022.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝐷 = (𝐺 NeighbVtx 𝑋)    &   ⊢ 𝑁 = (𝐺 NeighbVtx 𝑌)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ≠ 𝑌)    &   ⊢ (𝜑 → 𝑌 ∉ 𝐷)    &   ⊢ (𝜑 → 𝐺 ∈ FriendGraph )    &   ⊢ 𝐴 = (𝑥 ∈ 𝐷 ↦ (℩𝑦 ∈ 𝑁 {𝑥, 𝑦} ∈ 𝐸))    ⇒   ⊢ (𝜑 → 𝐴:𝐷–onto→𝑁)
Theorem	frgrncvvdeqlem10 30327*	Lemma 10 for frgrncvvdeq 30328. (Contributed by Alexander van der Vekens, 24-Dec-2017.) (Revised by AV, 10-May-2021.) (Proof shortened by AV, 30-Dec-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝐷 = (𝐺 NeighbVtx 𝑋)    &   ⊢ 𝑁 = (𝐺 NeighbVtx 𝑌)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑋 ≠ 𝑌)    &   ⊢ (𝜑 → 𝑌 ∉ 𝐷)    &   ⊢ (𝜑 → 𝐺 ∈ FriendGraph )    &   ⊢ 𝐴 = (𝑥 ∈ 𝐷 ↦ (℩𝑦 ∈ 𝑁 {𝑥, 𝑦} ∈ 𝐸))    ⇒   ⊢ (𝜑 → 𝐴:𝐷–1-1-onto→𝑁)
Theorem	frgrncvvdeq 30328*	In a friendship graph, two vertices which are not connected by an edge have the same degree. This corresponds to claim 1 in [Huneke] p. 1: "If x,y are elements of (the friendship graph) G and are not adjacent, then they have the same degree (i.e., the same number of adjacent vertices).". (Contributed by Alexander van der Vekens, 19-Dec-2017.) (Revised by AV, 10-May-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐷 = (VtxDeg‘𝐺)    ⇒   ⊢ (𝐺 ∈ FriendGraph → ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ (𝑉 ∖ {𝑥})(𝑦 ∉ (𝐺 NeighbVtx 𝑥) → (𝐷‘𝑥) = (𝐷‘𝑦)))
Theorem	frgrwopreglem4a 30329	In a friendship graph any two vertices with different degrees are connected. Alternate version of frgrwopreglem4 30334 without a fixed degree and without using the sets 𝐴 and 𝐵. (Contributed by Alexander van der Vekens, 30-Dec-2017.) (Revised by AV, 4-Feb-2022.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐷 = (VtxDeg‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ FriendGraph ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) ∧ (𝐷‘𝑋) ≠ (𝐷‘𝑌)) → {𝑋, 𝑌} ∈ 𝐸)
Theorem	frgrwopreglem5a 30330	If a friendship graph has two vertices with the same degree and two other vertices with different degrees, then there is a 4-cycle in the graph. Alternate version of frgrwopreglem5 30340 without a fixed degree and without using the sets 𝐴 and 𝐵. (Contributed by Alexander van der Vekens, 31-Dec-2017.) (Revised by AV, 4-Feb-2022.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐷 = (VtxDeg‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ FriendGraph ∧ ((𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉) ∧ (𝐵 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) ∧ ((𝐷‘𝐴) = (𝐷‘𝑋) ∧ (𝐷‘𝐴) ≠ (𝐷‘𝐵) ∧ (𝐷‘𝑋) ≠ (𝐷‘𝑌))) → (({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝑋} ∈ 𝐸) ∧ ({𝑋, 𝑌} ∈ 𝐸 ∧ {𝑌, 𝐴} ∈ 𝐸)))
Theorem	frgrwopreglem1 30331*	Lemma 1 for frgrwopreg 30342: the classes 𝐴 and 𝐵 are sets. The definition of 𝐴 and 𝐵 corresponds to definition 3 in [Huneke] p. 2: "Let A be the set of all vertices of degree k, let B be the set of all vertices of degree different from k, ..." (Contributed by Alexander van der Vekens, 31-Dec-2017.) (Revised by AV, 10-May-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐷 = (VtxDeg‘𝐺)    &   ⊢ 𝐴 = {𝑥 ∈ 𝑉 ∣ (𝐷‘𝑥) = 𝐾}    &   ⊢ 𝐵 = (𝑉 ∖ 𝐴)    ⇒   ⊢ (𝐴 ∈ V ∧ 𝐵 ∈ V)
Theorem	frgrwopreglem2 30332*	Lemma 2 for frgrwopreg 30342. If the set 𝐴 of vertices of degree 𝐾 is not empty in a friendship graph with at least two vertices, then 𝐾 must be greater than 1 . This is only an observation, which is not required for the proof the friendship theorem. (Contributed by Alexander van der Vekens, 30-Dec-2017.) (Revised by AV, 2-Jan-2022.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐷 = (VtxDeg‘𝐺)    &   ⊢ 𝐴 = {𝑥 ∈ 𝑉 ∣ (𝐷‘𝑥) = 𝐾}    &   ⊢ 𝐵 = (𝑉 ∖ 𝐴)    ⇒   ⊢ ((𝐺 ∈ FriendGraph ∧ 1 < (♯‘𝑉) ∧ 𝐴 ≠ ∅) → 2 ≤ 𝐾)
Theorem	frgrwopreglem3 30333*	Lemma 3 for frgrwopreg 30342. The vertices in the sets 𝐴 and 𝐵 have different degrees. (Contributed by Alexander van der Vekens, 30-Dec-2017.) (Revised by AV, 10-May-2021.) (Proof shortened by AV, 2-Jan-2022.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐷 = (VtxDeg‘𝐺)    &   ⊢ 𝐴 = {𝑥 ∈ 𝑉 ∣ (𝐷‘𝑥) = 𝐾}    &   ⊢ 𝐵 = (𝑉 ∖ 𝐴)    ⇒   ⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵) → (𝐷‘𝑋) ≠ (𝐷‘𝑌))
Theorem	frgrwopreglem4 30334*	Lemma 4 for frgrwopreg 30342. In a friendship graph each vertex with degree 𝐾 is connected with any vertex with degree other than 𝐾. This corresponds to statement 4 in [Huneke] p. 2: "By the first claim, every vertex in A is adjacent to every vertex in B.". (Contributed by Alexander van der Vekens, 30-Dec-2017.) (Revised by AV, 10-May-2021.) (Proof shortened by AV, 4-Feb-2022.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐷 = (VtxDeg‘𝐺)    &   ⊢ 𝐴 = {𝑥 ∈ 𝑉 ∣ (𝐷‘𝑥) = 𝐾}    &   ⊢ 𝐵 = (𝑉 ∖ 𝐴)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (𝐺 ∈ FriendGraph → ∀𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐵 {𝑎, 𝑏} ∈ 𝐸)
Theorem	frgrwopregasn 30335*	According to statement 5 in [Huneke] p. 2: "If A ... is a singleton, then that singleton is a universal friend". This version of frgrwopreg1 30337 is stricter (claiming that the singleton itself is a universal friend instead of claiming the existence of a universal friend only) and therefore closer to Huneke's statement. This strict variant, however, is not required for the proof of the friendship theorem. (Contributed by Alexander van der Vekens, 1-Jan-2018.) (Revised by AV, 4-Feb-2022.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐷 = (VtxDeg‘𝐺)    &   ⊢ 𝐴 = {𝑥 ∈ 𝑉 ∣ (𝐷‘𝑥) = 𝐾}    &   ⊢ 𝐵 = (𝑉 ∖ 𝐴)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝐴 = {𝑋}) → ∀𝑤 ∈ (𝑉 ∖ {𝑋}){𝑋, 𝑤} ∈ 𝐸)
Theorem	frgrwopregbsn 30336*	According to statement 5 in [Huneke] p. 2: "If ... B is a singleton, then that singleton is a universal friend". This version of frgrwopreg2 30338 is stricter (claiming that the singleton itself is a universal friend instead of claiming the existence of a universal friend only) and therefore closer to Huneke's statement. This strict variant, however, is not required for the proof of the friendship theorem. (Contributed by AV, 4-Feb-2022.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐷 = (VtxDeg‘𝐺)    &   ⊢ 𝐴 = {𝑥 ∈ 𝑉 ∣ (𝐷‘𝑥) = 𝐾}    &   ⊢ 𝐵 = (𝑉 ∖ 𝐴)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝐵 = {𝑋}) → ∀𝑤 ∈ (𝑉 ∖ {𝑋}){𝑋, 𝑤} ∈ 𝐸)
Theorem	frgrwopreg1 30337*	According to statement 5 in [Huneke] p. 2: "If A ... is a singleton, then that singleton is a universal friend". (Contributed by Alexander van der Vekens, 1-Jan-2018.) (Proof shortened by AV, 4-Feb-2022.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐷 = (VtxDeg‘𝐺)    &   ⊢ 𝐴 = {𝑥 ∈ 𝑉 ∣ (𝐷‘𝑥) = 𝐾}    &   ⊢ 𝐵 = (𝑉 ∖ 𝐴)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ FriendGraph ∧ (♯‘𝐴) = 1) → ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ 𝐸)
Theorem	frgrwopreg2 30338*	According to statement 5 in [Huneke] p. 2: "If ... B is a singleton, then that singleton is a universal friend". (Contributed by Alexander van der Vekens, 1-Jan-2018.) (Proof shortened by AV, 4-Feb-2022.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐷 = (VtxDeg‘𝐺)    &   ⊢ 𝐴 = {𝑥 ∈ 𝑉 ∣ (𝐷‘𝑥) = 𝐾}    &   ⊢ 𝐵 = (𝑉 ∖ 𝐴)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ FriendGraph ∧ (♯‘𝐵) = 1) → ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ 𝐸)
Theorem	frgrwopreglem5lem 30339*	Lemma for frgrwopreglem5 30340. (Contributed by AV, 5-Feb-2022.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐷 = (VtxDeg‘𝐺)    &   ⊢ 𝐴 = {𝑥 ∈ 𝑉 ∣ (𝐷‘𝑥) = 𝐾}    &   ⊢ 𝐵 = (𝑉 ∖ 𝐴)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (((𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((𝐷‘𝑎) = (𝐷‘𝑥) ∧ (𝐷‘𝑎) ≠ (𝐷‘𝑏) ∧ (𝐷‘𝑥) ≠ (𝐷‘𝑦)))
Theorem	frgrwopreglem5 30340*	Lemma 5 for frgrwopreg 30342. If 𝐴 as well as 𝐵 contain at least two vertices, there is a 4-cycle in a friendship graph. This corresponds to statement 6 in [Huneke] p. 2: "... otherwise, there are two different vertices in A, and they have two common neighbors in B, ...". (Contributed by Alexander van der Vekens, 31-Dec-2017.) (Proof shortened by AV, 5-Feb-2022.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐷 = (VtxDeg‘𝐺)    &   ⊢ 𝐴 = {𝑥 ∈ 𝑉 ∣ (𝐷‘𝑥) = 𝐾}    &   ⊢ 𝐵 = (𝑉 ∖ 𝐴)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ FriendGraph ∧ 1 < (♯‘𝐴) ∧ 1 < (♯‘𝐵)) → ∃𝑎 ∈ 𝐴 ∃𝑥 ∈ 𝐴 ∃𝑏 ∈ 𝐵 ∃𝑦 ∈ 𝐵 ((𝑎 ≠ 𝑥 ∧ 𝑏 ≠ 𝑦) ∧ ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑥} ∈ 𝐸) ∧ ({𝑥, 𝑦} ∈ 𝐸 ∧ {𝑦, 𝑎} ∈ 𝐸)))
Theorem	frgrwopreglem5ALT 30341*	Alternate direct proof of frgrwopreglem5 30340, not using frgrwopreglem5a 30330. This proof would be even a little bit shorter than the proof of frgrwopreglem5 30340 without using frgrwopreglem5lem 30339. (Contributed by Alexander van der Vekens, 31-Dec-2017.) (Revised by AV, 3-Jan-2022.) (Proof shortened by AV, 5-Feb-2022.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐷 = (VtxDeg‘𝐺)    &   ⊢ 𝐴 = {𝑥 ∈ 𝑉 ∣ (𝐷‘𝑥) = 𝐾}    &   ⊢ 𝐵 = (𝑉 ∖ 𝐴)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ FriendGraph ∧ 1 < (♯‘𝐴) ∧ 1 < (♯‘𝐵)) → ∃𝑎 ∈ 𝐴 ∃𝑥 ∈ 𝐴 ∃𝑏 ∈ 𝐵 ∃𝑦 ∈ 𝐵 ((𝑎 ≠ 𝑥 ∧ 𝑏 ≠ 𝑦) ∧ ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑥} ∈ 𝐸) ∧ ({𝑥, 𝑦} ∈ 𝐸 ∧ {𝑦, 𝑎} ∈ 𝐸)))
Theorem	frgrwopreg 30342*	In a friendship graph there are either no vertices (𝐴 = ∅) or exactly one vertex ((♯‘𝐴) = 1) having degree 𝐾, or all (𝐵 = ∅) or all except one vertices ((♯‘𝐵) = 1) have degree 𝐾. (Contributed by Alexander van der Vekens, 31-Dec-2017.) (Revised by AV, 10-May-2021.) (Proof shortened by AV, 3-Jan-2022.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐷 = (VtxDeg‘𝐺)    &   ⊢ 𝐴 = {𝑥 ∈ 𝑉 ∣ (𝐷‘𝑥) = 𝐾}    &   ⊢ 𝐵 = (𝑉 ∖ 𝐴)    ⇒   ⊢ (𝐺 ∈ FriendGraph → (((♯‘𝐴) = 1 ∨ 𝐴 = ∅) ∨ ((♯‘𝐵) = 1 ∨ 𝐵 = ∅)))
Theorem	frgrregorufr0 30343*	In a friendship graph there are either no vertices having degree 𝐾, or all vertices have degree 𝐾 for any (nonnegative integer) 𝐾, unless there is a universal friend. This corresponds to claim 2 in [Huneke] p. 2: "... all vertices have degree k, unless there is a universal friend." (Contributed by Alexander van der Vekens, 1-Jan-2018.) (Revised by AV, 11-May-2021.) (Proof shortened by AV, 3-Jan-2022.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝐷 = (VtxDeg‘𝐺)    ⇒   ⊢ (𝐺 ∈ FriendGraph → (∀𝑣 ∈ 𝑉 (𝐷‘𝑣) = 𝐾 ∨ ∀𝑣 ∈ 𝑉 (𝐷‘𝑣) ≠ 𝐾 ∨ ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ 𝐸))
Theorem	frgrregorufr 30344*	If there is a vertex having degree 𝐾 for each (nonnegative integer) 𝐾 in a friendship graph, then either all vertices have degree 𝐾 or there is a universal friend. This corresponds to claim 2 in [Huneke] p. 2: "Suppose there is a vertex of degree k > 1. ... all vertices have degree k, unless there is a universal friend. ... It follows that G is k-regular, i.e., the degree of every vertex is k". (Contributed by Alexander van der Vekens, 1-Jan-2018.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝐷 = (VtxDeg‘𝐺)    ⇒   ⊢ (𝐺 ∈ FriendGraph → (∃𝑎 ∈ 𝑉 (𝐷‘𝑎) = 𝐾 → (∀𝑣 ∈ 𝑉 (𝐷‘𝑣) = 𝐾 ∨ ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ 𝐸)))
Theorem	frgrregorufrg 30345*	If there is a vertex having degree 𝑘 for each nonnegative integer 𝑘 in a friendship graph, then there is a universal friend. This corresponds to claim 2 in [Huneke] p. 2: "Suppose there is a vertex of degree k > 1. ... all vertices have degree k, unless there is a universal friend. ... It follows that G is k-regular, i.e., the degree of every vertex is k". Variant of frgrregorufr 30344 with generalization. (Contributed by Alexander van der Vekens, 6-Sep-2018.) (Revised by AV, 26-May-2021.) (Proof shortened by AV, 12-Jan-2022.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (𝐺 ∈ FriendGraph → ∀𝑘 ∈ ℕ0 (∃𝑎 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑎) = 𝑘 → (𝐺 RegUSGraph 𝑘 ∨ ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ 𝐸)))
Theorem	frgr2wwlkeu 30346*	For two different vertices in a friendship graph, there is exactly one third vertex being the middle vertex of a (simple) path/walk of length 2 between the two vertices. (Contributed by Alexander van der Vekens, 18-Feb-2018.) (Revised by AV, 12-May-2021.) (Proof shortened by AV, 4-Jan-2022.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝐺 ∈ FriendGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → ∃!𝑐 ∈ 𝑉 ⟨“𝐴𝑐𝐵”⟩ ∈ (𝐴(2 WWalksNOn 𝐺)𝐵))
Theorem	frgr2wwlkn0 30347	In a friendship graph, there is always a path/walk of length 2 between two different vertices. (Contributed by Alexander van der Vekens, 18-Feb-2018.) (Revised by AV, 12-May-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝐺 ∈ FriendGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → (𝐴(2 WWalksNOn 𝐺)𝐵) ≠ ∅)
Theorem	frgr2wwlk1 30348	In a friendship graph, there is exactly one walk of length 2 between two different vertices. (Contributed by Alexander van der Vekens, 19-Feb-2018.) (Revised by AV, 13-May-2021.) (Proof shortened by AV, 16-Mar-2022.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝐺 ∈ FriendGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → (♯‘(𝐴(2 WWalksNOn 𝐺)𝐵)) = 1)
Theorem	frgr2wsp1 30349	In a friendship graph, there is exactly one simple path of length 2 between two different vertices. (Contributed by Alexander van der Vekens, 3-Mar-2018.) (Revised by AV, 13-May-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝐺 ∈ FriendGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) → (♯‘(𝐴(2 WSPathsNOn 𝐺)𝐵)) = 1)
Theorem	frgr2wwlkeqm 30350	If there is a (simple) path of length 2 from one vertex to another vertex and a (simple) path of length 2 from the other vertex back to the first vertex in a friendship graph, then the middle vertex is the same. This is only an observation, which is not required to proof the friendship theorem. (Contributed by Alexander van der Vekens, 20-Feb-2018.) (Revised by AV, 13-May-2021.) (Proof shortened by AV, 7-Jan-2022.)
⊢ ((𝐺 ∈ FriendGraph ∧ 𝐴 ≠ 𝐵 ∧ (𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑌)) → ((⟨“𝐴𝑃𝐵”⟩ ∈ (𝐴(2 WWalksNOn 𝐺)𝐵) ∧ ⟨“𝐵𝑄𝐴”⟩ ∈ (𝐵(2 WWalksNOn 𝐺)𝐴)) → 𝑄 = 𝑃))
Theorem	frgrhash2wsp 30351	The number of simple paths of length 2 is n*(n-1) in a friendship graph with n vertices. This corresponds to the proof of claim 3 in [Huneke] p. 2: "... the paths of length two in G: by assumption there are ( n 2 ) such paths.". However, Huneke counts undirected paths, so obtains the result ((𝑛C2) = ((𝑛 · (𝑛 − 1)) / 2)), whereas we count directed paths, obtaining twice that number. (Contributed by Alexander van der Vekens, 6-Mar-2018.) (Revised by AV, 10-Jan-2022.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin) → (♯‘(2 WSPathsN 𝐺)) = ((♯‘𝑉) · ((♯‘𝑉) − 1)))
Theorem	fusgreg2wsplem 30352*	Lemma for fusgreg2wsp 30355 and related theorems. (Contributed by AV, 8-Jan-2022.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑀 = (𝑎 ∈ 𝑉 ↦ {𝑤 ∈ (2 WSPathsN 𝐺) ∣ (𝑤‘1) = 𝑎})    ⇒   ⊢ (𝑁 ∈ 𝑉 → (𝑝 ∈ (𝑀‘𝑁) ↔ (𝑝 ∈ (2 WSPathsN 𝐺) ∧ (𝑝‘1) = 𝑁)))
Theorem	fusgr2wsp2nb 30353*	The set of paths of length 2 with a given vertex in the middle for a finite simple graph is the union of all paths of length 2 from one neighbor to another neighbor of this vertex via this vertex. (Contributed by Alexander van der Vekens, 9-Mar-2018.) (Revised by AV, 17-May-2021.) (Proof shortened by AV, 16-Mar-2022.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑀 = (𝑎 ∈ 𝑉 ↦ {𝑤 ∈ (2 WSPathsN 𝐺) ∣ (𝑤‘1) = 𝑎})    ⇒   ⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ 𝑉) → (𝑀‘𝑁) = ∪ 𝑥 ∈ (𝐺 NeighbVtx 𝑁)∪ 𝑦 ∈ ((𝐺 NeighbVtx 𝑁) ∖ {𝑥}){⟨“𝑥𝑁𝑦”⟩})
Theorem	fusgreghash2wspv 30354*	According to statement 7 in [Huneke] p. 2: "For each vertex v, there are exactly ( k 2 ) paths with length two having v in the middle, ..." in a finite k-regular graph. For directed simple paths of length 2 represented by length 3 strings, we have again k*(k-1) such paths, see also comment of frgrhash2wsp 30351. (Contributed by Alexander van der Vekens, 10-Mar-2018.) (Revised by AV, 17-May-2021.) (Proof shortened by AV, 12-Feb-2022.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑀 = (𝑎 ∈ 𝑉 ↦ {𝑤 ∈ (2 WSPathsN 𝐺) ∣ (𝑤‘1) = 𝑎})    ⇒   ⊢ (𝐺 ∈ FinUSGraph → ∀𝑣 ∈ 𝑉 (((VtxDeg‘𝐺)‘𝑣) = 𝐾 → (♯‘(𝑀‘𝑣)) = (𝐾 · (𝐾 − 1))))
Theorem	fusgreg2wsp 30355*	In a finite simple graph, the set of all paths of length 2 is the union of all the paths of length 2 over the vertices which are in the middle of such a path. (Contributed by Alexander van der Vekens, 10-Mar-2018.) (Revised by AV, 18-May-2021.) (Proof shortened by AV, 10-Jan-2022.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑀 = (𝑎 ∈ 𝑉 ↦ {𝑤 ∈ (2 WSPathsN 𝐺) ∣ (𝑤‘1) = 𝑎})    ⇒   ⊢ (𝐺 ∈ FinUSGraph → (2 WSPathsN 𝐺) = ∪ 𝑥 ∈ 𝑉 (𝑀‘𝑥))
Theorem	2wspmdisj 30356*	The sets of paths of length 2 with a given vertex in the middle are distinct for different vertices in the middle. (Contributed by Alexander van der Vekens, 11-Mar-2018.) (Revised by AV, 18-May-2021.) (Proof shortened by AV, 10-Jan-2022.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑀 = (𝑎 ∈ 𝑉 ↦ {𝑤 ∈ (2 WSPathsN 𝐺) ∣ (𝑤‘1) = 𝑎})    ⇒   ⊢ Disj 𝑥 ∈ 𝑉 (𝑀‘𝑥)
Theorem	fusgreghash2wsp 30357*	In a finite k-regular graph with N vertices there are N times "k choose 2" paths with length 2, according to statement 8 in [Huneke] p. 2: "... giving n * ( k 2 ) total paths of length two.", if the direction of traversing the path is not respected. For simple paths of length 2 represented by length 3 strings, however, we have again n*k*(k-1) such paths. (Contributed by Alexander van der Vekens, 11-Mar-2018.) (Revised by AV, 19-May-2021.) (Proof shortened by AV, 12-Jan-2022.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑉 ≠ ∅) → (∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾 → (♯‘(2 WSPathsN 𝐺)) = ((♯‘𝑉) · (𝐾 · (𝐾 − 1)))))
Theorem	frrusgrord0lem 30358*	Lemma for frrusgrord0 30359. (Contributed by AV, 12-Jan-2022.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (((𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧ ∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾) → (𝐾 ∈ ℂ ∧ (♯‘𝑉) ∈ ℂ ∧ (♯‘𝑉) ≠ 0))
Theorem	frrusgrord0 30359*	If a nonempty finite friendship graph is k-regular, its order is k(k-1)+1. This corresponds to claim 3 in [Huneke] p. 2: "Next we claim that the number n of vertices in G is exactly k(k-1)+1.". (Contributed by Alexander van der Vekens, 11-Mar-2018.) (Revised by AV, 26-May-2021.) (Proof shortened by AV, 12-Jan-2022.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → (∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾 → (♯‘𝑉) = ((𝐾 · (𝐾 − 1)) + 1)))
Theorem	frrusgrord 30360	If a nonempty finite friendship graph is k-regular, its order is k(k-1)+1. This corresponds to claim 3 in [Huneke] p. 2: "Next we claim that the number n of vertices in G is exactly k(k-1)+1.". Variant of frrusgrord0 30359, using the definition RegUSGraph (df-rusgr 29576). (Contributed by Alexander van der Vekens, 25-Aug-2018.) (Revised by AV, 26-May-2021.) (Proof shortened by AV, 12-Jan-2022.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) → ((𝐺 ∈ FriendGraph ∧ 𝐺 RegUSGraph 𝐾) → (♯‘𝑉) = ((𝐾 · (𝐾 − 1)) + 1)))
Theorem	numclwwlk2lem1lem 30361	Lemma for numclwwlk2lem1 30395. (Contributed by Alexander van der Vekens, 3-Oct-2018.) (Revised by AV, 27-May-2021.) (Revised by AV, 15-Mar-2022.)
⊢ ((𝑋 ∈ (Vtx‘𝐺) ∧ 𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ (lastS‘𝑊) ≠ (𝑊‘0)) → (((𝑊 ++ ⟨“𝑋”⟩)‘0) = (𝑊‘0) ∧ ((𝑊 ++ ⟨“𝑋”⟩)‘𝑁) ≠ (𝑊‘0)))
Theorem	2clwwlklem 30362	Lemma for clwwnonrepclwwnon 30364 and extwwlkfab 30371. (Contributed by Alexander van der Vekens, 18-Sep-2018.) (Revised by AV, 10-May-2022.) (Revised by AV, 30-Oct-2022.)
⊢ ((𝑊 ∈ (𝑁 ClWWalksN 𝐺) ∧ 𝑁 ∈ (ℤ≥‘3)) → ((𝑊 prefix (𝑁 − 2))‘0) = (𝑊‘0))
Theorem	clwwnrepclwwn 30363	If the initial vertex of a closed walk occurs another time in the walk, the walk starts with a closed walk. Notice that 3 ≤ 𝑁 is required, because for 𝑁 = 2, (𝑤 prefix (𝑁 − 2)) = (𝑤 prefix 0) = ∅, but ∅ (and anything else) is not a representation of an empty closed walk as word, see clwwlkn0 30047. (Contributed by Alexander van der Vekens, 15-Sep-2018.) (Revised by AV, 28-May-2021.) (Revised by AV, 30-Oct-2022.)
⊢ ((𝑁 ∈ (ℤ≥‘3) ∧ 𝑊 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑊‘(𝑁 − 2)) = (𝑊‘0)) → (𝑊 prefix (𝑁 − 2)) ∈ ((𝑁 − 2) ClWWalksN 𝐺))
Theorem	clwwnonrepclwwnon 30364	If the initial vertex of a closed walk occurs another time in the walk, the walk starts with a closed walk on this vertex. See also the remarks in clwwnrepclwwn 30363. (Contributed by AV, 24-Apr-2022.) (Revised by AV, 10-May-2022.) (Revised by AV, 30-Oct-2022.)
⊢ ((𝑁 ∈ (ℤ≥‘3) ∧ 𝑊 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ∧ (𝑊‘(𝑁 − 2)) = 𝑋) → (𝑊 prefix (𝑁 − 2)) ∈ (𝑋(ClWWalksNOn‘𝐺)(𝑁 − 2)))
Theorem	2clwwlk2clwwlklem 30365	Lemma for 2clwwlk2clwwlk 30369. (Contributed by AV, 27-Apr-2022.)
⊢ ((𝑁 ∈ (ℤ≥‘3) ∧ 𝑊 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ∧ (𝑊‘(𝑁 − 2)) = (𝑊‘0)) → (𝑊 substr ⟨(𝑁 − 2), 𝑁⟩) ∈ (𝑋(ClWWalksNOn‘𝐺)2))
Theorem	2clwwlk 30366*	Value of operation 𝐶, mapping a vertex v and an integer n greater than 1 to the "closed n-walks v(0) ... v(n-2) v(n-1) v(n) from v = v(0) = v(n) with v(n-2) = v" according to definition 6 in [Huneke] p. 2. Such closed walks are "double loops" consisting of a closed (n-2)-walk v = v(0) ... v(n-2) = v and a closed 2-walk v = v(n-2) v(n-1) v(n) = v, see 2clwwlk2clwwlk 30369. (𝑋𝐶𝑁) is called the "set of double loops of length 𝑁 on vertex 𝑋 " in the following. (Contributed by Alexander van der Vekens, 14-Sep-2018.) (Revised by AV, 29-May-2021.) (Revised by AV, 20-Apr-2022.)
⊢ 𝐶 = (𝑣 ∈ 𝑉, 𝑛 ∈ (ℤ≥‘2) ↦ {𝑤 ∈ (𝑣(ClWWalksNOn‘𝐺)𝑛) ∣ (𝑤‘(𝑛 − 2)) = 𝑣})    ⇒   ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2)) → (𝑋𝐶𝑁) = {𝑤 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ∣ (𝑤‘(𝑁 − 2)) = 𝑋})
Theorem	2clwwlk2 30367*	The set (𝑋𝐶2) of double loops of length 2 on a vertex 𝑋 is equal to the set of closed walks with length 2 on 𝑋. Considered as "double loops", the first of the two closed walks/loops is degenerated, i.e., has length 0. (Contributed by AV, 18-Feb-2022.) (Revised by AV, 20-Apr-2022.)
⊢ 𝐶 = (𝑣 ∈ 𝑉, 𝑛 ∈ (ℤ≥‘2) ↦ {𝑤 ∈ (𝑣(ClWWalksNOn‘𝐺)𝑛) ∣ (𝑤‘(𝑛 − 2)) = 𝑣})    ⇒   ⊢ (𝑋 ∈ 𝑉 → (𝑋𝐶2) = (𝑋(ClWWalksNOn‘𝐺)2))
Theorem	2clwwlkel 30368*	Characterization of an element of the value of operation 𝐶, i.e., of a word being a double loop of length 𝑁 on vertex 𝑋. (Contributed by Alexander van der Vekens, 24-Sep-2018.) (Revised by AV, 29-May-2021.) (Revised by AV, 20-Apr-2022.)
⊢ 𝐶 = (𝑣 ∈ 𝑉, 𝑛 ∈ (ℤ≥‘2) ↦ {𝑤 ∈ (𝑣(ClWWalksNOn‘𝐺)𝑛) ∣ (𝑤‘(𝑛 − 2)) = 𝑣})    ⇒   ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2)) → (𝑊 ∈ (𝑋𝐶𝑁) ↔ (𝑊 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ∧ (𝑊‘(𝑁 − 2)) = 𝑋)))
Theorem	2clwwlk2clwwlk 30369*	An element of the value of operation 𝐶, i.e., a word being a double loop of length 𝑁 on vertex 𝑋, is composed of two closed walks. (Contributed by AV, 28-Apr-2022.) (Proof shortened by AV, 3-Nov-2022.)
⊢ 𝐶 = (𝑣 ∈ 𝑉, 𝑛 ∈ (ℤ≥‘2) ↦ {𝑤 ∈ (𝑣(ClWWalksNOn‘𝐺)𝑛) ∣ (𝑤‘(𝑛 − 2)) = 𝑣})    ⇒   ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)) → (𝑊 ∈ (𝑋𝐶𝑁) ↔ ∃𝑎 ∈ (𝑋(ClWWalksNOn‘𝐺)(𝑁 − 2))∃𝑏 ∈ (𝑋(ClWWalksNOn‘𝐺)2)𝑊 = (𝑎 ++ 𝑏)))
Theorem	numclwwlk1lem2foalem 30370	Lemma for numclwwlk1lem2foa 30373. (Contributed by AV, 29-May-2021.) (Revised by AV, 1-Nov-2022.)
⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = (𝑁 − 2)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) ∧ 𝑁 ∈ (ℤ≥‘3)) → ((((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩) prefix (𝑁 − 2)) = 𝑊 ∧ (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(𝑁 − 1)) = 𝑌 ∧ (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(𝑁 − 2)) = 𝑋))
Theorem	extwwlkfab 30371*	The set (𝑋𝐶𝑁) of double loops of length 𝑁 on vertex 𝑋 can be constructed from the set 𝐹 of closed walks on 𝑋 with length smaller by 2 than the fixed length by appending a neighbor of the last vertex and afterwards the last vertex (which is the first vertex) itself ("walking forth and back" from the last vertex). 3 ≤ 𝑁 is required since for 𝑁 = 2: 𝐹 = (𝑋(ClWWalksNOn‘𝐺)0) = ∅ (see clwwlk0on0 30111 stating that a closed walk of length 0 is not represented as word), which would result in an empty set on the right hand side, but (𝑋𝐶𝑁) needs not be empty, see 2clwwlk2 30367. (Contributed by Alexander van der Vekens, 18-Sep-2018.) (Revised by AV, 29-May-2021.) (Revised by AV, 31-Oct-2022.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐶 = (𝑣 ∈ 𝑉, 𝑛 ∈ (ℤ≥‘2) ↦ {𝑤 ∈ (𝑣(ClWWalksNOn‘𝐺)𝑛) ∣ (𝑤‘(𝑛 − 2)) = 𝑣})    &   ⊢ 𝐹 = (𝑋(ClWWalksNOn‘𝐺)(𝑁 − 2))    ⇒   ⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)) → (𝑋𝐶𝑁) = {𝑤 ∈ (𝑁 ClWWalksN 𝐺) ∣ ((𝑤 prefix (𝑁 − 2)) ∈ 𝐹 ∧ (𝑤‘(𝑁 − 1)) ∈ (𝐺 NeighbVtx 𝑋) ∧ (𝑤‘(𝑁 − 2)) = 𝑋)})
Theorem	extwwlkfabel 30372*	Characterization of an element of the set (𝑋𝐶𝑁), i.e., a double loop of length 𝑁 on vertex 𝑋 with a construction from the set 𝐹 of closed walks on 𝑋 with length smaller by 2 than the fixed length by appending a neighbor of the last vertex and afterwards the last vertex (which is the first vertex) itself ("walking forth and back" from the last vertex). (Contributed by AV, 22-Feb-2022.) (Revised by AV, 31-Oct-2022.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐶 = (𝑣 ∈ 𝑉, 𝑛 ∈ (ℤ≥‘2) ↦ {𝑤 ∈ (𝑣(ClWWalksNOn‘𝐺)𝑛) ∣ (𝑤‘(𝑛 − 2)) = 𝑣})    &   ⊢ 𝐹 = (𝑋(ClWWalksNOn‘𝐺)(𝑁 − 2))    ⇒   ⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)) → (𝑊 ∈ (𝑋𝐶𝑁) ↔ (𝑊 ∈ (𝑁 ClWWalksN 𝐺) ∧ ((𝑊 prefix (𝑁 − 2)) ∈ 𝐹 ∧ (𝑊‘(𝑁 − 1)) ∈ (𝐺 NeighbVtx 𝑋) ∧ (𝑊‘(𝑁 − 2)) = 𝑋))))
Theorem	numclwwlk1lem2foa 30373*	Going forth and back from the end of a (closed) walk: 𝑊 represents the closed walk p0, ..., p(n-2), p0 = p(n-2). With 𝑋 = p(n-2) = p0 and 𝑌 = p(n-1), ((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩) represents the closed walk p0, ..., p(n-2), p(n-1), pn = p0 which is a double loop of length 𝑁 on vertex 𝑋. (Contributed by Alexander van der Vekens, 22-Sep-2018.) (Revised by AV, 29-May-2021.) (Revised by AV, 5-Mar-2022.) (Proof shortened by AV, 2-Nov-2022.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐶 = (𝑣 ∈ 𝑉, 𝑛 ∈ (ℤ≥‘2) ↦ {𝑤 ∈ (𝑣(ClWWalksNOn‘𝐺)𝑛) ∣ (𝑤‘(𝑛 − 2)) = 𝑣})    &   ⊢ 𝐹 = (𝑋(ClWWalksNOn‘𝐺)(𝑁 − 2))    ⇒   ⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)) → ((𝑊 ∈ 𝐹 ∧ 𝑌 ∈ (𝐺 NeighbVtx 𝑋)) → ((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩) ∈ (𝑋𝐶𝑁)))
Theorem	numclwwlk1lem2f 30374*	𝑇 is a function, mapping a double loop of length 𝑁 on vertex 𝑋 to the ordered pair of the first loop and the successor of 𝑋 in the second loop, which must be a neighbor of 𝑋. (Contributed by Alexander van der Vekens, 19-Sep-2018.) (Revised by AV, 29-May-2021.) (Proof shortened by AV, 23-Feb-2022.) (Revised by AV, 31-Oct-2022.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐶 = (𝑣 ∈ 𝑉, 𝑛 ∈ (ℤ≥‘2) ↦ {𝑤 ∈ (𝑣(ClWWalksNOn‘𝐺)𝑛) ∣ (𝑤‘(𝑛 − 2)) = 𝑣})    &   ⊢ 𝐹 = (𝑋(ClWWalksNOn‘𝐺)(𝑁 − 2))    &   ⊢ 𝑇 = (𝑢 ∈ (𝑋𝐶𝑁) ↦ ⟨(𝑢 prefix (𝑁 − 2)), (𝑢‘(𝑁 − 1))⟩)    ⇒   ⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)) → 𝑇:(𝑋𝐶𝑁)⟶(𝐹 × (𝐺 NeighbVtx 𝑋)))
Theorem	numclwwlk1lem2fv 30375*	Value of the function 𝑇. (Contributed by Alexander van der Vekens, 20-Sep-2018.) (Revised by AV, 29-May-2021.) (Revised by AV, 31-Oct-2022.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐶 = (𝑣 ∈ 𝑉, 𝑛 ∈ (ℤ≥‘2) ↦ {𝑤 ∈ (𝑣(ClWWalksNOn‘𝐺)𝑛) ∣ (𝑤‘(𝑛 − 2)) = 𝑣})    &   ⊢ 𝐹 = (𝑋(ClWWalksNOn‘𝐺)(𝑁 − 2))    &   ⊢ 𝑇 = (𝑢 ∈ (𝑋𝐶𝑁) ↦ ⟨(𝑢 prefix (𝑁 − 2)), (𝑢‘(𝑁 − 1))⟩)    ⇒   ⊢ (𝑊 ∈ (𝑋𝐶𝑁) → (𝑇‘𝑊) = ⟨(𝑊 prefix (𝑁 − 2)), (𝑊‘(𝑁 − 1))⟩)
Theorem	numclwwlk1lem2f1 30376*	𝑇 is a 1-1 function. (Contributed by AV, 26-Sep-2018.) (Revised by AV, 29-May-2021.) (Proof shortened by AV, 23-Feb-2022.) (Revised by AV, 31-Oct-2022.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐶 = (𝑣 ∈ 𝑉, 𝑛 ∈ (ℤ≥‘2) ↦ {𝑤 ∈ (𝑣(ClWWalksNOn‘𝐺)𝑛) ∣ (𝑤‘(𝑛 − 2)) = 𝑣})    &   ⊢ 𝐹 = (𝑋(ClWWalksNOn‘𝐺)(𝑁 − 2))    &   ⊢ 𝑇 = (𝑢 ∈ (𝑋𝐶𝑁) ↦ ⟨(𝑢 prefix (𝑁 − 2)), (𝑢‘(𝑁 − 1))⟩)    ⇒   ⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)) → 𝑇:(𝑋𝐶𝑁)–1-1→(𝐹 × (𝐺 NeighbVtx 𝑋)))
Theorem	numclwwlk1lem2fo 30377*	𝑇 is an onto function. (Contributed by Alexander van der Vekens, 20-Sep-2018.) (Revised by AV, 29-May-2021.) (Proof shortened by AV, 13-Feb-2022.) (Revised by AV, 31-Oct-2022.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐶 = (𝑣 ∈ 𝑉, 𝑛 ∈ (ℤ≥‘2) ↦ {𝑤 ∈ (𝑣(ClWWalksNOn‘𝐺)𝑛) ∣ (𝑤‘(𝑛 − 2)) = 𝑣})    &   ⊢ 𝐹 = (𝑋(ClWWalksNOn‘𝐺)(𝑁 − 2))    &   ⊢ 𝑇 = (𝑢 ∈ (𝑋𝐶𝑁) ↦ ⟨(𝑢 prefix (𝑁 − 2)), (𝑢‘(𝑁 − 1))⟩)    ⇒   ⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)) → 𝑇:(𝑋𝐶𝑁)–onto→(𝐹 × (𝐺 NeighbVtx 𝑋)))
Theorem	numclwwlk1lem2f1o 30378*	𝑇 is a 1-1 onto function. (Contributed by Alexander van der Vekens, 26-Sep-2018.) (Revised by AV, 29-May-2021.) (Revised by AV, 6-Mar-2022.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐶 = (𝑣 ∈ 𝑉, 𝑛 ∈ (ℤ≥‘2) ↦ {𝑤 ∈ (𝑣(ClWWalksNOn‘𝐺)𝑛) ∣ (𝑤‘(𝑛 − 2)) = 𝑣})    &   ⊢ 𝐹 = (𝑋(ClWWalksNOn‘𝐺)(𝑁 − 2))    &   ⊢ 𝑇 = (𝑢 ∈ (𝑋𝐶𝑁) ↦ ⟨(𝑢 prefix (𝑁 − 2)), (𝑢‘(𝑁 − 1))⟩)    ⇒   ⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)) → 𝑇:(𝑋𝐶𝑁)–1-1-onto→(𝐹 × (𝐺 NeighbVtx 𝑋)))
Theorem	numclwwlk1lem2 30379*	The set of double loops of length 𝑁 on vertex 𝑋 and the set of closed walks of length less by 2 on 𝑋 combined with the neighbors of 𝑋 are equinumerous. (Contributed by Alexander van der Vekens, 6-Jul-2018.) (Revised by AV, 29-May-2021.) (Revised by AV, 31-Jul-2022.) (Proof shortened by AV, 3-Nov-2022.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐶 = (𝑣 ∈ 𝑉, 𝑛 ∈ (ℤ≥‘2) ↦ {𝑤 ∈ (𝑣(ClWWalksNOn‘𝐺)𝑛) ∣ (𝑤‘(𝑛 − 2)) = 𝑣})    &   ⊢ 𝐹 = (𝑋(ClWWalksNOn‘𝐺)(𝑁 − 2))    ⇒   ⊢ ((𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)) → (𝑋𝐶𝑁) ≈ (𝐹 × (𝐺 NeighbVtx 𝑋)))
Theorem	numclwwlk1 30380*	Statement 9 in [Huneke] p. 2: "If n > 1, then the number of closed n-walks v(0) ... v(n-2) v(n-1) v(n) from v = v(0) = v(n) with v(n-2) = v is kf(n-2)". Since 𝐺 is k-regular, the vertex v(n-2) = v has k neighbors v(n-1), so there are k walks from v(n-2) = v to v(n) = v (via each of v's neighbors) completing each of the f(n-2) walks from v=v(0) to v(n-2)=v. This theorem holds even for k=0, but not for n=2, since 𝐹 = ∅, but (𝑋𝐶2), the set of closed walks with length 2 on 𝑋, see 2clwwlk2 30367, needs not be ∅ in this case. This is because of the special definition of 𝐹 and the usage of words to represent (closed) walks, and does not contradict Huneke's statement, which would read "the number of closed 2-walks v(0) v(1) v(2) from v = v(0) = v(2) ... is kf(0)", where f(0)=1 is the number of empty closed walks on v, see numclwlk1lem1 30388. If the general representation of (closed) walk is used, Huneke's statement can be proven even for n = 2, see numclwlk1 30390. This case, however, is not required to prove the friendship theorem. (Contributed by Alexander van der Vekens, 26-Sep-2018.) (Revised by AV, 29-May-2021.) (Revised by AV, 6-Mar-2022.) (Proof shortened by AV, 31-Jul-2022.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐶 = (𝑣 ∈ 𝑉, 𝑛 ∈ (ℤ≥‘2) ↦ {𝑤 ∈ (𝑣(ClWWalksNOn‘𝐺)𝑛) ∣ (𝑤‘(𝑛 − 2)) = 𝑣})    &   ⊢ 𝐹 = (𝑋(ClWWalksNOn‘𝐺)(𝑁 − 2))    ⇒   ⊢ (((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))) → (♯‘(𝑋𝐶𝑁)) = (𝐾 · (♯‘𝐹)))
Theorem	clwwlknonclwlknonf1o 30381*	𝐹 is a bijection between the two representations of closed walks of a fixed positive length on a fixed vertex. (Contributed by AV, 26-May-2022.) (Proof shortened by AV, 7-Aug-2022.) (Revised by AV, 1-Nov-2022.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑊 = {𝑤 ∈ (ClWalks‘𝐺) ∣ ((♯‘(1st ‘𝑤)) = 𝑁 ∧ ((2nd ‘𝑤)‘0) = 𝑋)}    &   ⊢ 𝐹 = (𝑐 ∈ 𝑊 ↦ ((2nd ‘𝑐) prefix (♯‘(1st ‘𝑐))))    ⇒   ⊢ ((𝐺 ∈ USPGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → 𝐹:𝑊–1-1-onto→(𝑋(ClWWalksNOn‘𝐺)𝑁))
Theorem	clwwlknonclwlknonen 30382*	The sets of the two representations of closed walks of a fixed positive length on a fixed vertex are equinumerous. (Contributed by AV, 27-May-2022.) (Proof shortened by AV, 3-Nov-2022.)
⊢ ((𝐺 ∈ USPGraph ∧ 𝑋 ∈ (Vtx‘𝐺) ∧ 𝑁 ∈ ℕ) → {𝑤 ∈ (ClWalks‘𝐺) ∣ ((♯‘(1st ‘𝑤)) = 𝑁 ∧ ((2nd ‘𝑤)‘0) = 𝑋)} ≈ (𝑋(ClWWalksNOn‘𝐺)𝑁))
Theorem	dlwwlknondlwlknonf1olem1 30383	Lemma 1 for dlwwlknondlwlknonf1o 30384. (Contributed by AV, 29-May-2022.) (Revised by AV, 1-Nov-2022.)
⊢ (((♯‘(1st ‘𝑐)) = 𝑁 ∧ 𝑐 ∈ (ClWalks‘𝐺) ∧ 𝑁 ∈ (ℤ≥‘2)) → (((2nd ‘𝑐) prefix (♯‘(1st ‘𝑐)))‘(𝑁 − 2)) = ((2nd ‘𝑐)‘(𝑁 − 2)))
Theorem	dlwwlknondlwlknonf1o 30384*	𝐹 is a bijection between the two representations of double loops of a fixed positive length on a fixed vertex. (Contributed by AV, 30-May-2022.) (Revised by AV, 1-Nov-2022.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑊 = {𝑤 ∈ (ClWalks‘𝐺) ∣ ((♯‘(1st ‘𝑤)) = 𝑁 ∧ ((2nd ‘𝑤)‘0) = 𝑋 ∧ ((2nd ‘𝑤)‘(𝑁 − 2)) = 𝑋)}    &   ⊢ 𝐷 = {𝑤 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ∣ (𝑤‘(𝑁 − 2)) = 𝑋}    &   ⊢ 𝐹 = (𝑐 ∈ 𝑊 ↦ ((2nd ‘𝑐) prefix (♯‘(1st ‘𝑐))))    ⇒   ⊢ ((𝐺 ∈ USPGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2)) → 𝐹:𝑊–1-1-onto→𝐷)
Theorem	dlwwlknondlwlknonen 30385*	The sets of the two representations of double loops of a fixed length on a fixed vertex are equinumerous. (Contributed by AV, 30-May-2022.) (Proof shortened by AV, 3-Nov-2022.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑊 = {𝑤 ∈ (ClWalks‘𝐺) ∣ ((♯‘(1st ‘𝑤)) = 𝑁 ∧ ((2nd ‘𝑤)‘0) = 𝑋 ∧ ((2nd ‘𝑤)‘(𝑁 − 2)) = 𝑋)}    &   ⊢ 𝐷 = {𝑤 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ∣ (𝑤‘(𝑁 − 2)) = 𝑋}    ⇒   ⊢ ((𝐺 ∈ USPGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2)) → 𝑊 ≈ 𝐷)
Theorem	wlkl0 30386*	There is exactly one walk of length 0 on each vertex 𝑋. (Contributed by AV, 4-Jun-2022.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (𝑋 ∈ 𝑉 → {𝑤 ∈ (ClWalks‘𝐺) ∣ ((♯‘(1st ‘𝑤)) = 0 ∧ ((2nd ‘𝑤)‘0) = 𝑋)} = {⟨∅, {⟨0, 𝑋⟩}⟩})
Theorem	clwlknon2num 30387*	There are k walks of length 2 on each vertex 𝑋 in a k-regular simple graph. Variant of clwwlknon2num 30124, using the general definition of walks instead of walks as words. (Contributed by AV, 4-Jun-2022.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾 ∧ 𝑋 ∈ 𝑉) → (♯‘{𝑤 ∈ (ClWalks‘𝐺) ∣ ((♯‘(1st ‘𝑤)) = 2 ∧ ((2nd ‘𝑤)‘0) = 𝑋)}) = 𝐾)
Theorem	numclwlk1lem1 30388*	Lemma 1 for numclwlk1 30390 (Statement 9 in [Huneke] p. 2 for n=2): "the number of closed 2-walks v(0) v(1) v(2) from v = v(0) = v(2) ... is kf(0)". (Contributed by AV, 23-May-2022.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐶 = {𝑤 ∈ (ClWalks‘𝐺) ∣ ((♯‘(1st ‘𝑤)) = 𝑁 ∧ ((2nd ‘𝑤)‘0) = 𝑋 ∧ ((2nd ‘𝑤)‘(𝑁 − 2)) = 𝑋)}    &   ⊢ 𝐹 = {𝑤 ∈ (ClWalks‘𝐺) ∣ ((♯‘(1st ‘𝑤)) = (𝑁 − 2) ∧ ((2nd ‘𝑤)‘0) = 𝑋)}    ⇒   ⊢ (((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 = 2)) → (♯‘𝐶) = (𝐾 · (♯‘𝐹)))
Theorem	numclwlk1lem2 30389*	Lemma 2 for numclwlk1 30390 (Statement 9 in [Huneke] p. 2 for n>2). This theorem corresponds to numclwwlk1 30380, using the general definition of walks instead of walks as words. (Contributed by AV, 4-Jun-2022.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐶 = {𝑤 ∈ (ClWalks‘𝐺) ∣ ((♯‘(1st ‘𝑤)) = 𝑁 ∧ ((2nd ‘𝑤)‘0) = 𝑋 ∧ ((2nd ‘𝑤)‘(𝑁 − 2)) = 𝑋)}    &   ⊢ 𝐹 = {𝑤 ∈ (ClWalks‘𝐺) ∣ ((♯‘(1st ‘𝑤)) = (𝑁 − 2) ∧ ((2nd ‘𝑤)‘0) = 𝑋)}    ⇒   ⊢ (((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))) → (♯‘𝐶) = (𝐾 · (♯‘𝐹)))
Theorem	numclwlk1 30390*	Statement 9 in [Huneke] p. 2: "If n > 1, then the number of closed n-walks v(0) ... v(n-2) v(n-1) v(n) from v = v(0) = v(n) with v(n-2) = v is kf(n-2)". Since 𝐺 is k-regular, the vertex v(n-2) = v has k neighbors v(n-1), so there are k walks from v(n-2) = v to v(n) = v (via each of v's neighbors) completing each of the f(n-2) walks from v=v(0) to v(n-2)=v. This theorem holds even for k=0. (Contributed by AV, 23-May-2022.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐶 = {𝑤 ∈ (ClWalks‘𝐺) ∣ ((♯‘(1st ‘𝑤)) = 𝑁 ∧ ((2nd ‘𝑤)‘0) = 𝑋 ∧ ((2nd ‘𝑤)‘(𝑁 − 2)) = 𝑋)}    &   ⊢ 𝐹 = {𝑤 ∈ (ClWalks‘𝐺) ∣ ((♯‘(1st ‘𝑤)) = (𝑁 − 2) ∧ ((2nd ‘𝑤)‘0) = 𝑋)}    ⇒   ⊢ (((𝑉 ∈ Fin ∧ 𝐺 RegUSGraph 𝐾) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2))) → (♯‘𝐶) = (𝐾 · (♯‘𝐹)))
Theorem	numclwwlkovh0 30391*	Value of operation 𝐻, mapping a vertex 𝑣 and an integer 𝑛 greater than 1 to the "closed n-walks v(0) ... v(n-2) v(n-1) v(n) from v = v(0) = v(n) ... with v(n-2) =/= v" according to definition 7 in [Huneke] p. 2. (Contributed by AV, 1-May-2022.)
⊢ 𝐻 = (𝑣 ∈ 𝑉, 𝑛 ∈ (ℤ≥‘2) ↦ {𝑤 ∈ (𝑣(ClWWalksNOn‘𝐺)𝑛) ∣ (𝑤‘(𝑛 − 2)) ≠ 𝑣})    ⇒   ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2)) → (𝑋𝐻𝑁) = {𝑤 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ∣ (𝑤‘(𝑁 − 2)) ≠ 𝑋})
Theorem	numclwwlkovh 30392*	Value of operation 𝐻, mapping a vertex 𝑣 and an integer 𝑛 greater than 1 to the "closed n-walks v(0) ... v(n-2) v(n-1) v(n) from v = v(0) = v(n) ... with v(n-2) =/= v" according to definition 7 in [Huneke] p. 2. Definition of ClWWalksNOn resolved. (Contributed by Alexander van der Vekens, 26-Aug-2018.) (Revised by AV, 30-May-2021.) (Revised by AV, 1-May-2022.)
⊢ 𝐻 = (𝑣 ∈ 𝑉, 𝑛 ∈ (ℤ≥‘2) ↦ {𝑤 ∈ (𝑣(ClWWalksNOn‘𝐺)𝑛) ∣ (𝑤‘(𝑛 − 2)) ≠ 𝑣})    ⇒   ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2)) → (𝑋𝐻𝑁) = {𝑤 ∈ (𝑁 ClWWalksN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ (𝑤‘(𝑁 − 2)) ≠ (𝑤‘0))})
Theorem	numclwwlkovq 30393*	Value of operation 𝑄, mapping a vertex 𝑣 and a positive integer 𝑛 to the not closed walks v(0) ... v(n) of length 𝑛 from a fixed vertex 𝑣 = v(0). "Not closed" means v(n) =/= v(0). Remark: 𝑛 ∈ ℕ0 would not be useful: numclwwlkqhash 30394 would not hold, because (𝐾↑0) = 1! (Contributed by Alexander van der Vekens, 27-Sep-2018.) (Revised by AV, 30-May-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑄 = (𝑣 ∈ 𝑉, 𝑛 ∈ ℕ ↦ {𝑤 ∈ (𝑛 WWalksN 𝐺) ∣ ((𝑤‘0) = 𝑣 ∧ (lastS‘𝑤) ≠ 𝑣)})    ⇒   ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (𝑋𝑄𝑁) = {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ ((𝑤‘0) = 𝑋 ∧ (lastS‘𝑤) ≠ 𝑋)})
Theorem	numclwwlkqhash 30394*	In a 𝐾-regular graph, the size of the set of walks of length 𝑁 starting with a fixed vertex 𝑋 and ending not at this vertex is the difference between 𝐾 to the power of 𝑁 and the size of the set of closed walks of length 𝑁 on vertex 𝑋. (Contributed by Alexander van der Vekens, 30-Sep-2018.) (Revised by AV, 30-May-2021.) (Revised by AV, 5-Mar-2022.) (Proof shortened by AV, 7-Jul-2022.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑄 = (𝑣 ∈ 𝑉, 𝑛 ∈ ℕ ↦ {𝑤 ∈ (𝑛 WWalksN 𝐺) ∣ ((𝑤‘0) = 𝑣 ∧ (lastS‘𝑤) ≠ 𝑣)})    ⇒   ⊢ (((𝐺 RegUSGraph 𝐾 ∧ 𝑉 ∈ Fin) ∧ (𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ)) → (♯‘(𝑋𝑄𝑁)) = ((𝐾↑𝑁) − (♯‘(𝑋(ClWWalksNOn‘𝐺)𝑁))))
Theorem	numclwwlk2lem1 30395*	In a friendship graph, for each walk of length 𝑛 starting at a fixed vertex 𝑣 and ending not at this vertex, there is a unique vertex so that the walk extended by an edge to this vertex and an edge from this vertex to the first vertex of the walk is a value of operation 𝐻. If the walk is represented as a word, it is sufficient to add one vertex to the word to obtain the closed walk contained in the value of operation 𝐻, since in a word representing a closed walk the starting vertex is not repeated at the end. This theorem generally holds only for friendship graphs, because these guarantee that for the first and last vertex there is a (unique) third vertex "in between". (Contributed by Alexander van der Vekens, 3-Oct-2018.) (Revised by AV, 30-May-2021.) (Revised by AV, 1-May-2022.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑄 = (𝑣 ∈ 𝑉, 𝑛 ∈ ℕ ↦ {𝑤 ∈ (𝑛 WWalksN 𝐺) ∣ ((𝑤‘0) = 𝑣 ∧ (lastS‘𝑤) ≠ 𝑣)})    &   ⊢ 𝐻 = (𝑣 ∈ 𝑉, 𝑛 ∈ (ℤ≥‘2) ↦ {𝑤 ∈ (𝑣(ClWWalksNOn‘𝐺)𝑛) ∣ (𝑤‘(𝑛 − 2)) ≠ 𝑣})    ⇒   ⊢ ((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (𝑊 ∈ (𝑋𝑄𝑁) → ∃!𝑣 ∈ 𝑉 (𝑊 ++ ⟨“𝑣”⟩) ∈ (𝑋𝐻(𝑁 + 2))))
Theorem	numclwlk2lem2f 30396*	𝑅 is a function mapping the "closed (n+2)-walks v(0) ... v(n-2) v(n-1) v(n) v(n+1) v(n+2) starting at 𝑋 = v(0) = v(n+2) with v(n) =/= X" to the words representing the prefix v(0) ... v(n-2) v(n-1) v(n) of the walk. (Contributed by Alexander van der Vekens, 5-Oct-2018.) (Revised by AV, 31-May-2021.) (Proof shortened by AV, 23-Mar-2022.) (Revised by AV, 1-Nov-2022.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑄 = (𝑣 ∈ 𝑉, 𝑛 ∈ ℕ ↦ {𝑤 ∈ (𝑛 WWalksN 𝐺) ∣ ((𝑤‘0) = 𝑣 ∧ (lastS‘𝑤) ≠ 𝑣)})    &   ⊢ 𝐻 = (𝑣 ∈ 𝑉, 𝑛 ∈ (ℤ≥‘2) ↦ {𝑤 ∈ (𝑣(ClWWalksNOn‘𝐺)𝑛) ∣ (𝑤‘(𝑛 − 2)) ≠ 𝑣})    &   ⊢ 𝑅 = (𝑥 ∈ (𝑋𝐻(𝑁 + 2)) ↦ (𝑥 prefix (𝑁 + 1)))    ⇒   ⊢ ((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → 𝑅:(𝑋𝐻(𝑁 + 2))⟶(𝑋𝑄𝑁))
Theorem	numclwlk2lem2fv 30397*	Value of the function 𝑅. (Contributed by Alexander van der Vekens, 6-Oct-2018.) (Revised by AV, 31-May-2021.) (Revised by AV, 1-Nov-2022.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑄 = (𝑣 ∈ 𝑉, 𝑛 ∈ ℕ ↦ {𝑤 ∈ (𝑛 WWalksN 𝐺) ∣ ((𝑤‘0) = 𝑣 ∧ (lastS‘𝑤) ≠ 𝑣)})    &   ⊢ 𝐻 = (𝑣 ∈ 𝑉, 𝑛 ∈ (ℤ≥‘2) ↦ {𝑤 ∈ (𝑣(ClWWalksNOn‘𝐺)𝑛) ∣ (𝑤‘(𝑛 − 2)) ≠ 𝑣})    &   ⊢ 𝑅 = (𝑥 ∈ (𝑋𝐻(𝑁 + 2)) ↦ (𝑥 prefix (𝑁 + 1)))    ⇒   ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (𝑊 ∈ (𝑋𝐻(𝑁 + 2)) → (𝑅‘𝑊) = (𝑊 prefix (𝑁 + 1))))
Theorem	numclwlk2lem2f1o 30398*	𝑅 is a 1-1 onto function. (Contributed by Alexander van der Vekens, 6-Oct-2018.) (Revised by AV, 21-Jan-2022.) (Proof shortened by AV, 17-Mar-2022.) (Revised by AV, 1-Nov-2022.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑄 = (𝑣 ∈ 𝑉, 𝑛 ∈ ℕ ↦ {𝑤 ∈ (𝑛 WWalksN 𝐺) ∣ ((𝑤‘0) = 𝑣 ∧ (lastS‘𝑤) ≠ 𝑣)})    &   ⊢ 𝐻 = (𝑣 ∈ 𝑉, 𝑛 ∈ (ℤ≥‘2) ↦ {𝑤 ∈ (𝑣(ClWWalksNOn‘𝐺)𝑛) ∣ (𝑤‘(𝑛 − 2)) ≠ 𝑣})    &   ⊢ 𝑅 = (𝑥 ∈ (𝑋𝐻(𝑁 + 2)) ↦ (𝑥 prefix (𝑁 + 1)))    ⇒   ⊢ ((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → 𝑅:(𝑋𝐻(𝑁 + 2))–1-1-onto→(𝑋𝑄𝑁))
Theorem	numclwwlk2lem3 30399*	In a friendship graph, the size of the set of walks of length 𝑁 starting with a fixed vertex 𝑋 and ending not at this vertex equals the size of the set of all closed walks of length (𝑁 + 2) starting at this vertex 𝑋 and not having this vertex as last but 2 vertex. (Contributed by Alexander van der Vekens, 6-Oct-2018.) (Revised by AV, 31-May-2021.) (Proof shortened by AV, 3-Nov-2022.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑄 = (𝑣 ∈ 𝑉, 𝑛 ∈ ℕ ↦ {𝑤 ∈ (𝑛 WWalksN 𝐺) ∣ ((𝑤‘0) = 𝑣 ∧ (lastS‘𝑤) ≠ 𝑣)})    &   ⊢ 𝐻 = (𝑣 ∈ 𝑉, 𝑛 ∈ (ℤ≥‘2) ↦ {𝑤 ∈ (𝑣(ClWWalksNOn‘𝐺)𝑛) ∣ (𝑤‘(𝑛 − 2)) ≠ 𝑣})    ⇒   ⊢ ((𝐺 ∈ FriendGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (♯‘(𝑋𝑄𝑁)) = (♯‘(𝑋𝐻(𝑁 + 2))))
Theorem	numclwwlk2 30400*	Statement 10 in [Huneke] p. 2: "If n > 1, then the number of closed n-walks v(0) ... v(n-2) v(n-1) v(n) from v = v(0) = v(n) ... with v(n-2) =/= v is k^(n-2) - f(n-2)." According to rusgrnumwlkg 29997, we have k^(n-2) different walks of length (n-2): v(0) ... v(n-2). From this number, the number of closed walks of length (n-2), which is f(n-2) per definition, must be subtracted, because for these walks v(n-2) =/= v(0) = v would hold. Because of the friendship condition, there is exactly one vertex v(n-1) which is a neighbor of v(n-2) as well as of v(n)=v=v(0), because v(n-2) and v(n)=v are different, so the number of walks v(0) ... v(n-2) is identical with the number of walks v(0) ... v(n), that means each (not closed) walk v(0) ... v(n-2) can be extended by two edges to a closed walk v(0) ... v(n)=v=v(0) in exactly one way. (Contributed by Alexander van der Vekens, 6-Oct-2018.) (Revised by AV, 31-May-2021.) (Revised by AV, 1-May-2022.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑄 = (𝑣 ∈ 𝑉, 𝑛 ∈ ℕ ↦ {𝑤 ∈ (𝑛 WWalksN 𝐺) ∣ ((𝑤‘0) = 𝑣 ∧ (lastS‘𝑤) ≠ 𝑣)})    &   ⊢ 𝐻 = (𝑣 ∈ 𝑉, 𝑛 ∈ (ℤ≥‘2) ↦ {𝑤 ∈ (𝑣(ClWWalksNOn‘𝐺)𝑛) ∣ (𝑤‘(𝑛 − 2)) ≠ 𝑣})    ⇒   ⊢ (((𝐺 RegUSGraph 𝐾 ∧ 𝐺 ∈ FriendGraph ) ∧ (𝑉 ∈ Fin ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3))) → (♯‘(𝑋𝐻𝑁)) = ((𝐾↑(𝑁 − 2)) − (♯‘(𝑋(ClWWalksNOn‘𝐺)(𝑁 − 2)))))