Home | Metamath
Proof Explorer Theorem List (p. 409 of 424) | < 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-27159) |
Hilbert Space Explorer
(27160-28684) |
Users' Mathboxes
(28685-42360) |
Type | Label | Description |
---|---|---|
Statement | ||
Definition | df-wlks 40801* |
Define the set of all walks (in a pseudograph). TODO-AV: This
corresponds to the definition of Walks, but can
be removed and the
defining theorem upgriswlk 40849 could be used instead.
According to Wikipedia ("Path (graph theory)", https://en.wikipedia.org/wiki/Path_(graph_theory), 3-Oct-2017): "A walk of length k in a graph is an alternating sequence of vertices and edges, v0 , e0 , v1 , e1 , v2 , ... , v(k-1) , e(k-1) , v(k) which begins and ends with vertices. If the graph is undirected, then the endpoints of e(i) are v(i) and v(i+1)." According to Bollobas: " A walk W in a graph is an alternating sequence of vertices and edges x0 , e1 , x1 , e2 , ... , e(l) , x(l) where e(i) = x(i-1)x(i), 0<i<=l.", see Definition of [Bollobas] p. 4. Therefore, a walk can be represented by two mappings f from { 1 , ... , n } and p from { 0 , ... , n }, where f enumerates the (indices of the) edges, and p enumerates the vertices. So the walk is represented by the following sequence: p(0) e(f(1)) p(1) e(f(2)) ... p(n-1) e(f(n)) p(n). Although this definition is also applicable for arbitrary hypergraphs, it allows only walks consisting of not proper hyperedges (i.e. edges connecting at most two vertices). Therefore, it should be used for pseudograhs only. (Contributed by Alexander van der Vekens and Mario Carneiro, 4-Oct-2017.) (Revised by AV, 28-Dec-2020.) |
⊢ UPWalks = (𝑔 ∈ V ↦ {〈𝑓, 𝑝〉 ∣ (𝑓 ∈ Word dom (iEdg‘𝑔) ∧ 𝑝:(0...(#‘𝑓))⟶(Vtx‘𝑔) ∧ ∀𝑘 ∈ (0..^(#‘𝑓))((iEdg‘𝑔)‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))})}) | ||
Definition | df-wlkson 40802* | Define the collection of walks with particular endpoints (in a hypergraph). The predicate 𝐹(𝐴(WalksOn‘𝐺)𝐵)𝑃 can be read as "The pair 〈𝐹, 𝑃〉 represents a walk from vertex 𝐴 to vertex 𝐵 in a graph 𝐺", see also iswlkOn 40865. This corresponds to the "x0-x(l)-walks", see Definition in [Bollobas] p. 5. (Contributed by Alexander van der Vekens and Mario Carneiro, 4-Oct-2017.) (Revised by AV, 28-Dec-2020.) |
⊢ WalksOn = (𝑔 ∈ V ↦ (𝑎 ∈ (Vtx‘𝑔), 𝑏 ∈ (Vtx‘𝑔) ↦ {〈𝑓, 𝑝〉 ∣ (𝑓(1Walks‘𝑔)𝑝 ∧ (𝑝‘0) = 𝑎 ∧ (𝑝‘(#‘𝑓)) = 𝑏)})) | ||
Theorem | ewlksfval 40803* | The set of s-walks of edges (in a hypergraph). (Contributed by AV, 4-Jan-2021.) |
⊢ 𝐼 = (iEdg‘𝐺) ⇒ ⊢ ((𝐺 ∈ 𝑊 ∧ 𝑆 ∈ ℕ0*) → (𝐺 EdgWalks 𝑆) = {𝑓 ∣ (𝑓 ∈ Word dom 𝐼 ∧ ∀𝑘 ∈ (1..^(#‘𝑓))𝑆 ≤ (#‘((𝐼‘(𝑓‘(𝑘 − 1))) ∩ (𝐼‘(𝑓‘𝑘)))))}) | ||
Theorem | isewlk 40804* | Conditions for a function (sequence of hyperedges) to be an s-walk of edges. (Contributed by AV, 4-Jan-2021.) |
⊢ 𝐼 = (iEdg‘𝐺) ⇒ ⊢ ((𝐺 ∈ 𝑊 ∧ 𝑆 ∈ ℕ0* ∧ 𝐹 ∈ 𝑈) → (𝐹 ∈ (𝐺 EdgWalks 𝑆) ↔ (𝐹 ∈ Word dom 𝐼 ∧ ∀𝑘 ∈ (1..^(#‘𝐹))𝑆 ≤ (#‘((𝐼‘(𝐹‘(𝑘 − 1))) ∩ (𝐼‘(𝐹‘𝑘))))))) | ||
Theorem | ewlkprop 40805* | Properties of an s-walk of edges. (Contributed by AV, 4-Jan-2021.) |
⊢ 𝐼 = (iEdg‘𝐺) ⇒ ⊢ (𝐹 ∈ (𝐺 EdgWalks 𝑆) → ((𝐺 ∈ V ∧ 𝑆 ∈ ℕ0*) ∧ 𝐹 ∈ Word dom 𝐼 ∧ ∀𝑘 ∈ (1..^(#‘𝐹))𝑆 ≤ (#‘((𝐼‘(𝐹‘(𝑘 − 1))) ∩ (𝐼‘(𝐹‘𝑘)))))) | ||
Theorem | ewlkinedg 40806 | The intersection (common vertices) of two adjacent edges in an s-walk of edges. (Contributed by AV, 4-Jan-2021.) |
⊢ 𝐼 = (iEdg‘𝐺) ⇒ ⊢ ((𝐹 ∈ (𝐺 EdgWalks 𝑆) ∧ 𝐾 ∈ (1..^(#‘𝐹))) → 𝑆 ≤ (#‘((𝐼‘(𝐹‘(𝐾 − 1))) ∩ (𝐼‘(𝐹‘𝐾))))) | ||
Theorem | ewlkle 40807 | An s-walk of edges is also a t-walk of edges if t <_ s. (Contributed by AV, 4-Jan-2021.) |
⊢ ((𝐹 ∈ (𝐺 EdgWalks 𝑆) ∧ 𝑇 ∈ ℕ0* ∧ 𝑇 ≤ 𝑆) → 𝐹 ∈ (𝐺 EdgWalks 𝑇)) | ||
Theorem | upgrewlkle2 40808 | In a pseudograph, there is no s-walk of edges of length greater than 1 with s>2. (Contributed by AV, 4-Jan-2021.) |
⊢ ((𝐺 ∈ UPGraph ∧ 𝐹 ∈ (𝐺 EdgWalks 𝑆) ∧ 1 < (#‘𝐹)) → 𝑆 ≤ 2) | ||
Theorem | 1wlkslem1 40809 | Lemma 1 for 1-walks to substitute the index of the condition for vertices and edges in a 1-walk. (Contributed by AV, 23-Apr-2021.) |
⊢ (𝐴 = 𝐵 → (if-((𝑃‘𝐴) = (𝑃‘(𝐴 + 1)), (𝐼‘(𝐹‘𝐴)) = {(𝑃‘𝐴)}, {(𝑃‘𝐴), (𝑃‘(𝐴 + 1))} ⊆ (𝐼‘(𝐹‘𝐴))) ↔ if-((𝑃‘𝐵) = (𝑃‘(𝐵 + 1)), (𝐼‘(𝐹‘𝐵)) = {(𝑃‘𝐵)}, {(𝑃‘𝐵), (𝑃‘(𝐵 + 1))} ⊆ (𝐼‘(𝐹‘𝐵))))) | ||
Theorem | 1wlkslem2 40810 | Lemma 2 for 1-walks to substitute the index of the condition for vertices and edges in a 1-walk. (Contributed by AV, 23-Apr-2021.) |
⊢ ((𝐴 = 𝐵 ∧ (𝐴 + 1) = 𝐶) → (if-((𝑃‘𝐴) = (𝑃‘(𝐴 + 1)), (𝐼‘(𝐹‘𝐴)) = {(𝑃‘𝐴)}, {(𝑃‘𝐴), (𝑃‘(𝐴 + 1))} ⊆ (𝐼‘(𝐹‘𝐴))) ↔ if-((𝑃‘𝐵) = (𝑃‘𝐶), (𝐼‘(𝐹‘𝐵)) = {(𝑃‘𝐵)}, {(𝑃‘𝐵), (𝑃‘𝐶)} ⊆ (𝐼‘(𝐹‘𝐵))))) | ||
Theorem | 1wlksfval 40811* | The set of 1-walks (in an undirected graph). (Contributed by AV, 30-Dec-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) ⇒ ⊢ (𝐺 ∈ 𝑊 → (1Walks‘𝐺) = {〈𝑓, 𝑝〉 ∣ (𝑓 ∈ Word dom 𝐼 ∧ 𝑝:(0...(#‘𝑓))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝑓))if-((𝑝‘𝑘) = (𝑝‘(𝑘 + 1)), (𝐼‘(𝑓‘𝑘)) = {(𝑝‘𝑘)}, {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))} ⊆ (𝐼‘(𝑓‘𝑘))))}) | ||
Theorem | wlksfval 40812* | The set of walks (in an undirected graph). (Contributed by Alexander van der Vekens, 19-Oct-2017.) (Revised by AV, 28-Dec-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) ⇒ ⊢ (𝐺 ∈ 𝑊 → (UPWalks‘𝐺) = {〈𝑓, 𝑝〉 ∣ (𝑓 ∈ Word dom 𝐼 ∧ 𝑝:(0...(#‘𝑓))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝑓))(𝐼‘(𝑓‘𝑘)) = {(𝑝‘𝑘), (𝑝‘(𝑘 + 1))})}) | ||
Theorem | is1wlk 40813* | Properties of a pair of functions to be a 1-walk. (Contributed by AV, 30-Dec-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) ⇒ ⊢ ((𝐺 ∈ 𝑊 ∧ 𝐹 ∈ 𝑈 ∧ 𝑃 ∈ 𝑍) → (𝐹(1Walks‘𝐺)𝑃 ↔ (𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘)))))) | ||
Theorem | isWlk 40814* | Properties of a pair of functions to be a walk. (Contributed by Alexander van der Vekens, 20-Oct-2017.) (Revised by AV, 28-Dec-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) ⇒ ⊢ ((𝐺 ∈ 𝑊 ∧ 𝐹 ∈ 𝑈 ∧ 𝑃 ∈ 𝑍) → (𝐹(UPWalks‘𝐺)𝑃 ↔ (𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}))) | ||
Theorem | wlkv 40815 | The classes involved in a 1-walk are sets. (Contributed by Alexander van der Vekens, 31-Oct-2017.) (Revised by AV, 3-Feb-2021.) |
⊢ (𝐹(1Walks‘𝐺)𝑃 → (𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V)) | ||
Theorem | is1wlkg 40816* | Generalisation of is1wlk 40813: Conditions for two classes to represent a 1-walk. (Contributed by Alexander van der Vekens, 23-Jun-2018.) (Revised by AV, 1-Jan-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) ⇒ ⊢ (𝐺 ∈ 𝑊 → (𝐹(1Walks‘𝐺)𝑃 ↔ (𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘)))))) | ||
Theorem | wlkbProp 40817 | Basic properties of a walk. (Contributed by Alexander van der Vekens, 31-Oct-2017.) (Revised by AV, 29-Dec-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) ⇒ ⊢ (𝐹(UPWalks‘𝐺)𝑃 → (𝐺 ∈ V ∧ 𝐹 ∈ V ∧ 𝑃 ∈ V)) | ||
Theorem | 2m1wlk 40818 | The two mappings determining a 1-walk. (Contributed by Alexander van der Vekens, 20-Oct-2017.) (Revised by AV, 30-Dec-2020.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) ⇒ ⊢ (𝐹(1Walks‘𝐺)𝑃 → (𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉)) | ||
Theorem | 1wlkf 40819 | The mapping enumerating the (indices of the) edges of a 1-walk is a word over the indices of the edges of the graph. (Contributed by AV, 5-Apr-2021.) |
⊢ 𝐼 = (iEdg‘𝐺) ⇒ ⊢ (𝐹(1Walks‘𝐺)𝑃 → 𝐹 ∈ Word dom 𝐼) | ||
Theorem | 1wlkcl 40820 | A 1-walk has length #(𝐹), which is an integer. Formerly proven for an Eulerian path, see eupthcl 41378. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by AV, 18-Feb-2021.) |
⊢ (𝐹(1Walks‘𝐺)𝑃 → (#‘𝐹) ∈ ℕ0) | ||
Theorem | 1wlkp 40821 | The mapping enumerating the vertices of a 1-walk is a function. (Contributed by AV, 5-Apr-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝐹(1Walks‘𝐺)𝑃 → 𝑃:(0...(#‘𝐹))⟶𝑉) | ||
Theorem | 1wlkpwrd 40822 | The sequence of vertices of a 1-walk is a word over the set of vertices. (Contributed by AV, 27-Jan-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝐹(1Walks‘𝐺)𝑃 → 𝑃 ∈ Word 𝑉) | ||
Theorem | 1wlklenvp1 40823 | The number of vertices of a walk (in an undirected graph) is the number of its edges plus 1. (Contributed by Alexander van der Vekens, 29-Jun-2018.) (Revised by AV, 1-May-2021.) |
⊢ (𝐹(1Walks‘𝐺)𝑃 → (#‘𝑃) = ((#‘𝐹) + 1)) | ||
Theorem | 1wlksv 40824* | The class of 1-walks is a set. (Contributed by AV, 15-Jan-2021.) |
⊢ {〈𝑓, 𝑝〉 ∣ 𝑓(1Walks‘𝐺)𝑝} ∈ V | ||
Theorem | 1wlkn0 40825 | The sequence of vertices of a walk cannot be empty, i.e. a walk always consists of at least one vertex. (Contributed by Alexander van der Vekens, 19-Jul-2018.) (Revised by AV, 2-Jan-2021.) |
⊢ (𝐹(1Walks‘𝐺)𝑃 → 𝑃 ≠ ∅) | ||
Theorem | 1wlklenvm1 40826 | The number of edges of a walk is the number of its vertices minus 1. (Contributed by Alexander van der Vekens, 1-Jul-2018.) (Revised by AV, 2-Jan-2021.) |
⊢ (𝐹(1Walks‘𝐺)𝑃 → (#‘𝐹) = ((#‘𝑃) − 1)) | ||
Theorem | 1wlkvtxeledglem 40827 | Lemma for 1wlkvtxeledg 40828: Two adjacent vertices in a 1-walk are incident with an edge. (Contributed by AV, 4-Apr-2021.) |
⊢ (if-((𝑃‘𝐾) = (𝑃‘(𝐾 + 1)), (𝐼‘(𝐹‘𝐾)) = {(𝑃‘𝐾)}, {(𝑃‘𝐾), (𝑃‘(𝐾 + 1))} ⊆ (𝐼‘(𝐹‘𝐾))) → {(𝑃‘𝐾), (𝑃‘(𝐾 + 1))} ⊆ (𝐼‘(𝐹‘𝐾))) | ||
Theorem | 1wlkvtxeledg 40828* | Each pair of adjacent vertices in a 1-walk is a subset of an edge. (Contributed by AV, 28-Jan-2021.) (Proof shortened by AV, 4-Apr-2021.) |
⊢ 𝐼 = (iEdg‘𝐺) ⇒ ⊢ (𝐹(1Walks‘𝐺)𝑃 → ∀𝑘 ∈ (0..^(#‘𝐹)){(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘))) | ||
Theorem | 1wlkvtxiedg 40829* | The vertices of a walk are connected by indexed edges. (Contributed by Alexander van der Vekens, 22-Jul-2018.) (Revised by AV, 2-Jan-2021.) (Proof shortened by AV, 4-Apr-2021.) |
⊢ 𝐼 = (iEdg‘𝐺) ⇒ ⊢ (𝐹(1Walks‘𝐺)𝑃 → ∀𝑘 ∈ (0..^(#‘𝐹))∃𝑒 ∈ ran 𝐼{(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ 𝑒) | ||
Theorem | rel1wlk 40830 | The set (1Walks‘𝐺) of all 1-walks on 𝐺 is a set of pairs by our definition of a 1-walk, and so is a relation. (Contributed by Alexander van der Vekens, 30-Jun-2018.) (Inspired by releupa 26491 contributed by Mario Carneiro, 12-Mar-2015.) (Revised by AV, 19-Feb-2021.) |
⊢ Rel (1Walks‘𝐺) | ||
Theorem | 1wlkvv 40831 | If there is at least one walk in the graph, all walks are in the universal class of ordered pairs. (Contributed by AV, 2-Jan-2021.) |
⊢ ((1st ‘𝑊)(1Walks‘𝐺)(2nd ‘𝑊) → 𝑊 ∈ (V × V)) | ||
Theorem | 1wlkop 40832 | A walk is an ordered pair. (Contributed by Alexander van der Vekens, 30-Jun-2018.) (Revised by AV, 1-Jan-2021.) |
⊢ (𝑊 ∈ (1Walks‘𝐺) → 𝑊 = 〈(1st ‘𝑊), (2nd ‘𝑊)〉) | ||
Theorem | 1wlkcpr 40833 | A walk as class with two components. (Contributed by Alexander van der Vekens, 22-Jul-2018.) (Revised by AV, 2-Jan-2021.) |
⊢ (𝑊 ∈ (1Walks‘𝐺) ↔ (1st ‘𝑊)(1Walks‘𝐺)(2nd ‘𝑊)) | ||
Theorem | 1wlk2f 40834* | If there is a 1-walk 𝑊 there is a pair of functions representing this 1-walk. (Contributed by Alexander van der Vekens, 22-Jul-2018.) |
⊢ (𝑊 ∈ (1Walks‘𝐺) → ∃𝑓∃𝑝 𝑓(1Walks‘𝐺)𝑝) | ||
Theorem | 1wlkcomp 40835* | A walk expressed by properties of its components. (Contributed by Alexander van der Vekens, 23-Jun-2018.) (Revised by AV, 1-Jan-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ 𝐹 = (1st ‘𝑊) & ⊢ 𝑃 = (2nd ‘𝑊) ⇒ ⊢ ((𝐺 ∈ 𝑈 ∧ 𝑊 ∈ (𝑆 × 𝑇)) → (𝑊 ∈ (1Walks‘𝐺) ↔ (𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘)))))) | ||
Theorem | 1wlkcompim 40836* | Implications for the properties of the components of a walk. (Contributed by Alexander van der Vekens, 23-Jun-2018.) (Revised by AV, 2-Jan-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ 𝐹 = (1st ‘𝑊) & ⊢ 𝑃 = (2nd ‘𝑊) ⇒ ⊢ (𝑊 ∈ (1Walks‘𝐺) → (𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘))))) | ||
Theorem | 1wlkelwrd 40837 | The components of a walk are words/functions over a zero based range of integers. (Contributed by Alexander van der Vekens, 23-Jun-2018.) (Revised by AV, 2-Jan-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ 𝐹 = (1st ‘𝑊) & ⊢ 𝑃 = (2nd ‘𝑊) ⇒ ⊢ (𝑊 ∈ (1Walks‘𝐺) → (𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉)) | ||
Theorem | 1wlkeq 40838* | Conditions for two walks (within the same graph) being the same. (Contributed by AV, 1-Jul-2018.) (Revised by AV, 16-May-2019.) (Revised by AV, 14-Apr-2021.) |
⊢ ((𝐴 ∈ (1Walks‘𝐺) ∧ 𝐵 ∈ (1Walks‘𝐺) ∧ 𝑁 = (#‘(1st ‘𝐴))) → (𝐴 = 𝐵 ↔ (𝑁 = (#‘(1st ‘𝐵)) ∧ ∀𝑥 ∈ (0..^𝑁)((1st ‘𝐴)‘𝑥) = ((1st ‘𝐵)‘𝑥) ∧ ∀𝑥 ∈ (0...𝑁)((2nd ‘𝐴)‘𝑥) = ((2nd ‘𝐵)‘𝑥)))) | ||
Theorem | edginwlk 40839 | The value of the edge function for an index of an edge within a walk is an edge. (Contributed by AV, 2-Jan-2021.) |
⊢ 𝐼 = (iEdg‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ ((𝐺 ∈ 𝑊 ∧ Fun 𝐼 ∧ 𝐹 ∈ Word dom 𝐼) → (𝐾 ∈ (0..^(#‘𝐹)) → (𝐼‘(𝐹‘𝐾)) ∈ 𝐸)) | ||
Theorem | upgredginwlk 40840 | The value of the edge function for an index of an edge within a walk is an edge. (Contributed by AV, 2-Jan-2021.) |
⊢ 𝐼 = (iEdg‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ ((𝐺 ∈ UPGraph ∧ 𝐹 ∈ Word dom 𝐼) → (𝐾 ∈ (0..^(#‘𝐹)) → (𝐼‘(𝐹‘𝐾)) ∈ 𝐸)) | ||
Theorem | iedginwlk 40841 | The value of the edge function for an index of an edge within a walk is an edge. (Contributed by AV, 23-Apr-2021.) |
⊢ 𝐼 = (iEdg‘𝐺) ⇒ ⊢ ((Fun 𝐼 ∧ 𝐹(1Walks‘𝐺)𝑃 ∧ 𝑋 ∈ (0..^(#‘𝐹))) → (𝐼‘(𝐹‘𝑋)) ∈ ran 𝐼) | ||
Theorem | 1wlkl1loop 40842 | A 1-walk of length 1 from a vertex to itself is a loop. (Contributed by AV, 23-Apr-2021.) |
⊢ (((Fun (iEdg‘𝐺) ∧ 𝐹(1Walks‘𝐺)𝑃) ∧ ((#‘𝐹) = 1 ∧ (𝑃‘0) = (𝑃‘1))) → {(𝑃‘0)} ∈ (Edg‘𝐺)) | ||
Theorem | 1wlk1walk 40843* | A 1-walk is a 1-walk "on the edge level" according to Aksoy et al. (Contributed by AV, 30-Dec-2020.) |
⊢ 𝐼 = (iEdg‘𝐺) ⇒ ⊢ (𝐹(1Walks‘𝐺)𝑃 → ∀𝑘 ∈ (1..^(#‘𝐹))1 ≤ (#‘((𝐼‘(𝐹‘(𝑘 − 1))) ∩ (𝐼‘(𝐹‘𝑘))))) | ||
Theorem | 1wlk1ewlk 40844 | A 1-walk is an s-walk "on the edge level" (with s=1) according to Aksoy et al. (Contributed by AV, 5-Jan-2021.) |
⊢ (𝐹(1Walks‘𝐺)𝑃 → 𝐹 ∈ (𝐺 EdgWalks 1)) | ||
Theorem | ifpprsnss 40845 | An unordered pair is a singleton or a subset of itself. This theorem is helpful to convert theorems about walks in arbitrary graphs into theorems about walks in pseudographs. (Contributed by AV, 27-Feb-2021.) |
⊢ (𝑃 = {𝐴, 𝐵} → if-(𝐴 = 𝐵, 𝑃 = {𝐴}, {𝐴, 𝐵} ⊆ 𝑃)) | ||
Theorem | wlk1wlk 40846 | A walk is a 1-walk. (Contributed by AV, 30-Dec-2020.) (Proof shortened by AV, 27-Feb-2021.) |
⊢ (𝐹(UPWalks‘𝐺)𝑃 → 𝐹(1Walks‘𝐺)𝑃) | ||
Theorem | upgr1wlkwlk 40847 | In a pseudograph, a 1-walk is a walk. (Contributed by AV, 30-Dec-2020.) (Proof shortened by AV, 2-Jan-2021.) |
⊢ ((𝐺 ∈ UPGraph ∧ 𝐹(1Walks‘𝐺)𝑃) → 𝐹(UPWalks‘𝐺)𝑃) | ||
Theorem | upgr1wlkwlkb 40848 | In a pseudograph, the definitions for a 1-walk and a walk are equivalent. (Contributed by AV, 30-Dec-2020.) |
⊢ (𝐺 ∈ UPGraph → (𝐹(1Walks‘𝐺)𝑃 ↔ 𝐹(UPWalks‘𝐺)𝑃)) | ||
Theorem | upgriswlk 40849* | Properties of a pair of functions to be a walk in a pseudograph. (Contributed by AV, 2-Jan-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) ⇒ ⊢ ((𝐺 ∈ UPGraph ∧ 𝐹 ∈ 𝑈 ∧ 𝑃 ∈ 𝑍) → (𝐹(1Walks‘𝐺)𝑃 ↔ (𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}))) | ||
Theorem | upgrwlkedg 40850* | The edges of a walk in a pseudograph join exactly the two corresponding adjacent vertices in the walk. (Contributed by AV, 27-Feb-2021.) |
⊢ 𝐼 = (iEdg‘𝐺) ⇒ ⊢ ((𝐺 ∈ UPGraph ∧ 𝐹(1Walks‘𝐺)𝑃) → ∀𝑘 ∈ (0..^(#‘𝐹))(𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))}) | ||
Theorem | upgr1wlkcompim 40851* | Implications for the properties of the components of a walk in a pseudograph. (Contributed by Alexander van der Vekens, 23-Jun-2018.) (Revised by AV, 14-Apr-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ 𝐹 = (1st ‘𝑊) & ⊢ 𝑃 = (2nd ‘𝑊) ⇒ ⊢ ((𝐺 ∈ UPGraph ∧ 𝑊 ∈ (1Walks‘𝐺)) → (𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))})) | ||
Theorem | 1wlkvtxedg 40852* | The vertices of a walk are connected by edges. (Contributed by Alexander van der Vekens, 22-Jul-2018.) (Revised by AV, 2-Jan-2021.) |
⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ (𝐹(1Walks‘𝐺)𝑃 → ∀𝑘 ∈ (0..^(#‘𝐹))∃𝑒 ∈ 𝐸 {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ 𝑒) | ||
Theorem | upgr1wlkvtxedg 40853* | The pairs of connected vertices of a walk are edges in a pseudograph. (Contributed by Alexander van der Vekens, 22-Jul-2018.) (Revised by AV, 2-Jan-2021.) |
⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ ((𝐺 ∈ UPGraph ∧ 𝐹(1Walks‘𝐺)𝑃) → ∀𝑘 ∈ (0..^(#‘𝐹)){(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸) | ||
Theorem | uspgr2wlkeq 40854* | Conditions for two walks within the same simple pseudograph being the same. It is sufficient that the vertices (in the same order) are identical. (Contributed by AV, 3-Jul-2018.) (Revised by AV, 14-Apr-2021.) |
⊢ ((𝐺 ∈ USPGraph ∧ (𝐴 ∈ (1Walks‘𝐺) ∧ 𝐵 ∈ (1Walks‘𝐺)) ∧ 𝑁 = (#‘(1st ‘𝐴))) → (𝐴 = 𝐵 ↔ (𝑁 = (#‘(1st ‘𝐵)) ∧ ∀𝑦 ∈ (0...𝑁)((2nd ‘𝐴)‘𝑦) = ((2nd ‘𝐵)‘𝑦)))) | ||
Theorem | uspgr2wlkeq2 40855 | Conditions for two walks within the same simple pseudograph to be identical. It is sufficient that the vertices (in the same order) are identical. (Contributed by Alexander van der Vekens, 25-Aug-2018.) (Revised by AV, 14-Apr-2021.) |
⊢ (((𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ0) ∧ (𝐴 ∈ (1Walks‘𝐺) ∧ (#‘(1st ‘𝐴)) = 𝑁) ∧ (𝐵 ∈ (1Walks‘𝐺) ∧ (#‘(1st ‘𝐵)) = 𝑁)) → ((2nd ‘𝐴) = (2nd ‘𝐵) → 𝐴 = 𝐵)) | ||
Theorem | uspgr2wlkeqi 40856 | Conditions for two walks within the same simple pseudograph to be identical. It is sufficient that the vertices (in the same order) are identical. (Contributed by AV, 6-May-2021.) |
⊢ ((𝐺 ∈ USPGraph ∧ (𝐴 ∈ (1Walks‘𝐺) ∧ 𝐵 ∈ (1Walks‘𝐺)) ∧ (2nd ‘𝐴) = (2nd ‘𝐵)) → 𝐴 = 𝐵) | ||
Theorem | umgr1wlknloop 40857* | In a multigraph, each walk has no loops! (Contributed by Alexander van der Vekens, 7-Nov-2017.) (Revised by AV, 3-Jan-2021.) |
⊢ ((𝐺 ∈ UMGraph ∧ 𝐹(1Walks‘𝐺)𝑃) → ∀𝑘 ∈ (0..^(#‘𝐹))(𝑃‘𝑘) ≠ (𝑃‘(𝑘 + 1))) | ||
Theorem | wlkRes 40858* | Restrictions of walks (i.e. special kinds of walks, for example paths - see pthsfval 40927) are sets. (Contributed by Alexander van der Vekens, 1-Nov-2017.) (Revised by AV, 30-Dec-2020.) (Proof shortened by AV, 15-Jan-2021.) |
⊢ (𝑓(𝑊‘𝐺)𝑝 → 𝑓(1Walks‘𝐺)𝑝) ⇒ ⊢ {〈𝑓, 𝑝〉 ∣ (𝑓(𝑊‘𝐺)𝑝 ∧ 𝜑)} ∈ V | ||
Theorem | 1wlkv0 40859 | If there is a walk in the null graph (a class without vertices), it would be the pair consisting of empty sets. (Contributed by Alexander van der Vekens, 2-Sep-2018.) (Revised by AV, 5-Mar-2021.) |
⊢ (((Vtx‘𝐺) = ∅ ∧ 𝑊 ∈ (1Walks‘𝐺)) → ((1st ‘𝑊) = ∅ ∧ (2nd ‘𝑊) = ∅)) | ||
Theorem | g01wlk0 40860 | There is no walk in a null graph (a class without vertices). (Contributed by Alexander van der Vekens, 2-Sep-2018.) (Revised by AV, 5-Mar-2021.) |
⊢ ((Vtx‘𝐺) = ∅ → (1Walks‘𝐺) = ∅) | ||
Theorem | 01wlk0 40861 | There is no walk for the empty set, i.e. in a null graph. (Contributed by Alexander van der Vekens, 2-Sep-2018.) (Revised by AV, 5-Mar-2021.) |
⊢ (1Walks‘∅) = ∅ | ||
Theorem | 1wlk0prc 40862 | There is no walk in a null graph (a class without vertices). (Contributed by Alexander van der Vekens, 2-Sep-2018.) (Revised by AV, 5-Mar-2021.) |
⊢ ((𝑆 ∉ V ∧ (Vtx‘𝑆) = (Vtx‘𝐺)) → (1Walks‘𝐺) = ∅) | ||
Theorem | 1wlklenvclwlk 40863 | The number of vertices in a walk equals the length of the walk after it is "closed" (i.e. enhanced by an edge from its last vertex to its first vertex). (Contributed by Alexander van der Vekens, 29-Jun-2018.) (Revised by AV, 2-May-2021.) |
⊢ ((𝑊 ∈ Word (Vtx‘𝐺) ∧ 1 ≤ (#‘𝑊)) → (〈𝐹, (𝑊 ++ 〈“(𝑊‘0)”〉)〉 ∈ (1Walks‘𝐺) → (#‘𝐹) = (#‘𝑊))) | ||
Theorem | wlkson 40864* | The set of walks between two vertices. (Contributed by Alexander van der Vekens, 12-Dec-2017.) (Revised by AV, 30-Dec-2020.) (Revised by AV, 22-Mar-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (𝐴(WalksOn‘𝐺)𝐵) = {〈𝑓, 𝑝〉 ∣ (𝑓(1Walks‘𝐺)𝑝 ∧ (𝑝‘0) = 𝐴 ∧ (𝑝‘(#‘𝑓)) = 𝐵)}) | ||
Theorem | iswlkOn 40865 | Properties of a pair of functions to be a walk between two given vertices (in an undirected graph). (Contributed by Alexander van der Vekens, 2-Nov-2017.) (Revised by AV, 31-Dec-2020.) (Revised by AV, 22-Mar-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐹 ∈ 𝑈 ∧ 𝑃 ∈ 𝑍)) → (𝐹(𝐴(WalksOn‘𝐺)𝐵)𝑃 ↔ (𝐹(1Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵))) | ||
Theorem | wlkOnprop 40866 | Properties of a walk between two vertices. (Contributed by Alexander van der Vekens, 12-Dec-2017.) (Revised by AV, 31-Dec-2020.) (Proof shortened by AV, 16-Jan-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝐹(𝐴(WalksOn‘𝐺)𝐵)𝑃 → ((𝐺 ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐹(1Walks‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(#‘𝐹)) = 𝐵))) | ||
Theorem | 1wlkpvtx 40867 | A 1-walk connects vertices. (Contributed by AV, 22-Feb-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝐹(1Walks‘𝐺)𝑃 → (𝑁 ∈ (0...(#‘𝐹)) → (𝑃‘𝑁) ∈ 𝑉)) | ||
Theorem | 1wlkepvtx 40868 | The endpoints of a walk are vertices. (Contributed by AV, 31-Jan-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝐹(1Walks‘𝐺)𝑃 → ((𝑃‘0) ∈ 𝑉 ∧ (𝑃‘(#‘𝐹)) ∈ 𝑉)) | ||
Theorem | wlkOniswlk 40869 | A walk between two vertices is a walk. (Contributed by Alexander van der Vekens, 12-Dec-2017.) (Revised by AV, 2-Jan-2021.) |
⊢ (𝐹(𝐴(WalksOn‘𝐺)𝐵)𝑃 → 𝐹(1Walks‘𝐺)𝑃) | ||
Theorem | wlkOnwlk 40870 | A walk is a walk between its endpoints. (Contributed by Alexander van der Vekens, 2-Nov-2017.) (Revised by AV, 2-Jan-2021.) (Proof shortened by AV, 31-Jan-2021.) |
⊢ (𝐹(1Walks‘𝐺)𝑃 → 𝐹((𝑃‘0)(WalksOn‘𝐺)(𝑃‘(#‘𝐹)))𝑃) | ||
Theorem | wlkOnwlk1l 40871 | A walk is a walk from its first vertex to its last vertex. (Contributed by AV, 7-Feb-2021.) (Revised by AV, 22-Mar-2021.) |
⊢ (𝜑 → 𝐹(1Walks‘𝐺)𝑃) ⇒ ⊢ (𝜑 → 𝐹((𝑃‘0)(WalksOn‘𝐺)( lastS ‘𝑃))𝑃) | ||
Theorem | wlksoneq1eq2 40872 | Two walks with identical sequences of vertices start and end at the same vertices. (Contributed by AV, 14-May-2021.) |
⊢ ((𝐹(𝐴(WalksOn‘𝐺)𝐵)𝑃 ∧ 𝐻(𝐶(WalksOn‘𝐺)𝐷)𝑃) → (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)) | ||
Theorem | wlkOnl1iedg 40873* | If there is a walk between two vertices 𝐴 and 𝐵 at least of length 1, then the start vertex 𝐴 is incident with an edge. (Contributed by AV, 4-Apr-2021.) |
⊢ 𝐼 = (iEdg‘𝐺) ⇒ ⊢ ((𝐹(𝐴(WalksOn‘𝐺)𝐵)𝑃 ∧ (#‘𝐹) ≠ 0) → ∃𝑒 ∈ ran 𝐼 𝐴 ∈ 𝑒) | ||
Theorem | wlkOn2n0 40874 | The length of a walk between two different vertices is not 0 (i.e. is at least 1). (Contributed by AV, 3-Apr-2021.) |
⊢ ((𝐹(𝐴(WalksOn‘𝐺)𝐵)𝑃 ∧ 𝐴 ≠ 𝐵) → (#‘𝐹) ≠ 0) | ||
Theorem | 2Wlklem 40875* | Lemma for upgr2wlk 40876 and 2wlklemA 26084. Identical with is2wlk 26095. (Contributed by Alexander van der Vekens, 1-Feb-2018.) |
⊢ (∀𝑘 ∈ {0, 1} (𝐸‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ↔ ((𝐸‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐸‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)})) | ||
Theorem | upgr2wlk 40876 | Properties of a pair of functions to be a walk of length 2 in a pseudograph. Note that the vertices need not to be distinct and the edges can be loops or multiedges. (Contributed by Alexander van der Vekens, 16-Feb-2018.) (Revised by AV, 3-Jan-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) ⇒ ⊢ ((𝐺 ∈ UPGraph ∧ (𝐹 ∈ 𝑊 ∧ 𝑃 ∈ 𝑍)) → ((𝐹(1Walks‘𝐺)𝑃 ∧ (#‘𝐹) = 2) ↔ (𝐹:(0..^2)⟶dom 𝐼 ∧ 𝑃:(0...2)⟶𝑉 ∧ ((𝐼‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐼‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)})))) | ||
Theorem | 1wlkreslem0 40877 | Lemma for 1wlkres 40879. TODO-AV: Will become obsolete if 𝐻 = (𝐹 ↾ (0..^𝑁)) is replaced by 𝐻 = (𝐹 substr 〈0, 𝑁〉) or 𝐻 = (𝐹 prefix 𝑁) in 1wlkres 40879 and trlres 40908. (Contributed by AV, 5-Mar-2021.) |
⊢ ((𝐹 ∈ Word 𝑆 ∧ 𝑁 ∈ (0...(#‘𝐹))) → (#‘(𝐹 ↾ (0..^𝑁))) = 𝑁) | ||
Theorem | 1wlkreslem 40878 | Lemma for 1wlkres 40879. (Contributed by AV, 5-Mar-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ (𝜑 → 𝐹(1Walks‘𝐺)𝑃) & ⊢ (𝜑 → 𝑁 ∈ (0..^(#‘𝐹))) & ⊢ (𝜑 → (Vtx‘𝑆) = 𝑉) & ⊢ (𝜑 → (iEdg‘𝑆) = (𝐼 ↾ (𝐹 “ (0..^𝑁)))) & ⊢ 𝐻 = (𝐹 ↾ (0..^𝑁)) & ⊢ 𝑄 = (𝑃 ↾ (0...𝑁)) ⇒ ⊢ (𝜑 → (𝑆 ∈ V ∧ 𝐻 ∈ V ∧ 𝑄 ∈ V)) | ||
Theorem | 1wlkres 40879 | The restriction 〈𝐻, 𝑄〉 of a 1-walk 〈𝐹, 𝑃〉 to an initial segment of the 1-walk (of length 𝑁) forms a 1-walk on the subgraph 𝑆 consisting of the edges in the initial segment. Formerly proven directly for Eulerian paths, see eupthres 41383. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Mario Carneiro, 3-May-2015.) (Revised by AV, 5-Mar-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ (𝜑 → 𝐹(1Walks‘𝐺)𝑃) & ⊢ (𝜑 → 𝑁 ∈ (0..^(#‘𝐹))) & ⊢ (𝜑 → (Vtx‘𝑆) = 𝑉) & ⊢ (𝜑 → (iEdg‘𝑆) = (𝐼 ↾ (𝐹 “ (0..^𝑁)))) & ⊢ 𝐻 = (𝐹 ↾ (0..^𝑁)) & ⊢ 𝑄 = (𝑃 ↾ (0...𝑁)) ⇒ ⊢ (𝜑 → 𝐻(1Walks‘𝑆)𝑄) | ||
Theorem | red1wlklem 40880 | Lemma for red1wlk 40881. (Contributed by Alexander van der Vekens, 1-Nov-2017.) (Revised by AV, 29-Jan-2021.) |
⊢ ((𝐹 ∈ Word 𝑆 ∧ 1 ≤ (#‘𝐹) ∧ 𝑃:(0...(#‘𝐹))⟶𝑉) → (𝑃 ↾ (0..^(#‘𝐹))):(0...(#‘(𝐹 ↾ (0..^((#‘𝐹) − 1)))))⟶𝑉) | ||
Theorem | red1wlk 40881 | A 1-walk ending at the last but one vertex of the walk is a 1-walk. (Contributed by Alexander van der Vekens, 1-Nov-2017.) (Revised by AV, 29-Jan-2021.) |
⊢ ((𝐹(1Walks‘𝐺)𝑃 ∧ 1 ≤ (#‘𝐹)) → (𝐹 ↾ (0..^((#‘𝐹) − 1)))(1Walks‘𝐺)(𝑃 ↾ (0..^(#‘𝐹)))) | ||
Theorem | 1wlkp1lem1 40882 | Lemma for 1wlkp1 40890. (Contributed by AV, 6-Mar-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ (𝜑 → Fun 𝐼) & ⊢ (𝜑 → 𝐼 ∈ Fin) & ⊢ (𝜑 → 𝐵 ∈ V) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → ¬ 𝐵 ∈ dom 𝐼) & ⊢ (𝜑 → 𝐹(1Walks‘𝐺)𝑃) & ⊢ 𝑁 = (#‘𝐹) ⇒ ⊢ (𝜑 → ¬ (𝑁 + 1) ∈ dom 𝑃) | ||
Theorem | 1wlkp1lem2 40883 | Lemma for 1wlkp1 40890. (Contributed by AV, 6-Mar-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ (𝜑 → Fun 𝐼) & ⊢ (𝜑 → 𝐼 ∈ Fin) & ⊢ (𝜑 → 𝐵 ∈ V) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → ¬ 𝐵 ∈ dom 𝐼) & ⊢ (𝜑 → 𝐹(1Walks‘𝐺)𝑃) & ⊢ 𝑁 = (#‘𝐹) & ⊢ (𝜑 → 𝐸 ∈ (Edg‘𝐺)) & ⊢ (𝜑 → {(𝑃‘𝑁), 𝐶} ⊆ 𝐸) & ⊢ (𝜑 → (iEdg‘𝑆) = (𝐼 ∪ {〈𝐵, 𝐸〉})) & ⊢ 𝐻 = (𝐹 ∪ {〈𝑁, 𝐵〉}) ⇒ ⊢ (𝜑 → (#‘𝐻) = (𝑁 + 1)) | ||
Theorem | 1wlkp1lem3 40884 | Lemma for 1wlkp1 40890. (Contributed by AV, 6-Mar-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ (𝜑 → Fun 𝐼) & ⊢ (𝜑 → 𝐼 ∈ Fin) & ⊢ (𝜑 → 𝐵 ∈ V) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → ¬ 𝐵 ∈ dom 𝐼) & ⊢ (𝜑 → 𝐹(1Walks‘𝐺)𝑃) & ⊢ 𝑁 = (#‘𝐹) & ⊢ (𝜑 → 𝐸 ∈ (Edg‘𝐺)) & ⊢ (𝜑 → {(𝑃‘𝑁), 𝐶} ⊆ 𝐸) & ⊢ (𝜑 → (iEdg‘𝑆) = (𝐼 ∪ {〈𝐵, 𝐸〉})) & ⊢ 𝐻 = (𝐹 ∪ {〈𝑁, 𝐵〉}) ⇒ ⊢ (𝜑 → ((iEdg‘𝑆)‘(𝐻‘𝑁)) = ((𝐼 ∪ {〈𝐵, 𝐸〉})‘𝐵)) | ||
Theorem | 1wlkp1lem4 40885 | Lemma for 1wlkp1 40890. (Contributed by AV, 6-Mar-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ (𝜑 → Fun 𝐼) & ⊢ (𝜑 → 𝐼 ∈ Fin) & ⊢ (𝜑 → 𝐵 ∈ V) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → ¬ 𝐵 ∈ dom 𝐼) & ⊢ (𝜑 → 𝐹(1Walks‘𝐺)𝑃) & ⊢ 𝑁 = (#‘𝐹) & ⊢ (𝜑 → 𝐸 ∈ (Edg‘𝐺)) & ⊢ (𝜑 → {(𝑃‘𝑁), 𝐶} ⊆ 𝐸) & ⊢ (𝜑 → (iEdg‘𝑆) = (𝐼 ∪ {〈𝐵, 𝐸〉})) & ⊢ 𝐻 = (𝐹 ∪ {〈𝑁, 𝐵〉}) & ⊢ 𝑄 = (𝑃 ∪ {〈(𝑁 + 1), 𝐶〉}) & ⊢ (𝜑 → (Vtx‘𝑆) = 𝑉) ⇒ ⊢ (𝜑 → (𝑆 ∈ V ∧ 𝐻 ∈ V ∧ 𝑄 ∈ V)) | ||
Theorem | 1wlkp1lem5 40886* | Lemma for 1wlkp1 40890. (Contributed by AV, 6-Mar-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ (𝜑 → Fun 𝐼) & ⊢ (𝜑 → 𝐼 ∈ Fin) & ⊢ (𝜑 → 𝐵 ∈ V) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → ¬ 𝐵 ∈ dom 𝐼) & ⊢ (𝜑 → 𝐹(1Walks‘𝐺)𝑃) & ⊢ 𝑁 = (#‘𝐹) & ⊢ (𝜑 → 𝐸 ∈ (Edg‘𝐺)) & ⊢ (𝜑 → {(𝑃‘𝑁), 𝐶} ⊆ 𝐸) & ⊢ (𝜑 → (iEdg‘𝑆) = (𝐼 ∪ {〈𝐵, 𝐸〉})) & ⊢ 𝐻 = (𝐹 ∪ {〈𝑁, 𝐵〉}) & ⊢ 𝑄 = (𝑃 ∪ {〈(𝑁 + 1), 𝐶〉}) & ⊢ (𝜑 → (Vtx‘𝑆) = 𝑉) ⇒ ⊢ (𝜑 → ∀𝑘 ∈ (0...𝑁)(𝑄‘𝑘) = (𝑃‘𝑘)) | ||
Theorem | 1wlkp1lem6 40887* | Lemma for 1wlkp1 40890. (Contributed by AV, 6-Mar-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ (𝜑 → Fun 𝐼) & ⊢ (𝜑 → 𝐼 ∈ Fin) & ⊢ (𝜑 → 𝐵 ∈ V) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → ¬ 𝐵 ∈ dom 𝐼) & ⊢ (𝜑 → 𝐹(1Walks‘𝐺)𝑃) & ⊢ 𝑁 = (#‘𝐹) & ⊢ (𝜑 → 𝐸 ∈ (Edg‘𝐺)) & ⊢ (𝜑 → {(𝑃‘𝑁), 𝐶} ⊆ 𝐸) & ⊢ (𝜑 → (iEdg‘𝑆) = (𝐼 ∪ {〈𝐵, 𝐸〉})) & ⊢ 𝐻 = (𝐹 ∪ {〈𝑁, 𝐵〉}) & ⊢ 𝑄 = (𝑃 ∪ {〈(𝑁 + 1), 𝐶〉}) & ⊢ (𝜑 → (Vtx‘𝑆) = 𝑉) ⇒ ⊢ (𝜑 → ∀𝑘 ∈ (0..^𝑁)((𝑄‘𝑘) = (𝑃‘𝑘) ∧ (𝑄‘(𝑘 + 1)) = (𝑃‘(𝑘 + 1)) ∧ ((iEdg‘𝑆)‘(𝐻‘𝑘)) = (𝐼‘(𝐹‘𝑘)))) | ||
Theorem | 1wlkp1lem7 40888 | Lemma for 1wlkp1 40890. (Contributed by AV, 6-Mar-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ (𝜑 → Fun 𝐼) & ⊢ (𝜑 → 𝐼 ∈ Fin) & ⊢ (𝜑 → 𝐵 ∈ V) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → ¬ 𝐵 ∈ dom 𝐼) & ⊢ (𝜑 → 𝐹(1Walks‘𝐺)𝑃) & ⊢ 𝑁 = (#‘𝐹) & ⊢ (𝜑 → 𝐸 ∈ (Edg‘𝐺)) & ⊢ (𝜑 → {(𝑃‘𝑁), 𝐶} ⊆ 𝐸) & ⊢ (𝜑 → (iEdg‘𝑆) = (𝐼 ∪ {〈𝐵, 𝐸〉})) & ⊢ 𝐻 = (𝐹 ∪ {〈𝑁, 𝐵〉}) & ⊢ 𝑄 = (𝑃 ∪ {〈(𝑁 + 1), 𝐶〉}) & ⊢ (𝜑 → (Vtx‘𝑆) = 𝑉) ⇒ ⊢ (𝜑 → {(𝑄‘𝑁), (𝑄‘(𝑁 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻‘𝑁))) | ||
Theorem | 1wlkp1lem8 40889* | Lemma for 1wlkp1 40890. (Contributed by AV, 6-Mar-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ (𝜑 → Fun 𝐼) & ⊢ (𝜑 → 𝐼 ∈ Fin) & ⊢ (𝜑 → 𝐵 ∈ V) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → ¬ 𝐵 ∈ dom 𝐼) & ⊢ (𝜑 → 𝐹(1Walks‘𝐺)𝑃) & ⊢ 𝑁 = (#‘𝐹) & ⊢ (𝜑 → 𝐸 ∈ (Edg‘𝐺)) & ⊢ (𝜑 → {(𝑃‘𝑁), 𝐶} ⊆ 𝐸) & ⊢ (𝜑 → (iEdg‘𝑆) = (𝐼 ∪ {〈𝐵, 𝐸〉})) & ⊢ 𝐻 = (𝐹 ∪ {〈𝑁, 𝐵〉}) & ⊢ 𝑄 = (𝑃 ∪ {〈(𝑁 + 1), 𝐶〉}) & ⊢ (𝜑 → (Vtx‘𝑆) = 𝑉) & ⊢ ((𝜑 ∧ 𝐶 = (𝑃‘𝑁)) → 𝐸 = {𝐶}) ⇒ ⊢ (𝜑 → ∀𝑘 ∈ (0..^(#‘𝐻))if-((𝑄‘𝑘) = (𝑄‘(𝑘 + 1)), ((iEdg‘𝑆)‘(𝐻‘𝑘)) = {(𝑄‘𝑘)}, {(𝑄‘𝑘), (𝑄‘(𝑘 + 1))} ⊆ ((iEdg‘𝑆)‘(𝐻‘𝑘)))) | ||
Theorem | 1wlkp1 40890 | Append one path segment (edge) 𝐸 from vertex (𝑃‘𝑁) to a vertex 𝐶 to a 1-walk 〈𝐹, 𝑃〉 to become a 1-walk 〈𝐻, 𝑄〉 of the supergraph 𝑆 obtained by adding the new edge to the graph 𝐺. Formerly proven directly for Eulerian paths (for pseudographs), see eupthp1 41384. (Contributed by Mario Carneiro, 7-Apr-2015.) (Revised by AV, 6-Mar-2021.) (Prove shortened by AV, 18-Apr-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ (𝜑 → Fun 𝐼) & ⊢ (𝜑 → 𝐼 ∈ Fin) & ⊢ (𝜑 → 𝐵 ∈ V) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → ¬ 𝐵 ∈ dom 𝐼) & ⊢ (𝜑 → 𝐹(1Walks‘𝐺)𝑃) & ⊢ 𝑁 = (#‘𝐹) & ⊢ (𝜑 → 𝐸 ∈ (Edg‘𝐺)) & ⊢ (𝜑 → {(𝑃‘𝑁), 𝐶} ⊆ 𝐸) & ⊢ (𝜑 → (iEdg‘𝑆) = (𝐼 ∪ {〈𝐵, 𝐸〉})) & ⊢ 𝐻 = (𝐹 ∪ {〈𝑁, 𝐵〉}) & ⊢ 𝑄 = (𝑃 ∪ {〈(𝑁 + 1), 𝐶〉}) & ⊢ (𝜑 → (Vtx‘𝑆) = 𝑉) & ⊢ ((𝜑 ∧ 𝐶 = (𝑃‘𝑁)) → 𝐸 = {𝐶}) ⇒ ⊢ (𝜑 → 𝐻(1Walks‘𝑆)𝑄) | ||
Theorem | 1wlkdlem1 40891* | Lemma 1 for 1wlkd 40895. (Contributed by AV, 7-Feb-2021.) |
⊢ (𝜑 → 𝑃 ∈ Word V) & ⊢ (𝜑 → 𝐹 ∈ Word V) & ⊢ (𝜑 → (#‘𝑃) = ((#‘𝐹) + 1)) & ⊢ (𝜑 → ∀𝑘 ∈ (0...(#‘𝐹))(𝑃‘𝑘) ∈ 𝑉) ⇒ ⊢ (𝜑 → 𝑃:(0...(#‘𝐹))⟶𝑉) | ||
Theorem | 1wlkdlem2 40892* | Lemma 2 for 1wlkd 40895. (Contributed by AV, 7-Feb-2021.) |
⊢ (𝜑 → 𝑃 ∈ Word V) & ⊢ (𝜑 → 𝐹 ∈ Word V) & ⊢ (𝜑 → (#‘𝑃) = ((#‘𝐹) + 1)) & ⊢ (𝜑 → ∀𝑘 ∈ (0..^(#‘𝐹)){(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘))) ⇒ ⊢ (𝜑 → (((#‘𝐹) ∈ ℕ → (𝑃‘(#‘𝐹)) ∈ (𝐼‘(𝐹‘((#‘𝐹) − 1)))) ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝑃‘𝑘) ∈ (𝐼‘(𝐹‘𝑘)))) | ||
Theorem | 1wlkdlem3 40893* | Lemma 3 for 1wlkd 40895. (Contributed by Alexander van der Vekens, 10-Nov-2017.) (Revised by AV, 7-Feb-2021.) |
⊢ (𝜑 → 𝑃 ∈ Word V) & ⊢ (𝜑 → 𝐹 ∈ Word V) & ⊢ (𝜑 → (#‘𝑃) = ((#‘𝐹) + 1)) & ⊢ (𝜑 → ∀𝑘 ∈ (0..^(#‘𝐹)){(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘))) ⇒ ⊢ (𝜑 → 𝐹 ∈ Word dom 𝐼) | ||
Theorem | 1wlkdlem4 40894* | Lemma 4 for 1wlkd 40895. (Contributed by Alexander van der Vekens, 1-Feb-2018.) (Revised by AV, 23-Jan-2021.) |
⊢ (𝜑 → 𝑃 ∈ Word V) & ⊢ (𝜑 → 𝐹 ∈ Word V) & ⊢ (𝜑 → (#‘𝑃) = ((#‘𝐹) + 1)) & ⊢ (𝜑 → ∀𝑘 ∈ (0..^(#‘𝐹)){(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘))) & ⊢ (𝜑 → ∀𝑘 ∈ (0..^(#‘𝐹))(𝑃‘𝑘) ≠ (𝑃‘(𝑘 + 1))) ⇒ ⊢ (𝜑 → ∀𝑘 ∈ (0..^(#‘𝐹))if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘)))) | ||
Theorem | 1wlkd 40895* | Two words representing a walk in a graph. (Contributed by AV, 7-Feb-2021.) |
⊢ (𝜑 → 𝑃 ∈ Word V) & ⊢ (𝜑 → 𝐹 ∈ Word V) & ⊢ (𝜑 → (#‘𝑃) = ((#‘𝐹) + 1)) & ⊢ (𝜑 → ∀𝑘 ∈ (0..^(#‘𝐹)){(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘))) & ⊢ (𝜑 → ∀𝑘 ∈ (0..^(#‘𝐹))(𝑃‘𝑘) ≠ (𝑃‘(𝑘 + 1))) & ⊢ (𝜑 → 𝐺 ∈ 𝑊) & ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ (𝜑 → ∀𝑘 ∈ (0...(#‘𝐹))(𝑃‘𝑘) ∈ 𝑉) ⇒ ⊢ (𝜑 → 𝐹(1Walks‘𝐺)𝑃) | ||
Theorem | lfgrwlkprop 40896* | Two adjacent vertices in a 1-walk are different in a loop-free graph. (Contributed by AV, 28-Jan-2021.) |
⊢ 𝐼 = (iEdg‘𝐺) ⇒ ⊢ ((𝐹(1Walks‘𝐺)𝑃 ∧ 𝐼:dom 𝐼⟶{𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ (#‘𝑥)}) → ∀𝑘 ∈ (0..^(#‘𝐹))(𝑃‘𝑘) ≠ (𝑃‘(𝑘 + 1))) | ||
Theorem | lfgriswlk 40897* | Conditions for a pair of functions to be a 1-walk in a loop-free graph. (Contributed by AV, 28-Jan-2021.) |
⊢ 𝐼 = (iEdg‘𝐺) & ⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ ((𝐺 ∈ 𝑊 ∧ 𝐼:dom 𝐼⟶{𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ (#‘𝑥)}) → (𝐹(1Walks‘𝐺)𝑃 ↔ (𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))((𝑃‘𝑘) ≠ (𝑃‘(𝑘 + 1)) ∧ {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘)))))) | ||
Theorem | lfgr1wlknloop 40898* | In a loop-free graph, each walk has no loops! (Contributed by AV, 2-Feb-2021.) |
⊢ 𝐼 = (iEdg‘𝐺) & ⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ ((𝐼:dom 𝐼⟶{𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ (#‘𝑥)} ∧ 𝐹(1Walks‘𝐺)𝑃) → ∀𝑘 ∈ (0..^(#‘𝐹))(𝑃‘𝑘) ≠ (𝑃‘(𝑘 + 1))) | ||
Syntax | ctrls 40899 | Extend class notation with trails (within a graph). |
class TrailS | ||
Syntax | ctrlson 40900 | Extend class notation with tails between two vertices (within a graph). |
class TrailsOn |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |