Home | Metamath
Proof Explorer Theorem List (p. 411 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 | ||
Theorem | crctisTrl 41001 | A circuit is a trail. (Contributed by Alexander van der Vekens, 30-Oct-2017.) (Revised by AV, 31-Jan-2021.) |
⊢ (𝐹(CircuitS‘𝐺)𝑃 → 𝐹(TrailS‘𝐺)𝑃) | ||
Theorem | crctis1wlk 41002 | A circuit is a walk. (Contributed by AV, 6-Apr-2021.) |
⊢ (𝐹(CircuitS‘𝐺)𝑃 → 𝐹(1Walks‘𝐺)𝑃) | ||
Theorem | cyclisPth 41003 | A cycle is a path. (Contributed by Alexander van der Vekens, 30-Oct-2017.) (Revised by AV, 31-Jan-2021.) |
⊢ (𝐹(CycleS‘𝐺)𝑃 → 𝐹(PathS‘𝐺)𝑃) | ||
Theorem | cyclisWlk 41004 | A cycle is a walk. (Contributed by Alexander van der Vekens, 7-Nov-2017.) (Revised by AV, 31-Jan-2021.) |
⊢ (𝐹(CycleS‘𝐺)𝑃 → 𝐹(1Walks‘𝐺)𝑃) | ||
Theorem | cyclisCrct 41005 | A cycle is a circuit. (Contributed by Alexander van der Vekens, 30-Oct-2017.) (Revised by AV, 31-Jan-2021.) |
⊢ (𝐹(CycleS‘𝐺)𝑃 → 𝐹(CircuitS‘𝐺)𝑃) | ||
Theorem | cyclnsPth 41006 | A (non trivial) cycle is not a simple path. (Contributed by Alexander van der Vekens, 30-Oct-2017.) (Revised by AV, 31-Jan-2021.) |
⊢ (𝐹 ≠ ∅ → (𝐹(CycleS‘𝐺)𝑃 → ¬ 𝐹(SPathS‘𝐺)𝑃)) | ||
Theorem | cyclisPthon 41007 | A cycle is a path starting and ending at its first vertex. (Contributed by Alexander van der Vekens, 8-Nov-2017.) (Revised by AV, 31-Jan-2021.) |
⊢ (𝐹(CycleS‘𝐺)𝑃 → 𝐹((𝑃‘0)(PathsOn‘𝐺)(𝑃‘0))𝑃) | ||
Theorem | lfgrn1cycl 41008* | In a loop-free graph there are no cycles with length 1 (consisting of one edge). (Contributed by Alexander van der Vekens, 7-Nov-2017.) (Revised by AV, 2-Feb-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) ⇒ ⊢ (𝐼:dom 𝐼⟶{𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ (#‘𝑥)} → (𝐹(CycleS‘𝐺)𝑃 → (#‘𝐹) ≠ 1)) | ||
Theorem | usgr2trlncrct 41009 | In a simple graph, any trail of length 2 is not a circuit. (Contributed by AV, 5-Jun-2021.) |
⊢ ((𝐺 ∈ USGraph ∧ (#‘𝐹) = 2) → (𝐹(TrailS‘𝐺)𝑃 → ¬ 𝐹(CircuitS‘𝐺)𝑃)) | ||
Theorem | umgrn1cycl 41010 | In a multigraph graph (with no loops!) there are no cycles with length 1 (consisting of one edge). (Contributed by Alexander van der Vekens, 7-Nov-2017.) (Revised by AV, 2-Feb-2021.) |
⊢ ((𝐺 ∈ UMGraph ∧ 𝐹(CycleS‘𝐺)𝑃) → (#‘𝐹) ≠ 1) | ||
Theorem | uspgrn2crct 41011 | In a simple pseudograph there are no circuits with length 2 (consisting of two edges). (Contributed by Alexander van der Vekens, 9-Nov-2017.) (Revised by AV, 3-Feb-2021.) |
⊢ ((𝐺 ∈ USPGraph ∧ 𝐹(CircuitS‘𝐺)𝑃) → (#‘𝐹) ≠ 2) | ||
Theorem | usgrn2cycl 41012 | In a simple graph there are no cycles with length 2 (consisting of two edges). (Contributed by Alexander van der Vekens, 9-Nov-2017.) (Revised by AV, 4-Feb-2021.) |
⊢ ((𝐺 ∈ USGraph ∧ 𝐹(CycleS‘𝐺)𝑃) → (#‘𝐹) ≠ 2) | ||
Theorem | crctcsh1wlkn0lem1 41013 | Lemma for crctcsh1wlkn0 41024. (Contributed by AV, 13-Mar-2021.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℕ) → ((𝐴 − 𝐵) + 1) ≤ 𝐴) | ||
Theorem | crctcsh1wlkn0lem2 41014* | Lemma for crctcsh1wlkn0 41024. (Contributed by AV, 12-Mar-2021.) |
⊢ (𝜑 → 𝑆 ∈ (1..^𝑁)) & ⊢ 𝑄 = (𝑥 ∈ (0...𝑁) ↦ if(𝑥 ≤ (𝑁 − 𝑆), (𝑃‘(𝑥 + 𝑆)), (𝑃‘((𝑥 + 𝑆) − 𝑁)))) ⇒ ⊢ ((𝜑 ∧ 𝐽 ∈ (0...(𝑁 − 𝑆))) → (𝑄‘𝐽) = (𝑃‘(𝐽 + 𝑆))) | ||
Theorem | crctcsh1wlkn0lem3 41015* | Lemma for crctcsh1wlkn0 41024. (Contributed by AV, 12-Mar-2021.) |
⊢ (𝜑 → 𝑆 ∈ (1..^𝑁)) & ⊢ 𝑄 = (𝑥 ∈ (0...𝑁) ↦ if(𝑥 ≤ (𝑁 − 𝑆), (𝑃‘(𝑥 + 𝑆)), (𝑃‘((𝑥 + 𝑆) − 𝑁)))) ⇒ ⊢ ((𝜑 ∧ 𝐽 ∈ (((𝑁 − 𝑆) + 1)...𝑁)) → (𝑄‘𝐽) = (𝑃‘((𝐽 + 𝑆) − 𝑁))) | ||
Theorem | crctcsh1wlkn0lem4 41016* | Lemma for crctcsh1wlkn0 41024. (Contributed by AV, 12-Mar-2021.) |
⊢ (𝜑 → 𝑆 ∈ (1..^𝑁)) & ⊢ 𝑄 = (𝑥 ∈ (0...𝑁) ↦ if(𝑥 ≤ (𝑁 − 𝑆), (𝑃‘(𝑥 + 𝑆)), (𝑃‘((𝑥 + 𝑆) − 𝑁)))) & ⊢ 𝐻 = (𝐹 cyclShift 𝑆) & ⊢ 𝑁 = (#‘𝐹) & ⊢ (𝜑 → 𝐹 ∈ Word 𝐴) & ⊢ (𝜑 → ∀𝑖 ∈ (0..^𝑁)if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖)))) ⇒ ⊢ (𝜑 → ∀𝑗 ∈ (0..^(𝑁 − 𝑆))if-((𝑄‘𝑗) = (𝑄‘(𝑗 + 1)), (𝐼‘(𝐻‘𝑗)) = {(𝑄‘𝑗)}, {(𝑄‘𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻‘𝑗)))) | ||
Theorem | crctcsh1wlkn0lem5 41017* | Lemma for crctcsh1wlkn0 41024. (Contributed by AV, 12-Mar-2021.) |
⊢ (𝜑 → 𝑆 ∈ (1..^𝑁)) & ⊢ 𝑄 = (𝑥 ∈ (0...𝑁) ↦ if(𝑥 ≤ (𝑁 − 𝑆), (𝑃‘(𝑥 + 𝑆)), (𝑃‘((𝑥 + 𝑆) − 𝑁)))) & ⊢ 𝐻 = (𝐹 cyclShift 𝑆) & ⊢ 𝑁 = (#‘𝐹) & ⊢ (𝜑 → 𝐹 ∈ Word 𝐴) & ⊢ (𝜑 → ∀𝑖 ∈ (0..^𝑁)if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖)))) ⇒ ⊢ (𝜑 → ∀𝑗 ∈ (((𝑁 − 𝑆) + 1)..^𝑁)if-((𝑄‘𝑗) = (𝑄‘(𝑗 + 1)), (𝐼‘(𝐻‘𝑗)) = {(𝑄‘𝑗)}, {(𝑄‘𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻‘𝑗)))) | ||
Theorem | crctcsh1wlkn0lem6 41018* | Lemma for crctcsh1wlkn0 41024. (Contributed by AV, 12-Mar-2021.) |
⊢ (𝜑 → 𝑆 ∈ (1..^𝑁)) & ⊢ 𝑄 = (𝑥 ∈ (0...𝑁) ↦ if(𝑥 ≤ (𝑁 − 𝑆), (𝑃‘(𝑥 + 𝑆)), (𝑃‘((𝑥 + 𝑆) − 𝑁)))) & ⊢ 𝐻 = (𝐹 cyclShift 𝑆) & ⊢ 𝑁 = (#‘𝐹) & ⊢ (𝜑 → 𝐹 ∈ Word 𝐴) & ⊢ (𝜑 → ∀𝑖 ∈ (0..^𝑁)if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖)))) & ⊢ (𝜑 → (𝑃‘𝑁) = (𝑃‘0)) ⇒ ⊢ ((𝜑 ∧ 𝐽 = (𝑁 − 𝑆)) → if-((𝑄‘𝐽) = (𝑄‘(𝐽 + 1)), (𝐼‘(𝐻‘𝐽)) = {(𝑄‘𝐽)}, {(𝑄‘𝐽), (𝑄‘(𝐽 + 1))} ⊆ (𝐼‘(𝐻‘𝐽)))) | ||
Theorem | crctcsh1wlkn0lem7 41019* | Lemma for crctcsh1wlkn0 41024. (Contributed by AV, 12-Mar-2021.) |
⊢ (𝜑 → 𝑆 ∈ (1..^𝑁)) & ⊢ 𝑄 = (𝑥 ∈ (0...𝑁) ↦ if(𝑥 ≤ (𝑁 − 𝑆), (𝑃‘(𝑥 + 𝑆)), (𝑃‘((𝑥 + 𝑆) − 𝑁)))) & ⊢ 𝐻 = (𝐹 cyclShift 𝑆) & ⊢ 𝑁 = (#‘𝐹) & ⊢ (𝜑 → 𝐹 ∈ Word 𝐴) & ⊢ (𝜑 → ∀𝑖 ∈ (0..^𝑁)if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖)))) & ⊢ (𝜑 → (𝑃‘𝑁) = (𝑃‘0)) ⇒ ⊢ (𝜑 → ∀𝑗 ∈ (0..^𝑁)if-((𝑄‘𝑗) = (𝑄‘(𝑗 + 1)), (𝐼‘(𝐻‘𝑗)) = {(𝑄‘𝑗)}, {(𝑄‘𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻‘𝑗)))) | ||
Theorem | crctcshlem1 41020 | Lemma for crctcsh 41027. (Contributed by AV, 10-Mar-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ (𝜑 → 𝐹(CircuitS‘𝐺)𝑃) & ⊢ 𝑁 = (#‘𝐹) ⇒ ⊢ (𝜑 → 𝑁 ∈ ℕ0) | ||
Theorem | crctcshlem2 41021 | Lemma for crctcsh 41027. (Contributed by AV, 10-Mar-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ (𝜑 → 𝐹(CircuitS‘𝐺)𝑃) & ⊢ 𝑁 = (#‘𝐹) & ⊢ (𝜑 → 𝑆 ∈ (0..^𝑁)) & ⊢ 𝐻 = (𝐹 cyclShift 𝑆) ⇒ ⊢ (𝜑 → (#‘𝐻) = 𝑁) | ||
Theorem | crctcshlem3 41022* | Lemma for crctcsh 41027. (Contributed by AV, 10-Mar-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ (𝜑 → 𝐹(CircuitS‘𝐺)𝑃) & ⊢ 𝑁 = (#‘𝐹) & ⊢ (𝜑 → 𝑆 ∈ (0..^𝑁)) & ⊢ 𝐻 = (𝐹 cyclShift 𝑆) & ⊢ 𝑄 = (𝑥 ∈ (0...𝑁) ↦ if(𝑥 ≤ (𝑁 − 𝑆), (𝑃‘(𝑥 + 𝑆)), (𝑃‘((𝑥 + 𝑆) − 𝑁)))) ⇒ ⊢ (𝜑 → (𝐺 ∈ V ∧ 𝐻 ∈ V ∧ 𝑄 ∈ V)) | ||
Theorem | crctcshlem4 41023* | Lemma for crctcsh 41027. (Contributed by AV, 10-Mar-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ (𝜑 → 𝐹(CircuitS‘𝐺)𝑃) & ⊢ 𝑁 = (#‘𝐹) & ⊢ (𝜑 → 𝑆 ∈ (0..^𝑁)) & ⊢ 𝐻 = (𝐹 cyclShift 𝑆) & ⊢ 𝑄 = (𝑥 ∈ (0...𝑁) ↦ if(𝑥 ≤ (𝑁 − 𝑆), (𝑃‘(𝑥 + 𝑆)), (𝑃‘((𝑥 + 𝑆) − 𝑁)))) ⇒ ⊢ ((𝜑 ∧ 𝑆 = 0) → (𝐻 = 𝐹 ∧ 𝑄 = 𝑃)) | ||
Theorem | crctcsh1wlkn0 41024* | Cyclically shifting the indices of a circuit 〈𝐹, 𝑃〉 results in a 1-walk 〈𝐻, 𝑄〉. (Contributed by AV, 10-Mar-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ (𝜑 → 𝐹(CircuitS‘𝐺)𝑃) & ⊢ 𝑁 = (#‘𝐹) & ⊢ (𝜑 → 𝑆 ∈ (0..^𝑁)) & ⊢ 𝐻 = (𝐹 cyclShift 𝑆) & ⊢ 𝑄 = (𝑥 ∈ (0...𝑁) ↦ if(𝑥 ≤ (𝑁 − 𝑆), (𝑃‘(𝑥 + 𝑆)), (𝑃‘((𝑥 + 𝑆) − 𝑁)))) ⇒ ⊢ ((𝜑 ∧ 𝑆 ≠ 0) → 𝐻(1Walks‘𝐺)𝑄) | ||
Theorem | crctcsh1wlk 41025* | Cyclically shifting the indices of a circuit 〈𝐹, 𝑃〉 results in a 1-walk 〈𝐻, 𝑄〉. (Contributed by AV, 10-Mar-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ (𝜑 → 𝐹(CircuitS‘𝐺)𝑃) & ⊢ 𝑁 = (#‘𝐹) & ⊢ (𝜑 → 𝑆 ∈ (0..^𝑁)) & ⊢ 𝐻 = (𝐹 cyclShift 𝑆) & ⊢ 𝑄 = (𝑥 ∈ (0...𝑁) ↦ if(𝑥 ≤ (𝑁 − 𝑆), (𝑃‘(𝑥 + 𝑆)), (𝑃‘((𝑥 + 𝑆) − 𝑁)))) ⇒ ⊢ (𝜑 → 𝐻(1Walks‘𝐺)𝑄) | ||
Theorem | crctcshtrl 41026* | Cyclically shifting the indices of a circuit 〈𝐹, 𝑃〉 results in a trail 〈𝐻, 𝑄〉. (Contributed by AV, 14-Mar-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ (𝜑 → 𝐹(CircuitS‘𝐺)𝑃) & ⊢ 𝑁 = (#‘𝐹) & ⊢ (𝜑 → 𝑆 ∈ (0..^𝑁)) & ⊢ 𝐻 = (𝐹 cyclShift 𝑆) & ⊢ 𝑄 = (𝑥 ∈ (0...𝑁) ↦ if(𝑥 ≤ (𝑁 − 𝑆), (𝑃‘(𝑥 + 𝑆)), (𝑃‘((𝑥 + 𝑆) − 𝑁)))) ⇒ ⊢ (𝜑 → 𝐻(TrailS‘𝐺)𝑄) | ||
Theorem | crctcsh 41027* | Cyclically shifting the indices of a circuit 〈𝐹, 𝑃〉 results in a circuit 〈𝐻, 𝑄〉. (Contributed by AV, 10-Mar-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ (𝜑 → 𝐹(CircuitS‘𝐺)𝑃) & ⊢ 𝑁 = (#‘𝐹) & ⊢ (𝜑 → 𝑆 ∈ (0..^𝑁)) & ⊢ 𝐻 = (𝐹 cyclShift 𝑆) & ⊢ 𝑄 = (𝑥 ∈ (0...𝑁) ↦ if(𝑥 ≤ (𝑁 − 𝑆), (𝑃‘(𝑥 + 𝑆)), (𝑃‘((𝑥 + 𝑆) − 𝑁)))) ⇒ ⊢ (𝜑 → 𝐻(CircuitS‘𝐺)𝑄) | ||
In general, a walk is an alternating sequence of vertices and edges, as defined in df-1wlks 40800: p(0) e(f(1)) p(1) e(f(2)) ... p(n-1) e(f(n)) p(n). Often, it is sufficient to refer to a walk by the natural sequence of its vertices, i.e omitting its edges in its representation: p(0) p(1) ... p(n-1) p(n), see the corresponding remark in [Diestel] p. 6. The concept of a Word, see df-word 13154, is the appropriate way to define such a sequence (being finite and starting at index 0) of vertices. Therefore, it is used in definitions df-wwlks 41033 and df-wwlksn 41034, and the representation of a walk as sequence of its vertices is called "walk as word". Only for simple pseudographs, however, the edges can be uniquely reconstructed from such a representation. In other cases, there could be more than one edge between two adjacent vertices in the walk (in a multigraph), or two adjacent vertices could be connected by two different hyperedges involving additional vertices (in a hypergraph). | ||
Syntax | cwwlks 41028 | Extend class notation with walks (in a graph) as word over the set of vertices. |
class WWalkS | ||
Syntax | cwwlksn 41029 | Extend class notation with walks (in a graph) of a fixed length as word over the set of vertices. |
class WWalkSN | ||
Syntax | cwwlksnon 41030 | Extend class notation with walks between two vertices (in a graph) of a fixed length as word over the set of vertices. |
class WWalksNOn | ||
Syntax | cwwspthsn 41031 | Extend class notation with simple paths (in a graph) of a fixed length as word over the set of vertices. |
class WSPathsN | ||
Syntax | cwwspthsnon 41032 | Extend class notation with simple paths between two vertices (in a graph) of a fixed length as word over the set of vertices. |
class WSPathsNOn | ||
Definition | df-wwlks 41033* | Define the set of all walks (in an undirected graph) as words over the set of vertices. Such a word corresponds to the sequence p(0) p(1) ... p(n-1) p(n) of the vertices in a walk p(0) e(f(1)) p(1) e(f(2)) ... p(n-1) e(f(n)) p(n) as defined in df-1wlks 40800. 𝑤 = ∅ has to be excluded because a walk always consists of at least one vertex, see wlkn0 26055. (Contributed by Alexander van der Vekens, 15-Jul-2018.) (Revised by AV, 8-Apr-2021.) |
⊢ WWalkS = (𝑔 ∈ V ↦ {𝑤 ∈ Word (Vtx‘𝑔) ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ (Edg‘𝑔))}) | ||
Definition | df-wwlksn 41034* | Define the set of all walks (in an undirected graph) of a fixed length n as words over the set of vertices. Such a word corresponds to the sequence p(0) p(1) ... p(n) of the vertices in a walk p(0) e(f(1)) p(1) e(f(2)) ... p(n-1) e(f(n)) p(n) as defined in df-1wlks 40800. (Contributed by Alexander van der Vekens, 15-Jul-2018.) (Revised by AV, 8-Apr-2021.) |
⊢ WWalkSN = (𝑛 ∈ ℕ0, 𝑔 ∈ V ↦ {𝑤 ∈ (WWalkS‘𝑔) ∣ (#‘𝑤) = (𝑛 + 1)}) | ||
Definition | df-wwlksnon 41035* | Define the collection of walks of a fixed length with particular endpoints as word over the set of vertices. (Contributed by Alexander van der Vekens, 15-Feb-2018.) (Revised by AV, 11-May-2021.) |
⊢ WWalksNOn = (𝑛 ∈ ℕ0, 𝑔 ∈ V ↦ (𝑎 ∈ (Vtx‘𝑔), 𝑏 ∈ (Vtx‘𝑔) ↦ {𝑤 ∈ (𝑛 WWalkSN 𝑔) ∣ ((𝑤‘0) = 𝑎 ∧ (𝑤‘𝑛) = 𝑏)})) | ||
Definition | df-wspthsn 41036* | Define the collection of simple paths of a fixed length as word over the set of vertices. (Contributed by Alexander van der Vekens, 1-Mar-2018.) (Revised by AV, 11-May-2021.) |
⊢ WSPathsN = (𝑛 ∈ ℕ0, 𝑔 ∈ V ↦ {𝑤 ∈ (𝑛 WWalkSN 𝑔) ∣ ∃𝑓 𝑓(SPathS‘𝑔)𝑤}) | ||
Definition | df-wspthsnon 41037* | Define the collection of simple paths of a fixed length with particular endpoints as word over the set of vertices. (Contributed by Alexander van der Vekens, 1-Mar-2018.) (Revised by AV, 11-May-2021.) |
⊢ WSPathsNOn = (𝑛 ∈ ℕ0, 𝑔 ∈ V ↦ (𝑎 ∈ (Vtx‘𝑔), 𝑏 ∈ (Vtx‘𝑔) ↦ {𝑤 ∈ (𝑎(𝑛 WWalksNOn 𝑔)𝑏) ∣ ∃𝑓 𝑓(𝑎(SPathsOn‘𝑔)𝑏)𝑤})) | ||
Theorem | wwlks 41038* | The set of walks (in an undirected graph) as words over the set of vertices. (Contributed by Alexander van der Vekens, 15-Jul-2018.) (Revised by AV, 8-Apr-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ (WWalkS‘𝐺) = {𝑤 ∈ Word 𝑉 ∣ (𝑤 ≠ ∅ ∧ ∀𝑖 ∈ (0..^((#‘𝑤) − 1)){(𝑤‘𝑖), (𝑤‘(𝑖 + 1))} ∈ 𝐸)} | ||
Theorem | iswwlks 41039* | A word over the set of vertices representing a walk (in an undirected graph). (Contributed by Alexander van der Vekens, 15-Jul-2018.) (Revised by AV, 8-Apr-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ (𝑊 ∈ (WWalkS‘𝐺) ↔ (𝑊 ≠ ∅ ∧ 𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸)) | ||
Theorem | wwlksn 41040* | The set of walks (in an undirected graph) of a fixed length as words over the set of vertices. (Contributed by Alexander van der Vekens, 15-Jul-2018.) (Revised by AV, 8-Apr-2021.) |
⊢ (𝑁 ∈ ℕ0 → (𝑁 WWalkSN 𝐺) = {𝑤 ∈ (WWalkS‘𝐺) ∣ (#‘𝑤) = (𝑁 + 1)}) | ||
Theorem | iswwlksn 41041 | A word over the set of vertices representing a walk of a fixed length (in an undirected graph). (Contributed by Alexander van der Vekens, 15-Jul-2018.) (Revised by AV, 8-Apr-2021.) |
⊢ (𝑁 ∈ ℕ0 → (𝑊 ∈ (𝑁 WWalkSN 𝐺) ↔ (𝑊 ∈ (WWalkS‘𝐺) ∧ (#‘𝑊) = (𝑁 + 1)))) | ||
Theorem | iswwlksnx 41042* | Properties of a word to represent a walk of a fixed length, definition of WWalkS expanded. (Contributed by AV, 28-Apr-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ (𝑁 ∈ ℕ0 → (𝑊 ∈ (𝑁 WWalkSN 𝐺) ↔ (𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ (#‘𝑊) = (𝑁 + 1)))) | ||
Theorem | wwlkbp 41043 | Basic properties of a walk (in an undirected graph) as word. (Contributed by Alexander van der Vekens, 15-Jul-2018.) (Revised by AV, 9-Apr-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝑊 ∈ (WWalkS‘𝐺) → (𝐺 ∈ V ∧ 𝑊 ∈ Word 𝑉)) | ||
Theorem | wwlknbp 41044 | Basic properties of a walk of a fixed length (in an undirected graph) as word. (Contributed by Alexander van der Vekens, 16-Jul-2018.) (Revised by AV, 9-Apr-2021.) (Proof shortened by AV, 20-May-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝑊 ∈ (𝑁 WWalkSN 𝐺) → (𝐺 ∈ V ∧ 𝑁 ∈ ℕ0 ∧ 𝑊 ∈ Word 𝑉)) | ||
Theorem | wwlknp 41045* | Properties of a set being a walk of length n (represented by a word). (Contributed by Alexander van der Vekens, 17-Jun-2018.) (Revised by AV, 9-Apr-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ (𝑊 ∈ (𝑁 WWalkSN 𝐺) → (𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = (𝑁 + 1) ∧ ∀𝑖 ∈ (0..^𝑁){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸)) | ||
Theorem | wspthsn 41046* | The set of simple paths of a fixed length as word. (Contributed by Alexander van der Vekens, 1-Mar-2018.) (Revised by AV, 11-May-2021.) |
⊢ (𝑁 WSPathsN 𝐺) = {𝑤 ∈ (𝑁 WWalkSN 𝐺) ∣ ∃𝑓 𝑓(SPathS‘𝐺)𝑤} | ||
Theorem | iswspthn 41047* | An element of the set of simple paths of a fixed length as word. (Contributed by Alexander van der Vekens, 1-Mar-2018.) (Revised by AV, 11-May-2021.) |
⊢ (𝑊 ∈ (𝑁 WSPathsN 𝐺) ↔ (𝑊 ∈ (𝑁 WWalkSN 𝐺) ∧ ∃𝑓 𝑓(SPathS‘𝐺)𝑊)) | ||
Theorem | wspthnp 41048* | Properties of a set being a simple path of a fixed length as word. (Contributed by AV, 18-May-2021.) |
⊢ (𝑊 ∈ (𝑁 WSPathsN 𝐺) → ((𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V) ∧ 𝑊 ∈ (𝑁 WWalkSN 𝐺) ∧ ∃𝑓 𝑓(SPathS‘𝐺)𝑊)) | ||
Theorem | wwlksnon 41049* | The set of walks of a fixed length between two vertices as word. (Contributed by Alexander van der Vekens, 15-Feb-2018.) (Revised by AV, 11-May-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐺 ∈ 𝑈) → (𝑁 WWalksNOn 𝐺) = (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {𝑤 ∈ (𝑁 WWalkSN 𝐺) ∣ ((𝑤‘0) = 𝑎 ∧ (𝑤‘𝑁) = 𝑏)})) | ||
Theorem | wspthsnon 41050* | The set of simple paths of a fixed length between two vertices as word. (Contributed by Alexander van der Vekens, 1-Mar-2018.) (Revised by AV, 11-May-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐺 ∈ 𝑈) → (𝑁 WSPathsNOn 𝐺) = (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {𝑤 ∈ (𝑎(𝑁 WWalksNOn 𝐺)𝑏) ∣ ∃𝑓 𝑓(𝑎(SPathsOn‘𝐺)𝑏)𝑤})) | ||
Theorem | iswwlksnon 41051* | The set of walks of a fixed length between two vertices as word. (Contributed by Alexander van der Vekens, 15-Feb-2018.) (Revised by AV, 12-May-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (𝐴(𝑁 WWalksNOn 𝐺)𝐵) = {𝑤 ∈ (𝑁 WWalkSN 𝐺) ∣ ((𝑤‘0) = 𝐴 ∧ (𝑤‘𝑁) = 𝐵)}) | ||
Theorem | iswspthsnon 41052* | The set of simple paths of a fixed length between two vertices as word. (Contributed by Alexander van der Vekens, 1-Mar-2018.) (Revised by AV, 12-May-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (𝐴(𝑁 WSPathsNOn 𝐺)𝐵) = {𝑤 ∈ (𝐴(𝑁 WWalksNOn 𝐺)𝐵) ∣ ∃𝑓 𝑓(𝐴(SPathsOn‘𝐺)𝐵)𝑤}) | ||
Theorem | wwlknon 41053 | An element of the set of walks of a fixed length between two vertices as word. (Contributed by Alexander van der Vekens, 15-Feb-2018.) (Revised by AV, 12-May-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (𝑊 ∈ (𝐴(𝑁 WWalksNOn 𝐺)𝐵) ↔ (𝑊 ∈ (𝑁 WWalkSN 𝐺) ∧ (𝑊‘0) = 𝐴 ∧ (𝑊‘𝑁) = 𝐵))) | ||
Theorem | wspthnon 41054* | An element of the set of simple paths of a fixed length between two vertices as word. (Contributed by Alexander van der Vekens, 1-Mar-2018.) (Revised by AV, 12-May-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (𝑊 ∈ (𝐴(𝑁 WSPathsNOn 𝐺)𝐵) ↔ (𝑊 ∈ (𝐴(𝑁 WWalksNOn 𝐺)𝐵) ∧ ∃𝑓 𝑓(𝐴(SPathsOn‘𝐺)𝐵)𝑊))) | ||
Theorem | wspthnonp 41055* | Properties of a set being a simple path of a fixed length between two vertices as word. (Contributed by AV, 14-May-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝑊 ∈ (𝐴(𝑁 WSPathsNOn 𝐺)𝐵) → ((𝑁 ∈ ℕ0 ∧ 𝐺 ∈ V) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝑊 ∈ (𝐴(𝑁 WWalksNOn 𝐺)𝐵) ∧ ∃𝑓 𝑓(𝐴(SPathsOn‘𝐺)𝐵)𝑊))) | ||
Theorem | wspthneq1eq2 41056 | Two simple paths with identical sequences of vertices start and end at the same vertices. (Contributed by AV, 14-May-2021.) |
⊢ ((𝑃 ∈ (𝐴(𝑁 WSPathsNOn 𝐺)𝐵) ∧ 𝑃 ∈ (𝐶(𝑁 WSPathsNOn 𝐺)𝐷)) → (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)) | ||
Theorem | wwlksn0s 41057* | The set of all walks as words of length 0 is the set of all words of length 1 over the vertices. (Contributed by Alexander van der Vekens, 22-Jul-2018.) (Revised by AV, 12-Apr-2021.) |
⊢ (0 WWalkSN 𝐺) = {𝑤 ∈ Word (Vtx‘𝐺) ∣ (#‘𝑤) = 1} | ||
Theorem | wwlkssswrd 41058 | Walks (represented by words) are words. (Contributed by Alexander van der Vekens, 17-Jul-2018.) (Revised by AV, 9-Apr-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (WWalkS‘𝐺) ⊆ Word 𝑉 | ||
Theorem | wwlksn0 41059* | A walk of length 0 is represented by a singleton word. (Contributed by Alexander van der Vekens, 20-Jul-2018.) (Revised by AV, 9-Apr-2021.) (Proof shortened by AV, 21-May-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝑊 ∈ (0 WWalkSN 𝐺) → ∃𝑣 ∈ 𝑉 𝑊 = 〈“𝑣”〉) | ||
Theorem | 0enwwlksnge1 41060 | In graphs without edges, there are no walks of length greater than 0. (Contributed by Alexander van der Vekens, 26-Jul-2018.) (Revised by AV, 7-May-2021.) |
⊢ (((Edg‘𝐺) = ∅ ∧ 𝑁 ∈ ℕ) → (𝑁 WWalkSN 𝐺) = ∅) | ||
Theorem | wwlkswwlksn 41061 | A walk of a fixed length as word is a walk (in an undirected graph) as word. (Contributed by Alexander van der Vekens, 17-Jul-2018.) (Revised by AV, 12-Apr-2021.) |
⊢ (𝑊 ∈ (𝑁 WWalkSN 𝐺) → 𝑊 ∈ (WWalkS‘𝐺)) | ||
Theorem | wwlkssswwlksn 41062 | The walks of a fixed length as words are walks (in an undirected graph) as words. (Contributed by Alexander van der Vekens, 17-Jul-2018.) (Revised by AV, 12-Apr-2021.) |
⊢ (𝑁 WWalkSN 𝐺) ⊆ (WWalkS‘𝐺) | ||
Theorem | wwlknbp2 41063 | Other basic properties of a set being a walk of length n (represented by a word). (Contributed by Alexander van der Vekens, 3-Oct-2018.) (Revised by AV, 12-Apr-2021.) |
⊢ (𝑊 ∈ (𝑁 WWalkSN 𝐺) → (𝑊 ∈ Word (Vtx‘𝐺) ∧ (#‘𝑊) = (𝑁 + 1))) | ||
Theorem | 1wlkiswwlks1 41064 | The sequence of vertices in a walk is a walk as word in a pseudograph. (Contributed by Alexander van der Vekens, 20-Jul-2018.) (Revised by AV, 9-Apr-2021.) |
⊢ (𝐺 ∈ UPGraph → (𝐹(1Walks‘𝐺)𝑃 → 𝑃 ∈ (WWalkS‘𝐺))) | ||
Theorem | 1wlklnwwlkln1 41065 | The sequence of vertices in a walk of length 𝑁 is a walk as word of length 𝑁 in a pseudograph. (Contributed by Alexander van der Vekens, 21-Jul-2018.) (Revised by AV, 12-Apr-2021.) |
⊢ (𝐺 ∈ UPGraph → ((𝐹(1Walks‘𝐺)𝑃 ∧ (#‘𝐹) = 𝑁) → 𝑃 ∈ (𝑁 WWalkSN 𝐺))) | ||
Theorem | 1wlkiswwlks2lem1 41066* | Lemma 1 for 1wlkiswwlks2 41072. (Contributed by Alexander van der Vekens, 20-Jul-2018.) |
⊢ 𝐹 = (𝑥 ∈ (0..^((#‘𝑃) − 1)) ↦ (◡𝐸‘{(𝑃‘𝑥), (𝑃‘(𝑥 + 1))})) ⇒ ⊢ ((𝑃 ∈ Word 𝑉 ∧ 1 ≤ (#‘𝑃)) → (#‘𝐹) = ((#‘𝑃) − 1)) | ||
Theorem | 1wlkiswwlks2lem2 41067* | Lemma 2 for 1wlkiswwlks2 41072. (Contributed by Alexander van der Vekens, 20-Jul-2018.) |
⊢ 𝐹 = (𝑥 ∈ (0..^((#‘𝑃) − 1)) ↦ (◡𝐸‘{(𝑃‘𝑥), (𝑃‘(𝑥 + 1))})) ⇒ ⊢ (((#‘𝑃) ∈ ℕ0 ∧ 𝐼 ∈ (0..^((#‘𝑃) − 1))) → (𝐹‘𝐼) = (◡𝐸‘{(𝑃‘𝐼), (𝑃‘(𝐼 + 1))})) | ||
Theorem | 1wlkiswwlks2lem3 41068* | Lemma 3 for 1wlkiswwlks2 41072. (Contributed by Alexander van der Vekens, 20-Jul-2018.) |
⊢ 𝐹 = (𝑥 ∈ (0..^((#‘𝑃) − 1)) ↦ (◡𝐸‘{(𝑃‘𝑥), (𝑃‘(𝑥 + 1))})) ⇒ ⊢ ((𝑃 ∈ Word 𝑉 ∧ 1 ≤ (#‘𝑃)) → 𝑃:(0...(#‘𝐹))⟶𝑉) | ||
Theorem | 1wlkiswwlks2lem4 41069* | Lemma 4 for 1wlkiswwlks2 41072. (Contributed by Alexander van der Vekens, 20-Jul-2018.) (Revised by AV, 10-Apr-2021.) |
⊢ 𝐹 = (𝑥 ∈ (0..^((#‘𝑃) − 1)) ↦ (◡𝐸‘{(𝑃‘𝑥), (𝑃‘(𝑥 + 1))})) & ⊢ 𝐸 = (iEdg‘𝐺) ⇒ ⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ (#‘𝑃)) → (∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 → ∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))})) | ||
Theorem | 1wlkiswwlks2lem5 41070* | Lemma 5 for 1wlkiswwlks2 41072. (Contributed by Alexander van der Vekens, 21-Jul-2018.) (Revised by AV, 10-Apr-2021.) |
⊢ 𝐹 = (𝑥 ∈ (0..^((#‘𝑃) − 1)) ↦ (◡𝐸‘{(𝑃‘𝑥), (𝑃‘(𝑥 + 1))})) & ⊢ 𝐸 = (iEdg‘𝐺) ⇒ ⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ (#‘𝑃)) → (∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 → 𝐹 ∈ Word dom 𝐸)) | ||
Theorem | 1wlkiswwlks2lem6 41071* | Lemma 6 for 1wlkiswwlks2 41072. (Contributed by Alexander van der Vekens, 21-Jul-2018.) (Revised by AV, 10-Apr-2021.) |
⊢ 𝐹 = (𝑥 ∈ (0..^((#‘𝑃) − 1)) ↦ (◡𝐸‘{(𝑃‘𝑥), (𝑃‘(𝑥 + 1))})) & ⊢ 𝐸 = (iEdg‘𝐺) ⇒ ⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ (#‘𝑃)) → (∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 → (𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}))) | ||
Theorem | 1wlkiswwlks2 41072* | A walk as word corresponds to the sequence of vertices in a walk in a simple pseudograph. (Contributed by Alexander van der Vekens, 21-Jul-2018.) (Revised by AV, 10-Apr-2021.) |
⊢ (𝐺 ∈ USPGraph → (𝑃 ∈ (WWalkS‘𝐺) → ∃𝑓 𝑓(1Walks‘𝐺)𝑃)) | ||
Theorem | 1wlkiswwlks 41073* | A walk as word corresponds to a walk in a simple pseudograph. (Contributed by Alexander van der Vekens, 21-Jul-2018.) (Revised by AV, 10-Apr-2021.) |
⊢ (𝐺 ∈ USPGraph → (∃𝑓 𝑓(1Walks‘𝐺)𝑃 ↔ 𝑃 ∈ (WWalkS‘𝐺))) | ||
Theorem | 1wlkiswwlksupgr2 41074* | A walk as word corresponds to the sequence of vertices in a walk in a pseudograph. This variant of 1wlkiswwlks2 41072 does not require 𝐺 to be a simple pseudograph, but it requires the Axiom of Choice (ac6 9185) for its proof. Notice that only the existence of a function 𝑓 can be proven, but, in general, it cannot be "constructed" (as in 1wlkiswwlks2 41072). (Contributed by Alexander van der Vekens, 21-Jul-2018.) (Revised by AV, 10-Apr-2021.) |
⊢ (𝐺 ∈ UPGraph → (𝑃 ∈ (WWalkS‘𝐺) → ∃𝑓 𝑓(1Walks‘𝐺)𝑃)) | ||
Theorem | 1wlkiswwlkupgr 41075* | A walk as word corresponds to a walk in a pseudograph. This variant of 1wlkiswwlks 41073 does not require 𝐺 to be a simple pseudograph, but it requires (indirectly) the Axiom of Choice for its proof. (Contributed by Alexander van der Vekens, 21-Jul-2018.) (Revised by AV, 10-Apr-2021.) |
⊢ (𝐺 ∈ UPGraph → (∃𝑓 𝑓(1Walks‘𝐺)𝑃 ↔ 𝑃 ∈ (WWalkS‘𝐺))) | ||
Theorem | 1wlkpwwlkf1ouspgr 41076* | The mapping of (ordinary) walks to their sequences of vertices is a bijection in a simple pseudograph. (Contributed by AV, 6-May-2021.) |
⊢ 𝐹 = (𝑤 ∈ (1Walks‘𝐺) ↦ (2nd ‘𝑤)) ⇒ ⊢ (𝐺 ∈ USPGraph → 𝐹:(1Walks‘𝐺)–1-1-onto→(WWalkS‘𝐺)) | ||
Theorem | 1wlkisowwlkupgr 41077* | The set of walks as words and the set of (ordinary) walks are isomorphic in a simple pseudograph. (Contributed by AV, 6-May-2021.) |
⊢ (𝐺 ∈ USPGraph → ∃𝑓 𝑓:(1Walks‘𝐺)–1-1-onto→(WWalkS‘𝐺)) | ||
Theorem | wwlksm1edg 41078 | Removing the trailing edge from a walk (as word) with at least one edge results in a walk. (Contributed by Alexander van der Vekens, 1-Aug-2018.) (Revised by AV, 19-Apr-2021.) |
⊢ ((𝑊 ∈ (WWalkS‘𝐺) ∧ 2 ≤ (#‘𝑊)) → (𝑊 substr 〈0, ((#‘𝑊) − 1)〉) ∈ (WWalkS‘𝐺)) | ||
Theorem | 1wlklnwwlkln2lem 41079* | Lemma for 1wlklnwwlkln2 41080 and 1wlklnwwlklnupgr2 41082. Formerly part of proof for 1wlklnwwlkln2 41080. (Contributed by Alexander van der Vekens, 21-Jul-2018.) (Revised by AV, 12-Apr-2021.) |
⊢ (𝜑 → (𝑃 ∈ (WWalkS‘𝐺) → ∃𝑓 𝑓(1Walks‘𝐺)𝑃)) ⇒ ⊢ (𝜑 → (𝑃 ∈ (𝑁 WWalkSN 𝐺) → ∃𝑓(𝑓(1Walks‘𝐺)𝑃 ∧ (#‘𝑓) = 𝑁))) | ||
Theorem | 1wlklnwwlkln2 41080* | A walk of length 𝑁 as word corresponds to the sequence of vertices in a walk of length 𝑁 in a simple pseudograph. (Contributed by Alexander van der Vekens, 21-Jul-2018.) (Revised by AV, 12-Apr-2021.) |
⊢ (𝐺 ∈ USPGraph → (𝑃 ∈ (𝑁 WWalkSN 𝐺) → ∃𝑓(𝑓(1Walks‘𝐺)𝑃 ∧ (#‘𝑓) = 𝑁))) | ||
Theorem | 1wlklnwwlkn 41081* | A walk of length 𝑁 as word corresponds to a walk with length 𝑁 in a simple pseudograph. (Contributed by Alexander van der Vekens, 21-Jul-2018.) (Revised by AV, 12-Apr-2021.) |
⊢ (𝐺 ∈ USPGraph → (∃𝑓(𝑓(1Walks‘𝐺)𝑃 ∧ (#‘𝑓) = 𝑁) ↔ 𝑃 ∈ (𝑁 WWalkSN 𝐺))) | ||
Theorem | 1wlklnwwlklnupgr2 41082* | A walk of length 𝑁 as word corresponds to the sequence of vertices in a walk of length 𝑁 in a pseudograph. This variant of 1wlklnwwlkln2 41080 does not require 𝐺 to be a simple pseudograph, but it requires (indirectly) the Axiom of Choice. (Contributed by Alexander van der Vekens, 21-Jul-2018.) (Revised by AV, 12-Apr-2021.) |
⊢ (𝐺 ∈ UPGraph → (𝑃 ∈ (𝑁 WWalkSN 𝐺) → ∃𝑓(𝑓(1Walks‘𝐺)𝑃 ∧ (#‘𝑓) = 𝑁))) | ||
Theorem | 1wlklnwwlknupgr 41083* | A walk of length 𝑁 as word corresponds to a walk with length 𝑁 in a pseudograph. This variant of 1wlkiswwlks 40197 does not require 𝐺 to be a simple pseudograph, but it requires (indirectly) the Axiom of Choice for its proof. (Contributed by Alexander van der Vekens, 21-Jul-2018.) (Revised by AV, 12-Apr-2021.) |
⊢ (𝐺 ∈ UPGraph → (∃𝑓(𝑓(1Walks‘𝐺)𝑃 ∧ (#‘𝑓) = 𝑁) ↔ 𝑃 ∈ (𝑁 WWalkSN 𝐺))) | ||
Theorem | wlknewwlksn 41084 | If a walk in a pseudograph has length 𝑁, then the sequence of the vertices of the walk is a word representing the walk as word of length 𝑁. (Contributed by Alexander van der Vekens, 25-Aug-2018.) (Revised by AV, 11-Apr-2021.) |
⊢ (((𝐺 ∈ UPGraph ∧ 𝑊 ∈ (1Walks‘𝐺)) ∧ (𝑁 ∈ ℕ0 ∧ (#‘(1st ‘𝑊)) = 𝑁)) → (2nd ‘𝑊) ∈ (𝑁 WWalkSN 𝐺)) | ||
Theorem | wlknwwlksnfun 41085* | Lemma 1 for wlknwwlksnbij2 41089. (Contributed by Alexander van der Vekens, 25-Aug-2018.) (Revised by AV, 14-Apr-2021.) |
⊢ 𝑇 = {𝑝 ∈ (1Walks‘𝐺) ∣ (#‘(1st ‘𝑝)) = 𝑁} & ⊢ 𝑊 = (𝑁 WWalkSN 𝐺) & ⊢ 𝐹 = (𝑡 ∈ 𝑇 ↦ (2nd ‘𝑡)) ⇒ ⊢ ((𝐺 ∈ UPGraph ∧ 𝑁 ∈ ℕ0) → 𝐹:𝑇⟶𝑊) | ||
Theorem | wlknwwlksninj 41086* | Lemma 2 for wlknwwlksnbij2 41089. (Contributed by Alexander van der Vekens, 25-Aug-2018.) (Revised by AV, 14-Apr-2021.) |
⊢ 𝑇 = {𝑝 ∈ (1Walks‘𝐺) ∣ (#‘(1st ‘𝑝)) = 𝑁} & ⊢ 𝑊 = (𝑁 WWalkSN 𝐺) & ⊢ 𝐹 = (𝑡 ∈ 𝑇 ↦ (2nd ‘𝑡)) ⇒ ⊢ ((𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ0) → 𝐹:𝑇–1-1→𝑊) | ||
Theorem | wlknwwlksnsur 41087* | Lemma 3 for wlknwwlksnbij2 41089. (Contributed by Alexander van der Vekens, 25-Aug-2018.) (Revised by AV, 14-Apr-2021.) |
⊢ 𝑇 = {𝑝 ∈ (1Walks‘𝐺) ∣ (#‘(1st ‘𝑝)) = 𝑁} & ⊢ 𝑊 = (𝑁 WWalkSN 𝐺) & ⊢ 𝐹 = (𝑡 ∈ 𝑇 ↦ (2nd ‘𝑡)) ⇒ ⊢ ((𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ0) → 𝐹:𝑇–onto→𝑊) | ||
Theorem | wlknwwlksnbij 41088* | Lemma 4 for wlknwwlksnbij2 41089. (Contributed by Alexander van der Vekens, 25-Aug-2018.) (Revised by AV, 14-Apr-2021.) |
⊢ 𝑇 = {𝑝 ∈ (1Walks‘𝐺) ∣ (#‘(1st ‘𝑝)) = 𝑁} & ⊢ 𝑊 = (𝑁 WWalkSN 𝐺) & ⊢ 𝐹 = (𝑡 ∈ 𝑇 ↦ (2nd ‘𝑡)) ⇒ ⊢ ((𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ0) → 𝐹:𝑇–1-1-onto→𝑊) | ||
Theorem | wlknwwlksnbij2 41089* | There is a bijection between the set of walks of a fixed length and the set of walks represented by words of the same length in a simple pseudograph. (Contributed by Alexander van der Vekens, 25-Aug-2018.) (Revised by AV, 15-Apr-2021.) |
⊢ ((𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ0) → ∃𝑓 𝑓:{𝑝 ∈ (1Walks‘𝐺) ∣ (#‘(1st ‘𝑝)) = 𝑁}–1-1-onto→(𝑁 WWalkSN 𝐺)) | ||
Theorem | wlknwwlksnen 41090* | In a simple pseudograph, the set of walks of a fixed length and the set of walks represented by words are equinumerous. (Contributed by Alexander van der Vekens, 25-Aug-2018.) (Revised by AV, 15-Apr-2021.) |
⊢ ((𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ0) → {𝑝 ∈ (1Walks‘𝐺) ∣ (#‘(1st ‘𝑝)) = 𝑁} ≈ (𝑁 WWalkSN 𝐺)) | ||
Theorem | wlknwwlksneqs 41091* | The set of walks of a fixed length and the set of walks represented by words have the same size. (Contributed by Alexander van der Vekens, 25-Aug-2018.) (Revised by AV, 15-Apr-2021.) |
⊢ ((𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ0) → (#‘{𝑝 ∈ (1Walks‘𝐺) ∣ (#‘(1st ‘𝑝)) = 𝑁}) = (#‘(𝑁 WWalkSN 𝐺))) | ||
Theorem | wlkwwlkfun 41092* | Lemma 1 for wlkwwlkbij2 41096. (Contributed by Alexander van der Vekens, 22-Jul-2018.) (Proof shortened by Alexander van der Vekens, 25-Aug-2018.) (Revised by AV, 15-Apr-2021.) |
⊢ 𝑇 = {𝑝 ∈ (1Walks‘𝐺) ∣ ((#‘(1st ‘𝑝)) = 𝑁 ∧ ((2nd ‘𝑝)‘0) = 𝑃)} & ⊢ 𝑊 = {𝑤 ∈ (𝑁 WWalkSN 𝐺) ∣ (𝑤‘0) = 𝑃} & ⊢ 𝐹 = (𝑡 ∈ 𝑇 ↦ (2nd ‘𝑡)) ⇒ ⊢ ((𝐺 ∈ UPGraph ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → 𝐹:𝑇⟶𝑊) | ||
Theorem | wlkwwlkinj 41093* | Lemma 2 for wlkwwlkbij2 41096. (Contributed by Alexander van der Vekens, 23-Jul-2018.) (Proof shortened by Alexander van der Vekens, 25-Aug-2018.) (Revised by AV, 16-Apr-2021.) |
⊢ 𝑇 = {𝑝 ∈ (1Walks‘𝐺) ∣ ((#‘(1st ‘𝑝)) = 𝑁 ∧ ((2nd ‘𝑝)‘0) = 𝑃)} & ⊢ 𝑊 = {𝑤 ∈ (𝑁 WWalkSN 𝐺) ∣ (𝑤‘0) = 𝑃} & ⊢ 𝐹 = (𝑡 ∈ 𝑇 ↦ (2nd ‘𝑡)) ⇒ ⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → 𝐹:𝑇–1-1→𝑊) | ||
Theorem | wlkwwlksur 41094* | Lemma 3 for wlkwwlkbij2 41096. (Contributed by Alexander van der Vekens, 23-Jul-2018.) (Revised by AV, 16-Apr-2021.) |
⊢ 𝑇 = {𝑝 ∈ (1Walks‘𝐺) ∣ ((#‘(1st ‘𝑝)) = 𝑁 ∧ ((2nd ‘𝑝)‘0) = 𝑃)} & ⊢ 𝑊 = {𝑤 ∈ (𝑁 WWalkSN 𝐺) ∣ (𝑤‘0) = 𝑃} & ⊢ 𝐹 = (𝑡 ∈ 𝑇 ↦ (2nd ‘𝑡)) ⇒ ⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → 𝐹:𝑇–onto→𝑊) | ||
Theorem | wlkwwlkbij 41095* | Lemma 4 for wlkwwlkbij2 41096. (Contributed by Alexander van der Vekens, 22-Jul-2018.) (Revised by AV, 16-Apr-2021.) |
⊢ 𝑇 = {𝑝 ∈ (1Walks‘𝐺) ∣ ((#‘(1st ‘𝑝)) = 𝑁 ∧ ((2nd ‘𝑝)‘0) = 𝑃)} & ⊢ 𝑊 = {𝑤 ∈ (𝑁 WWalkSN 𝐺) ∣ (𝑤‘0) = 𝑃} & ⊢ 𝐹 = (𝑡 ∈ 𝑇 ↦ (2nd ‘𝑡)) ⇒ ⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → 𝐹:𝑇–1-1-onto→𝑊) | ||
Theorem | wlkwwlkbij2 41096* | There is a bijection between the set of walks of a fixed length, starting at a fixed vertex, and the set of walks represented as words of the same length, starting at the same vertex. (Contributed by Alexander van der Vekens, 22-Jul-2018.) (Revised by AV, 16-Apr-2021.) |
⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → ∃𝑓 𝑓:{𝑝 ∈ (1Walks‘𝐺) ∣ ((#‘(1st ‘𝑝)) = 𝑁 ∧ ((2nd ‘𝑝)‘0) = 𝑃)}–1-1-onto→{𝑤 ∈ (𝑁 WWalkSN 𝐺) ∣ (𝑤‘0) = 𝑃}) | ||
Theorem | wwlkseq 41097* | Equality of two walks (as words). (Contributed by Alexander van der Vekens, 4-Aug-2018.) (Revised by AV, 16-Apr-2021.) |
⊢ ((𝑊 ∈ (WWalkS‘𝐺) ∧ 𝑇 ∈ (WWalkS‘𝐺)) → (𝑊 = 𝑇 ↔ ((#‘𝑊) = (#‘𝑇) ∧ ∀𝑖 ∈ (0..^(#‘𝑊))(𝑊‘𝑖) = (𝑇‘𝑖)))) | ||
Theorem | wwlksnred 41098 | Reduction of a walk (as word) by removing the trailing edge/vertex. (Contributed by Alexander van der Vekens, 4-Aug-2018.) (Revised by AV, 16-Apr-2021.) |
⊢ (𝑁 ∈ ℕ0 → (𝑊 ∈ ((𝑁 + 1) WWalkSN 𝐺) → (𝑊 substr 〈0, (𝑁 + 1)〉) ∈ (𝑁 WWalkSN 𝐺))) | ||
Theorem | wwlksnext 41099 | Extension of a walk (as word) by adding an edge/vertex. (Contributed by Alexander van der Vekens, 4-Aug-2018.) (Revised by AV, 16-Apr-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ ((𝑇 ∈ (𝑁 WWalkSN 𝐺) ∧ 𝑆 ∈ 𝑉 ∧ {( lastS ‘𝑇), 𝑆} ∈ 𝐸) → (𝑇 ++ 〈“𝑆”〉) ∈ ((𝑁 + 1) WWalkSN 𝐺)) | ||
Theorem | wwlksnextbi 41100 | Extension of a walk (as word) by adding an edge/vertex. (Contributed by Alexander van der Vekens, 5-Aug-2018.) (Revised by AV, 16-Apr-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ (((𝑁 ∈ ℕ0 ∧ 𝑆 ∈ 𝑉) ∧ (𝑇 ∈ Word 𝑉 ∧ 𝑊 = (𝑇 ++ 〈“𝑆”〉) ∧ {( lastS ‘𝑇), 𝑆} ∈ 𝐸)) → (𝑊 ∈ ((𝑁 + 1) WWalkSN 𝐺) ↔ 𝑇 ∈ (𝑁 WWalkSN 𝐺))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |