![]() |
Metamath
Proof Explorer Theorem List (p. 303 of 491) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-30946) |
![]() (30947-32469) |
![]() (32470-49035) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | 3trlond 30201 | A trail of length 3 from one vertex to another, different vertex via a third vertex. (Contributed by AV, 8-Feb-2021.) (Revised by AV, 24-Mar-2021.) |
⊢ 𝑃 = 〈“𝐴𝐵𝐶𝐷”〉 & ⊢ 𝐹 = 〈“𝐽𝐾𝐿”〉 & ⊢ (𝜑 → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉))) & ⊢ (𝜑 → ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶) ∧ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷) ∧ 𝐶 ≠ 𝐷)) & ⊢ (𝜑 → ({𝐴, 𝐵} ⊆ (𝐼‘𝐽) ∧ {𝐵, 𝐶} ⊆ (𝐼‘𝐾) ∧ {𝐶, 𝐷} ⊆ (𝐼‘𝐿))) & ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ (𝜑 → (𝐽 ≠ 𝐾 ∧ 𝐽 ≠ 𝐿 ∧ 𝐾 ≠ 𝐿)) ⇒ ⊢ (𝜑 → 𝐹(𝐴(TrailsOn‘𝐺)𝐷)𝑃) | ||
Theorem | 3pthd 30202 | A path of length 3 from one vertex to another vertex via a third vertex. (Contributed by Alexander van der Vekens, 6-Dec-2017.) (Revised by AV, 10-Feb-2021.) (Revised by AV, 24-Mar-2021.) |
⊢ 𝑃 = 〈“𝐴𝐵𝐶𝐷”〉 & ⊢ 𝐹 = 〈“𝐽𝐾𝐿”〉 & ⊢ (𝜑 → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉))) & ⊢ (𝜑 → ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶) ∧ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷) ∧ 𝐶 ≠ 𝐷)) & ⊢ (𝜑 → ({𝐴, 𝐵} ⊆ (𝐼‘𝐽) ∧ {𝐵, 𝐶} ⊆ (𝐼‘𝐾) ∧ {𝐶, 𝐷} ⊆ (𝐼‘𝐿))) & ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ (𝜑 → (𝐽 ≠ 𝐾 ∧ 𝐽 ≠ 𝐿 ∧ 𝐾 ≠ 𝐿)) ⇒ ⊢ (𝜑 → 𝐹(Paths‘𝐺)𝑃) | ||
Theorem | 3pthond 30203 | A path of length 3 from one vertex to another, different vertex via a third vertex. (Contributed by AV, 10-Feb-2021.) (Revised by AV, 24-Mar-2021.) |
⊢ 𝑃 = 〈“𝐴𝐵𝐶𝐷”〉 & ⊢ 𝐹 = 〈“𝐽𝐾𝐿”〉 & ⊢ (𝜑 → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉))) & ⊢ (𝜑 → ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶) ∧ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷) ∧ 𝐶 ≠ 𝐷)) & ⊢ (𝜑 → ({𝐴, 𝐵} ⊆ (𝐼‘𝐽) ∧ {𝐵, 𝐶} ⊆ (𝐼‘𝐾) ∧ {𝐶, 𝐷} ⊆ (𝐼‘𝐿))) & ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ (𝜑 → (𝐽 ≠ 𝐾 ∧ 𝐽 ≠ 𝐿 ∧ 𝐾 ≠ 𝐿)) ⇒ ⊢ (𝜑 → 𝐹(𝐴(PathsOn‘𝐺)𝐷)𝑃) | ||
Theorem | 3spthd 30204 | A simple path of length 3 from one vertex to another, different vertex via a third vertex. (Contributed by AV, 10-Feb-2021.) (Revised by AV, 24-Mar-2021.) (Proof shortened by AV, 30-Oct-2021.) |
⊢ 𝑃 = 〈“𝐴𝐵𝐶𝐷”〉 & ⊢ 𝐹 = 〈“𝐽𝐾𝐿”〉 & ⊢ (𝜑 → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉))) & ⊢ (𝜑 → ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶) ∧ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷) ∧ 𝐶 ≠ 𝐷)) & ⊢ (𝜑 → ({𝐴, 𝐵} ⊆ (𝐼‘𝐽) ∧ {𝐵, 𝐶} ⊆ (𝐼‘𝐾) ∧ {𝐶, 𝐷} ⊆ (𝐼‘𝐿))) & ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ (𝜑 → (𝐽 ≠ 𝐾 ∧ 𝐽 ≠ 𝐿 ∧ 𝐾 ≠ 𝐿)) & ⊢ (𝜑 → 𝐴 ≠ 𝐷) ⇒ ⊢ (𝜑 → 𝐹(SPaths‘𝐺)𝑃) | ||
Theorem | 3spthond 30205 | A simple path of length 3 from one vertex to another, different vertex via a third vertex. (Contributed by AV, 10-Feb-2021.) (Revised by AV, 24-Mar-2021.) |
⊢ 𝑃 = 〈“𝐴𝐵𝐶𝐷”〉 & ⊢ 𝐹 = 〈“𝐽𝐾𝐿”〉 & ⊢ (𝜑 → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉))) & ⊢ (𝜑 → ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶) ∧ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷) ∧ 𝐶 ≠ 𝐷)) & ⊢ (𝜑 → ({𝐴, 𝐵} ⊆ (𝐼‘𝐽) ∧ {𝐵, 𝐶} ⊆ (𝐼‘𝐾) ∧ {𝐶, 𝐷} ⊆ (𝐼‘𝐿))) & ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ (𝜑 → (𝐽 ≠ 𝐾 ∧ 𝐽 ≠ 𝐿 ∧ 𝐾 ≠ 𝐿)) & ⊢ (𝜑 → 𝐴 ≠ 𝐷) ⇒ ⊢ (𝜑 → 𝐹(𝐴(SPathsOn‘𝐺)𝐷)𝑃) | ||
Theorem | 3cycld 30206 | Construction of a 3-cycle from three given edges in a graph. (Contributed by Alexander van der Vekens, 13-Nov-2017.) (Revised by AV, 10-Feb-2021.) (Revised by AV, 24-Mar-2021.) (Proof shortened by AV, 30-Oct-2021.) |
⊢ 𝑃 = 〈“𝐴𝐵𝐶𝐷”〉 & ⊢ 𝐹 = 〈“𝐽𝐾𝐿”〉 & ⊢ (𝜑 → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉))) & ⊢ (𝜑 → ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶) ∧ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷) ∧ 𝐶 ≠ 𝐷)) & ⊢ (𝜑 → ({𝐴, 𝐵} ⊆ (𝐼‘𝐽) ∧ {𝐵, 𝐶} ⊆ (𝐼‘𝐾) ∧ {𝐶, 𝐷} ⊆ (𝐼‘𝐿))) & ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ (𝜑 → (𝐽 ≠ 𝐾 ∧ 𝐽 ≠ 𝐿 ∧ 𝐾 ≠ 𝐿)) & ⊢ (𝜑 → 𝐴 = 𝐷) ⇒ ⊢ (𝜑 → 𝐹(Cycles‘𝐺)𝑃) | ||
Theorem | 3cyclpd 30207 | Construction of a 3-cycle from three given edges in a graph, containing an endpoint of one of these edges. (Contributed by Alexander van der Vekens, 17-Nov-2017.) (Revised by AV, 10-Feb-2021.) (Revised by AV, 24-Mar-2021.) |
⊢ 𝑃 = 〈“𝐴𝐵𝐶𝐷”〉 & ⊢ 𝐹 = 〈“𝐽𝐾𝐿”〉 & ⊢ (𝜑 → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉))) & ⊢ (𝜑 → ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶) ∧ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷) ∧ 𝐶 ≠ 𝐷)) & ⊢ (𝜑 → ({𝐴, 𝐵} ⊆ (𝐼‘𝐽) ∧ {𝐵, 𝐶} ⊆ (𝐼‘𝐾) ∧ {𝐶, 𝐷} ⊆ (𝐼‘𝐿))) & ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ (𝜑 → (𝐽 ≠ 𝐾 ∧ 𝐽 ≠ 𝐿 ∧ 𝐾 ≠ 𝐿)) & ⊢ (𝜑 → 𝐴 = 𝐷) ⇒ ⊢ (𝜑 → (𝐹(Cycles‘𝐺)𝑃 ∧ (♯‘𝐹) = 3 ∧ (𝑃‘0) = 𝐴)) | ||
Theorem | upgr3v3e3cycl 30208* | If there is a cycle of length 3 in a pseudograph, there are three distinct vertices in the graph which are mutually connected by edges. (Contributed by Alexander van der Vekens, 9-Nov-2017.) |
⊢ 𝐸 = (Edg‘𝐺) & ⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ ((𝐺 ∈ UPGraph ∧ 𝐹(Cycles‘𝐺)𝑃 ∧ (♯‘𝐹) = 3) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ∧ 𝑐 ≠ 𝑎))) | ||
Theorem | uhgr3cyclexlem 30209 | Lemma for uhgr3cyclex 30210. (Contributed by AV, 12-Feb-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) ⇒ ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) ∧ ((𝐽 ∈ dom 𝐼 ∧ {𝐵, 𝐶} = (𝐼‘𝐽)) ∧ (𝐾 ∈ dom 𝐼 ∧ {𝐶, 𝐴} = (𝐼‘𝐾)))) → 𝐽 ≠ 𝐾) | ||
Theorem | uhgr3cyclex 30210* | If there are three different vertices in a hypergraph which are mutually connected by edges, there is a 3-cycle in the graph containing one of these vertices. (Contributed by Alexander van der Vekens, 17-Nov-2017.) (Revised by AV, 12-Feb-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ ((𝐺 ∈ UHGraph ∧ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) ∧ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸)) → ∃𝑓∃𝑝(𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 3 ∧ (𝑝‘0) = 𝐴)) | ||
Theorem | umgr3cyclex 30211* | If there are three (different) vertices in a multigraph which are mutually connected by edges, there is a 3-cycle in the graph containing one of these vertices. (Contributed by Alexander van der Vekens, 17-Nov-2017.) (Revised by AV, 12-Feb-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ ((𝐺 ∈ UMGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ ({𝐴, 𝐵} ∈ 𝐸 ∧ {𝐵, 𝐶} ∈ 𝐸 ∧ {𝐶, 𝐴} ∈ 𝐸)) → ∃𝑓∃𝑝(𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 3 ∧ (𝑝‘0) = 𝐴)) | ||
Theorem | umgr3v3e3cycl 30212* | If and only if there is a 3-cycle in a multigraph, there are three (different) vertices in the graph which are mutually connected by edges. (Contributed by Alexander van der Vekens, 14-Nov-2017.) (Revised by AV, 12-Feb-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ (𝐺 ∈ UMGraph → (∃𝑓∃𝑝(𝑓(Cycles‘𝐺)𝑝 ∧ (♯‘𝑓) = 3) ↔ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸))) | ||
Theorem | upgr4cycl4dv4e 30213* | If there is a cycle of length 4 in a pseudograph, there are four (different) vertices in the graph which are mutually connected by edges. (Contributed by Alexander van der Vekens, 9-Nov-2017.) (Revised by AV, 13-Feb-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ ((𝐺 ∈ UPGraph ∧ 𝐹(Cycles‘𝐺)𝑃 ∧ (♯‘𝐹) = 4) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 ((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸)) ∧ ((𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑)))) | ||
Syntax | cconngr 30214 | Extend class notation with connected graphs. |
class ConnGraph | ||
Definition | df-conngr 30215* | Define the class of all connected graphs. A graph is called connected if there is a path between every pair of (distinct) vertices. The distinctness of the vertices is not necessary for the definition, because there is always a path (of length 0) from a vertex to itself, see 0pthonv 30157 and dfconngr1 30216. (Contributed by Alexander van der Vekens, 2-Dec-2017.) (Revised by AV, 15-Feb-2021.) |
⊢ ConnGraph = {𝑔 ∣ [(Vtx‘𝑔) / 𝑣]∀𝑘 ∈ 𝑣 ∀𝑛 ∈ 𝑣 ∃𝑓∃𝑝 𝑓(𝑘(PathsOn‘𝑔)𝑛)𝑝} | ||
Theorem | dfconngr1 30216* | Alternative definition of the class of all connected graphs, requiring paths between distinct vertices. (Contributed by Alexander van der Vekens, 3-Dec-2017.) (Revised by AV, 15-Feb-2021.) |
⊢ ConnGraph = {𝑔 ∣ [(Vtx‘𝑔) / 𝑣]∀𝑘 ∈ 𝑣 ∀𝑛 ∈ (𝑣 ∖ {𝑘})∃𝑓∃𝑝 𝑓(𝑘(PathsOn‘𝑔)𝑛)𝑝} | ||
Theorem | isconngr 30217* | The property of being a connected graph. (Contributed by Alexander van der Vekens, 2-Dec-2017.) (Revised by AV, 15-Feb-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝐺 ∈ 𝑊 → (𝐺 ∈ ConnGraph ↔ ∀𝑘 ∈ 𝑉 ∀𝑛 ∈ 𝑉 ∃𝑓∃𝑝 𝑓(𝑘(PathsOn‘𝐺)𝑛)𝑝)) | ||
Theorem | isconngr1 30218* | The property of being a connected graph. (Contributed by Alexander van der Vekens, 2-Dec-2017.) (Revised by AV, 15-Feb-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝐺 ∈ 𝑊 → (𝐺 ∈ ConnGraph ↔ ∀𝑘 ∈ 𝑉 ∀𝑛 ∈ (𝑉 ∖ {𝑘})∃𝑓∃𝑝 𝑓(𝑘(PathsOn‘𝐺)𝑛)𝑝)) | ||
Theorem | cusconngr 30219 | A complete hypergraph is connected. (Contributed by Alexander van der Vekens, 4-Dec-2017.) (Revised by AV, 15-Feb-2021.) |
⊢ ((𝐺 ∈ UHGraph ∧ 𝐺 ∈ ComplGraph) → 𝐺 ∈ ConnGraph) | ||
Theorem | 0conngr 30220 | A graph without vertices is connected. (Contributed by Alexander van der Vekens, 2-Dec-2017.) (Revised by AV, 15-Feb-2021.) |
⊢ ∅ ∈ ConnGraph | ||
Theorem | 0vconngr 30221 | A graph without vertices is connected. (Contributed by Alexander van der Vekens, 2-Dec-2017.) (Revised by AV, 15-Feb-2021.) |
⊢ ((𝐺 ∈ 𝑊 ∧ (Vtx‘𝐺) = ∅) → 𝐺 ∈ ConnGraph) | ||
Theorem | 1conngr 30222 | A graph with (at most) one vertex is connected. (Contributed by Alexander van der Vekens, 2-Dec-2017.) (Revised by AV, 15-Feb-2021.) |
⊢ ((𝐺 ∈ 𝑊 ∧ (Vtx‘𝐺) = {𝑁}) → 𝐺 ∈ ConnGraph) | ||
Theorem | conngrv2edg 30223* | A vertex in a connected graph with more than one vertex is incident with at least one edge. Formerly part of proof for vdgn0frgrv2 30323. (Contributed by Alexander van der Vekens, 9-Dec-2017.) (Revised by AV, 4-Apr-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) ⇒ ⊢ ((𝐺 ∈ ConnGraph ∧ 𝑁 ∈ 𝑉 ∧ 1 < (♯‘𝑉)) → ∃𝑒 ∈ ran 𝐼 𝑁 ∈ 𝑒) | ||
Theorem | vdn0conngrumgrv2 30224 | A vertex in a connected multigraph 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‘𝐺) ⇒ ⊢ (((𝐺 ∈ ConnGraph ∧ 𝐺 ∈ UMGraph) ∧ (𝑁 ∈ 𝑉 ∧ 1 < (♯‘𝑉))) → ((VtxDeg‘𝐺)‘𝑁) ≠ 0) | ||
According to Wikipedia ("Eulerian path", 9-Mar-2021, https://en.wikipedia.org/wiki/Eulerian_path): "In graph theory, an Eulerian trail (or Eulerian path) is a trail in a finite graph that visits every edge exactly once (allowing for revisiting vertices). Similarly, an Eulerian circuit or Eulerian cycle is an Eulerian trail that starts and ends on the same vertex. ... The term Eulerian graph has two common meanings in graph theory. One meaning is a graph with an Eulerian circuit, and the other is a graph with every vertex of even degree. These definitions coincide for connected graphs. ... A graph that has an Eulerian trail but not an Eulerian circuit is called semi-Eulerian." Correspondingly, an Eulerian path is defined as "a trail containing all edges" (see definition in [Bollobas] p. 16) in df-eupth 30226 resp. iseupth 30229. (EulerPaths‘𝐺) is the set of all Eulerian paths in graph 𝐺, see eupths 30228. An Eulerian circuit (called Euler tour in the definition in [Diestel] p. 22) is "a circuit in a graph containing all the edges" (see definition in [Bollobas] p. 16), or, with other words, a circuit which is an Eulerian path. The function mapping a graph to the set of its Eulerian paths is defined as EulerPaths in df-eupth 30226, whereas there is no explicit definition for Eulerian circuits (yet): The statement "〈𝐹, 𝑃〉 is an Eulerian circuit" is formally expressed by (𝐹(EulerPaths‘𝐺)𝑃 ∧ 𝐹(Circuits‘𝐺)𝑃). Each Eulerian path can be made an Eulerian circuit by adding an edge which connects the endpoints of the Eulerian path (see eupth2eucrct 30245). Vice versa, removing one edge from a graph with an Eulerian circuit results in a graph with an Eulerian path, see eucrct2eupth 30273. An Eulerian path does not have to be a path in the meaning of definition df-pths 29748, because it may traverse some vertices more than once. Therefore, "Eulerian trail" would be a more appropriate name. The main result of this section is (one direction of) Euler's Theorem: "A non-trivial connected graph has an Euler[ian] circuit iff each vertex has even degree." (see part 1 of theorem 12 in [Bollobas] p. 16 and theorem 1.8.1 in [Diestel] p. 22) or, expressed with Eulerian paths: "A connected graph has an Euler[ian] trail from a vertex x to a vertex y (not equal with x) iff x and y are the only vertices of odd degree." (see part 2 of theorem 12 in [Bollobas] p. 17). In eulerpath 30269, it is shown that a pseudograph with an Eulerian path has either zero or two vertices of odd degree, and eulercrct 30270 shows that a pseudograph with an Eulerian circuit has only vertices of even degree. | ||
Syntax | ceupth 30225 | Extend class notation with Eulerian paths. |
class EulerPaths | ||
Definition | df-eupth 30226* | Define the set of all Eulerian paths on an arbitrary graph. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by AV, 18-Feb-2021.) |
⊢ EulerPaths = (𝑔 ∈ V ↦ {〈𝑓, 𝑝〉 ∣ (𝑓(Trails‘𝑔)𝑝 ∧ 𝑓:(0..^(♯‘𝑓))–onto→dom (iEdg‘𝑔))}) | ||
Theorem | releupth 30227 | 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 30228* | 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 30229 | 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 30230 | 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 30231 | 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 30232 | 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 30233 | 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 30234 | 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 30235* | 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 30236* | 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 30237 | 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 30238 | 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 30239 | 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 30240 | An Eulerian path is a walk. (Contributed by AV, 6-Apr-2021.) |
⊢ (𝐹(EulerPaths‘𝐺)𝑃 → 𝐹(Walks‘𝐺)𝑃) | ||
Theorem | eupthpf 30241 | 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 30242 | 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 30243 | 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 30244 | 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 30245 | 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 30246 | Lemma for eupth2 30267. (Contributed by Mario Carneiro, 8-Apr-2015.) |
⊢ (𝑈 ∈ 𝑉 → (𝑈 ∈ if(𝐴 = 𝐵, ∅, {𝐴, 𝐵}) ↔ (𝐴 ≠ 𝐵 ∧ (𝑈 = 𝐴 ∨ 𝑈 = 𝐵)))) | ||
Theorem | eupth2lem2 30247 | Lemma for eupth2 30267. (Contributed by Mario Carneiro, 8-Apr-2015.) |
⊢ 𝐵 ∈ V ⇒ ⊢ ((𝐵 ≠ 𝐶 ∧ 𝐵 = 𝑈) → (¬ 𝑈 ∈ if(𝐴 = 𝐵, ∅, {𝐴, 𝐵}) ↔ 𝑈 ∈ if(𝐴 = 𝐶, ∅, {𝐴, 𝐶}))) | ||
Theorem | trlsegvdeglem1 30248 | Lemma for trlsegvdeg 30255. (Contributed by AV, 20-Feb-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ (𝜑 → Fun 𝐼) & ⊢ (𝜑 → 𝑁 ∈ (0..^(♯‘𝐹))) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ (𝜑 → 𝐹(Trails‘𝐺)𝑃) ⇒ ⊢ (𝜑 → ((𝑃‘𝑁) ∈ 𝑉 ∧ (𝑃‘(𝑁 + 1)) ∈ 𝑉)) | ||
Theorem | trlsegvdeglem2 30249 | Lemma for trlsegvdeg 30255. (Contributed by AV, 20-Feb-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ (𝜑 → Fun 𝐼) & ⊢ (𝜑 → 𝑁 ∈ (0..^(♯‘𝐹))) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ (𝜑 → 𝐹(Trails‘𝐺)𝑃) & ⊢ (𝜑 → (Vtx‘𝑋) = 𝑉) & ⊢ (𝜑 → (Vtx‘𝑌) = 𝑉) & ⊢ (𝜑 → (Vtx‘𝑍) = 𝑉) & ⊢ (𝜑 → (iEdg‘𝑋) = (𝐼 ↾ (𝐹 “ (0..^𝑁)))) & ⊢ (𝜑 → (iEdg‘𝑌) = {〈(𝐹‘𝑁), (𝐼‘(𝐹‘𝑁))〉}) & ⊢ (𝜑 → (iEdg‘𝑍) = (𝐼 ↾ (𝐹 “ (0...𝑁)))) ⇒ ⊢ (𝜑 → Fun (iEdg‘𝑋)) | ||
Theorem | trlsegvdeglem3 30250 | Lemma for trlsegvdeg 30255. (Contributed by AV, 20-Feb-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ (𝜑 → Fun 𝐼) & ⊢ (𝜑 → 𝑁 ∈ (0..^(♯‘𝐹))) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ (𝜑 → 𝐹(Trails‘𝐺)𝑃) & ⊢ (𝜑 → (Vtx‘𝑋) = 𝑉) & ⊢ (𝜑 → (Vtx‘𝑌) = 𝑉) & ⊢ (𝜑 → (Vtx‘𝑍) = 𝑉) & ⊢ (𝜑 → (iEdg‘𝑋) = (𝐼 ↾ (𝐹 “ (0..^𝑁)))) & ⊢ (𝜑 → (iEdg‘𝑌) = {〈(𝐹‘𝑁), (𝐼‘(𝐹‘𝑁))〉}) & ⊢ (𝜑 → (iEdg‘𝑍) = (𝐼 ↾ (𝐹 “ (0...𝑁)))) ⇒ ⊢ (𝜑 → Fun (iEdg‘𝑌)) | ||
Theorem | trlsegvdeglem4 30251 | Lemma for trlsegvdeg 30255. (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 30252 | Lemma for trlsegvdeg 30255. (Contributed by AV, 21-Feb-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ (𝜑 → Fun 𝐼) & ⊢ (𝜑 → 𝑁 ∈ (0..^(♯‘𝐹))) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ (𝜑 → 𝐹(Trails‘𝐺)𝑃) & ⊢ (𝜑 → (Vtx‘𝑋) = 𝑉) & ⊢ (𝜑 → (Vtx‘𝑌) = 𝑉) & ⊢ (𝜑 → (Vtx‘𝑍) = 𝑉) & ⊢ (𝜑 → (iEdg‘𝑋) = (𝐼 ↾ (𝐹 “ (0..^𝑁)))) & ⊢ (𝜑 → (iEdg‘𝑌) = {〈(𝐹‘𝑁), (𝐼‘(𝐹‘𝑁))〉}) & ⊢ (𝜑 → (iEdg‘𝑍) = (𝐼 ↾ (𝐹 “ (0...𝑁)))) ⇒ ⊢ (𝜑 → dom (iEdg‘𝑌) = {(𝐹‘𝑁)}) | ||
Theorem | trlsegvdeglem6 30253 | Lemma for trlsegvdeg 30255. (Contributed by AV, 21-Feb-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ (𝜑 → Fun 𝐼) & ⊢ (𝜑 → 𝑁 ∈ (0..^(♯‘𝐹))) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ (𝜑 → 𝐹(Trails‘𝐺)𝑃) & ⊢ (𝜑 → (Vtx‘𝑋) = 𝑉) & ⊢ (𝜑 → (Vtx‘𝑌) = 𝑉) & ⊢ (𝜑 → (Vtx‘𝑍) = 𝑉) & ⊢ (𝜑 → (iEdg‘𝑋) = (𝐼 ↾ (𝐹 “ (0..^𝑁)))) & ⊢ (𝜑 → (iEdg‘𝑌) = {〈(𝐹‘𝑁), (𝐼‘(𝐹‘𝑁))〉}) & ⊢ (𝜑 → (iEdg‘𝑍) = (𝐼 ↾ (𝐹 “ (0...𝑁)))) ⇒ ⊢ (𝜑 → dom (iEdg‘𝑋) ∈ Fin) | ||
Theorem | trlsegvdeglem7 30254 | Lemma for trlsegvdeg 30255. (Contributed by AV, 21-Feb-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ (𝜑 → Fun 𝐼) & ⊢ (𝜑 → 𝑁 ∈ (0..^(♯‘𝐹))) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ (𝜑 → 𝐹(Trails‘𝐺)𝑃) & ⊢ (𝜑 → (Vtx‘𝑋) = 𝑉) & ⊢ (𝜑 → (Vtx‘𝑌) = 𝑉) & ⊢ (𝜑 → (Vtx‘𝑍) = 𝑉) & ⊢ (𝜑 → (iEdg‘𝑋) = (𝐼 ↾ (𝐹 “ (0..^𝑁)))) & ⊢ (𝜑 → (iEdg‘𝑌) = {〈(𝐹‘𝑁), (𝐼‘(𝐹‘𝑁))〉}) & ⊢ (𝜑 → (iEdg‘𝑍) = (𝐼 ↾ (𝐹 “ (0...𝑁)))) ⇒ ⊢ (𝜑 → dom (iEdg‘𝑌) ∈ Fin) | ||
Theorem | trlsegvdeg 30255 | Formerly part of proof of eupth2lem3 30264: If a trail in a graph 𝐺 induces a subgraph 𝑍 with the vertices 𝑉 of 𝐺 and the edges being the edges of the walk, and a subgraph 𝑋 with the vertices 𝑉 of 𝐺 and the edges being the edges of the walk except the last one, and a subgraph 𝑌 with the vertices 𝑉 of 𝐺 and one edges being the last edge of the walk, then the vertex degree of any vertex 𝑈 of 𝐺 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.) (Revised by AV, 20-Feb-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ (𝜑 → Fun 𝐼) & ⊢ (𝜑 → 𝑁 ∈ (0..^(♯‘𝐹))) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ (𝜑 → 𝐹(Trails‘𝐺)𝑃) & ⊢ (𝜑 → (Vtx‘𝑋) = 𝑉) & ⊢ (𝜑 → (Vtx‘𝑌) = 𝑉) & ⊢ (𝜑 → (Vtx‘𝑍) = 𝑉) & ⊢ (𝜑 → (iEdg‘𝑋) = (𝐼 ↾ (𝐹 “ (0..^𝑁)))) & ⊢ (𝜑 → (iEdg‘𝑌) = {〈(𝐹‘𝑁), (𝐼‘(𝐹‘𝑁))〉}) & ⊢ (𝜑 → (iEdg‘𝑍) = (𝐼 ↾ (𝐹 “ (0...𝑁)))) ⇒ ⊢ (𝜑 → ((VtxDeg‘𝑍)‘𝑈) = (((VtxDeg‘𝑋)‘𝑈) + ((VtxDeg‘𝑌)‘𝑈))) | ||
Theorem | eupth2lem3lem1 30256 | Lemma for eupth2lem3 30264. (Contributed by AV, 21-Feb-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ (𝜑 → Fun 𝐼) & ⊢ (𝜑 → 𝑁 ∈ (0..^(♯‘𝐹))) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ (𝜑 → 𝐹(Trails‘𝐺)𝑃) & ⊢ (𝜑 → (Vtx‘𝑋) = 𝑉) & ⊢ (𝜑 → (Vtx‘𝑌) = 𝑉) & ⊢ (𝜑 → (Vtx‘𝑍) = 𝑉) & ⊢ (𝜑 → (iEdg‘𝑋) = (𝐼 ↾ (𝐹 “ (0..^𝑁)))) & ⊢ (𝜑 → (iEdg‘𝑌) = {〈(𝐹‘𝑁), (𝐼‘(𝐹‘𝑁))〉}) & ⊢ (𝜑 → (iEdg‘𝑍) = (𝐼 ↾ (𝐹 “ (0...𝑁)))) ⇒ ⊢ (𝜑 → ((VtxDeg‘𝑋)‘𝑈) ∈ ℕ0) | ||
Theorem | eupth2lem3lem2 30257 | Lemma for eupth2lem3 30264. (Contributed by AV, 21-Feb-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ (𝜑 → Fun 𝐼) & ⊢ (𝜑 → 𝑁 ∈ (0..^(♯‘𝐹))) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ (𝜑 → 𝐹(Trails‘𝐺)𝑃) & ⊢ (𝜑 → (Vtx‘𝑋) = 𝑉) & ⊢ (𝜑 → (Vtx‘𝑌) = 𝑉) & ⊢ (𝜑 → (Vtx‘𝑍) = 𝑉) & ⊢ (𝜑 → (iEdg‘𝑋) = (𝐼 ↾ (𝐹 “ (0..^𝑁)))) & ⊢ (𝜑 → (iEdg‘𝑌) = {〈(𝐹‘𝑁), (𝐼‘(𝐹‘𝑁))〉}) & ⊢ (𝜑 → (iEdg‘𝑍) = (𝐼 ↾ (𝐹 “ (0...𝑁)))) ⇒ ⊢ (𝜑 → ((VtxDeg‘𝑌)‘𝑈) ∈ ℕ0) | ||
Theorem | eupth2lem3lem3 30258* | Lemma for eupth2lem3 30264, formerly part of proof of eupth2lem3 30264: 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 30259* | Lemma for eupth2lem3 30264, formerly part of proof of eupth2lem3 30264: 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 30260* | Lemma for eupth2 30267. (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 30261* | Formerly part of proof of eupth2lem3 30264: 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 30262* | Lemma for eupth2lem3 30264: Combining trlsegvdeg 30255, eupth2lem3lem3 30258, eupth2lem3lem4 30259 and eupth2lem3lem6 30261. (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 30263 | Formerly part of proof of eupth2 30267: 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 30264* | Lemma for eupth2 30267. (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 30265* | Lemma for eupth2 30267 (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 30267. (Contributed by Mario Carneiro, 8-Apr-2015.) (Revised by AV, 26-Feb-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ UPGraph) & ⊢ (𝜑 → Fun 𝐼) & ⊢ (𝜑 → 𝐹(EulerPaths‘𝐺)𝑃) ⇒ ⊢ (𝜑 → {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((VtxDeg‘〈𝑉, (𝐼 ↾ (𝐹 “ (0..^0)))〉)‘𝑥)} = ∅) | ||
Theorem | eupth2lems 30266* | Lemma for eupth2 30267 (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 30267. (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 30267* | 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 30268* | 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 30269* | 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 30270* | 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 30271* | 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 30272 | 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 30273 (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 30273* | 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‘𝑆)𝑄) | ||
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 30279. konigsberg 30285 shows that the Königsberg graph has no Eulerian path, thus the Königsberg Bridge problem has no solution. | ||
Theorem | konigsbergvtx 30274 | 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 30275 | 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 30276* | 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 30277* | 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 30278* | 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 30279 | 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 30280 | Lemma 1 for konigsberg 30285: 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 30281 | Lemma 2 for konigsberg 30285: 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 30282 | Lemma 3 for konigsberg 30285: 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 30283* | Lemma 4 for konigsberg 30285: 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 30284* | Lemma 5 for konigsberg 30285: 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 30285 | 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 30269 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‘𝐺) = ∅ | ||
Syntax | cfrgr 30286 | Extend class notation with friendship graphs. |
class FriendGraph | ||
Definition | df-frgr 30287* | 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 30288* | 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 30289 | 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 30290 | 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 30291 | 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 30292 | Any null graph (without vertices) represented as hypergraph is a friendship graph. (Contributed by AV, 29-Mar-2021.) |
⊢ ((𝐺 ∈ UHGraph ∧ (Vtx‘𝐺) = ∅) → 𝐺 ∈ FriendGraph ) | ||
Theorem | frgr0 30293 | The null graph (graph without vertices) is a friendship graph. (Contributed by AV, 29-Mar-2021.) |
⊢ ∅ ∈ FriendGraph | ||
Theorem | frcond1 30294* | 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 30295* | 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 30296* | Variant of frcond2 30295: 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 30297* | 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 30298* | 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 𝑙)) = {𝑥}) | ||
Theorem | frgr1v 30299 | 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 30300 | 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 ) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |