Home | Metamath
Proof Explorer Theorem List (p. 280 of 450) | < 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: | Metamath Proof Explorer
(1-28695) |
Hilbert Space Explorer
(28696-30218) |
Users' Mathboxes
(30219-44926) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | 0trl 27901 | A pair of an empty set (of edges) and a second set (of vertices) is a trail iff the second set contains exactly one vertex. (Contributed by Alexander van der Vekens, 30-Oct-2017.) (Revised by AV, 7-Jan-2021.) (Revised by AV, 30-Oct-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝐺 ∈ 𝑈 → (∅(Trails‘𝐺)𝑃 ↔ 𝑃:(0...0)⟶𝑉)) | ||
Theorem | is0trl 27902 | A pair of an empty set (of edges) and a sequence of one vertex is a trail (of length 0). (Contributed by AV, 7-Jan-2021.) (Revised by AV, 23-Mar-2021.) (Proof shortened by AV, 30-Oct-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ ((𝑃 = {〈0, 𝑁〉} ∧ 𝑁 ∈ 𝑉) → ∅(Trails‘𝐺)𝑃) | ||
Theorem | 0trlon 27903 | A trail of length 0 from a vertex to itself. (Contributed by Alexander van der Vekens, 2-Dec-2017.) (Revised by AV, 8-Jan-2021.) (Revised by AV, 23-Mar-2021.) (Proof shortened by AV, 30-Oct-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ ((𝑃:(0...0)⟶𝑉 ∧ (𝑃‘0) = 𝑁) → ∅(𝑁(TrailsOn‘𝐺)𝑁)𝑃) | ||
Theorem | 0pth 27904 | A pair of an empty set (of edges) and a second set (of vertices) is a path iff the second set contains exactly one vertex. (Contributed by Alexander van der Vekens, 30-Oct-2017.) (Revised by AV, 19-Jan-2021.) (Revised by AV, 30-Oct-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝐺 ∈ 𝑊 → (∅(Paths‘𝐺)𝑃 ↔ 𝑃:(0...0)⟶𝑉)) | ||
Theorem | 0spth 27905 | A pair of an empty set (of edges) and a second set (of vertices) is a simple path iff the second set contains exactly one vertex. (Contributed by Alexander van der Vekens, 30-Oct-2017.) (Revised by AV, 18-Jan-2021.) (Revised by AV, 30-Oct-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝐺 ∈ 𝑊 → (∅(SPaths‘𝐺)𝑃 ↔ 𝑃:(0...0)⟶𝑉)) | ||
Theorem | 0pthon 27906 | A path of length 0 from a vertex to itself. (Contributed by Alexander van der Vekens, 3-Dec-2017.) (Revised by AV, 20-Jan-2021.) (Revised by AV, 30-Oct-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ ((𝑃:(0...0)⟶𝑉 ∧ (𝑃‘0) = 𝑁) → ∅(𝑁(PathsOn‘𝐺)𝑁)𝑃) | ||
Theorem | 0pthon1 27907 | A path of length 0 from a vertex to itself. (Contributed by Alexander van der Vekens, 3-Dec-2017.) (Revised by AV, 20-Jan-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝑁 ∈ 𝑉 → ∅(𝑁(PathsOn‘𝐺)𝑁){〈0, 𝑁〉}) | ||
Theorem | 0pthonv 27908* | For each vertex there is a path of length 0 from the vertex to itself. (Contributed by Alexander van der Vekens, 3-Dec-2017.) (Revised by AV, 21-Jan-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝑁 ∈ 𝑉 → ∃𝑓∃𝑝 𝑓(𝑁(PathsOn‘𝐺)𝑁)𝑝) | ||
Theorem | 0clwlk 27909 | A pair of an empty set (of edges) and a second set (of vertices) is a closed walk if and only if the second set contains exactly one vertex (in an undirected graph). (Contributed by Alexander van der Vekens, 15-Mar-2018.) (Revised by AV, 17-Feb-2021.) (Revised by AV, 30-Oct-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝐺 ∈ 𝑋 → (∅(ClWalks‘𝐺)𝑃 ↔ 𝑃:(0...0)⟶𝑉)) | ||
Theorem | 0clwlkv 27910 | Any vertex (more precisely, a pair of an empty set (of edges) and a singleton function to this vertex) determines a closed walk of length 0. (Contributed by AV, 11-Feb-2022.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ ((𝑋 ∈ 𝑉 ∧ 𝐹 = ∅ ∧ 𝑃:{0}⟶{𝑋}) → 𝐹(ClWalks‘𝐺)𝑃) | ||
Theorem | 0clwlk0 27911 | There is no closed walk in the empty set (i.e. the null graph). (Contributed by Alexander van der Vekens, 2-Sep-2018.) (Revised by AV, 5-Mar-2021.) |
⊢ (ClWalks‘∅) = ∅ | ||
Theorem | 0crct 27912 | A pair of an empty set (of edges) and a second set (of vertices) is a circuit if and only if the second set contains exactly one vertex (in an undirected graph). (Contributed by Alexander van der Vekens, 30-Oct-2017.) (Revised by AV, 31-Jan-2021.) (Revised by AV, 30-Oct-2021.) |
⊢ (𝐺 ∈ 𝑊 → (∅(Circuits‘𝐺)𝑃 ↔ 𝑃:(0...0)⟶(Vtx‘𝐺))) | ||
Theorem | 0cycl 27913 | A pair of an empty set (of edges) and a second set (of vertices) is a cycle if and only if the second set contains exactly one vertex (in an undirected graph). (Contributed by Alexander van der Vekens, 30-Oct-2017.) (Revised by AV, 31-Jan-2021.) (Revised by AV, 30-Oct-2021.) |
⊢ (𝐺 ∈ 𝑊 → (∅(Cycles‘𝐺)𝑃 ↔ 𝑃:(0...0)⟶(Vtx‘𝐺))) | ||
Theorem | 1pthdlem1 27914 | Lemma 1 for 1pthd 27922. (Contributed by Alexander van der Vekens, 4-Dec-2017.) (Revised by AV, 22-Jan-2021.) |
⊢ 𝑃 = 〈“𝑋𝑌”〉 & ⊢ 𝐹 = 〈“𝐽”〉 ⇒ ⊢ Fun ◡(𝑃 ↾ (1..^(♯‘𝐹))) | ||
Theorem | 1pthdlem2 27915 | Lemma 2 for 1pthd 27922. (Contributed by Alexander van der Vekens, 4-Dec-2017.) (Revised by AV, 22-Jan-2021.) |
⊢ 𝑃 = 〈“𝑋𝑌”〉 & ⊢ 𝐹 = 〈“𝐽”〉 ⇒ ⊢ ((𝑃 “ {0, (♯‘𝐹)}) ∩ (𝑃 “ (1..^(♯‘𝐹)))) = ∅ | ||
Theorem | 1wlkdlem1 27916 | Lemma 1 for 1wlkd 27920. (Contributed by AV, 22-Jan-2021.) |
⊢ 𝑃 = 〈“𝑋𝑌”〉 & ⊢ 𝐹 = 〈“𝐽”〉 & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) ⇒ ⊢ (𝜑 → 𝑃:(0...(♯‘𝐹))⟶𝑉) | ||
Theorem | 1wlkdlem2 27917 | Lemma 2 for 1wlkd 27920. (Contributed by AV, 22-Jan-2021.) |
⊢ 𝑃 = 〈“𝑋𝑌”〉 & ⊢ 𝐹 = 〈“𝐽”〉 & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑋 = 𝑌) → (𝐼‘𝐽) = {𝑋}) & ⊢ ((𝜑 ∧ 𝑋 ≠ 𝑌) → {𝑋, 𝑌} ⊆ (𝐼‘𝐽)) ⇒ ⊢ (𝜑 → 𝑋 ∈ (𝐼‘𝐽)) | ||
Theorem | 1wlkdlem3 27918 | Lemma 3 for 1wlkd 27920. (Contributed by AV, 22-Jan-2021.) |
⊢ 𝑃 = 〈“𝑋𝑌”〉 & ⊢ 𝐹 = 〈“𝐽”〉 & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑋 = 𝑌) → (𝐼‘𝐽) = {𝑋}) & ⊢ ((𝜑 ∧ 𝑋 ≠ 𝑌) → {𝑋, 𝑌} ⊆ (𝐼‘𝐽)) ⇒ ⊢ (𝜑 → 𝐹 ∈ Word dom 𝐼) | ||
Theorem | 1wlkdlem4 27919* | Lemma 4 for 1wlkd 27920. (Contributed by AV, 22-Jan-2021.) |
⊢ 𝑃 = 〈“𝑋𝑌”〉 & ⊢ 𝐹 = 〈“𝐽”〉 & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑋 = 𝑌) → (𝐼‘𝐽) = {𝑋}) & ⊢ ((𝜑 ∧ 𝑋 ≠ 𝑌) → {𝑋, 𝑌} ⊆ (𝐼‘𝐽)) ⇒ ⊢ (𝜑 → ∀𝑘 ∈ (0..^(♯‘𝐹))if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘)))) | ||
Theorem | 1wlkd 27920 | In a graph with two vertices and an edge connecting these two vertices, to go from one vertex to the other vertex via this edge is a walk. The two vertices need not be distinct (in the case of a loop). (Contributed by AV, 22-Jan-2021.) (Revised by AV, 23-Mar-2021.) |
⊢ 𝑃 = 〈“𝑋𝑌”〉 & ⊢ 𝐹 = 〈“𝐽”〉 & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑋 = 𝑌) → (𝐼‘𝐽) = {𝑋}) & ⊢ ((𝜑 ∧ 𝑋 ≠ 𝑌) → {𝑋, 𝑌} ⊆ (𝐼‘𝐽)) & ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) ⇒ ⊢ (𝜑 → 𝐹(Walks‘𝐺)𝑃) | ||
Theorem | 1trld 27921 | In a graph 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 Alexander van der Vekens, 3-Dec-2017.) (Revised by AV, 22-Jan-2021.) (Revised by AV, 23-Mar-2021.) (Proof shortened by AV, 30-Oct-2021.) |
⊢ 𝑃 = 〈“𝑋𝑌”〉 & ⊢ 𝐹 = 〈“𝐽”〉 & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑋 = 𝑌) → (𝐼‘𝐽) = {𝑋}) & ⊢ ((𝜑 ∧ 𝑋 ≠ 𝑌) → {𝑋, 𝑌} ⊆ (𝐼‘𝐽)) & ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) ⇒ ⊢ (𝜑 → 𝐹(Trails‘𝐺)𝑃) | ||
Theorem | 1pthd 27922 | In a graph 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 Alexander van der Vekens, 3-Dec-2017.) (Revised by AV, 22-Jan-2021.) (Revised by AV, 23-Mar-2021.) (Proof shortened by AV, 30-Oct-2021.) |
⊢ 𝑃 = 〈“𝑋𝑌”〉 & ⊢ 𝐹 = 〈“𝐽”〉 & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑋 = 𝑌) → (𝐼‘𝐽) = {𝑋}) & ⊢ ((𝜑 ∧ 𝑋 ≠ 𝑌) → {𝑋, 𝑌} ⊆ (𝐼‘𝐽)) & ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) ⇒ ⊢ (𝜑 → 𝐹(Paths‘𝐺)𝑃) | ||
Theorem | 1pthond 27923 | In a graph 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 Alexander van der Vekens, 4-Dec-2017.) (Revised by AV, 22-Jan-2021.) (Revised by AV, 23-Mar-2021.) |
⊢ 𝑃 = 〈“𝑋𝑌”〉 & ⊢ 𝐹 = 〈“𝐽”〉 & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑋 = 𝑌) → (𝐼‘𝐽) = {𝑋}) & ⊢ ((𝜑 ∧ 𝑋 ≠ 𝑌) → {𝑋, 𝑌} ⊆ (𝐼‘𝐽)) & ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) ⇒ ⊢ (𝜑 → 𝐹(𝑋(PathsOn‘𝐺)𝑌)𝑃) | ||
Theorem | upgr1wlkdlem1 27924 | Lemma 1 for upgr1wlkd 27926. (Contributed by AV, 22-Jan-2021.) |
⊢ 𝑃 = 〈“𝑋𝑌”〉 & ⊢ 𝐹 = 〈“𝐽”〉 & ⊢ (𝜑 → 𝑋 ∈ (Vtx‘𝐺)) & ⊢ (𝜑 → 𝑌 ∈ (Vtx‘𝐺)) & ⊢ (𝜑 → ((iEdg‘𝐺)‘𝐽) = {𝑋, 𝑌}) ⇒ ⊢ ((𝜑 ∧ 𝑋 = 𝑌) → ((iEdg‘𝐺)‘𝐽) = {𝑋}) | ||
Theorem | upgr1wlkdlem2 27925 | Lemma 2 for upgr1wlkd 27926. (Contributed by AV, 22-Jan-2021.) |
⊢ 𝑃 = 〈“𝑋𝑌”〉 & ⊢ 𝐹 = 〈“𝐽”〉 & ⊢ (𝜑 → 𝑋 ∈ (Vtx‘𝐺)) & ⊢ (𝜑 → 𝑌 ∈ (Vtx‘𝐺)) & ⊢ (𝜑 → ((iEdg‘𝐺)‘𝐽) = {𝑋, 𝑌}) ⇒ ⊢ ((𝜑 ∧ 𝑋 ≠ 𝑌) → {𝑋, 𝑌} ⊆ ((iEdg‘𝐺)‘𝐽)) | ||
Theorem | upgr1wlkd 27926 | 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 walk. The two vertices need not be distinct (in the case of a loop). (Contributed by AV, 22-Jan-2021.) |
⊢ 𝑃 = 〈“𝑋𝑌”〉 & ⊢ 𝐹 = 〈“𝐽”〉 & ⊢ (𝜑 → 𝑋 ∈ (Vtx‘𝐺)) & ⊢ (𝜑 → 𝑌 ∈ (Vtx‘𝐺)) & ⊢ (𝜑 → ((iEdg‘𝐺)‘𝐽) = {𝑋, 𝑌}) & ⊢ (𝜑 → 𝐺 ∈ UPGraph) ⇒ ⊢ (𝜑 → 𝐹(Walks‘𝐺)𝑃) | ||
Theorem | upgr1trld 27927 | 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 27928 | 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 27929 | 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 27930 | 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 27931 | 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 27932* | 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 27933* | 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 27934 | Lemma 1 for wlk2v2e 27936: 𝐹 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 27935* | Lemma 2 for wlk2v2e 27936: 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 27936 | 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 27937 | 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 27936, 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 27938 | Lemma 1 for 3wlkd 27949. (Contributed by AV, 7-Feb-2021.) |
⊢ 𝑃 = 〈“𝐴𝐵𝐶𝐷”〉 & ⊢ 𝐹 = 〈“𝐽𝐾𝐿”〉 ⇒ ⊢ (♯‘𝑃) = ((♯‘𝐹) + 1) | ||
Theorem | 3wlkdlem2 27939 | Lemma 2 for 3wlkd 27949. (Contributed by AV, 7-Feb-2021.) |
⊢ 𝑃 = 〈“𝐴𝐵𝐶𝐷”〉 & ⊢ 𝐹 = 〈“𝐽𝐾𝐿”〉 ⇒ ⊢ (0..^(♯‘𝐹)) = {0, 1, 2} | ||
Theorem | 3wlkdlem3 27940 | Lemma 3 for 3wlkd 27949. (Contributed by Alexander van der Vekens, 10-Nov-2017.) (Revised by AV, 7-Feb-2021.) |
⊢ 𝑃 = 〈“𝐴𝐵𝐶𝐷”〉 & ⊢ 𝐹 = 〈“𝐽𝐾𝐿”〉 & ⊢ (𝜑 → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉))) ⇒ ⊢ (𝜑 → (((𝑃‘0) = 𝐴 ∧ (𝑃‘1) = 𝐵) ∧ ((𝑃‘2) = 𝐶 ∧ (𝑃‘3) = 𝐷))) | ||
Theorem | 3wlkdlem4 27941* | Lemma 4 for 3wlkd 27949. (Contributed by Alexander van der Vekens, 11-Nov-2017.) (Revised by AV, 7-Feb-2021.) |
⊢ 𝑃 = 〈“𝐴𝐵𝐶𝐷”〉 & ⊢ 𝐹 = 〈“𝐽𝐾𝐿”〉 & ⊢ (𝜑 → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉))) ⇒ ⊢ (𝜑 → ∀𝑘 ∈ (0...(♯‘𝐹))(𝑃‘𝑘) ∈ 𝑉) | ||
Theorem | 3wlkdlem5 27942* | Lemma 5 for 3wlkd 27949. (Contributed by Alexander van der Vekens, 11-Nov-2017.) (Revised by AV, 7-Feb-2021.) |
⊢ 𝑃 = 〈“𝐴𝐵𝐶𝐷”〉 & ⊢ 𝐹 = 〈“𝐽𝐾𝐿”〉 & ⊢ (𝜑 → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉))) & ⊢ (𝜑 → ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶) ∧ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷) ∧ 𝐶 ≠ 𝐷)) ⇒ ⊢ (𝜑 → ∀𝑘 ∈ (0..^(♯‘𝐹))(𝑃‘𝑘) ≠ (𝑃‘(𝑘 + 1))) | ||
Theorem | 3pthdlem1 27943* | Lemma 1 for 3pthd 27953. (Contributed by AV, 9-Feb-2021.) |
⊢ 𝑃 = 〈“𝐴𝐵𝐶𝐷”〉 & ⊢ 𝐹 = 〈“𝐽𝐾𝐿”〉 & ⊢ (𝜑 → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉))) & ⊢ (𝜑 → ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶) ∧ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷) ∧ 𝐶 ≠ 𝐷)) ⇒ ⊢ (𝜑 → ∀𝑘 ∈ (0..^(♯‘𝑃))∀𝑗 ∈ (1..^(♯‘𝐹))(𝑘 ≠ 𝑗 → (𝑃‘𝑘) ≠ (𝑃‘𝑗))) | ||
Theorem | 3wlkdlem6 27944 | Lemma 6 for 3wlkd 27949. (Contributed by AV, 7-Feb-2021.) |
⊢ 𝑃 = 〈“𝐴𝐵𝐶𝐷”〉 & ⊢ 𝐹 = 〈“𝐽𝐾𝐿”〉 & ⊢ (𝜑 → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉))) & ⊢ (𝜑 → ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶) ∧ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷) ∧ 𝐶 ≠ 𝐷)) & ⊢ (𝜑 → ({𝐴, 𝐵} ⊆ (𝐼‘𝐽) ∧ {𝐵, 𝐶} ⊆ (𝐼‘𝐾) ∧ {𝐶, 𝐷} ⊆ (𝐼‘𝐿))) ⇒ ⊢ (𝜑 → (𝐴 ∈ (𝐼‘𝐽) ∧ 𝐵 ∈ (𝐼‘𝐾) ∧ 𝐶 ∈ (𝐼‘𝐿))) | ||
Theorem | 3wlkdlem7 27945 | Lemma 7 for 3wlkd 27949. (Contributed by AV, 7-Feb-2021.) |
⊢ 𝑃 = 〈“𝐴𝐵𝐶𝐷”〉 & ⊢ 𝐹 = 〈“𝐽𝐾𝐿”〉 & ⊢ (𝜑 → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉))) & ⊢ (𝜑 → ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶) ∧ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷) ∧ 𝐶 ≠ 𝐷)) & ⊢ (𝜑 → ({𝐴, 𝐵} ⊆ (𝐼‘𝐽) ∧ {𝐵, 𝐶} ⊆ (𝐼‘𝐾) ∧ {𝐶, 𝐷} ⊆ (𝐼‘𝐿))) ⇒ ⊢ (𝜑 → (𝐽 ∈ V ∧ 𝐾 ∈ V ∧ 𝐿 ∈ V)) | ||
Theorem | 3wlkdlem8 27946 | Lemma 8 for 3wlkd 27949. (Contributed by Alexander van der Vekens, 12-Nov-2017.) (Revised by AV, 7-Feb-2021.) |
⊢ 𝑃 = 〈“𝐴𝐵𝐶𝐷”〉 & ⊢ 𝐹 = 〈“𝐽𝐾𝐿”〉 & ⊢ (𝜑 → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉))) & ⊢ (𝜑 → ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶) ∧ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷) ∧ 𝐶 ≠ 𝐷)) & ⊢ (𝜑 → ({𝐴, 𝐵} ⊆ (𝐼‘𝐽) ∧ {𝐵, 𝐶} ⊆ (𝐼‘𝐾) ∧ {𝐶, 𝐷} ⊆ (𝐼‘𝐿))) ⇒ ⊢ (𝜑 → ((𝐹‘0) = 𝐽 ∧ (𝐹‘1) = 𝐾 ∧ (𝐹‘2) = 𝐿)) | ||
Theorem | 3wlkdlem9 27947 | Lemma 9 for 3wlkd 27949. (Contributed by AV, 7-Feb-2021.) |
⊢ 𝑃 = 〈“𝐴𝐵𝐶𝐷”〉 & ⊢ 𝐹 = 〈“𝐽𝐾𝐿”〉 & ⊢ (𝜑 → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉))) & ⊢ (𝜑 → ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶) ∧ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷) ∧ 𝐶 ≠ 𝐷)) & ⊢ (𝜑 → ({𝐴, 𝐵} ⊆ (𝐼‘𝐽) ∧ {𝐵, 𝐶} ⊆ (𝐼‘𝐾) ∧ {𝐶, 𝐷} ⊆ (𝐼‘𝐿))) ⇒ ⊢ (𝜑 → ({𝐴, 𝐵} ⊆ (𝐼‘(𝐹‘0)) ∧ {𝐵, 𝐶} ⊆ (𝐼‘(𝐹‘1)) ∧ {𝐶, 𝐷} ⊆ (𝐼‘(𝐹‘2)))) | ||
Theorem | 3wlkdlem10 27948* | Lemma 10 for 3wlkd 27949. (Contributed by Alexander van der Vekens, 12-Nov-2017.) (Revised by AV, 7-Feb-2021.) |
⊢ 𝑃 = 〈“𝐴𝐵𝐶𝐷”〉 & ⊢ 𝐹 = 〈“𝐽𝐾𝐿”〉 & ⊢ (𝜑 → ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉))) & ⊢ (𝜑 → ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶) ∧ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷) ∧ 𝐶 ≠ 𝐷)) & ⊢ (𝜑 → ({𝐴, 𝐵} ⊆ (𝐼‘𝐽) ∧ {𝐵, 𝐶} ⊆ (𝐼‘𝐾) ∧ {𝐶, 𝐷} ⊆ (𝐼‘𝐿))) ⇒ ⊢ (𝜑 → ∀𝑘 ∈ (0..^(♯‘𝐹)){(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘))) | ||
Theorem | 3wlkd 27949 | 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 27950 | 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 27951 | 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 27952 | 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 27953 | 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 27954 | 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 27955 | 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 27956 | 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 27957 | 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 27958 | 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 27959* | 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 27960 | Lemma for uhgr3cyclex 27961. (Contributed by AV, 12-Feb-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) ⇒ ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴 ≠ 𝐵) ∧ ((𝐽 ∈ dom 𝐼 ∧ {𝐵, 𝐶} = (𝐼‘𝐽)) ∧ (𝐾 ∈ dom 𝐼 ∧ {𝐶, 𝐴} = (𝐼‘𝐾)))) → 𝐽 ≠ 𝐾) | ||
Theorem | uhgr3cyclex 27961* | 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 27962* | 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 27963* | 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 27964* | 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 27965 | Extend class notation with connected graphs. |
class ConnGraph | ||
Definition | df-conngr 27966* | 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 27908 and dfconngr1 27967. (Contributed by Alexander van der Vekens, 2-Dec-2017.) (Revised by AV, 15-Feb-2021.) |
⊢ ConnGraph = {𝑔 ∣ [(Vtx‘𝑔) / 𝑣]∀𝑘 ∈ 𝑣 ∀𝑛 ∈ 𝑣 ∃𝑓∃𝑝 𝑓(𝑘(PathsOn‘𝑔)𝑛)𝑝} | ||
Theorem | dfconngr1 27967* | 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 27968* | 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 27969* | 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 27970 | 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 27971 | A graph without vertices is connected. (Contributed by Alexander van der Vekens, 2-Dec-2017.) (Revised by AV, 15-Feb-2021.) |
⊢ ∅ ∈ ConnGraph | ||
Theorem | 0vconngr 27972 | 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 27973 | 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 27974* | A vertex in a connected graph with more than one vertex is incident with at least one edge. Formerly part of proof for vdgn0frgrv2 28074. (Contributed by Alexander van der Vekens, 9-Dec-2017.) (Revised by AV, 4-Apr-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) ⇒ ⊢ ((𝐺 ∈ ConnGraph ∧ 𝑁 ∈ 𝑉 ∧ 1 < (♯‘𝑉)) → ∃𝑒 ∈ ran 𝐼 𝑁 ∈ 𝑒) | ||
Theorem | vdn0conngrumgrv2 27975 | 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 27977 resp. iseupth 27980. (EulerPaths‘𝐺) is the set of all Eulerian paths in graph 𝐺, see eupths 27979. 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 27977, 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 27996). Vice versa, removing one edge from a graph with an Eulerian circuit results in a graph with an Eulerian path, see eucrct2eupth 28024. An Eulerian path does not have to be a path in the meaning of definition df-pths 27497, 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 28020, it is shown that a pseudograph with an Eulerian path has either zero or two vertices of odd degree, and eulercrct 28021 shows that a pseudograph with an Eulerian circuit has only vertices of even degree. | ||
Syntax | ceupth 27976 | Extend class notation with Eulerian paths. |
class EulerPaths | ||
Definition | df-eupth 27977* | 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 27978 | 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 27979* | 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 27980 | 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 27981 | 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 27982 | 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 27983 | 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 27984 | 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 27985 | 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 27986* | 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 27987* | 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 27988 | 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 27989 | 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 27990 | 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 27991 | An Eulerian path is a walk. (Contributed by AV, 6-Apr-2021.) |
⊢ (𝐹(EulerPaths‘𝐺)𝑃 → 𝐹(Walks‘𝐺)𝑃) | ||
Theorem | eupthpf 27992 | 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 27993 | 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 27994 | 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 27995 | 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.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ (𝜑 → Fun 𝐼) & ⊢ (𝜑 → 𝐼 ∈ Fin) & ⊢ (𝜑 → 𝐵 ∈ V) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → ¬ 𝐵 ∈ dom 𝐼) & ⊢ (𝜑 → 𝐹(EulerPaths‘𝐺)𝑃) & ⊢ 𝑁 = (♯‘𝐹) & ⊢ (𝜑 → 𝐸 ∈ (Edg‘𝐺)) & ⊢ (𝜑 → {(𝑃‘𝑁), 𝐶} ⊆ 𝐸) & ⊢ (iEdg‘𝑆) = (𝐼 ∪ {〈𝐵, 𝐸〉}) & ⊢ 𝐻 = (𝐹 ∪ {〈𝑁, 𝐵〉}) & ⊢ 𝑄 = (𝑃 ∪ {〈(𝑁 + 1), 𝐶〉}) & ⊢ (Vtx‘𝑆) = 𝑉 & ⊢ ((𝜑 ∧ 𝐶 = (𝑃‘𝑁)) → 𝐸 = {𝐶}) ⇒ ⊢ (𝜑 → 𝐻(EulerPaths‘𝑆)𝑄) | ||
Theorem | eupth2eucrct 27996 | 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.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ (𝜑 → Fun 𝐼) & ⊢ (𝜑 → 𝐼 ∈ Fin) & ⊢ (𝜑 → 𝐵 ∈ V) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → ¬ 𝐵 ∈ dom 𝐼) & ⊢ (𝜑 → 𝐹(EulerPaths‘𝐺)𝑃) & ⊢ 𝑁 = (♯‘𝐹) & ⊢ (𝜑 → 𝐸 ∈ (Edg‘𝐺)) & ⊢ (𝜑 → {(𝑃‘𝑁), 𝐶} ⊆ 𝐸) & ⊢ (iEdg‘𝑆) = (𝐼 ∪ {〈𝐵, 𝐸〉}) & ⊢ 𝐻 = (𝐹 ∪ {〈𝑁, 𝐵〉}) & ⊢ 𝑄 = (𝑃 ∪ {〈(𝑁 + 1), 𝐶〉}) & ⊢ (Vtx‘𝑆) = 𝑉 & ⊢ ((𝜑 ∧ 𝐶 = (𝑃‘𝑁)) → 𝐸 = {𝐶}) & ⊢ (𝜑 → 𝐶 = (𝑃‘0)) ⇒ ⊢ (𝜑 → (𝐻(EulerPaths‘𝑆)𝑄 ∧ 𝐻(Circuits‘𝑆)𝑄)) | ||
Theorem | eupth2lem1 27997 | Lemma for eupth2 28018. (Contributed by Mario Carneiro, 8-Apr-2015.) |
⊢ (𝑈 ∈ 𝑉 → (𝑈 ∈ if(𝐴 = 𝐵, ∅, {𝐴, 𝐵}) ↔ (𝐴 ≠ 𝐵 ∧ (𝑈 = 𝐴 ∨ 𝑈 = 𝐵)))) | ||
Theorem | eupth2lem2 27998 | Lemma for eupth2 28018. (Contributed by Mario Carneiro, 8-Apr-2015.) |
⊢ 𝐵 ∈ V ⇒ ⊢ ((𝐵 ≠ 𝐶 ∧ 𝐵 = 𝑈) → (¬ 𝑈 ∈ if(𝐴 = 𝐵, ∅, {𝐴, 𝐵}) ↔ 𝑈 ∈ if(𝐴 = 𝐶, ∅, {𝐴, 𝐶}))) | ||
Theorem | trlsegvdeglem1 27999 | Lemma for trlsegvdeg 28006. (Contributed by AV, 20-Feb-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ (𝜑 → Fun 𝐼) & ⊢ (𝜑 → 𝑁 ∈ (0..^(♯‘𝐹))) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ (𝜑 → 𝐹(Trails‘𝐺)𝑃) ⇒ ⊢ (𝜑 → ((𝑃‘𝑁) ∈ 𝑉 ∧ (𝑃‘(𝑁 + 1)) ∈ 𝑉)) | ||
Theorem | trlsegvdeglem2 28000 | Lemma for trlsegvdeg 28006. (Contributed by AV, 20-Feb-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ (𝜑 → Fun 𝐼) & ⊢ (𝜑 → 𝑁 ∈ (0..^(♯‘𝐹))) & ⊢ (𝜑 → 𝑈 ∈ 𝑉) & ⊢ (𝜑 → 𝐹(Trails‘𝐺)𝑃) & ⊢ (𝜑 → (Vtx‘𝑋) = 𝑉) & ⊢ (𝜑 → (Vtx‘𝑌) = 𝑉) & ⊢ (𝜑 → (Vtx‘𝑍) = 𝑉) & ⊢ (𝜑 → (iEdg‘𝑋) = (𝐼 ↾ (𝐹 “ (0..^𝑁)))) & ⊢ (𝜑 → (iEdg‘𝑌) = {〈(𝐹‘𝑁), (𝐼‘(𝐹‘𝑁))〉}) & ⊢ (𝜑 → (iEdg‘𝑍) = (𝐼 ↾ (𝐹 “ (0...𝑁)))) ⇒ ⊢ (𝜑 → Fun (iEdg‘𝑋)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |