P. 295 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 29401-29500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	upgr1trld 29401	In a pseudograph with two vertices and an edge connecting these two vertices, to go from one vertex to the other vertex via this edge is a trail. The two vertices need not be distinct (in the case of a loop). (Contributed by AV, 22-Jan-2021.)
⊢ 𝑃 = ⟨“𝑋𝑌”⟩    &   ⊢ 𝐹 = ⟨“𝐽”⟩    &   ⊢ (𝜑 → 𝑋 ∈ (Vtx‘𝐺))    &   ⊢ (𝜑 → 𝑌 ∈ (Vtx‘𝐺))    &   ⊢ (𝜑 → ((iEdg‘𝐺)‘𝐽) = {𝑋, 𝑌})    &   ⊢ (𝜑 → 𝐺 ∈ UPGraph)    ⇒   ⊢ (𝜑 → 𝐹(Trails‘𝐺)𝑃)
Theorem	upgr1pthd 29402	In a pseudograph with two vertices and an edge connecting these two vertices, to go from one vertex to the other vertex via this edge is a path. The two vertices need not be distinct (in the case of a loop) - in this case, however, the path is not a simple path. (Contributed by AV, 22-Jan-2021.)
⊢ 𝑃 = ⟨“𝑋𝑌”⟩    &   ⊢ 𝐹 = ⟨“𝐽”⟩    &   ⊢ (𝜑 → 𝑋 ∈ (Vtx‘𝐺))    &   ⊢ (𝜑 → 𝑌 ∈ (Vtx‘𝐺))    &   ⊢ (𝜑 → ((iEdg‘𝐺)‘𝐽) = {𝑋, 𝑌})    &   ⊢ (𝜑 → 𝐺 ∈ UPGraph)    ⇒   ⊢ (𝜑 → 𝐹(Paths‘𝐺)𝑃)
Theorem	upgr1pthond 29403	In a pseudograph with two vertices and an edge connecting these two vertices, to go from one vertex to the other vertex via this edge is a path from one of these vertices to the other vertex. The two vertices need not be distinct (in the case of a loop) - in this case, however, the path is not a simple path. (Contributed by AV, 22-Jan-2021.)
⊢ 𝑃 = ⟨“𝑋𝑌”⟩    &   ⊢ 𝐹 = ⟨“𝐽”⟩    &   ⊢ (𝜑 → 𝑋 ∈ (Vtx‘𝐺))    &   ⊢ (𝜑 → 𝑌 ∈ (Vtx‘𝐺))    &   ⊢ (𝜑 → ((iEdg‘𝐺)‘𝐽) = {𝑋, 𝑌})    &   ⊢ (𝜑 → 𝐺 ∈ UPGraph)    ⇒   ⊢ (𝜑 → 𝐹(𝑋(PathsOn‘𝐺)𝑌)𝑃)
Theorem	lppthon 29404	A loop (which is an edge at index 𝐽) induces a path of length 1 from a vertex to itself in a hypergraph. (Contributed by AV, 1-Feb-2021.)
⊢ 𝐼 = (iEdg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UHGraph ∧ 𝐽 ∈ dom 𝐼 ∧ (𝐼‘𝐽) = {𝐴}) → ⟨“𝐽”⟩(𝐴(PathsOn‘𝐺)𝐴)⟨“𝐴𝐴”⟩)
Theorem	lp1cycl 29405	A loop (which is an edge at index 𝐽) induces a cycle of length 1 in a hypergraph. (Contributed by AV, 2-Feb-2021.) (Proof shortened by AV, 30-Oct-2021.)
⊢ 𝐼 = (iEdg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UHGraph ∧ 𝐽 ∈ dom 𝐼 ∧ (𝐼‘𝐽) = {𝐴}) → ⟨“𝐽”⟩(Cycles‘𝐺)⟨“𝐴𝐴”⟩)
Theorem	1pthon2v 29406*	For each pair of adjacent vertices there is a path of length 1 from one vertex to the other in a hypergraph. (Contributed by Alexander van der Vekens, 4-Dec-2017.) (Revised by AV, 22-Jan-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UHGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ ∃𝑒 ∈ 𝐸 {𝐴, 𝐵} ⊆ 𝑒) → ∃𝑓∃𝑝 𝑓(𝐴(PathsOn‘𝐺)𝐵)𝑝)
Theorem	1pthon2ve 29407*	For each pair of adjacent vertices there is a path of length 1 from one vertex to the other in a hypergraph. (Contributed by Alexander van der Vekens, 4-Dec-2017.) (Revised by AV, 22-Jan-2021.) (Proof shortened by AV, 15-Feb-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ UHGraph ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ {𝐴, 𝐵} ∈ 𝐸) → ∃𝑓∃𝑝 𝑓(𝐴(PathsOn‘𝐺)𝐵)𝑝)
Theorem	wlk2v2elem1 29408	Lemma 1 for wlk2v2e 29410: 𝐹 is a length 2 word of over {0}, the domain of the singleton word 𝐼. (Contributed by Alexander van der Vekens, 22-Oct-2017.) (Revised by AV, 9-Jan-2021.)
⊢ 𝐼 = ⟨“{𝑋, 𝑌}”⟩    &   ⊢ 𝐹 = ⟨“00”⟩    ⇒   ⊢ 𝐹 ∈ Word dom 𝐼
Theorem	wlk2v2elem2 29409*	Lemma 2 for wlk2v2e 29410: The values of 𝐼 after 𝐹 are edges between two vertices enumerated by 𝑃. (Contributed by Alexander van der Vekens, 22-Oct-2017.) (Revised by AV, 9-Jan-2021.)
⊢ 𝐼 = ⟨“{𝑋, 𝑌}”⟩    &   ⊢ 𝐹 = ⟨“00”⟩    &   ⊢ 𝑋 ∈ V    &   ⊢ 𝑌 ∈ V    &   ⊢ 𝑃 = ⟨“𝑋𝑌𝑋”⟩    ⇒   ⊢ ∀𝑘 ∈ (0..^(♯‘𝐹))(𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}
Theorem	wlk2v2e 29410	In a graph with two vertices and one edge connecting these two vertices, to go from one vertex to the other and back to the first vertex via the same/only edge is a walk. Notice that 𝐺 is a simple graph (without loops) only if 𝑋 ≠ 𝑌. (Contributed by Alexander van der Vekens, 22-Oct-2017.) (Revised by AV, 8-Jan-2021.)
⊢ 𝐼 = ⟨“{𝑋, 𝑌}”⟩    &   ⊢ 𝐹 = ⟨“00”⟩    &   ⊢ 𝑋 ∈ V    &   ⊢ 𝑌 ∈ V    &   ⊢ 𝑃 = ⟨“𝑋𝑌𝑋”⟩    &   ⊢ 𝐺 = ⟨{𝑋, 𝑌}, 𝐼⟩    ⇒   ⊢ 𝐹(Walks‘𝐺)𝑃
Theorem	ntrl2v2e 29411	A walk which is not a trail: In a graph with two vertices and one edge connecting these two vertices, to go from one vertex to the other and back to the first vertex via the same/only edge is a walk, see wlk2v2e 29410, but not a trail. Notice that 𝐺 is a simple graph (without loops) only if 𝑋 ≠ 𝑌. (Contributed by Alexander van der Vekens, 22-Oct-2017.) (Revised by AV, 8-Jan-2021.) (Proof shortened by AV, 30-Oct-2021.)
⊢ 𝐼 = ⟨“{𝑋, 𝑌}”⟩    &   ⊢ 𝐹 = ⟨“00”⟩    &   ⊢ 𝑋 ∈ V    &   ⊢ 𝑌 ∈ V    &   ⊢ 𝑃 = ⟨“𝑋𝑌𝑋”⟩    &   ⊢ 𝐺 = ⟨{𝑋, 𝑌}, 𝐼⟩    ⇒   ⊢ ¬ 𝐹(Trails‘𝐺)𝑃
Theorem	3wlkdlem1 29412	Lemma 1 for 3wlkd 29423. (Contributed by AV, 7-Feb-2021.)
⊢ 𝑃 = ⟨“𝐴𝐵𝐶𝐷”⟩    &   ⊢ 𝐹 = ⟨“𝐽𝐾𝐿”⟩    ⇒   ⊢ (♯‘𝑃) = ((♯‘𝐹) + 1)
Theorem	3wlkdlem2 29413	Lemma 2 for 3wlkd 29423. (Contributed by AV, 7-Feb-2021.)
⊢ 𝑃 = ⟨“𝐴𝐵𝐶𝐷”⟩    &   ⊢ 𝐹 = ⟨“𝐽𝐾𝐿”⟩    ⇒   ⊢ (0..^(♯‘𝐹)) = {0, 1, 2}
Theorem	3wlkdlem3 29414	Lemma 3 for 3wlkd 29423. (Contributed by Alexander van der Vekens, 10-Nov-2017.) (Revised by AV, 7-Feb-2021.)
⊢ 𝑃 = ⟨“𝐴𝐵𝐶𝐷”⟩    &   ⊢ 𝐹 = ⟨“𝐽𝐾𝐿”⟩    &   ⊢ (𝜑 → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉)))    ⇒   ⊢ (𝜑 → (((𝑃‘0) = 𝐴 ∧ (𝑃‘1) = 𝐵) ∧ ((𝑃‘2) = 𝐶 ∧ (𝑃‘3) = 𝐷)))
Theorem	3wlkdlem4 29415*	Lemma 4 for 3wlkd 29423. (Contributed by Alexander van der Vekens, 11-Nov-2017.) (Revised by AV, 7-Feb-2021.)
⊢ 𝑃 = ⟨“𝐴𝐵𝐶𝐷”⟩    &   ⊢ 𝐹 = ⟨“𝐽𝐾𝐿”⟩    &   ⊢ (𝜑 → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉)))    ⇒   ⊢ (𝜑 → ∀𝑘 ∈ (0...(♯‘𝐹))(𝑃‘𝑘) ∈ 𝑉)
Theorem	3wlkdlem5 29416*	Lemma 5 for 3wlkd 29423. (Contributed by Alexander van der Vekens, 11-Nov-2017.) (Revised by AV, 7-Feb-2021.)
⊢ 𝑃 = ⟨“𝐴𝐵𝐶𝐷”⟩    &   ⊢ 𝐹 = ⟨“𝐽𝐾𝐿”⟩    &   ⊢ (𝜑 → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉)))    &   ⊢ (𝜑 → ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶) ∧ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷) ∧ 𝐶 ≠ 𝐷))    ⇒   ⊢ (𝜑 → ∀𝑘 ∈ (0..^(♯‘𝐹))(𝑃‘𝑘) ≠ (𝑃‘(𝑘 + 1)))
Theorem	3pthdlem1 29417*	Lemma 1 for 3pthd 29427. (Contributed by AV, 9-Feb-2021.)
⊢ 𝑃 = ⟨“𝐴𝐵𝐶𝐷”⟩    &   ⊢ 𝐹 = ⟨“𝐽𝐾𝐿”⟩    &   ⊢ (𝜑 → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉)))    &   ⊢ (𝜑 → ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶) ∧ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷) ∧ 𝐶 ≠ 𝐷))    ⇒   ⊢ (𝜑 → ∀𝑘 ∈ (0..^(♯‘𝑃))∀𝑗 ∈ (1..^(♯‘𝐹))(𝑘 ≠ 𝑗 → (𝑃‘𝑘) ≠ (𝑃‘𝑗)))
Theorem	3wlkdlem6 29418	Lemma 6 for 3wlkd 29423. (Contributed by AV, 7-Feb-2021.)
⊢ 𝑃 = ⟨“𝐴𝐵𝐶𝐷”⟩    &   ⊢ 𝐹 = ⟨“𝐽𝐾𝐿”⟩    &   ⊢ (𝜑 → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉)))    &   ⊢ (𝜑 → ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶) ∧ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷) ∧ 𝐶 ≠ 𝐷))    &   ⊢ (𝜑 → ({𝐴, 𝐵} ⊆ (𝐼‘𝐽) ∧ {𝐵, 𝐶} ⊆ (𝐼‘𝐾) ∧ {𝐶, 𝐷} ⊆ (𝐼‘𝐿)))    ⇒   ⊢ (𝜑 → (𝐴 ∈ (𝐼‘𝐽) ∧ 𝐵 ∈ (𝐼‘𝐾) ∧ 𝐶 ∈ (𝐼‘𝐿)))
Theorem	3wlkdlem7 29419	Lemma 7 for 3wlkd 29423. (Contributed by AV, 7-Feb-2021.)
⊢ 𝑃 = ⟨“𝐴𝐵𝐶𝐷”⟩    &   ⊢ 𝐹 = ⟨“𝐽𝐾𝐿”⟩    &   ⊢ (𝜑 → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉)))    &   ⊢ (𝜑 → ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶) ∧ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷) ∧ 𝐶 ≠ 𝐷))    &   ⊢ (𝜑 → ({𝐴, 𝐵} ⊆ (𝐼‘𝐽) ∧ {𝐵, 𝐶} ⊆ (𝐼‘𝐾) ∧ {𝐶, 𝐷} ⊆ (𝐼‘𝐿)))    ⇒   ⊢ (𝜑 → (𝐽 ∈ V ∧ 𝐾 ∈ V ∧ 𝐿 ∈ V))
Theorem	3wlkdlem8 29420	Lemma 8 for 3wlkd 29423. (Contributed by Alexander van der Vekens, 12-Nov-2017.) (Revised by AV, 7-Feb-2021.)
⊢ 𝑃 = ⟨“𝐴𝐵𝐶𝐷”⟩    &   ⊢ 𝐹 = ⟨“𝐽𝐾𝐿”⟩    &   ⊢ (𝜑 → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉)))    &   ⊢ (𝜑 → ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶) ∧ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷) ∧ 𝐶 ≠ 𝐷))    &   ⊢ (𝜑 → ({𝐴, 𝐵} ⊆ (𝐼‘𝐽) ∧ {𝐵, 𝐶} ⊆ (𝐼‘𝐾) ∧ {𝐶, 𝐷} ⊆ (𝐼‘𝐿)))    ⇒   ⊢ (𝜑 → ((𝐹‘0) = 𝐽 ∧ (𝐹‘1) = 𝐾 ∧ (𝐹‘2) = 𝐿))
Theorem	3wlkdlem9 29421	Lemma 9 for 3wlkd 29423. (Contributed by AV, 7-Feb-2021.)
⊢ 𝑃 = ⟨“𝐴𝐵𝐶𝐷”⟩    &   ⊢ 𝐹 = ⟨“𝐽𝐾𝐿”⟩    &   ⊢ (𝜑 → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉)))    &   ⊢ (𝜑 → ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶) ∧ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷) ∧ 𝐶 ≠ 𝐷))    &   ⊢ (𝜑 → ({𝐴, 𝐵} ⊆ (𝐼‘𝐽) ∧ {𝐵, 𝐶} ⊆ (𝐼‘𝐾) ∧ {𝐶, 𝐷} ⊆ (𝐼‘𝐿)))    ⇒   ⊢ (𝜑 → ({𝐴, 𝐵} ⊆ (𝐼‘(𝐹‘0)) ∧ {𝐵, 𝐶} ⊆ (𝐼‘(𝐹‘1)) ∧ {𝐶, 𝐷} ⊆ (𝐼‘(𝐹‘2))))
Theorem	3wlkdlem10 29422*	Lemma 10 for 3wlkd 29423. (Contributed by Alexander van der Vekens, 12-Nov-2017.) (Revised by AV, 7-Feb-2021.)
⊢ 𝑃 = ⟨“𝐴𝐵𝐶𝐷”⟩    &   ⊢ 𝐹 = ⟨“𝐽𝐾𝐿”⟩    &   ⊢ (𝜑 → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉)))    &   ⊢ (𝜑 → ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶) ∧ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷) ∧ 𝐶 ≠ 𝐷))    &   ⊢ (𝜑 → ({𝐴, 𝐵} ⊆ (𝐼‘𝐽) ∧ {𝐵, 𝐶} ⊆ (𝐼‘𝐾) ∧ {𝐶, 𝐷} ⊆ (𝐼‘𝐿)))    ⇒   ⊢ (𝜑 → ∀𝑘 ∈ (0..^(♯‘𝐹)){(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘)))
Theorem	3wlkd 29423	Construction of a walk from two given edges in a graph. (Contributed by AV, 7-Feb-2021.) (Revised by AV, 24-Mar-2021.)
⊢ 𝑃 = ⟨“𝐴𝐵𝐶𝐷”⟩    &   ⊢ 𝐹 = ⟨“𝐽𝐾𝐿”⟩    &   ⊢ (𝜑 → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉)))    &   ⊢ (𝜑 → ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶) ∧ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷) ∧ 𝐶 ≠ 𝐷))    &   ⊢ (𝜑 → ({𝐴, 𝐵} ⊆ (𝐼‘𝐽) ∧ {𝐵, 𝐶} ⊆ (𝐼‘𝐾) ∧ {𝐶, 𝐷} ⊆ (𝐼‘𝐿)))    &   ⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    ⇒   ⊢ (𝜑 → 𝐹(Walks‘𝐺)𝑃)
Theorem	3wlkond 29424	A walk 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‘𝐺)    ⇒   ⊢ (𝜑 → 𝐹(𝐴(WalksOn‘𝐺)𝐷)𝑃)
Theorem	3trld 29425	Construction of a trail from two given edges in a graph. (Contributed by Alexander van der Vekens, 13-Nov-2017.) (Revised by AV, 8-Feb-2021.) (Revised by AV, 24-Mar-2021.) (Proof shortened by AV, 30-Oct-2021.)
⊢ 𝑃 = ⟨“𝐴𝐵𝐶𝐷”⟩    &   ⊢ 𝐹 = ⟨“𝐽𝐾𝐿”⟩    &   ⊢ (𝜑 → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉)))    &   ⊢ (𝜑 → ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶) ∧ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷) ∧ 𝐶 ≠ 𝐷))    &   ⊢ (𝜑 → ({𝐴, 𝐵} ⊆ (𝐼‘𝐽) ∧ {𝐵, 𝐶} ⊆ (𝐼‘𝐾) ∧ {𝐶, 𝐷} ⊆ (𝐼‘𝐿)))    &   ⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ (𝜑 → (𝐽 ≠ 𝐾 ∧ 𝐽 ≠ 𝐿 ∧ 𝐾 ≠ 𝐿))    ⇒   ⊢ (𝜑 → 𝐹(Trails‘𝐺)𝑃)
Theorem	3trlond 29426	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 29427	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 29428	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 29429	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 29430	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 29431	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 29432	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 29433*	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 29434	Lemma for uhgr3cyclex 29435. (Contributed by AV, 12-Feb-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐸 = (Edg‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    ⇒   ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) ∧ ((𝐽 ∈ dom 𝐼 ∧ {𝐵, 𝐶} = (𝐼‘𝐽)) ∧ (𝐾 ∈ dom 𝐼 ∧ {𝐶, 𝐴} = (𝐼‘𝐾)))) → 𝐽 ≠ 𝐾)
Theorem	uhgr3cyclex 29435*	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 29436*	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 29437*	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 29438*	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) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 ∃𝑐 ∈ 𝑉 ∃𝑑 ∈ 𝑉 ((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸)) ∧ ((𝑎 ≠ 𝑏 ∧ 𝑎 ≠ 𝑐 ∧ 𝑎 ≠ 𝑑) ∧ (𝑏 ≠ 𝑐 ∧ 𝑏 ≠ 𝑑 ∧ 𝑐 ≠ 𝑑))))
17.3.12  Connected graphs
Syntax	cconngr 29439	Extend class notation with connected graphs.
class ConnGraph
Definition	df-conngr 29440*	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 29382 and dfconngr1 29441. (Contributed by Alexander van der Vekens, 2-Dec-2017.) (Revised by AV, 15-Feb-2021.)
⊢ ConnGraph = {𝑔 ∣ [(Vtx‘𝑔) / 𝑣]∀𝑘 ∈ 𝑣 ∀𝑛 ∈ 𝑣 ∃𝑓∃𝑝 𝑓(𝑘(PathsOn‘𝑔)𝑛)𝑝}
Theorem	dfconngr1 29441*	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 29442*	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 29443*	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 29444	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 29445	A graph without vertices is connected. (Contributed by Alexander van der Vekens, 2-Dec-2017.) (Revised by AV, 15-Feb-2021.)
⊢ ∅ ∈ ConnGraph
Theorem	0vconngr 29446	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 29447	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 29448*	A vertex in a connected graph with more than one vertex is incident with at least one edge. Formerly part of proof for vdgn0frgrv2 29548. (Contributed by Alexander van der Vekens, 9-Dec-2017.) (Revised by AV, 4-Apr-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ ConnGraph ∧ 𝑁 ∈ 𝑉 ∧ 1 < (♯‘𝑉)) → ∃𝑒 ∈ ran 𝐼 𝑁 ∈ 𝑒)
Theorem	vdn0conngrumgrv2 29449	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)
17.4  Eulerian paths and the Konigsberg Bridge problem
17.4.1  Eulerian paths 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 29451 resp. iseupth 29454. (EulerPaths‘𝐺) is the set of all Eulerian paths in graph 𝐺, see eupths 29453. 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 29451, 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 29470). Vice versa, removing one edge from a graph with an Eulerian circuit results in a graph with an Eulerian path, see eucrct2eupth 29498. An Eulerian path does not have to be a path in the meaning of definition df-pths 28973, 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 29494, it is shown that a pseudograph with an Eulerian path has either zero or two vertices of odd degree, and eulercrct 29495 shows that a pseudograph with an Eulerian circuit has only vertices of even degree.
Syntax	ceupth 29450	Extend class notation with Eulerian paths.
class EulerPaths
Definition	df-eupth 29451*	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 29452	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 29453*	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 29454	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 29455	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 29456	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 29457	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 29458	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 29459	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 29460*	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 29461*	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 29462	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 29463	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 29464	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 29465	An Eulerian path is a walk. (Contributed by AV, 6-Apr-2021.)
⊢ (𝐹(EulerPaths‘𝐺)𝑃 → 𝐹(Walks‘𝐺)𝑃)
Theorem	eupthpf 29466	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 29467	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 29468	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 29469	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 29470	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 29471	Lemma for eupth2 29492. (Contributed by Mario Carneiro, 8-Apr-2015.)
⊢ (𝑈 ∈ 𝑉 → (𝑈 ∈ if(𝐴 = 𝐵, ∅, {𝐴, 𝐵}) ↔ (𝐴 ≠ 𝐵 ∧ (𝑈 = 𝐴 ∨ 𝑈 = 𝐵))))
Theorem	eupth2lem2 29472	Lemma for eupth2 29492. (Contributed by Mario Carneiro, 8-Apr-2015.)
⊢ 𝐵 ∈ V    ⇒   ⊢ ((𝐵 ≠ 𝐶 ∧ 𝐵 = 𝑈) → (¬ 𝑈 ∈ if(𝐴 = 𝐵, ∅, {𝐴, 𝐵}) ↔ 𝑈 ∈ if(𝐴 = 𝐶, ∅, {𝐴, 𝐶})))
Theorem	trlsegvdeglem1 29473	Lemma for trlsegvdeg 29480. (Contributed by AV, 20-Feb-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ (𝜑 → Fun 𝐼)    &   ⊢ (𝜑 → 𝑁 ∈ (0..^(♯‘𝐹)))    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹(Trails‘𝐺)𝑃)    ⇒   ⊢ (𝜑 → ((𝑃‘𝑁) ∈ 𝑉 ∧ (𝑃‘(𝑁 + 1)) ∈ 𝑉))
Theorem	trlsegvdeglem2 29474	Lemma for trlsegvdeg 29480. (Contributed by AV, 20-Feb-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ (𝜑 → Fun 𝐼)    &   ⊢ (𝜑 → 𝑁 ∈ (0..^(♯‘𝐹)))    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹(Trails‘𝐺)𝑃)    &   ⊢ (𝜑 → (Vtx‘𝑋) = 𝑉)    &   ⊢ (𝜑 → (Vtx‘𝑌) = 𝑉)    &   ⊢ (𝜑 → (Vtx‘𝑍) = 𝑉)    &   ⊢ (𝜑 → (iEdg‘𝑋) = (𝐼 ↾ (𝐹 “ (0..^𝑁))))    &   ⊢ (𝜑 → (iEdg‘𝑌) = {⟨(𝐹‘𝑁), (𝐼‘(𝐹‘𝑁))⟩})    &   ⊢ (𝜑 → (iEdg‘𝑍) = (𝐼 ↾ (𝐹 “ (0...𝑁))))    ⇒   ⊢ (𝜑 → Fun (iEdg‘𝑋))
Theorem	trlsegvdeglem3 29475	Lemma for trlsegvdeg 29480. (Contributed by AV, 20-Feb-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ (𝜑 → Fun 𝐼)    &   ⊢ (𝜑 → 𝑁 ∈ (0..^(♯‘𝐹)))    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹(Trails‘𝐺)𝑃)    &   ⊢ (𝜑 → (Vtx‘𝑋) = 𝑉)    &   ⊢ (𝜑 → (Vtx‘𝑌) = 𝑉)    &   ⊢ (𝜑 → (Vtx‘𝑍) = 𝑉)    &   ⊢ (𝜑 → (iEdg‘𝑋) = (𝐼 ↾ (𝐹 “ (0..^𝑁))))    &   ⊢ (𝜑 → (iEdg‘𝑌) = {⟨(𝐹‘𝑁), (𝐼‘(𝐹‘𝑁))⟩})    &   ⊢ (𝜑 → (iEdg‘𝑍) = (𝐼 ↾ (𝐹 “ (0...𝑁))))    ⇒   ⊢ (𝜑 → Fun (iEdg‘𝑌))
Theorem	trlsegvdeglem4 29476	Lemma for trlsegvdeg 29480. (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 29477	Lemma for trlsegvdeg 29480. (Contributed by AV, 21-Feb-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ (𝜑 → Fun 𝐼)    &   ⊢ (𝜑 → 𝑁 ∈ (0..^(♯‘𝐹)))    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹(Trails‘𝐺)𝑃)    &   ⊢ (𝜑 → (Vtx‘𝑋) = 𝑉)    &   ⊢ (𝜑 → (Vtx‘𝑌) = 𝑉)    &   ⊢ (𝜑 → (Vtx‘𝑍) = 𝑉)    &   ⊢ (𝜑 → (iEdg‘𝑋) = (𝐼 ↾ (𝐹 “ (0..^𝑁))))    &   ⊢ (𝜑 → (iEdg‘𝑌) = {⟨(𝐹‘𝑁), (𝐼‘(𝐹‘𝑁))⟩})    &   ⊢ (𝜑 → (iEdg‘𝑍) = (𝐼 ↾ (𝐹 “ (0...𝑁))))    ⇒   ⊢ (𝜑 → dom (iEdg‘𝑌) = {(𝐹‘𝑁)})
Theorem	trlsegvdeglem6 29478	Lemma for trlsegvdeg 29480. (Contributed by AV, 21-Feb-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ (𝜑 → Fun 𝐼)    &   ⊢ (𝜑 → 𝑁 ∈ (0..^(♯‘𝐹)))    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹(Trails‘𝐺)𝑃)    &   ⊢ (𝜑 → (Vtx‘𝑋) = 𝑉)    &   ⊢ (𝜑 → (Vtx‘𝑌) = 𝑉)    &   ⊢ (𝜑 → (Vtx‘𝑍) = 𝑉)    &   ⊢ (𝜑 → (iEdg‘𝑋) = (𝐼 ↾ (𝐹 “ (0..^𝑁))))    &   ⊢ (𝜑 → (iEdg‘𝑌) = {⟨(𝐹‘𝑁), (𝐼‘(𝐹‘𝑁))⟩})    &   ⊢ (𝜑 → (iEdg‘𝑍) = (𝐼 ↾ (𝐹 “ (0...𝑁))))    ⇒   ⊢ (𝜑 → dom (iEdg‘𝑋) ∈ Fin)
Theorem	trlsegvdeglem7 29479	Lemma for trlsegvdeg 29480. (Contributed by AV, 21-Feb-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ (𝜑 → Fun 𝐼)    &   ⊢ (𝜑 → 𝑁 ∈ (0..^(♯‘𝐹)))    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹(Trails‘𝐺)𝑃)    &   ⊢ (𝜑 → (Vtx‘𝑋) = 𝑉)    &   ⊢ (𝜑 → (Vtx‘𝑌) = 𝑉)    &   ⊢ (𝜑 → (Vtx‘𝑍) = 𝑉)    &   ⊢ (𝜑 → (iEdg‘𝑋) = (𝐼 ↾ (𝐹 “ (0..^𝑁))))    &   ⊢ (𝜑 → (iEdg‘𝑌) = {⟨(𝐹‘𝑁), (𝐼‘(𝐹‘𝑁))⟩})    &   ⊢ (𝜑 → (iEdg‘𝑍) = (𝐼 ↾ (𝐹 “ (0...𝑁))))    ⇒   ⊢ (𝜑 → dom (iEdg‘𝑌) ∈ Fin)
Theorem	trlsegvdeg 29480	Formerly part of proof of eupth2lem3 29489: 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 29481	Lemma for eupth2lem3 29489. (Contributed by AV, 21-Feb-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ (𝜑 → Fun 𝐼)    &   ⊢ (𝜑 → 𝑁 ∈ (0..^(♯‘𝐹)))    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹(Trails‘𝐺)𝑃)    &   ⊢ (𝜑 → (Vtx‘𝑋) = 𝑉)    &   ⊢ (𝜑 → (Vtx‘𝑌) = 𝑉)    &   ⊢ (𝜑 → (Vtx‘𝑍) = 𝑉)    &   ⊢ (𝜑 → (iEdg‘𝑋) = (𝐼 ↾ (𝐹 “ (0..^𝑁))))    &   ⊢ (𝜑 → (iEdg‘𝑌) = {⟨(𝐹‘𝑁), (𝐼‘(𝐹‘𝑁))⟩})    &   ⊢ (𝜑 → (iEdg‘𝑍) = (𝐼 ↾ (𝐹 “ (0...𝑁))))    ⇒   ⊢ (𝜑 → ((VtxDeg‘𝑋)‘𝑈) ∈ ℕ0)
Theorem	eupth2lem3lem2 29482	Lemma for eupth2lem3 29489. (Contributed by AV, 21-Feb-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ (𝜑 → Fun 𝐼)    &   ⊢ (𝜑 → 𝑁 ∈ (0..^(♯‘𝐹)))    &   ⊢ (𝜑 → 𝑈 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹(Trails‘𝐺)𝑃)    &   ⊢ (𝜑 → (Vtx‘𝑋) = 𝑉)    &   ⊢ (𝜑 → (Vtx‘𝑌) = 𝑉)    &   ⊢ (𝜑 → (Vtx‘𝑍) = 𝑉)    &   ⊢ (𝜑 → (iEdg‘𝑋) = (𝐼 ↾ (𝐹 “ (0..^𝑁))))    &   ⊢ (𝜑 → (iEdg‘𝑌) = {⟨(𝐹‘𝑁), (𝐼‘(𝐹‘𝑁))⟩})    &   ⊢ (𝜑 → (iEdg‘𝑍) = (𝐼 ↾ (𝐹 “ (0...𝑁))))    ⇒   ⊢ (𝜑 → ((VtxDeg‘𝑌)‘𝑈) ∈ ℕ0)
Theorem	eupth2lem3lem3 29483*	Lemma for eupth2lem3 29489, formerly part of proof of eupth2lem3 29489: 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 29484*	Lemma for eupth2lem3 29489, formerly part of proof of eupth2lem3 29489: 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 29485*	Lemma for eupth2 29492. (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 29486*	Formerly part of proof of eupth2lem3 29489: 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 29487*	Lemma for eupth2lem3 29489: Combining trlsegvdeg 29480, eupth2lem3lem3 29483, eupth2lem3lem4 29484 and eupth2lem3lem6 29486. (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 29488	Formerly part of proof of eupth2 29492: 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 29489*	Lemma for eupth2 29492. (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 29490*	Lemma for eupth2 29492 (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 29492. (Contributed by Mario Carneiro, 8-Apr-2015.) (Revised by AV, 26-Feb-2021.)
⊢ 𝑉 = (Vtx‘𝐺)    &   ⊢ 𝐼 = (iEdg‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ UPGraph)    &   ⊢ (𝜑 → Fun 𝐼)    &   ⊢ (𝜑 → 𝐹(EulerPaths‘𝐺)𝑃)    ⇒   ⊢ (𝜑 → {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((VtxDeg‘⟨𝑉, (𝐼 ↾ (𝐹 “ (0..^0)))⟩)‘𝑥)} = ∅)
Theorem	eupth2lems 29491*	Lemma for eupth2 29492 (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 29492. (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 29492*	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 29493*	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 29494*	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 29495*	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 29496*	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 29497	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 29498 (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 29498*	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 29504. konigsberg 29510 shows that the Königsberg graph has no Eulerian path, thus the Königsberg Bridge problem has no solution.
Theorem	konigsbergvtx 29499	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 29500	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}”⟩