P. 309 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 30801-30900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	releupth 30801	The set (EulerPaths‘𝐺) of all Eulerian paths on 𝐺 is a set of pairs by our definition of an Eulerian path, and so is a relation. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by AV, 18-Feb-2021.)
⊢ Rel (EulerPaths‘𝐺)
Theorem	eupths 30802*	The Eulerian paths on the graph 𝐺. (Contributed by AV, 18-Feb-2021.) (Revised by AV, 29-Oct-2021.)
⊢ 𝐼 = (iEdg‘𝐺)    ⇒   ⊢ (EulerPaths‘𝐺) = {⟨𝑓, 𝑝⟩ ∣ (𝑓(Trails‘𝐺)𝑝 ∧ 𝑓:(0..^(♯‘𝑓))–onto→dom 𝐼)}
Theorem	iseupth 30803	The property "⟨𝐹, 𝑃⟩ is an Eulerian path on the graph 𝐺". An Eulerian path is defined as bijection 𝐹 from the edges to a set 0...(𝑁 − 1) and a function 𝑃:(0...𝑁)⟶𝑉 into the vertices such that for each 0 ≤ 𝑘 < 𝑁, 𝐹(𝑘) is an edge from 𝑃(𝑘) to 𝑃(𝑘 + 1). (Since the edges are undirected and there are possibly many edges between any two given vertices, we need to list both the edges and the vertices of the path separately.) (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Mario Carneiro, 3-May-2015.) (Revised by AV, 18-Feb-2021.) (Revised by AV, 30-Oct-2021.)
⊢ 𝐼 = (iEdg‘𝐺)    ⇒   ⊢ (𝐹(EulerPaths‘𝐺)𝑃 ↔ (𝐹(Trails‘𝐺)𝑃 ∧ 𝐹:(0..^(♯‘𝐹))–onto→dom 𝐼))
Theorem	iseupthf1o 30804	The property "⟨𝐹, 𝑃⟩ is an Eulerian path on the graph 𝐺". An Eulerian path is defined as bijection 𝐹 from the edges to a set 0...(𝑁 − 1) and a function 𝑃:(0...𝑁)⟶𝑉 into the vertices such that for each 0 ≤ 𝑘 < 𝑁, 𝐹(𝑘) is an edge from 𝑃(𝑘) to 𝑃(𝑘 + 1). (Since the edges are undirected and there are possibly many edges between any two given vertices, we need to list both the edges and the vertices of the path separately.) (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Mario Carneiro, 3-May-2015.) (Revised by AV, 18-Feb-2021.) (Revised by AV, 30-Oct-2021.)
⊢ 𝐼 = (iEdg‘𝐺)    ⇒   ⊢ (𝐹(EulerPaths‘𝐺)𝑃 ↔ (𝐹(Walks‘𝐺)𝑃 ∧ 𝐹:(0..^(♯‘𝐹))–1-1-onto→dom 𝐼))
Theorem	eupthi 30805	Properties of an Eulerian path. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by AV, 18-Feb-2021.) (Proof shortened by AV, 30-Oct-2021.)
⊢ 𝐼 = (iEdg‘𝐺)    ⇒   ⊢ (𝐹(EulerPaths‘𝐺)𝑃 → (𝐹(Walks‘𝐺)𝑃 ∧ 𝐹:(0..^(♯‘𝐹))–1-1-onto→dom 𝐼))
Theorem	eupthf1o 30806	The 𝐹 function in an Eulerian path is a bijection from a half-open range of nonnegative integers to the set of edges. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by AV, 18-Feb-2021.)
⊢ 𝐼 = (iEdg‘𝐺)    ⇒   ⊢ (𝐹(EulerPaths‘𝐺)𝑃 → 𝐹:(0..^(♯‘𝐹))–1-1-onto→dom 𝐼)
Theorem	eupthfi 30807	Any graph with an Eulerian path is of finite size, i.e. with a finite number of edges. (Contributed by Mario Carneiro, 7-Apr-2015.) (Revised by AV, 18-Feb-2021.)
⊢ 𝐼 = (iEdg‘𝐺)    ⇒   ⊢ (𝐹(EulerPaths‘𝐺)𝑃 → dom 𝐼 ∈ Fin)
Theorem	eupthseg 30808	The 𝑁-th edge in an eulerian path is the edge having 𝑃(𝑁) and 𝑃(𝑁 + 1) as endpoints . (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by AV, 18-Feb-2021.)
⊢ 𝐼 = (iEdg‘𝐺)    ⇒   ⊢ ((𝐹(EulerPaths‘𝐺)𝑃 ∧ 𝑁 ∈ (0..^(♯‘𝐹))) → {(𝑃‘𝑁), (𝑃‘(𝑁 + 1))} ⊆ (𝐼‘(𝐹‘𝑁)))
Theorem	upgriseupth 30809*	The property "⟨𝐹, 𝑃⟩ is an Eulerian path on the pseudograph 𝐺". (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Mario Carneiro, 3-May-2015.) (Revised by AV, 18-Feb-2021.) (Revised by AV, 30-Oct-2021.)
⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ (𝐺 ∈ UPGraph → (𝐹(EulerPaths‘𝐺)𝑃 ↔ (𝐹:(0..^(♯‘𝐹))–1-1-onto→dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(♯‘𝐹))(𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))})))
Theorem	upgreupthi 30810*	Properties of an Eulerian path in a pseudograph. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by AV, 18-Feb-2021.) (Proof shortened by AV, 30-Oct-2021.)
⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UPGraph ∧ 𝐹(EulerPaths‘𝐺)𝑃) → (𝐹:(0..^(♯‘𝐹))–1-1-onto→dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(♯‘𝐹))(𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}))
Theorem	upgreupthseg 30811	The 𝑁-th edge in an eulerian path is the edge from 𝑃(𝑁) to 𝑃(𝑁 + 1). (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by AV, 18-Feb-2021.)
⊢ 𝐼 = (iEdg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UPGraph ∧ 𝐹(EulerPaths‘𝐺)𝑃 ∧ 𝑁 ∈ (0..^(♯‘𝐹))) → (𝐼‘(𝐹‘𝑁)) = {(𝑃‘𝑁), (𝑃‘(𝑁 + 1))})
Theorem	eupthcl 30812	An Eulerian path has length ♯(𝐹), which is an integer. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by AV, 18-Feb-2021.)
⊢ (𝐹(EulerPaths‘𝐺)𝑃 → (♯‘𝐹) ∈ ℕ0)
Theorem	eupthistrl 30813	An Eulerian path is a trail. (Contributed by Alexander van der Vekens, 24-Nov-2017.) (Revised by AV, 18-Feb-2021.)
⊢ (𝐹(EulerPaths‘𝐺)𝑃 → 𝐹(Trails‘𝐺)𝑃)
Theorem	eupthiswlk 30814	An Eulerian path is a walk. (Contributed by AV, 6-Apr-2021.)
⊢ (𝐹(EulerPaths‘𝐺)𝑃 → 𝐹(Walks‘𝐺)𝑃)
Theorem	eupthpf 30815	The 𝑃 function in an Eulerian path is a function from a finite sequence of nonnegative integers to the vertices. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by AV, 18-Feb-2021.)
⊢ (𝐹(EulerPaths‘𝐺)𝑃 → 𝑃:(0...(♯‘𝐹))⟶(Vtx‘𝐺))
Theorem	eupth0 30816	There is an Eulerian path on an empty graph, i.e. a graph with at least one vertex, but without an edge. (Contributed by Mario Carneiro, 7-Apr-2015.) (Revised by AV, 5-Mar-2021.) (Proof shortened by AV, 30-Oct-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐼 = ∅) → ∅(EulerPaths‘𝐺){⟨0, 𝐴⟩})
Theorem	eupthres 30817	The restriction ⟨𝐻, 𝑄⟩ of an Eulerian path ⟨𝐹, 𝑃⟩ to an initial segment of the path (of length 𝑁) forms an Eulerian path on the subgraph 𝑆 consisting of the edges in the initial segment. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Mario Carneiro, 3-May-2015.) (Revised by AV, 6-Mar-2021.) Hypothesis revised using the prefix operation. (Revised by AV, 30-Nov-2022.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ (𝜑 → 𝐹(EulerPaths‘𝐺)𝑃)    &   ⊢ (𝜑 → 𝑁 ∈ (0..^(♯‘𝐹)))    &   ⊢ (𝜑 → (iEdg‘𝑆) = (𝐼 ↾ (𝐹 “ (0..^𝑁))))    &   ⊢ 𝐻 = (𝐹 prefix 𝑁)    &   ⊢ 𝑄 = (𝑃 ↾ (0...𝑁))    &   ⊢ (Vtx‘𝑆) = 𝑉    ⇒   ⊢ (𝜑 → 𝐻(EulerPaths‘𝑆)𝑄)
Theorem	eupthp1 30818	Append one path segment to an Eulerian path ⟨𝐹, 𝑃⟩ to become an Eulerian path ⟨𝐻, 𝑄⟩ of the supergraph 𝑆 obtained by adding the new edge to the graph 𝐺. (Contributed by Mario Carneiro, 7-Apr-2015.) (Revised by AV, 7-Mar-2021.) (Proof shortened by AV, 30-Oct-2021.) (Revised by AV, 8-Apr-2024.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ (𝜑 → Fun 𝐼)    &   ⊢ (𝜑 → 𝐼 ∈ Fin)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → ¬ 𝐵 ∈ dom 𝐼)    &   ⊢ (𝜑 → 𝐹(EulerPaths‘𝐺)𝑃)    &   ⊢ 𝑁 = (♯‘𝐹)    &   ⊢ (𝜑 → 𝐸 ∈ (Edg‘𝐺))    &   ⊢ (𝜑 → {(𝑃‘𝑁), 𝐶} ⊆ 𝐸)    &   ⊢ (iEdg‘𝑆) = (𝐼 ∪ {⟨𝐵, 𝐸⟩})    &   ⊢ 𝐻 = (𝐹 ∪ {⟨𝑁, 𝐵⟩})    &   ⊢ 𝑄 = (𝑃 ∪ {⟨(𝑁 + 1), 𝐶⟩})    &   ⊢ (Vtx‘𝑆) = 𝑉    &   ⊢ ((𝜑 ∧ 𝐶 = (𝑃‘𝑁)) → 𝐸 = {𝐶})    ⇒   ⊢ (𝜑 → 𝐻(EulerPaths‘𝑆)𝑄)
Theorem	eupth2eucrct 30819	Append one path segment to an Eulerian path ⟨𝐹, 𝑃⟩ which may not be an (Eulerian) circuit to become an Eulerian circuit ⟨𝐻, 𝑄⟩ of the supergraph 𝑆 obtained by adding the new edge to the graph 𝐺. (Contributed by AV, 11-Mar-2021.) (Proof shortened by AV, 30-Oct-2021.) (Revised by AV, 8-Apr-2024.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ (𝜑 → Fun 𝐼)    &   ⊢ (𝜑 → 𝐼 ∈ Fin)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → ¬ 𝐵 ∈ dom 𝐼)    &   ⊢ (𝜑 → 𝐹(EulerPaths‘𝐺)𝑃)    &   ⊢ 𝑁 = (♯‘𝐹)    &   ⊢ (𝜑 → 𝐸 ∈ (Edg‘𝐺))    &   ⊢ (𝜑 → {(𝑃‘𝑁), 𝐶} ⊆ 𝐸)    &   ⊢ (iEdg‘𝑆) = (𝐼 ∪ {⟨𝐵, 𝐸⟩})    &   ⊢ 𝐻 = (𝐹 ∪ {⟨𝑁, 𝐵⟩})    &   ⊢ 𝑄 = (𝑃 ∪ {⟨(𝑁 + 1), 𝐶⟩})    &   ⊢ (Vtx‘𝑆) = 𝑉    &   ⊢ ((𝜑 ∧ 𝐶 = (𝑃‘𝑁)) → 𝐸 = {𝐶})    &   ⊢ (𝜑 → 𝐶 = (𝑃‘0))    ⇒   ⊢ (𝜑 → (𝐻(EulerPaths‘𝑆)𝑄 ∧ 𝐻(Circuits‘𝑆)𝑄))
Theorem	eupth2lem1 30820	Lemma for eupth2 30841. (Contributed by Mario Carneiro, 8-Apr-2015.)
⊢ (𝑈 ∈ 𝑉 → (𝑈 ∈ if(𝐴 = 𝐵, ∅, {𝐴, 𝐵}) ↔ (𝐴 ≠ 𝐵 ∧ (𝑈 = 𝐴 ∨ 𝑈 = 𝐵))))
Theorem	eupth2lem2 30821	Lemma for eupth2 30841. (Contributed by Mario Carneiro, 8-Apr-2015.)
⊢ 𝐵 ∈ V    ⇒   ⊢ ((𝐵 ≠ 𝐶 ∧ 𝐵 = 𝑈) → (¬ 𝑈 ∈ if(𝐴 = 𝐵, ∅, {𝐴, 𝐵}) ↔ 𝑈 ∈ if(𝐴 = 𝐶, ∅, {𝐴, 𝐶})))
Theorem	trlsegvdeglem1 30822	Lemma for trlsegvdeg 30829. (Contributed by AV, 20-Feb-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ (𝜑 → Fun 𝐼)    &   ⊢ (𝜑 → 𝑁 ∈ (0..^(♯‘𝐹)))    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹(Trails‘𝐺)𝑃)    ⇒   ⊢ (𝜑 → ((𝑃‘𝑁) ∈ 𝑉 ∧ (𝑃‘(𝑁 + 1)) ∈ 𝑉))
Theorem	trlsegvdeglem2 30823	Lemma for trlsegvdeg 30829. (Contributed by AV, 20-Feb-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ (𝜑 → Fun 𝐼)    &   ⊢ (𝜑 → 𝑁 ∈ (0..^(♯‘𝐹)))    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹(Trails‘𝐺)𝑃)    &   ⊢ (𝜑 → (Vtx‘𝑋) = 𝑉)    &   ⊢ (𝜑 → (Vtx‘𝑌) = 𝑉)    &   ⊢ (𝜑 → (Vtx‘𝑍) = 𝑉)    &   ⊢ (𝜑 → (iEdg‘𝑋) = (𝐼 ↾ (𝐹 “ (0..^𝑁))))    &   ⊢ (𝜑 → (iEdg‘𝑌) = {⟨(𝐹‘𝑁), (𝐼‘(𝐹‘𝑁))⟩})    &   ⊢ (𝜑 → (iEdg‘𝑍) = (𝐼 ↾ (𝐹 “ (0...𝑁))))    ⇒   ⊢ (𝜑 → Fun (iEdg‘𝑋))
Theorem	trlsegvdeglem3 30824	Lemma for trlsegvdeg 30829. (Contributed by AV, 20-Feb-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ (𝜑 → Fun 𝐼)    &   ⊢ (𝜑 → 𝑁 ∈ (0..^(♯‘𝐹)))    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹(Trails‘𝐺)𝑃)    &   ⊢ (𝜑 → (Vtx‘𝑋) = 𝑉)    &   ⊢ (𝜑 → (Vtx‘𝑌) = 𝑉)    &   ⊢ (𝜑 → (Vtx‘𝑍) = 𝑉)    &   ⊢ (𝜑 → (iEdg‘𝑋) = (𝐼 ↾ (𝐹 “ (0..^𝑁))))    &   ⊢ (𝜑 → (iEdg‘𝑌) = {⟨(𝐹‘𝑁), (𝐼‘(𝐹‘𝑁))⟩})    &   ⊢ (𝜑 → (iEdg‘𝑍) = (𝐼 ↾ (𝐹 “ (0...𝑁))))    ⇒   ⊢ (𝜑 → Fun (iEdg‘𝑌))
Theorem	trlsegvdeglem4 30825	Lemma for trlsegvdeg 30829. (Contributed by AV, 21-Feb-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ (𝜑 → Fun 𝐼)    &   ⊢ (𝜑 → 𝑁 ∈ (0..^(♯‘𝐹)))    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹(Trails‘𝐺)𝑃)    &   ⊢ (𝜑 → (Vtx‘𝑋) = 𝑉)    &   ⊢ (𝜑 → (Vtx‘𝑌) = 𝑉)    &   ⊢ (𝜑 → (Vtx‘𝑍) = 𝑉)    &   ⊢ (𝜑 → (iEdg‘𝑋) = (𝐼 ↾ (𝐹 “ (0..^𝑁))))    &   ⊢ (𝜑 → (iEdg‘𝑌) = {⟨(𝐹‘𝑁), (𝐼‘(𝐹‘𝑁))⟩})    &   ⊢ (𝜑 → (iEdg‘𝑍) = (𝐼 ↾ (𝐹 “ (0...𝑁))))    ⇒   ⊢ (𝜑 → dom (iEdg‘𝑋) = ((𝐹 “ (0..^𝑁)) ∩ dom 𝐼))
Theorem	trlsegvdeglem5 30826	Lemma for trlsegvdeg 30829. (Contributed by AV, 21-Feb-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ (𝜑 → Fun 𝐼)    &   ⊢ (𝜑 → 𝑁 ∈ (0..^(♯‘𝐹)))    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹(Trails‘𝐺)𝑃)    &   ⊢ (𝜑 → (Vtx‘𝑋) = 𝑉)    &   ⊢ (𝜑 → (Vtx‘𝑌) = 𝑉)    &   ⊢ (𝜑 → (Vtx‘𝑍) = 𝑉)    &   ⊢ (𝜑 → (iEdg‘𝑋) = (𝐼 ↾ (𝐹 “ (0..^𝑁))))    &   ⊢ (𝜑 → (iEdg‘𝑌) = {⟨(𝐹‘𝑁), (𝐼‘(𝐹‘𝑁))⟩})    &   ⊢ (𝜑 → (iEdg‘𝑍) = (𝐼 ↾ (𝐹 “ (0...𝑁))))    ⇒   ⊢ (𝜑 → dom (iEdg‘𝑌) = {(𝐹‘𝑁)})
Theorem	trlsegvdeglem6 30827	Lemma for trlsegvdeg 30829. (Contributed by AV, 21-Feb-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ (𝜑 → Fun 𝐼)    &   ⊢ (𝜑 → 𝑁 ∈ (0..^(♯‘𝐹)))    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹(Trails‘𝐺)𝑃)    &   ⊢ (𝜑 → (Vtx‘𝑋) = 𝑉)    &   ⊢ (𝜑 → (Vtx‘𝑌) = 𝑉)    &   ⊢ (𝜑 → (Vtx‘𝑍) = 𝑉)    &   ⊢ (𝜑 → (iEdg‘𝑋) = (𝐼 ↾ (𝐹 “ (0..^𝑁))))    &   ⊢ (𝜑 → (iEdg‘𝑌) = {⟨(𝐹‘𝑁), (𝐼‘(𝐹‘𝑁))⟩})    &   ⊢ (𝜑 → (iEdg‘𝑍) = (𝐼 ↾ (𝐹 “ (0...𝑁))))    ⇒   ⊢ (𝜑 → dom (iEdg‘𝑋) ∈ Fin)
Theorem	trlsegvdeglem7 30828	Lemma for trlsegvdeg 30829. (Contributed by AV, 21-Feb-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ (𝜑 → Fun 𝐼)    &   ⊢ (𝜑 → 𝑁 ∈ (0..^(♯‘𝐹)))    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹(Trails‘𝐺)𝑃)    &   ⊢ (𝜑 → (Vtx‘𝑋) = 𝑉)    &   ⊢ (𝜑 → (Vtx‘𝑌) = 𝑉)    &   ⊢ (𝜑 → (Vtx‘𝑍) = 𝑉)    &   ⊢ (𝜑 → (iEdg‘𝑋) = (𝐼 ↾ (𝐹 “ (0..^𝑁))))    &   ⊢ (𝜑 → (iEdg‘𝑌) = {⟨(𝐹‘𝑁), (𝐼‘(𝐹‘𝑁))⟩})    &   ⊢ (𝜑 → (iEdg‘𝑍) = (𝐼 ↾ (𝐹 “ (0...𝑁))))    ⇒   ⊢ (𝜑 → dom (iEdg‘𝑌) ∈ Fin)
Theorem	trlsegvdeg 30829	The effect on vertex degree of adding one edge to a trail.. In the following, a subgraph induced by a segment of a trail is called a "subtrail": For any subtrail 𝑍 of a trail ⟨𝐹, 𝑃⟩ in a pseudograph 𝐺 which is composed of subtrails 𝑋 and 𝑌, where 𝑌 consists of a single edge, the vertex degree of any vertex 𝑈 within 𝑍 is the sum of the vertex degree of 𝑈 within 𝑋 and the vertex degree of 𝑈 within 𝑌. Note that this theorem would not hold for arbitrary walks (if the last edge was identical with a previous edge, the degree of the vertices incident with this edge would not be increased because of this edge). (Contributed by Mario Carneiro, 8-Apr-2015.) Formerly part of proof of eupth2lem3 30838. (Revised by AV, 20-Feb-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ (𝜑 → Fun 𝐼)    &   ⊢ (𝜑 → 𝑁 ∈ (0..^(♯‘𝐹)))    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹(Trails‘𝐺)𝑃)    &   ⊢ (𝜑 → (Vtx‘𝑋) = 𝑉)    &   ⊢ (𝜑 → (Vtx‘𝑌) = 𝑉)    &   ⊢ (𝜑 → (Vtx‘𝑍) = 𝑉)    &   ⊢ (𝜑 → (iEdg‘𝑋) = (𝐼 ↾ (𝐹 “ (0..^𝑁))))    &   ⊢ (𝜑 → (iEdg‘𝑌) = {⟨(𝐹‘𝑁), (𝐼‘(𝐹‘𝑁))⟩})    &   ⊢ (𝜑 → (iEdg‘𝑍) = (𝐼 ↾ (𝐹 “ (0...𝑁))))    ⇒   ⊢ (𝜑 → ((VtxDeg‘𝑍)‘𝑈) = (((VtxDeg‘𝑋)‘𝑈) + ((VtxDeg‘𝑌)‘𝑈)))
Theorem	eupth2lem3lem1 30830	Lemma for eupth2lem3 30838. (Contributed by AV, 21-Feb-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ (𝜑 → Fun 𝐼)    &   ⊢ (𝜑 → 𝑁 ∈ (0..^(♯‘𝐹)))    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹(Trails‘𝐺)𝑃)    &   ⊢ (𝜑 → (Vtx‘𝑋) = 𝑉)    &   ⊢ (𝜑 → (Vtx‘𝑌) = 𝑉)    &   ⊢ (𝜑 → (Vtx‘𝑍) = 𝑉)    &   ⊢ (𝜑 → (iEdg‘𝑋) = (𝐼 ↾ (𝐹 “ (0..^𝑁))))    &   ⊢ (𝜑 → (iEdg‘𝑌) = {⟨(𝐹‘𝑁), (𝐼‘(𝐹‘𝑁))⟩})    &   ⊢ (𝜑 → (iEdg‘𝑍) = (𝐼 ↾ (𝐹 “ (0...𝑁))))    ⇒   ⊢ (𝜑 → ((VtxDeg‘𝑋)‘𝑈) ∈ ℕ0)
Theorem	eupth2lem3lem2 30831	Lemma for eupth2lem3 30838. (Contributed by AV, 21-Feb-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ (𝜑 → Fun 𝐼)    &   ⊢ (𝜑 → 𝑁 ∈ (0..^(♯‘𝐹)))    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹(Trails‘𝐺)𝑃)    &   ⊢ (𝜑 → (Vtx‘𝑋) = 𝑉)    &   ⊢ (𝜑 → (Vtx‘𝑌) = 𝑉)    &   ⊢ (𝜑 → (Vtx‘𝑍) = 𝑉)    &   ⊢ (𝜑 → (iEdg‘𝑋) = (𝐼 ↾ (𝐹 “ (0..^𝑁))))    &   ⊢ (𝜑 → (iEdg‘𝑌) = {⟨(𝐹‘𝑁), (𝐼‘(𝐹‘𝑁))⟩})    &   ⊢ (𝜑 → (iEdg‘𝑍) = (𝐼 ↾ (𝐹 “ (0...𝑁))))    ⇒   ⊢ (𝜑 → ((VtxDeg‘𝑌)‘𝑈) ∈ ℕ0)
Theorem	eupth2lem3lem3 30832*	Lemma for eupth2lem3 30838, formerly part of proof of eupth2lem3 30838: If a loop {(𝑃‘𝑁), (𝑃‘(𝑁 + 1))} is added to a trail, the degree of the vertices with odd degree remains odd (regarding the subgraphs induced by the involved trails). (Contributed by Mario Carneiro, 8-Apr-2015.) (Revised by AV, 21-Feb-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ (𝜑 → Fun 𝐼)    &   ⊢ (𝜑 → 𝑁 ∈ (0..^(♯‘𝐹)))    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹(Trails‘𝐺)𝑃)    &   ⊢ (𝜑 → (Vtx‘𝑋) = 𝑉)    &   ⊢ (𝜑 → (Vtx‘𝑌) = 𝑉)    &   ⊢ (𝜑 → (Vtx‘𝑍) = 𝑉)    &   ⊢ (𝜑 → (iEdg‘𝑋) = (𝐼 ↾ (𝐹 “ (0..^𝑁))))    &   ⊢ (𝜑 → (iEdg‘𝑌) = {⟨(𝐹‘𝑁), (𝐼‘(𝐹‘𝑁))⟩})    &   ⊢ (𝜑 → (iEdg‘𝑍) = (𝐼 ↾ (𝐹 “ (0...𝑁))))    &   ⊢ (𝜑 → {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((VtxDeg‘𝑋)‘𝑥)} = if((𝑃‘0) = (𝑃‘𝑁), ∅, {(𝑃‘0), (𝑃‘𝑁)}))    &   ⊢ (𝜑 → if-((𝑃‘𝑁) = (𝑃‘(𝑁 + 1)), (𝐼‘(𝐹‘𝑁)) = {(𝑃‘𝑁)}, {(𝑃‘𝑁), (𝑃‘(𝑁 + 1))} ⊆ (𝐼‘(𝐹‘𝑁))))    ⇒   ⊢ ((𝜑 ∧ (𝑃‘𝑁) = (𝑃‘(𝑁 + 1))) → (¬ 2 ∥ (((VtxDeg‘𝑋)‘𝑈) + ((VtxDeg‘𝑌)‘𝑈)) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃‘(𝑁 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑁 + 1))})))
Theorem	eupth2lem3lem4 30833*	Lemma for eupth2lem3 30838, formerly part of proof of eupth2lem3 30838: If an edge (not a loop) is added to a trail, the degree of the end vertices of this edge remains odd if it was odd before (regarding the subgraphs induced by the involved trails). (Contributed by Mario Carneiro, 8-Apr-2015.) (Revised by AV, 25-Feb-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ (𝜑 → Fun 𝐼)    &   ⊢ (𝜑 → 𝑁 ∈ (0..^(♯‘𝐹)))    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹(Trails‘𝐺)𝑃)    &   ⊢ (𝜑 → (Vtx‘𝑋) = 𝑉)    &   ⊢ (𝜑 → (Vtx‘𝑌) = 𝑉)    &   ⊢ (𝜑 → (Vtx‘𝑍) = 𝑉)    &   ⊢ (𝜑 → (iEdg‘𝑋) = (𝐼 ↾ (𝐹 “ (0..^𝑁))))    &   ⊢ (𝜑 → (iEdg‘𝑌) = {⟨(𝐹‘𝑁), (𝐼‘(𝐹‘𝑁))⟩})    &   ⊢ (𝜑 → (iEdg‘𝑍) = (𝐼 ↾ (𝐹 “ (0...𝑁))))    &   ⊢ (𝜑 → {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((VtxDeg‘𝑋)‘𝑥)} = if((𝑃‘0) = (𝑃‘𝑁), ∅, {(𝑃‘0), (𝑃‘𝑁)}))    &   ⊢ (𝜑 → if-((𝑃‘𝑁) = (𝑃‘(𝑁 + 1)), (𝐼‘(𝐹‘𝑁)) = {(𝑃‘𝑁)}, {(𝑃‘𝑁), (𝑃‘(𝑁 + 1))} ⊆ (𝐼‘(𝐹‘𝑁))))    &   ⊢ (𝜑 → (𝐼‘(𝐹‘𝑁)) ∈ 𝒫 𝑉)    ⇒   ⊢ ((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1)) ∧ (𝑈 = (𝑃‘𝑁) ∨ 𝑈 = (𝑃‘(𝑁 + 1)))) → (¬ 2 ∥ (((VtxDeg‘𝑋)‘𝑈) + ((VtxDeg‘𝑌)‘𝑈)) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃‘(𝑁 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑁 + 1))})))
Theorem	eupth2lem3lem5 30834*	Lemma for eupth2 30841. (Contributed by AV, 25-Feb-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ (𝜑 → Fun 𝐼)    &   ⊢ (𝜑 → 𝑁 ∈ (0..^(♯‘𝐹)))    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹(Trails‘𝐺)𝑃)    &   ⊢ (𝜑 → (Vtx‘𝑋) = 𝑉)    &   ⊢ (𝜑 → (Vtx‘𝑌) = 𝑉)    &   ⊢ (𝜑 → (Vtx‘𝑍) = 𝑉)    &   ⊢ (𝜑 → (iEdg‘𝑋) = (𝐼 ↾ (𝐹 “ (0..^𝑁))))    &   ⊢ (𝜑 → (iEdg‘𝑌) = {⟨(𝐹‘𝑁), (𝐼‘(𝐹‘𝑁))⟩})    &   ⊢ (𝜑 → (iEdg‘𝑍) = (𝐼 ↾ (𝐹 “ (0...𝑁))))    &   ⊢ (𝜑 → {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((VtxDeg‘𝑋)‘𝑥)} = if((𝑃‘0) = (𝑃‘𝑁), ∅, {(𝑃‘0), (𝑃‘𝑁)}))    &   ⊢ (𝜑 → (𝐼‘(𝐹‘𝑁)) = {(𝑃‘𝑁), (𝑃‘(𝑁 + 1))})    ⇒   ⊢ (𝜑 → (𝐼‘(𝐹‘𝑁)) ∈ 𝒫 𝑉)
Theorem	eupth2lem3lem6 30835*	Formerly part of proof of eupth2lem3 30838: If an edge (not a loop) is added to a trail, the degree of vertices not being end vertices of this edge remains odd if it was odd before (regarding the subgraphs induced by the involved trails). Remark: This seems to be not valid for hyperedges joining more vertices than (𝑃‘0) and (𝑃‘𝑁): if there is a third vertex in the edge, and this vertex is already contained in the trail, then the degree of this vertex could be affected by this edge! (Contributed by Mario Carneiro, 8-Apr-2015.) (Revised by AV, 25-Feb-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ (𝜑 → Fun 𝐼)    &   ⊢ (𝜑 → 𝑁 ∈ (0..^(♯‘𝐹)))    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹(Trails‘𝐺)𝑃)    &   ⊢ (𝜑 → (Vtx‘𝑋) = 𝑉)    &   ⊢ (𝜑 → (Vtx‘𝑌) = 𝑉)    &   ⊢ (𝜑 → (Vtx‘𝑍) = 𝑉)    &   ⊢ (𝜑 → (iEdg‘𝑋) = (𝐼 ↾ (𝐹 “ (0..^𝑁))))    &   ⊢ (𝜑 → (iEdg‘𝑌) = {⟨(𝐹‘𝑁), (𝐼‘(𝐹‘𝑁))⟩})    &   ⊢ (𝜑 → (iEdg‘𝑍) = (𝐼 ↾ (𝐹 “ (0...𝑁))))    &   ⊢ (𝜑 → {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((VtxDeg‘𝑋)‘𝑥)} = if((𝑃‘0) = (𝑃‘𝑁), ∅, {(𝑃‘0), (𝑃‘𝑁)}))    &   ⊢ (𝜑 → (𝐼‘(𝐹‘𝑁)) = {(𝑃‘𝑁), (𝑃‘(𝑁 + 1))})    ⇒   ⊢ ((𝜑 ∧ (𝑃‘𝑁) ≠ (𝑃‘(𝑁 + 1)) ∧ (𝑈 ≠ (𝑃‘𝑁) ∧ 𝑈 ≠ (𝑃‘(𝑁 + 1)))) → (¬ 2 ∥ (((VtxDeg‘𝑋)‘𝑈) + ((VtxDeg‘𝑌)‘𝑈)) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃‘(𝑁 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑁 + 1))})))
Theorem	eupth2lem3lem7 30836*	Lemma for eupth2lem3 30838: Combining trlsegvdeg 30829, eupth2lem3lem3 30832, eupth2lem3lem4 30833 and eupth2lem3lem6 30835. (Contributed by Mario Carneiro, 8-Apr-2015.) (Revised by AV, 27-Feb-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ (𝜑 → Fun 𝐼)    &   ⊢ (𝜑 → 𝑁 ∈ (0..^(♯‘𝐹)))    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹(Trails‘𝐺)𝑃)    &   ⊢ (𝜑 → (Vtx‘𝑋) = 𝑉)    &   ⊢ (𝜑 → (Vtx‘𝑌) = 𝑉)    &   ⊢ (𝜑 → (Vtx‘𝑍) = 𝑉)    &   ⊢ (𝜑 → (iEdg‘𝑋) = (𝐼 ↾ (𝐹 “ (0..^𝑁))))    &   ⊢ (𝜑 → (iEdg‘𝑌) = {⟨(𝐹‘𝑁), (𝐼‘(𝐹‘𝑁))⟩})    &   ⊢ (𝜑 → (iEdg‘𝑍) = (𝐼 ↾ (𝐹 “ (0...𝑁))))    &   ⊢ (𝜑 → {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((VtxDeg‘𝑋)‘𝑥)} = if((𝑃‘0) = (𝑃‘𝑁), ∅, {(𝑃‘0), (𝑃‘𝑁)}))    &   ⊢ (𝜑 → (𝐼‘(𝐹‘𝑁)) = {(𝑃‘𝑁), (𝑃‘(𝑁 + 1))})    ⇒   ⊢ (𝜑 → (¬ 2 ∥ ((VtxDeg‘𝑍)‘𝑈) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃‘(𝑁 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑁 + 1))})))
Theorem	eupthvdres 30837	Formerly part of proof of eupth2 30841: The vertex degree remains the same for all vertices if the edges are restricted to the edges of an Eulerian path. (Contributed by Mario Carneiro, 8-Apr-2015.) (Revised by AV, 26-Feb-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑊)    &   ⊢ (𝜑 → Fun 𝐼)    &   ⊢ (𝜑 → 𝐹(EulerPaths‘𝐺)𝑃)    &   ⊢ 𝐻 = ⟨𝑉, (𝐼 ↾ (𝐹 “ (0..^(♯‘𝐹))))⟩    ⇒   ⊢ (𝜑 → (VtxDeg‘𝐻) = (VtxDeg‘𝐺))
Theorem	eupth2lem3 30838*	Lemma for eupth2 30841. (Contributed by Mario Carneiro, 8-Apr-2015.) (Revised by AV, 26-Feb-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ UPGraph)    &   ⊢ (𝜑 → Fun 𝐼)    &   ⊢ (𝜑 → 𝐹(EulerPaths‘𝐺)𝑃)    &   ⊢ 𝐻 = ⟨𝑉, (𝐼 ↾ (𝐹 “ (0..^𝑁)))⟩    &   ⊢ 𝑋 = ⟨𝑉, (𝐼 ↾ (𝐹 “ (0..^(𝑁 + 1))))⟩    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → (𝑁 + 1) ≤ (♯‘𝐹))    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((VtxDeg‘𝐻)‘𝑥)} = if((𝑃‘0) = (𝑃‘𝑁), ∅, {(𝑃‘0), (𝑃‘𝑁)}))    ⇒   ⊢ (𝜑 → (¬ 2 ∥ ((VtxDeg‘𝑋)‘𝑈) ↔ 𝑈 ∈ if((𝑃‘0) = (𝑃‘(𝑁 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑁 + 1))})))
Theorem	eupth2lemb 30839*	Lemma for eupth2 30841 (induction basis): There are no vertices of odd degree in an Eulerian path of length 0, having no edge and identical endpoints (the single vertex of the Eulerian path). Formerly part of proof for eupth2 30841. (Contributed by Mario Carneiro, 8-Apr-2015.) (Revised by AV, 26-Feb-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ UPGraph)    &   ⊢ (𝜑 → Fun 𝐼)    &   ⊢ (𝜑 → 𝐹(EulerPaths‘𝐺)𝑃)    ⇒   ⊢ (𝜑 → {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((VtxDeg‘⟨𝑉, (𝐼 ↾ (𝐹 “ (0..^0)))⟩)‘𝑥)} = ∅)
Theorem	eupth2lems 30840*	Lemma for eupth2 30841 (induction step): The only vertices of odd degree in a graph with an Eulerian path are the endpoints, and then only if the endpoints are distinct, if the Eulerian path shortened by one edge has this property. Formerly part of proof for eupth2 30841. (Contributed by Mario Carneiro, 8-Apr-2015.) (Revised by AV, 26-Feb-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ UPGraph)    &   ⊢ (𝜑 → Fun 𝐼)    &   ⊢ (𝜑 → 𝐹(EulerPaths‘𝐺)𝑃)    ⇒   ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → ((𝑛 ≤ (♯‘𝐹) → {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((VtxDeg‘⟨𝑉, (𝐼 ↾ (𝐹 “ (0..^𝑛)))⟩)‘𝑥)} = if((𝑃‘0) = (𝑃‘𝑛), ∅, {(𝑃‘0), (𝑃‘𝑛)})) → ((𝑛 + 1) ≤ (♯‘𝐹) → {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((VtxDeg‘⟨𝑉, (𝐼 ↾ (𝐹 “ (0..^(𝑛 + 1))))⟩)‘𝑥)} = if((𝑃‘0) = (𝑃‘(𝑛 + 1)), ∅, {(𝑃‘0), (𝑃‘(𝑛 + 1))}))))
Theorem	eupth2 30841*	The only vertices of odd degree in a graph with an Eulerian path are the endpoints, and then only if the endpoints are distinct. (Contributed by Mario Carneiro, 8-Apr-2015.) (Revised by AV, 26-Feb-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ UPGraph)    &   ⊢ (𝜑 → Fun 𝐼)    &   ⊢ (𝜑 → 𝐹(EulerPaths‘𝐺)𝑃)    ⇒   ⊢ (𝜑 → {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((VtxDeg‘𝐺)‘𝑥)} = if((𝑃‘0) = (𝑃‘(♯‘𝐹)), ∅, {(𝑃‘0), (𝑃‘(♯‘𝐹))}))
Theorem	eulerpathpr 30842*	A graph with an Eulerian path has either zero or two vertices of odd degree. (Contributed by Mario Carneiro, 7-Apr-2015.) (Revised by AV, 26-Feb-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UPGraph ∧ 𝐹(EulerPaths‘𝐺)𝑃) → (♯‘{𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((VtxDeg‘𝐺)‘𝑥)}) ∈ {0, 2})
Theorem	eulerpath 30843*	A pseudograph with an Eulerian path has either zero or two vertices of odd degree. (Contributed by Mario Carneiro, 7-Apr-2015.) (Revised by AV, 26-Feb-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UPGraph ∧ (EulerPaths‘𝐺) ≠ ∅) → (♯‘{𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((VtxDeg‘𝐺)‘𝑥)}) ∈ {0, 2})
Theorem	eulercrct 30844*	A pseudograph with an Eulerian circuit ⟨𝐹, 𝑃⟩ (an "Eulerian pseudograph") has only vertices of even degree. (Contributed by AV, 12-Mar-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UPGraph ∧ 𝐹(EulerPaths‘𝐺)𝑃 ∧ 𝐹(Circuits‘𝐺)𝑃) → ∀𝑥 ∈ 𝑉 2 ∥ ((VtxDeg‘𝐺)‘𝑥))
Theorem	eucrctshift 30845*	Cyclically shifting the indices of an Eulerian circuit ⟨𝐹, 𝑃⟩ results in an Eulerian circuit ⟨𝐻, 𝑄⟩. (Contributed by AV, 15-Mar-2021.) (Proof shortened by AV, 30-Oct-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ (𝜑 → 𝐹(Circuits‘𝐺)𝑃)    &   ⊢ 𝑁 = (♯‘𝐹)    &   ⊢ (𝜑 → 𝑆 ∈ (0..^𝑁))    &   ⊢ 𝐻 = (𝐹 cyclShift 𝑆)    &   ⊢ 𝑄 = (𝑥 ∈ (0...𝑁) ↦ if(𝑥 ≤ (𝑁 − 𝑆), (𝑃‘(𝑥 + 𝑆)), (𝑃‘((𝑥 + 𝑆) − 𝑁))))    &   ⊢ (𝜑 → 𝐹(EulerPaths‘𝐺)𝑃)    ⇒   ⊢ (𝜑 → (𝐻(EulerPaths‘𝐺)𝑄 ∧ 𝐻(Circuits‘𝐺)𝑄))
Theorem	eucrct2eupth1 30846	Removing one edge (𝐼‘(𝐹‘𝑁)) from a nonempty graph 𝐺 with an Eulerian circuit ⟨𝐹, 𝑃⟩ results in a graph 𝑆 with an Eulerian path ⟨𝐻, 𝑄⟩. This is the special case of eucrct2eupth 30847 (with 𝐽 = (𝑁 − 1)) where the last segment/edge of the circuit is removed. (Contributed by AV, 11-Mar-2021.) Hypothesis revised using the prefix operation. (Revised by AV, 30-Nov-2022.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ (𝜑 → 𝐹(EulerPaths‘𝐺)𝑃)    &   ⊢ (𝜑 → 𝐹(Circuits‘𝐺)𝑃)    &   ⊢ (Vtx‘𝑆) = 𝑉    &   ⊢ (𝜑 → 0 < (♯‘𝐹))    &   ⊢ (𝜑 → 𝑁 = ((♯‘𝐹) − 1))    &   ⊢ (𝜑 → (iEdg‘𝑆) = (𝐼 ↾ (𝐹 “ (0..^𝑁))))    &   ⊢ 𝐻 = (𝐹 prefix 𝑁)    &   ⊢ 𝑄 = (𝑃 ↾ (0...𝑁))    ⇒   ⊢ (𝜑 → 𝐻(EulerPaths‘𝑆)𝑄)
Theorem	eucrct2eupth 30847*	Removing one edge (𝐼‘(𝐹‘𝐽)) from a graph 𝐺 with an Eulerian circuit ⟨𝐹, 𝑃⟩ results in a graph 𝑆 with an Eulerian path ⟨𝐻, 𝑄⟩. (Contributed by AV, 17-Mar-2021.) Hypothesis revised using the prefix operation. (Revised by AV, 30-Nov-2022.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ (𝜑 → 𝐹(EulerPaths‘𝐺)𝑃)    &   ⊢ (𝜑 → 𝐹(Circuits‘𝐺)𝑃)    &   ⊢ (Vtx‘𝑆) = 𝑉    &   ⊢ (𝜑 → 𝑁 = (♯‘𝐹))    &   ⊢ (𝜑 → 𝐽 ∈ (0..^𝑁))    &   ⊢ (𝜑 → (iEdg‘𝑆) = (𝐼 ↾ (𝐹 “ ((0..^𝑁) ∖ {𝐽}))))    &   ⊢ 𝐾 = (𝐽 + 1)    &   ⊢ 𝐻 = ((𝐹 cyclShift 𝐾) prefix (𝑁 − 1))    &   ⊢ 𝑄 = (𝑥 ∈ (0..^𝑁) ↦ if(𝑥 ≤ (𝑁 − 𝐾), (𝑃‘(𝑥 + 𝐾)), (𝑃‘((𝑥 + 𝐾) − 𝑁))))    ⇒   ⊢ (𝜑 → 𝐻(EulerPaths‘𝑆)𝑄)
17.4.2  The Königsberg Bridge problem According to Wikipedia ("Seven Bridges of Königsberg", 9-Mar-2021, https://en.wikipedia.org/wiki/Seven_Bridges_of_Koenigsberg): "The Seven Bridges of Königsberg is a historically notable problem in mathematics. Its negative resolution by Leonhard Euler in 1736 laid the foundations of graph theory and prefigured the idea of topology. The city of Königsberg in [East] Prussia (now Kaliningrad, Russia) was set on both sides of the Pregel River, and included two large islands - Kneiphof and Lomse - which were connected to each other, or to the two mainland portions of the city, by seven bridges. The problem was to devise a walk through the city that would cross each of those bridges once and only once.". Euler proved that the problem has no solution by applying Euler's theorem to the Königsberg graph, which is obtained by replacing each land mass with an abstract "vertex" or node, and each bridge with an abstract connection, an "edge", which connects two land masses/vertices. The Königsberg graph 𝐺 is a multigraph consisting of 4 vertices and 7 edges, represented by the following ordered pair: 𝐺 = ⟨(0...3), ⟨“{0, 1}{0, 2} {0, 3}{1, 2}{1, 2}{2, 3}{2, 3}”⟩⟩, see konigsbergumgr 30853. konigsberg 30859 shows that the Königsberg graph has no Eulerian path, thus the Königsberg Bridge problem has no solution.
Theorem	konigsbergvtx 30848	The set of vertices of the Königsberg graph 𝐺. (Contributed by AV, 28-Feb-2021.)
⊢ 𝑉 = (0...3)    &   ⊢ 𝐸 = ⟨“{0, 1} {0, 2} {0, 3} {1, 2} {1, 2} {2, 3} {2, 3}”⟩    &   ⊢ 𝐺 = ⟨𝑉, 𝐸⟩    ⇒   ⊢ (Vtx‘𝐺) = (0...3)
Theorem	konigsbergiedg 30849	The indexed edges of the Königsberg graph 𝐺. (Contributed by AV, 28-Feb-2021.)
⊢ 𝑉 = (0...3)    &   ⊢ 𝐸 = ⟨“{0, 1} {0, 2} {0, 3} {1, 2} {1, 2} {2, 3} {2, 3}”⟩    &   ⊢ 𝐺 = ⟨𝑉, 𝐸⟩    ⇒   ⊢ (iEdg‘𝐺) = ⟨“{0, 1} {0, 2} {0, 3} {1, 2} {1, 2} {2, 3} {2, 3}”⟩
Theorem	konigsbergiedgw 30850*	The indexed edges of the Königsberg graph 𝐺 is a word over the pairs of vertices. (Contributed by AV, 28-Feb-2021.)
⊢ 𝑉 = (0...3)    &   ⊢ 𝐸 = ⟨“{0, 1} {0, 2} {0, 3} {1, 2} {1, 2} {2, 3} {2, 3}”⟩    &   ⊢ 𝐺 = ⟨𝑉, 𝐸⟩    ⇒   ⊢ 𝐸 ∈ Word {𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 2}
Theorem	konigsbergssiedgwpr 30851*	Each subset of the indexed edges of the Königsberg graph 𝐺 is a word over the pairs of vertices. (Contributed by AV, 28-Feb-2021.)
⊢ 𝑉 = (0...3)    &   ⊢ 𝐸 = ⟨“{0, 1} {0, 2} {0, 3} {1, 2} {1, 2} {2, 3} {2, 3}”⟩    &   ⊢ 𝐺 = ⟨𝑉, 𝐸⟩    ⇒   ⊢ ((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V ∧ 𝐸 = (𝐴 ++ 𝐵)) → 𝐴 ∈ Word {𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 2})
Theorem	konigsbergssiedgw 30852*	Each subset of the indexed edges of the Königsberg graph 𝐺 is a word over the pairs of vertices. (Contributed by AV, 28-Feb-2021.)
⊢ 𝑉 = (0...3)    &   ⊢ 𝐸 = ⟨“{0, 1} {0, 2} {0, 3} {1, 2} {1, 2} {2, 3} {2, 3}”⟩    &   ⊢ 𝐺 = ⟨𝑉, 𝐸⟩    ⇒   ⊢ ((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V ∧ 𝐸 = (𝐴 ++ 𝐵)) → 𝐴 ∈ Word {𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (♯‘𝑥) ≤ 2})
Theorem	konigsbergumgr 30853	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 30854	Lemma 1 for konigsberg 30859: 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 30855	Lemma 2 for konigsberg 30859: 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 30856	Lemma 3 for konigsberg 30859: 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 30857*	Lemma 4 for konigsberg 30859: 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 30858*	Lemma 5 for konigsberg 30859: 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 30859	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 30843 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 30860	Extend class notation with friendship graphs.
class FriendGraph
Definition	df-frgr 30861*	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 30862*	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 30863	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 30864	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 30865	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 30866	Any null graph (without vertices) represented as hypergraph is a friendship graph. (Contributed by AV, 29-Mar-2021.)
⊢ ((𝐺 ∈ UHGraph ∧ (Vtx‘𝐺) = ∅) → 𝐺 ∈ FriendGraph )
Theorem	frgr0 30867	The null graph (graph without vertices) is a friendship graph. (Contributed by AV, 29-Mar-2021.)
⊢ ∅ ∈ FriendGraph
Theorem	frcond1 30868*	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 30869*	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 30870*	Variant of frcond2 30869: 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 30871*	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 30872*	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 30873	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 30874	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 30875*	Lemma 1 for frgr3v 30877. (Contributed by Alexander van der Vekens, 4-Oct-2017.) (Revised by AV, 29-Mar-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → ∀𝑥∀𝑦(((𝑥 ∈ {𝐴, 𝐵, 𝐶} ∧ {{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ 𝐸) ∧ (𝑦 ∈ {𝐴, 𝐵, 𝐶} ∧ {{𝑦, 𝐴}, {𝑦, 𝐵}} ⊆ 𝐸)) → 𝑥 = 𝑦))
Theorem	frgr3vlem2 30876*	Lemma 2 for frgr3v 30877. (Contributed by Alexander van der Vekens, 4-Oct-2017.) (Revised by AV, 29-Mar-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑍) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → ((𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph) → (∃!𝑥 ∈ {𝐴, 𝐵, 𝐶} {{𝑥, 𝐴}, {𝑥, 𝐵}} ⊆ 𝐸 ↔ ({𝐶, 𝐴} ∈ 𝐸 ∧ {𝐶, 𝐵} ∈ 𝐸))))
Theorem	frgr3v 30877	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 30878*	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 30879*	Lemma for 3vfriswmgr 30880. (Contributed by Alexander van der Vekens, 6-Oct-2017.) (Revised by AV, 31-Mar-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐴 ≠ 𝐵) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph)) → ({𝐴, 𝐵} ∈ 𝐸 → ∃!𝑤 ∈ {𝐴, 𝐵} {𝐴, 𝑤} ∈ 𝐸))
Theorem	3vfriswmgr 30880*	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 30881*	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 30882*	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 30883*	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 30884*	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 30885*	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 30886*	Between any two (different) vertices in a friendship graph, there 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 30887*	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 30888*	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 30889*	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 30890*	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 30891	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 30892*	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 30893	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 30894	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 30895	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 30896	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 30897	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 30898	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 30899*	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 30900	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‘𝐺)‘𝑁)))