P. 296 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 29501-29600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	konigsbergumgr 29501	The Königsberg graph 𝐺 is a multigraph. (Contributed by AV, 28-Feb-2021.) (Revised by AV, 9-Mar-2021.)
⊢ 𝑉 = (0...3)    &   ⊢ 𝐸 = ⟨“{0, 1} {0, 2} {0, 3} {1, 2} {1, 2} {2, 3} {2, 3}”⟩    &   ⊢ 𝐺 = ⟨𝑉, 𝐸⟩    ⇒   ⊢ 𝐺 ∈ UMGraph
Theorem	konigsberglem1 29502	Lemma 1 for konigsberg 29507: Vertex 0 has degree three. (Contributed by Mario Carneiro, 11-Mar-2015.) (Revised by Mario Carneiro, 28-Feb-2016.) (Revised by AV, 4-Mar-2021.)
⊢ 𝑉 = (0...3)    &   ⊢ 𝐸 = ⟨“{0, 1} {0, 2} {0, 3} {1, 2} {1, 2} {2, 3} {2, 3}”⟩    &   ⊢ 𝐺 = ⟨𝑉, 𝐸⟩    ⇒   ⊢ ((VtxDeg‘𝐺)‘0) = 3
Theorem	konigsberglem2 29503	Lemma 2 for konigsberg 29507: Vertex 1 has degree three. (Contributed by Mario Carneiro, 11-Mar-2015.) (Revised by Mario Carneiro, 28-Feb-2016.) (Revised by AV, 4-Mar-2021.)
⊢ 𝑉 = (0...3)    &   ⊢ 𝐸 = ⟨“{0, 1} {0, 2} {0, 3} {1, 2} {1, 2} {2, 3} {2, 3}”⟩    &   ⊢ 𝐺 = ⟨𝑉, 𝐸⟩    ⇒   ⊢ ((VtxDeg‘𝐺)‘1) = 3
Theorem	konigsberglem3 29504	Lemma 3 for konigsberg 29507: Vertex 3 has degree three. (Contributed by Mario Carneiro, 11-Mar-2015.) (Revised by Mario Carneiro, 28-Feb-2016.) (Revised by AV, 4-Mar-2021.)
⊢ 𝑉 = (0...3)    &   ⊢ 𝐸 = ⟨“{0, 1} {0, 2} {0, 3} {1, 2} {1, 2} {2, 3} {2, 3}”⟩    &   ⊢ 𝐺 = ⟨𝑉, 𝐸⟩    ⇒   ⊢ ((VtxDeg‘𝐺)‘3) = 3
Theorem	konigsberglem4 29505*	Lemma 4 for konigsberg 29507: Vertices 0, 1, 3 are vertices of odd degree. (Contributed by Mario Carneiro, 11-Mar-2015.) (Revised by AV, 28-Feb-2021.)
⊢ 𝑉 = (0...3)    &   ⊢ 𝐸 = ⟨“{0, 1} {0, 2} {0, 3} {1, 2} {1, 2} {2, 3} {2, 3}”⟩    &   ⊢ 𝐺 = ⟨𝑉, 𝐸⟩    ⇒   ⊢ {0, 1, 3} ⊆ {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((VtxDeg‘𝐺)‘𝑥)}
Theorem	konigsberglem5 29506*	Lemma 5 for konigsberg 29507: The set of vertices of odd degree is greater than 2. (Contributed by Mario Carneiro, 11-Mar-2015.) (Revised by AV, 28-Feb-2021.)
⊢ 𝑉 = (0...3)    &   ⊢ 𝐸 = ⟨“{0, 1} {0, 2} {0, 3} {1, 2} {1, 2} {2, 3} {2, 3}”⟩    &   ⊢ 𝐺 = ⟨𝑉, 𝐸⟩    ⇒   ⊢ 2 < (♯‘{𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((VtxDeg‘𝐺)‘𝑥)})
Theorem	konigsberg 29507	The Königsberg Bridge problem. If 𝐺 is the Königsberg graph, i.e. a graph on four vertices 0, 1, 2, 3, with edges {0, 1}, {0, 2}, {0, 3}, {1, 2}, {1, 2}, {2, 3}, {2, 3}, then vertices 0, 1, 3 each have degree three, and 2 has degree five, so there are four vertices of odd degree and thus by eulerpath 29491 the graph cannot have an Eulerian path. It is sufficient to show that there are 3 vertices of odd degree, since a graph having an Eulerian path can only have 0 or 2 vertices of odd degree. This is Metamath 100 proof #54. (Contributed by Mario Carneiro, 11-Mar-2015.) (Revised by Mario Carneiro, 28-Feb-2016.) (Revised by AV, 9-Mar-2021.)
⊢ 𝑉 = (0...3)    &   ⊢ 𝐸 = ⟨“{0, 1} {0, 2} {0, 3} {1, 2} {1, 2} {2, 3} {2, 3}”⟩    &   ⊢ 𝐺 = ⟨𝑉, 𝐸⟩    ⇒   ⊢ (EulerPaths‘𝐺) = ∅
17.5  The Friendship Theorem
17.5.1  Friendship graphs - basics
Syntax	cfrgr 29508	Extend class notation with friendship graphs.
class FriendGraph
Definition	df-frgr 29509*	Define the class of all friendship graphs: a simple graph is called a friendship graph if every pair of its vertices has exactly one common neighbor. This condition is called the friendship condition , see definition in [MertziosUnger] p. 152. (Contributed by Alexander van der Vekens and Mario Carneiro, 2-Oct-2017.) (Revised by AV, 29-Mar-2021.) (Revised by AV, 3-Jan-2024.)
⊢ FriendGraph = {𝑔 ∈ USGraph ∣ [(Vtx‘𝑔) / 𝑣][(Edg‘𝑔) / 𝑒]∀𝑘 ∈ 𝑣 ∀𝑙 ∈ (𝑣 ∖ {𝑘})∃!𝑥 ∈ 𝑣 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝑒}
Theorem	isfrgr 29510*	The property of being a friendship graph. (Contributed by Alexander van der Vekens, 4-Oct-2017.) (Revised by AV, 29-Mar-2021.) (Revised by AV, 3-Jan-2024.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (𝐺 ∈ FriendGraph ↔ (𝐺 ∈ USGraph ∧ ∀𝑘 ∈ 𝑉 ∀𝑙 ∈ (𝑉 ∖ {𝑘})∃!𝑥 ∈ 𝑉 {{𝑥, 𝑘}, {𝑥, 𝑙}} ⊆ 𝐸))
Theorem	frgrusgr 29511	A friendship graph is a simple graph. (Contributed by Alexander van der Vekens, 4-Oct-2017.) (Revised by AV, 29-Mar-2021.)
⊢ (𝐺 ∈ FriendGraph → 𝐺 ∈ USGraph)
Theorem	frgr0v 29512	Any null graph (set with no vertices) is a friendship graph iff its edge function is empty. (Contributed by Alexander van der Vekens, 4-Oct-2017.) (Revised by AV, 29-Mar-2021.)
⊢ ((𝐺 ∈ 𝑊 ∧ (Vtx‘𝐺) = ∅) → (𝐺 ∈ FriendGraph ↔ (iEdg‘𝐺) = ∅))
Theorem	frgr0vb 29513	Any null graph (without vertices and edges) is a friendship graph. (Contributed by Alexander van der Vekens, 30-Sep-2017.) (Revised by AV, 29-Mar-2021.)
⊢ ((𝐺 ∈ 𝑊 ∧ (Vtx‘𝐺) = ∅ ∧ (iEdg‘𝐺) = ∅) → 𝐺 ∈ FriendGraph )
Theorem	frgruhgr0v 29514	Any null graph (without vertices) represented as hypergraph is a friendship graph. (Contributed by AV, 29-Mar-2021.)
⊢ ((𝐺 ∈ UHGraph ∧ (Vtx‘𝐺) = ∅) → 𝐺 ∈ FriendGraph )
Theorem	frgr0 29515	The null graph (graph without vertices) is a friendship graph. (Contributed by AV, 29-Mar-2021.)
⊢ ∅ ∈ FriendGraph
Theorem	frcond1 29516*	The friendship condition: any two (different) vertices in a friendship graph have a unique common neighbor. (Contributed by Alexander van der Vekens, 19-Dec-2017.) (Revised by AV, 29-Mar-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (𝐺 ∈ FriendGraph → ((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ∧ 𝐴 ≠ 𝐶) → ∃!𝑏 ∈ 𝑉 {{𝐴, 𝑏}, {𝑏, 𝐶}} ⊆ 𝐸))
Theorem	frcond2 29517*	The friendship condition: any two (different) vertices in a friendship graph have a unique common neighbor. (Contributed by Alexander van der Vekens, 19-Dec-2017.) (Revised by AV, 29-Mar-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (𝐺 ∈ FriendGraph → ((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ∧ 𝐴 ≠ 𝐶) → ∃!𝑏 ∈ 𝑉 ({𝐴, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝐶} ∈ 𝐸)))
Theorem	frgreu 29518*	Variant of frcond2 29517: Any two (different) vertices in a friendship graph have a unique common neighbor. (Contributed by Alexander van der Vekens, 18-Feb-2018.) (Revised by AV, 12-May-2021.) (Proof shortened by AV, 4-Jan-2022.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (𝐺 ∈ FriendGraph → ((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ∧ 𝐴 ≠ 𝐶) → ∃!𝑏({𝐴, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝐶} ∈ 𝐸)))
Theorem	frcond3 29519*	The friendship condition, expressed by neighborhoods: in a friendship graph, the neighborhood of a vertex and the neighborhood of a second, different vertex have exactly one vertex in common. (Contributed by Alexander van der Vekens, 19-Dec-2017.) (Revised by AV, 30-Dec-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (𝐺 ∈ FriendGraph → ((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ∧ 𝐴 ≠ 𝐶) → ∃𝑥 ∈ 𝑉 ((𝐺 NeighbVtx 𝐴) ∩ (𝐺 NeighbVtx 𝐶)) = {𝑥}))
Theorem	frcond4 29520*	The friendship condition, alternatively expressed by neighborhoods: in a friendship graph, the neighborhoods of two different vertices have exactly one vertex in common. (Contributed by Alexander van der Vekens, 19-Dec-2017.) (Revised by AV, 29-Mar-2021.) (Proof shortened by AV, 30-Dec-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (𝐺 ∈ FriendGraph → ∀𝑘 ∈ 𝑉 ∀𝑙 ∈ (𝑉 ∖ {𝑘})∃𝑥 ∈ 𝑉 ((𝐺 NeighbVtx 𝑘) ∩ (𝐺 NeighbVtx 𝑙)) = {𝑥})
17.5.2  The friendship theorem for small graphs
Theorem	frgr1v 29521	Any graph with (at most) one vertex is a friendship graph. (Contributed by Alexander van der Vekens, 4-Oct-2017.) (Revised by AV, 29-Mar-2021.)
⊢ ((𝐺 ∈ USGraph ∧ (Vtx‘𝐺) = {𝑁}) → 𝐺 ∈ FriendGraph )
Theorem	nfrgr2v 29522	Any graph with two (different) vertices is not a friendship graph. (Contributed by Alexander van der Vekens, 30-Sep-2017.) (Proof shortened by Alexander van der Vekens, 13-Sep-2018.) (Revised by AV, 29-Mar-2021.)
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐴 ≠ 𝐵) ∧ (Vtx‘𝐺) = {𝐴, 𝐵}) → 𝐺 ∉ FriendGraph )
Theorem	frgr3vlem1 29523*	Lemma 1 for frgr3v 29525. (Contributed by Alexander van der Vekens, 4-Oct-2017.) (Revised by AV, 29-Mar-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → ∀𝑥∀𝑦(((𝑥 ∈ {𝐴, 𝐵, 𝐶} ∧ {{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ 𝐸) ∧ (𝑦 ∈ {𝐴, 𝐵, 𝐶} ∧ {{𝑦, 𝐴}, {𝑦, 𝐵}} ⊆ 𝐸)) → 𝑥 = 𝑦))
Theorem	frgr3vlem2 29524*	Lemma 2 for frgr3v 29525. (Contributed by Alexander van der Vekens, 4-Oct-2017.) (Revised by AV, 29-Mar-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → ((𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph) → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ 𝐸 ↔ ({𝐶, 𝐴} ∈ 𝐸 ∧ {𝐶, 𝐵} ∈ 𝐸))))
Theorem	frgr3v 29525	Any graph with three vertices which are completely connected with each other is a friendship graph. (Contributed by Alexander van der Vekens, 5-Oct-2017.) (Revised by AV, 29-Mar-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → ((𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph) → (𝐺 ∈ FriendGraph ↔ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸))))
Theorem	1vwmgr 29526*	Every graph with one vertex (which may be connect with itself by (multiple) loops!) is a windmill graph. (Contributed by Alexander van der Vekens, 5-Oct-2017.) (Revised by AV, 31-Mar-2021.)
⊢ ((𝐴 ∈ 𝑋 ∧ 𝑉 = {𝐴}) → ∃ℎ ∈ 𝑉 ∀𝑣 ∈ (𝑉 ∖ {ℎ})({𝑣, ℎ} ∈ 𝐸 ∧ ∃!𝑤 ∈ (𝑉 ∖ {ℎ}){𝑣, 𝑤} ∈ 𝐸))
Theorem	3vfriswmgrlem 29527*	Lemma for 3vfriswmgr 29528. (Contributed by Alexander van der Vekens, 6-Oct-2017.) (Revised by AV, 31-Mar-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐴 ≠ 𝐵) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → ({𝐴, 𝐵} ∈ 𝐸 → ∃!𝑤 ∈ {𝐴, 𝐵} {𝐴, 𝑤} ∈ 𝐸))
Theorem	3vfriswmgr 29528*	Every friendship graph with three (different) vertices is a windmill graph. (Contributed by Alexander van der Vekens, 6-Oct-2017.) (Revised by AV, 31-Mar-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) ∧ 𝑉 = {𝐴, 𝐵, 𝐶}) → (𝐺 ∈ FriendGraph → ∃ℎ ∈ 𝑉 ∀𝑣 ∈ (𝑉 ∖ {ℎ})({𝑣, ℎ} ∈ 𝐸 ∧ ∃!𝑤 ∈ (𝑉 ∖ {ℎ}){𝑣, 𝑤} ∈ 𝐸)))
Theorem	1to2vfriswmgr 29529*	Every friendship graph with one or two vertices is a windmill graph. (Contributed by Alexander van der Vekens, 6-Oct-2017.) (Revised by AV, 31-Mar-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝐴 ∈ 𝑋 ∧ (𝑉 = {𝐴} ∨ 𝑉 = {𝐴, 𝐵})) → (𝐺 ∈ FriendGraph → ∃ℎ ∈ 𝑉 ∀𝑣 ∈ (𝑉 ∖ {ℎ})({𝑣, ℎ} ∈ 𝐸 ∧ ∃!𝑤 ∈ (𝑉 ∖ {ℎ}){𝑣, 𝑤} ∈ 𝐸)))
Theorem	1to3vfriswmgr 29530*	Every friendship graph with one, two or three vertices is a windmill graph. (Contributed by Alexander van der Vekens, 6-Oct-2017.) (Revised by AV, 31-Mar-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝐴 ∈ 𝑋 ∧ (𝑉 = {𝐴} ∨ 𝑉 = {𝐴, 𝐵} ∨ 𝑉 = {𝐴, 𝐵, 𝐶})) → (𝐺 ∈ FriendGraph → ∃ℎ ∈ 𝑉 ∀𝑣 ∈ (𝑉 ∖ {ℎ})({𝑣, ℎ} ∈ 𝐸 ∧ ∃!𝑤 ∈ (𝑉 ∖ {ℎ}){𝑣, 𝑤} ∈ 𝐸)))
Theorem	1to3vfriendship 29531*	The friendship theorem for small graphs: In every friendship graph with one, two or three vertices, there is a vertex which is adjacent to all other vertices. (Contributed by Alexander van der Vekens, 6-Oct-2017.) (Revised by AV, 31-Mar-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝐴 ∈ 𝑋 ∧ (𝑉 = {𝐴} ∨ 𝑉 = {𝐴, 𝐵} ∨ 𝑉 = {𝐴, 𝐵, 𝐶})) → (𝐺 ∈ FriendGraph → ∃𝑣 ∈ 𝑉 ∀𝑤 ∈ (𝑉 ∖ {𝑣}){𝑣, 𝑤} ∈ 𝐸))
17.5.3  Theorems according to Mertzios and Unger
Theorem	2pthfrgrrn 29532*	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 29533*	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 29534*	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 29535*	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 29536*	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 29537*	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 29538*	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 29539	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 29540*	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 29541	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 29542	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 29543	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 29544	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 29545	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 29546	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 29547*	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 29548	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 29649 is proven by formalizing Huneke's proof, see [Huneke] pp. 1-2. The three claims (see frgrncvvdeq 29559, frgrregorufr 29575 and frrusgrord0 29590) 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 29549	Lemma 1 for frgrncvvdeq 29559. (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 29550*	Lemma 2 for frgrncvvdeq 29559. 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 29551*	Lemma 3 for frgrncvvdeq 29559. 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 29552*	Lemma 4 for frgrncvvdeq 29559. 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 29553*	Lemma 5 for frgrncvvdeq 29559. 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 29554*	Lemma 6 for frgrncvvdeq 29559. (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 29555*	Lemma 7 for frgrncvvdeq 29559. 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 29556*	Lemma 8 for frgrncvvdeq 29559. 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 29557*	Lemma 9 for frgrncvvdeq 29559. 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 29558*	Lemma 10 for frgrncvvdeq 29559. (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 29559*	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 29560	In a friendship graph any two vertices with different degrees are connected. Alternate version of frgrwopreglem4 29565 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 29561	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 29571 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 29562*	Lemma 1 for frgrwopreg 29573: 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 29563*	Lemma 2 for frgrwopreg 29573. 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 29564*	Lemma 3 for frgrwopreg 29573. 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 29565*	Lemma 4 for frgrwopreg 29573. 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 29566*	According to statement 5 in [Huneke] p. 2: "If A ... is a singleton, then that singleton is a universal friend". This version of frgrwopreg1 29568 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 29567*	According to statement 5 in [Huneke] p. 2: "If ... B is a singleton, then that singleton is a universal friend". This version of frgrwopreg2 29569 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 29568*	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 29569*	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 29570*	Lemma for frgrwopreglem5 29571. (Contributed by AV, 5-Feb-2022.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐷 = (VtxDeg‘𝐺)    &   ⊢ 𝐴 = {𝑥 ∈ 𝑉 ∣ (𝐷‘𝑥) = 𝐾}    &   ⊢ 𝐵 = (𝑉 ∖ 𝐴)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (((𝑎 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → ((𝐷‘𝑎) = (𝐷‘𝑥) ∧ (𝐷‘𝑎) ≠ (𝐷‘𝑏) ∧ (𝐷‘𝑥) ≠ (𝐷‘𝑦)))
Theorem	frgrwopreglem5 29571*	Lemma 5 for frgrwopreg 29573. 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 29572*	Alternate direct proof of frgrwopreglem5 29571, not using frgrwopreglem5a 29561. This proof would be even a little bit shorter than the proof of frgrwopreglem5 29571 without using frgrwopreglem5lem 29570. (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 29573*	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 29574*	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 29575*	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 29576*	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 29575 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 29577*	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 29578	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 29579	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 29580	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 29581	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 29582	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 29583*	Lemma for fusgreg2wsp 29586 and related theorems. (Contributed by AV, 8-Jan-2022.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝑀 = (𝑎 ∈ 𝑉 ↦ {𝑤 ∈ (2 WSPathsN 𝐺) ∣ (𝑤‘1) = 𝑎})    ⇒   ⊢ (𝑁 ∈ 𝑉 → (𝑝 ∈ (𝑀‘𝑁) ↔ (𝑝 ∈ (2 WSPathsN 𝐺) ∧ (𝑝‘1) = 𝑁)))
Theorem	fusgr2wsp2nb 29584*	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 29585*	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 29582. (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 29586*	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 29587*	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 29588*	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 29589*	Lemma for frrusgrord0 29590. (Contributed by AV, 12-Jan-2022.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (((𝐺 ∈ FriendGraph ∧ 𝑉 ∈ Fin ∧ 𝑉 ≠ ∅) ∧ ∀𝑣 ∈ 𝑉 ((VtxDeg‘𝐺)‘𝑣) = 𝐾) → (𝐾 ∈ ℂ ∧ (♯‘𝑉) ∈ ℂ ∧ (♯‘𝑉) ≠ 0))
Theorem	frrusgrord0 29590*	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 29591	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 29590, using the definition RegUSGraph (df-rusgr 28812). (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 29592	Lemma for numclwwlk2lem1 29626. (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 29593	Lemma for clwwnonrepclwwnon 29595 and extwwlkfab 29602. (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 29594	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 29278. (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 29595	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 29594. (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 29596	Lemma for 2clwwlk2clwwlk 29600. (Contributed by AV, 27-Apr-2022.)
⊢ ((𝑁 ∈ (ℤ≥‘3) ∧ 𝑊 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ∧ (𝑊‘(𝑁 − 2)) = (𝑊‘0)) → (𝑊 substr ⟨(𝑁 − 2), 𝑁⟩) ∈ (𝑋(ClWWalksNOn‘𝐺)2))
Theorem	2clwwlk 29597*	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 29600. (𝑋𝐶𝑁) 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 29598*	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 29599*	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 29600*	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)𝑊 = (𝑎 ++ 𝑏)))