![]() |
Metamath
Proof Explorer Theorem List (p. 276 of 454) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-28701) |
![]() (28702-30224) |
![]() (30225-45333) |
Type | Label | Description |
---|---|---|
Statement | ||
Syntax | cpths 27501 | Extend class notation with paths (of a graph). |
class Paths | ||
Syntax | cspths 27502 | Extend class notation with simple paths (of a graph). |
class SPaths | ||
Syntax | cpthson 27503 | Extend class notation with paths between two vertices (within a graph). |
class PathsOn | ||
Syntax | cspthson 27504 | Extend class notation with simple paths between two vertices (within a graph). |
class SPathsOn | ||
Definition | df-pths 27505* |
Define the set of all paths (in an undirected graph).
According to Wikipedia ("Path (graph theory)", https://en.wikipedia.org/wiki/Path_(graph_theory), 3-Oct-2017): "A path is a trail in which all vertices (except possibly the first and last) are distinct. ... use the term simple path to refer to a path which contains no repeated vertices." According to Bollobas: "... a path is a walk with distinct vertices.", see Notation of [Bollobas] p. 5. (A walk with distinct vertices is actually a simple path, see upgrwlkdvspth 27528). Therefore, a path can be represented by an injective mapping f from { 1 , ... , n } and a mapping p from { 0 , ... , n }, which is injective restricted to the set { 1 , ... , n }, where f enumerates the (indices of the) different edges, and p enumerates the vertices. So the path is also represented by the following sequence: p(0) e(f(1)) p(1) e(f(2)) ... p(n-1) e(f(n)) p(n). (Contributed by Alexander van der Vekens and Mario Carneiro, 4-Oct-2017.) (Revised by AV, 9-Jan-2021.) |
⊢ Paths = (𝑔 ∈ V ↦ {〈𝑓, 𝑝〉 ∣ (𝑓(Trails‘𝑔)𝑝 ∧ Fun ◡(𝑝 ↾ (1..^(♯‘𝑓))) ∧ ((𝑝 “ {0, (♯‘𝑓)}) ∩ (𝑝 “ (1..^(♯‘𝑓)))) = ∅)}) | ||
Definition | df-spths 27506* |
Define the set of all simple paths (in an undirected graph).
According to Wikipedia ("Path (graph theory)", https://en.wikipedia.org/wiki/Path_(graph_theory), 3-Oct-2017): "A path is a trail in which all vertices (except possibly the first and last) are distinct. ... use the term simple path to refer to a path which contains no repeated vertices." Therefore, a simple path can be represented by an injective mapping f from { 1 , ... , n } and an injective mapping p from { 0 , ... , n }, where f enumerates the (indices of the) different edges, and p enumerates the vertices. So the simple path is also represented by the following sequence: p(0) e(f(1)) p(1) e(f(2)) ... p(n-1) e(f(n)) p(n). (Contributed by Alexander van der Vekens, 20-Oct-2017.) (Revised by AV, 9-Jan-2021.) |
⊢ SPaths = (𝑔 ∈ V ↦ {〈𝑓, 𝑝〉 ∣ (𝑓(Trails‘𝑔)𝑝 ∧ Fun ◡𝑝)}) | ||
Definition | df-pthson 27507* | Define the collection of paths with particular endpoints (in an undirected graph). (Contributed by Alexander van der Vekens and Mario Carneiro, 4-Oct-2017.) (Revised by AV, 9-Jan-2021.) |
⊢ PathsOn = (𝑔 ∈ V ↦ (𝑎 ∈ (Vtx‘𝑔), 𝑏 ∈ (Vtx‘𝑔) ↦ {〈𝑓, 𝑝〉 ∣ (𝑓(𝑎(TrailsOn‘𝑔)𝑏)𝑝 ∧ 𝑓(Paths‘𝑔)𝑝)})) | ||
Definition | df-spthson 27508* | Define the collection of simple paths with particular endpoints (in an undirected graph). (Contributed by Alexander van der Vekens, 1-Mar-2018.) (Revised by AV, 9-Jan-2021.) |
⊢ SPathsOn = (𝑔 ∈ V ↦ (𝑎 ∈ (Vtx‘𝑔), 𝑏 ∈ (Vtx‘𝑔) ↦ {〈𝑓, 𝑝〉 ∣ (𝑓(𝑎(TrailsOn‘𝑔)𝑏)𝑝 ∧ 𝑓(SPaths‘𝑔)𝑝)})) | ||
Theorem | relpths 27509 | The set (Paths‘𝐺) of all paths on 𝐺 is a set of pairs by our definition of a path, and so is a relation. (Contributed by AV, 30-Oct-2021.) |
⊢ Rel (Paths‘𝐺) | ||
Theorem | pthsfval 27510* | The set of paths (in an undirected graph). (Contributed by Alexander van der Vekens, 20-Oct-2017.) (Revised by AV, 9-Jan-2021.) (Revised by AV, 29-Oct-2021.) |
⊢ (Paths‘𝐺) = {〈𝑓, 𝑝〉 ∣ (𝑓(Trails‘𝐺)𝑝 ∧ Fun ◡(𝑝 ↾ (1..^(♯‘𝑓))) ∧ ((𝑝 “ {0, (♯‘𝑓)}) ∩ (𝑝 “ (1..^(♯‘𝑓)))) = ∅)} | ||
Theorem | spthsfval 27511* | The set of simple paths (in an undirected graph). (Contributed by Alexander van der Vekens, 21-Oct-2017.) (Revised by AV, 9-Jan-2021.) (Revised by AV, 29-Oct-2021.) |
⊢ (SPaths‘𝐺) = {〈𝑓, 𝑝〉 ∣ (𝑓(Trails‘𝐺)𝑝 ∧ Fun ◡𝑝)} | ||
Theorem | ispth 27512 | Conditions for a pair of classes/functions to be a path (in an undirected graph). (Contributed by Alexander van der Vekens, 21-Oct-2017.) (Revised by AV, 9-Jan-2021.) (Revised by AV, 29-Oct-2021.) |
⊢ (𝐹(Paths‘𝐺)𝑃 ↔ (𝐹(Trails‘𝐺)𝑃 ∧ Fun ◡(𝑃 ↾ (1..^(♯‘𝐹))) ∧ ((𝑃 “ {0, (♯‘𝐹)}) ∩ (𝑃 “ (1..^(♯‘𝐹)))) = ∅)) | ||
Theorem | isspth 27513 | Conditions for a pair of classes/functions to be a simple path (in an undirected graph). (Contributed by Alexander van der Vekens, 21-Oct-2017.) (Revised by AV, 9-Jan-2021.) (Revised by AV, 29-Oct-2021.) |
⊢ (𝐹(SPaths‘𝐺)𝑃 ↔ (𝐹(Trails‘𝐺)𝑃 ∧ Fun ◡𝑃)) | ||
Theorem | pthistrl 27514 | A path is a trail (in an undirected graph). (Contributed by Alexander van der Vekens, 21-Oct-2017.) (Revised by AV, 9-Jan-2021.) (Proof shortened by AV, 30-Oct-2021.) |
⊢ (𝐹(Paths‘𝐺)𝑃 → 𝐹(Trails‘𝐺)𝑃) | ||
Theorem | spthispth 27515 | A simple path is a path (in an undirected graph). (Contributed by Alexander van der Vekens, 21-Oct-2017.) (Revised by AV, 9-Jan-2021.) (Proof shortened by AV, 30-Oct-2021.) |
⊢ (𝐹(SPaths‘𝐺)𝑃 → 𝐹(Paths‘𝐺)𝑃) | ||
Theorem | pthiswlk 27516 | A path is a walk (in an undirected graph). (Contributed by AV, 6-Feb-2021.) |
⊢ (𝐹(Paths‘𝐺)𝑃 → 𝐹(Walks‘𝐺)𝑃) | ||
Theorem | spthiswlk 27517 | A simple path is a walk (in an undirected graph). (Contributed by AV, 16-May-2021.) |
⊢ (𝐹(SPaths‘𝐺)𝑃 → 𝐹(Walks‘𝐺)𝑃) | ||
Theorem | pthdivtx 27518 | The inner vertices of a path are distinct from all other vertices. (Contributed by AV, 5-Feb-2021.) (Proof shortened by AV, 31-Oct-2021.) |
⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ (𝐼 ∈ (1..^(♯‘𝐹)) ∧ 𝐽 ∈ (0...(♯‘𝐹)) ∧ 𝐼 ≠ 𝐽)) → (𝑃‘𝐼) ≠ (𝑃‘𝐽)) | ||
Theorem | pthdadjvtx 27519 | The adjacent vertices of a path of length at least 2 are distinct. (Contributed by AV, 5-Feb-2021.) |
⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹) ∧ 𝐼 ∈ (0..^(♯‘𝐹))) → (𝑃‘𝐼) ≠ (𝑃‘(𝐼 + 1))) | ||
Theorem | 2pthnloop 27520* | A path of length at least 2 does not contain a loop. In contrast, a path of length 1 can contain/be a loop, see lppthon 27936. (Contributed by AV, 6-Feb-2021.) |
⊢ 𝐼 = (iEdg‘𝐺) ⇒ ⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹)) → ∀𝑖 ∈ (0..^(♯‘𝐹))2 ≤ (♯‘(𝐼‘(𝐹‘𝑖)))) | ||
Theorem | upgr2pthnlp 27521* | A path of length at least 2 in a pseudograph does not contain a loop. (Contributed by AV, 6-Feb-2021.) |
⊢ 𝐼 = (iEdg‘𝐺) ⇒ ⊢ ((𝐺 ∈ UPGraph ∧ 𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹)) → ∀𝑖 ∈ (0..^(♯‘𝐹))(♯‘(𝐼‘(𝐹‘𝑖))) = 2) | ||
Theorem | spthdifv 27522 | The vertices of a simple path are distinct, so the vertex function is one-to-one. (Contributed by Alexander van der Vekens, 26-Jan-2018.) (Revised by AV, 5-Jun-2021.) (Proof shortened by AV, 30-Oct-2021.) |
⊢ (𝐹(SPaths‘𝐺)𝑃 → 𝑃:(0...(♯‘𝐹))–1-1→(Vtx‘𝐺)) | ||
Theorem | spthdep 27523 | A simple path (at least of length 1) has different start and end points (in an undirected graph). (Contributed by AV, 31-Jan-2021.) (Proof shortened by AV, 30-Oct-2021.) |
⊢ ((𝐹(SPaths‘𝐺)𝑃 ∧ (♯‘𝐹) ≠ 0) → (𝑃‘0) ≠ (𝑃‘(♯‘𝐹))) | ||
Theorem | pthdepisspth 27524 | A path with different start and end points is a simple path (in an undirected graph). (Contributed by Alexander van der Vekens, 31-Oct-2017.) (Revised by AV, 12-Jan-2021.) (Proof shortened by AV, 30-Oct-2021.) |
⊢ ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) ≠ (𝑃‘(♯‘𝐹))) → 𝐹(SPaths‘𝐺)𝑃) | ||
Theorem | upgrwlkdvdelem 27525* | Lemma for upgrwlkdvde 27526. (Contributed by Alexander van der Vekens, 27-Oct-2017.) (Proof shortened by AV, 17-Jan-2021.) |
⊢ ((𝑃:(0...(♯‘𝐹))–1-1→𝑉 ∧ 𝐹 ∈ Word dom 𝐼) → (∀𝑘 ∈ (0..^(♯‘𝐹))(𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} → Fun ◡𝐹)) | ||
Theorem | upgrwlkdvde 27526 | In a pseudograph, all edges of a walk consisting of different vertices are different. Notice that this theorem would not hold for arbitrary hypergraphs, see the counterexample given in the comment of upgrspthswlk 27527. (Contributed by AV, 17-Jan-2021.) |
⊢ ((𝐺 ∈ UPGraph ∧ 𝐹(Walks‘𝐺)𝑃 ∧ Fun ◡𝑃) → Fun ◡𝐹) | ||
Theorem | upgrspthswlk 27527* | The set of simple paths in a pseudograph, expressed as walk. Notice that this theorem would not hold for arbitrary hypergraphs, since a walk with distinct vertices does not need to be a trail: let E = { p0, p1, p2 } be a hyperedge, then ( p0, e, p1, e, p2 ) is walk with distinct vertices, but not with distinct edges. Therefore, E is not a trail and, by definition, also no path. (Contributed by AV, 11-Jan-2021.) (Proof shortened by AV, 17-Jan-2021.) (Proof shortened by AV, 30-Oct-2021.) |
⊢ (𝐺 ∈ UPGraph → (SPaths‘𝐺) = {〈𝑓, 𝑝〉 ∣ (𝑓(Walks‘𝐺)𝑝 ∧ Fun ◡𝑝)}) | ||
Theorem | upgrwlkdvspth 27528 | A walk consisting of different vertices is a simple path. Notice that this theorem would not hold for arbitrary hypergraphs, see the counterexample given in the comment of upgrspthswlk 27527. (Contributed by Alexander van der Vekens, 27-Oct-2017.) (Revised by AV, 17-Jan-2021.) |
⊢ ((𝐺 ∈ UPGraph ∧ 𝐹(Walks‘𝐺)𝑃 ∧ Fun ◡𝑃) → 𝐹(SPaths‘𝐺)𝑃) | ||
Theorem | pthsonfval 27529* | The set of paths between two vertices (in an undirected graph). (Contributed by Alexander van der Vekens, 8-Nov-2017.) (Revised by AV, 16-Jan-2021.) (Revised by AV, 21-Mar-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (𝐴(PathsOn‘𝐺)𝐵) = {〈𝑓, 𝑝〉 ∣ (𝑓(𝐴(TrailsOn‘𝐺)𝐵)𝑝 ∧ 𝑓(Paths‘𝐺)𝑝)}) | ||
Theorem | spthson 27530* | The set of simple paths between two vertices (in an undirected graph). (Contributed by Alexander van der Vekens, 1-Mar-2018.) (Revised by AV, 16-Jan-2021.) (Revised by AV, 21-Mar-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (𝐴(SPathsOn‘𝐺)𝐵) = {〈𝑓, 𝑝〉 ∣ (𝑓(𝐴(TrailsOn‘𝐺)𝐵)𝑝 ∧ 𝑓(SPaths‘𝐺)𝑝)}) | ||
Theorem | ispthson 27531 | Properties of a pair of functions to be a path between two given vertices. (Contributed by Alexander van der Vekens, 8-Nov-2017.) (Revised by AV, 16-Jan-2021.) (Revised by AV, 21-Mar-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐹 ∈ 𝑈 ∧ 𝑃 ∈ 𝑍)) → (𝐹(𝐴(PathsOn‘𝐺)𝐵)𝑃 ↔ (𝐹(𝐴(TrailsOn‘𝐺)𝐵)𝑃 ∧ 𝐹(Paths‘𝐺)𝑃))) | ||
Theorem | isspthson 27532 | Properties of a pair of functions to be a simple path between two given vertices. (Contributed by Alexander van der Vekens, 1-Mar-2018.) (Revised by AV, 16-Jan-2021.) (Revised by AV, 21-Mar-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐹 ∈ 𝑈 ∧ 𝑃 ∈ 𝑍)) → (𝐹(𝐴(SPathsOn‘𝐺)𝐵)𝑃 ↔ (𝐹(𝐴(TrailsOn‘𝐺)𝐵)𝑃 ∧ 𝐹(SPaths‘𝐺)𝑃))) | ||
Theorem | pthsonprop 27533 | Properties of a path between two vertices. (Contributed by Alexander van der Vekens, 12-Dec-2017.) (Revised by AV, 16-Jan-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝐹(𝐴(PathsOn‘𝐺)𝐵)𝑃 → ((𝐺 ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐹(𝐴(TrailsOn‘𝐺)𝐵)𝑃 ∧ 𝐹(Paths‘𝐺)𝑃))) | ||
Theorem | spthonprop 27534 | Properties of a simple path between two vertices. (Contributed by Alexander van der Vekens, 1-Mar-2018.) (Revised by AV, 16-Jan-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝐹(𝐴(SPathsOn‘𝐺)𝐵)𝑃 → ((𝐺 ∈ V ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V) ∧ (𝐹(𝐴(TrailsOn‘𝐺)𝐵)𝑃 ∧ 𝐹(SPaths‘𝐺)𝑃))) | ||
Theorem | pthonispth 27535 | A path between two vertices is a path. (Contributed by Alexander van der Vekens, 12-Dec-2017.) (Revised by AV, 17-Jan-2021.) |
⊢ (𝐹(𝐴(PathsOn‘𝐺)𝐵)𝑃 → 𝐹(Paths‘𝐺)𝑃) | ||
Theorem | pthontrlon 27536 | A path between two vertices is a trail between these vertices. (Contributed by AV, 24-Jan-2021.) |
⊢ (𝐹(𝐴(PathsOn‘𝐺)𝐵)𝑃 → 𝐹(𝐴(TrailsOn‘𝐺)𝐵)𝑃) | ||
Theorem | pthonpth 27537 | A path is a path between its endpoints. (Contributed by AV, 31-Jan-2021.) |
⊢ (𝐹(Paths‘𝐺)𝑃 → 𝐹((𝑃‘0)(PathsOn‘𝐺)(𝑃‘(♯‘𝐹)))𝑃) | ||
Theorem | isspthonpth 27538 | A pair of functions is a simple path between two given vertices iff it is a simple path starting and ending at the two vertices. (Contributed by Alexander van der Vekens, 9-Mar-2018.) (Revised by AV, 17-Jan-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐹 ∈ 𝑊 ∧ 𝑃 ∈ 𝑍)) → (𝐹(𝐴(SPathsOn‘𝐺)𝐵)𝑃 ↔ (𝐹(SPaths‘𝐺)𝑃 ∧ (𝑃‘0) = 𝐴 ∧ (𝑃‘(♯‘𝐹)) = 𝐵))) | ||
Theorem | spthonisspth 27539 | A simple path between to vertices is a simple path. (Contributed by Alexander van der Vekens, 2-Mar-2018.) (Revised by AV, 18-Jan-2021.) |
⊢ (𝐹(𝐴(SPathsOn‘𝐺)𝐵)𝑃 → 𝐹(SPaths‘𝐺)𝑃) | ||
Theorem | spthonpthon 27540 | A simple path between two vertices is a path between these vertices. (Contributed by AV, 24-Jan-2021.) |
⊢ (𝐹(𝐴(SPathsOn‘𝐺)𝐵)𝑃 → 𝐹(𝐴(PathsOn‘𝐺)𝐵)𝑃) | ||
Theorem | spthonepeq 27541 | The endpoints of a simple path between two vertices are equal iff the path is of length 0. (Contributed by Alexander van der Vekens, 1-Mar-2018.) (Revised by AV, 18-Jan-2021.) (Proof shortened by AV, 31-Oct-2021.) |
⊢ (𝐹(𝐴(SPathsOn‘𝐺)𝐵)𝑃 → (𝐴 = 𝐵 ↔ (♯‘𝐹) = 0)) | ||
Theorem | uhgrwkspthlem1 27542 | Lemma 1 for uhgrwkspth 27544. (Contributed by AV, 25-Jan-2021.) |
⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ (♯‘𝐹) = 1) → Fun ◡𝐹) | ||
Theorem | uhgrwkspthlem2 27543 | Lemma 2 for uhgrwkspth 27544. (Contributed by AV, 25-Jan-2021.) |
⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ ((♯‘𝐹) = 1 ∧ 𝐴 ≠ 𝐵) ∧ ((𝑃‘0) = 𝐴 ∧ (𝑃‘(♯‘𝐹)) = 𝐵)) → Fun ◡𝑃) | ||
Theorem | uhgrwkspth 27544 | Any walk of length 1 between two different vertices is a simple path. (Contributed by AV, 25-Jan-2021.) (Proof shortened by AV, 31-Oct-2021.) (Revised by AV, 7-Jul-2022.) |
⊢ ((𝐺 ∈ 𝑊 ∧ (♯‘𝐹) = 1 ∧ 𝐴 ≠ 𝐵) → (𝐹(𝐴(WalksOn‘𝐺)𝐵)𝑃 ↔ 𝐹(𝐴(SPathsOn‘𝐺)𝐵)𝑃)) | ||
Theorem | usgr2wlkneq 27545 | The vertices and edges are pairwise different in a walk of length 2 in a simple graph. (Contributed by Alexander van der Vekens, 2-Mar-2018.) (Revised by AV, 26-Jan-2021.) |
⊢ (((𝐺 ∈ USGraph ∧ 𝐹(Walks‘𝐺)𝑃) ∧ ((♯‘𝐹) = 2 ∧ (𝑃‘0) ≠ (𝑃‘(♯‘𝐹)))) → (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ (𝑃‘2)) ∧ (𝐹‘0) ≠ (𝐹‘1))) | ||
Theorem | usgr2wlkspthlem1 27546 | Lemma 1 for usgr2wlkspth 27548. (Contributed by Alexander van der Vekens, 2-Mar-2018.) (Revised by AV, 26-Jan-2021.) |
⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ (𝐺 ∈ USGraph ∧ (♯‘𝐹) = 2 ∧ (𝑃‘0) ≠ (𝑃‘(♯‘𝐹)))) → Fun ◡𝐹) | ||
Theorem | usgr2wlkspthlem2 27547 | Lemma 2 for usgr2wlkspth 27548. (Contributed by Alexander van der Vekens, 2-Mar-2018.) (Revised by AV, 27-Jan-2021.) |
⊢ ((𝐹(Walks‘𝐺)𝑃 ∧ (𝐺 ∈ USGraph ∧ (♯‘𝐹) = 2 ∧ (𝑃‘0) ≠ (𝑃‘(♯‘𝐹)))) → Fun ◡𝑃) | ||
Theorem | usgr2wlkspth 27548 | In a simple graph, any walk of length 2 between two different vertices is a simple path. (Contributed by Alexander van der Vekens, 2-Mar-2018.) (Revised by AV, 27-Jan-2021.) (Proof shortened by AV, 31-Oct-2021.) |
⊢ ((𝐺 ∈ USGraph ∧ (♯‘𝐹) = 2 ∧ 𝐴 ≠ 𝐵) → (𝐹(𝐴(WalksOn‘𝐺)𝐵)𝑃 ↔ 𝐹(𝐴(SPathsOn‘𝐺)𝐵)𝑃)) | ||
Theorem | usgr2trlncl 27549 | In a simple graph, any trail of length 2 does not start and end at the same vertex. (Contributed by AV, 5-Jun-2021.) (Proof shortened by AV, 31-Oct-2021.) |
⊢ ((𝐺 ∈ USGraph ∧ (♯‘𝐹) = 2) → (𝐹(Trails‘𝐺)𝑃 → (𝑃‘0) ≠ (𝑃‘2))) | ||
Theorem | usgr2trlspth 27550 | In a simple graph, any trail of length 2 is a simple path. (Contributed by AV, 5-Jun-2021.) |
⊢ ((𝐺 ∈ USGraph ∧ (♯‘𝐹) = 2) → (𝐹(Trails‘𝐺)𝑃 ↔ 𝐹(SPaths‘𝐺)𝑃)) | ||
Theorem | usgr2pthspth 27551 | In a simple graph, any path of length 2 is a simple path. (Contributed by Alexander van der Vekens, 25-Jan-2018.) (Revised by AV, 5-Jun-2021.) |
⊢ ((𝐺 ∈ USGraph ∧ (♯‘𝐹) = 2) → (𝐹(Paths‘𝐺)𝑃 ↔ 𝐹(SPaths‘𝐺)𝑃)) | ||
Theorem | usgr2pthlem 27552* | Lemma for usgr2pth 27553. (Contributed by Alexander van der Vekens, 27-Jan-2018.) (Revised by AV, 5-Jun-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) ⇒ ⊢ ((𝐹:(0..^(♯‘𝐹))–1-1→dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(♯‘𝐹))(𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) → ((𝐺 ∈ USGraph ∧ (♯‘𝐹) = 2) → ∃𝑥 ∈ 𝑉 ∃𝑦 ∈ (𝑉 ∖ {𝑥})∃𝑧 ∈ (𝑉 ∖ {𝑥, 𝑦})(((𝑃‘0) = 𝑥 ∧ (𝑃‘1) = 𝑦 ∧ (𝑃‘2) = 𝑧) ∧ ((𝐼‘(𝐹‘0)) = {𝑥, 𝑦} ∧ (𝐼‘(𝐹‘1)) = {𝑦, 𝑧})))) | ||
Theorem | usgr2pth 27553* | In a simple graph, there is a path of length 2 iff there are three distinct vertices so that one of them is connected to each of the two others by an edge. (Contributed by Alexander van der Vekens, 27-Jan-2018.) (Revised by AV, 5-Jun-2021.) (Proof shortened by AV, 31-Oct-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) ⇒ ⊢ (𝐺 ∈ USGraph → ((𝐹(Paths‘𝐺)𝑃 ∧ (♯‘𝐹) = 2) ↔ (𝐹:(0..^2)–1-1→dom 𝐼 ∧ 𝑃:(0...2)–1-1→𝑉 ∧ ∃𝑥 ∈ 𝑉 ∃𝑦 ∈ (𝑉 ∖ {𝑥})∃𝑧 ∈ (𝑉 ∖ {𝑥, 𝑦})(((𝑃‘0) = 𝑥 ∧ (𝑃‘1) = 𝑦 ∧ (𝑃‘2) = 𝑧) ∧ ((𝐼‘(𝐹‘0)) = {𝑥, 𝑦} ∧ (𝐼‘(𝐹‘1)) = {𝑦, 𝑧}))))) | ||
Theorem | usgr2pth0 27554* | In a simply graph, there is a path of length 2 iff there are three distinct vertices so that one of them is connected to each of the two others by an edge. (Contributed by Alexander van der Vekens, 27-Jan-2018.) (Revised by AV, 5-Jun-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) ⇒ ⊢ (𝐺 ∈ USGraph → ((𝐹(Paths‘𝐺)𝑃 ∧ (♯‘𝐹) = 2) ↔ (𝐹:(0..^2)–1-1→dom 𝐼 ∧ 𝑃:(0...2)–1-1→𝑉 ∧ ∃𝑥 ∈ 𝑉 ∃𝑦 ∈ (𝑉 ∖ {𝑥})∃𝑧 ∈ (𝑉 ∖ {𝑥, 𝑦})(((𝑃‘0) = 𝑥 ∧ (𝑃‘1) = 𝑧 ∧ (𝑃‘2) = 𝑦) ∧ ((𝐼‘(𝐹‘0)) = {𝑥, 𝑧} ∧ (𝐼‘(𝐹‘1)) = {𝑧, 𝑦}))))) | ||
Theorem | pthdlem1 27555* | Lemma 1 for pthd 27558. (Contributed by Alexander van der Vekens, 13-Nov-2017.) (Revised by AV, 9-Feb-2021.) |
⊢ (𝜑 → 𝑃 ∈ Word V) & ⊢ 𝑅 = ((♯‘𝑃) − 1) & ⊢ (𝜑 → ∀𝑖 ∈ (0..^(♯‘𝑃))∀𝑗 ∈ (1..^𝑅)(𝑖 ≠ 𝑗 → (𝑃‘𝑖) ≠ (𝑃‘𝑗))) ⇒ ⊢ (𝜑 → Fun ◡(𝑃 ↾ (1..^𝑅))) | ||
Theorem | pthdlem2lem 27556* | Lemma for pthdlem2 27557. (Contributed by AV, 10-Feb-2021.) |
⊢ (𝜑 → 𝑃 ∈ Word V) & ⊢ 𝑅 = ((♯‘𝑃) − 1) & ⊢ (𝜑 → ∀𝑖 ∈ (0..^(♯‘𝑃))∀𝑗 ∈ (1..^𝑅)(𝑖 ≠ 𝑗 → (𝑃‘𝑖) ≠ (𝑃‘𝑗))) ⇒ ⊢ ((𝜑 ∧ (♯‘𝑃) ∈ ℕ ∧ (𝐼 = 0 ∨ 𝐼 = 𝑅)) → (𝑃‘𝐼) ∉ (𝑃 “ (1..^𝑅))) | ||
Theorem | pthdlem2 27557* | Lemma 2 for pthd 27558. (Contributed by Alexander van der Vekens, 11-Nov-2017.) (Revised by AV, 10-Feb-2021.) |
⊢ (𝜑 → 𝑃 ∈ Word V) & ⊢ 𝑅 = ((♯‘𝑃) − 1) & ⊢ (𝜑 → ∀𝑖 ∈ (0..^(♯‘𝑃))∀𝑗 ∈ (1..^𝑅)(𝑖 ≠ 𝑗 → (𝑃‘𝑖) ≠ (𝑃‘𝑗))) ⇒ ⊢ (𝜑 → ((𝑃 “ {0, 𝑅}) ∩ (𝑃 “ (1..^𝑅))) = ∅) | ||
Theorem | pthd 27558* | Two words representing a trail which also represent a path in a graph. (Contributed by AV, 10-Feb-2021.) (Proof shortened by AV, 30-Oct-2021.) |
⊢ (𝜑 → 𝑃 ∈ Word V) & ⊢ 𝑅 = ((♯‘𝑃) − 1) & ⊢ (𝜑 → ∀𝑖 ∈ (0..^(♯‘𝑃))∀𝑗 ∈ (1..^𝑅)(𝑖 ≠ 𝑗 → (𝑃‘𝑖) ≠ (𝑃‘𝑗))) & ⊢ (♯‘𝐹) = 𝑅 & ⊢ (𝜑 → 𝐹(Trails‘𝐺)𝑃) ⇒ ⊢ (𝜑 → 𝐹(Paths‘𝐺)𝑃) | ||
Syntax | cclwlks 27559 | Extend class notation with closed walks (of a graph). |
class ClWalks | ||
Definition | df-clwlks 27560* |
Define the set of all closed walks (in an undirected graph).
According to definition 4 in [Huneke] p. 2: "A walk of length n on (a graph) G is an ordered sequence v0 , v1 , ... v(n) of vertices such that v(i) and v(i+1) are neighbors (i.e are connected by an edge). We say the walk is closed if v(n) = v0". According to the definition of a walk as two mappings f from { 0 , ... , ( n - 1 ) } and p from { 0 , ... , n }, where f enumerates the (indices of the) edges, and p enumerates the vertices, a closed walk is represented by the following sequence: p(0) e(f(0)) p(1) e(f(1)) ... p(n-1) e(f(n-1)) p(n)=p(0). Notice that by this definition, a single vertex can be considered as a closed walk of length 0, see also 0clwlk 27915. (Contributed by Alexander van der Vekens, 12-Mar-2018.) (Revised by AV, 16-Feb-2021.) |
⊢ ClWalks = (𝑔 ∈ V ↦ {〈𝑓, 𝑝〉 ∣ (𝑓(Walks‘𝑔)𝑝 ∧ (𝑝‘0) = (𝑝‘(♯‘𝑓)))}) | ||
Theorem | clwlks 27561* | The set of closed walks (in an undirected graph). (Contributed by Alexander van der Vekens, 15-Mar-2018.) (Revised by AV, 16-Feb-2021.) (Revised by AV, 29-Oct-2021.) |
⊢ (ClWalks‘𝐺) = {〈𝑓, 𝑝〉 ∣ (𝑓(Walks‘𝐺)𝑝 ∧ (𝑝‘0) = (𝑝‘(♯‘𝑓)))} | ||
Theorem | isclwlk 27562 | A pair of functions represents a closed walk iff it represents a walk in which the first vertex is equal to the last vertex. (Contributed by Alexander van der Vekens, 24-Jun-2018.) (Revised by AV, 16-Feb-2021.) (Proof shortened by AV, 30-Oct-2021.) |
⊢ (𝐹(ClWalks‘𝐺)𝑃 ↔ (𝐹(Walks‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹)))) | ||
Theorem | clwlkiswlk 27563 | A closed walk is a walk (in an undirected graph). (Contributed by Alexander van der Vekens, 15-Mar-2018.) (Revised by AV, 16-Feb-2021.) (Proof shortened by AV, 30-Oct-2021.) |
⊢ (𝐹(ClWalks‘𝐺)𝑃 → 𝐹(Walks‘𝐺)𝑃) | ||
Theorem | clwlkwlk 27564 | Closed walks are walks (in an undirected graph). (Contributed by Alexander van der Vekens, 23-Jun-2018.) (Revised by AV, 16-Feb-2021.) (Proof shortened by AV, 30-Oct-2021.) |
⊢ (𝑊 ∈ (ClWalks‘𝐺) → 𝑊 ∈ (Walks‘𝐺)) | ||
Theorem | clwlkswks 27565 | Closed walks are walks (in an undirected graph). (Contributed by Alexander van der Vekens, 25-Aug-2018.) (Revised by AV, 16-Feb-2021.) |
⊢ (ClWalks‘𝐺) ⊆ (Walks‘𝐺) | ||
Theorem | isclwlke 27566* | Properties of a pair of functions to be a closed walk (in an undirected graph). (Contributed by Alexander van der Vekens, 24-Jun-2018.) (Revised by AV, 16-Feb-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) ⇒ ⊢ (𝐺 ∈ 𝑋 → (𝐹(ClWalks‘𝐺)𝑃 ↔ ((𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉) ∧ (∀𝑘 ∈ (0..^(♯‘𝐹))if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘))) ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹)))))) | ||
Theorem | isclwlkupgr 27567* | Properties of a pair of functions to be a closed walk (in a pseudograph). (Contributed by Alexander van der Vekens, 24-Jun-2018.) (Revised by AV, 11-Apr-2021.) (Revised by AV, 28-Oct-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) ⇒ ⊢ (𝐺 ∈ UPGraph → (𝐹(ClWalks‘𝐺)𝑃 ↔ ((𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉) ∧ (∀𝑘 ∈ (0..^(♯‘𝐹))(𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹)))))) | ||
Theorem | clwlkcomp 27568* | A closed walk expressed by properties of its components. (Contributed by Alexander van der Vekens, 24-Jun-2018.) (Revised by AV, 17-Feb-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ 𝐹 = (1st ‘𝑊) & ⊢ 𝑃 = (2nd ‘𝑊) ⇒ ⊢ ((𝐺 ∈ 𝑋 ∧ 𝑊 ∈ (𝑆 × 𝑇)) → (𝑊 ∈ (ClWalks‘𝐺) ↔ ((𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉) ∧ (∀𝑘 ∈ (0..^(♯‘𝐹))if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘))) ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹)))))) | ||
Theorem | clwlkcompim 27569* | Implications for the properties of the components of a closed walk. (Contributed by Alexander van der Vekens, 24-Jun-2018.) (Revised by AV, 17-Feb-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ 𝐹 = (1st ‘𝑊) & ⊢ 𝑃 = (2nd ‘𝑊) ⇒ ⊢ (𝑊 ∈ (ClWalks‘𝐺) → ((𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉) ∧ (∀𝑘 ∈ (0..^(♯‘𝐹))if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘))) ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))))) | ||
Theorem | upgrclwlkcompim 27570* | Implications for the properties of the components of a closed walk in a pseudograph. (Contributed by Alexander van der Vekens, 24-Jun-2018.) (Revised by AV, 2-May-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐼 = (iEdg‘𝐺) & ⊢ 𝐹 = (1st ‘𝑊) & ⊢ 𝑃 = (2nd ‘𝑊) ⇒ ⊢ ((𝐺 ∈ UPGraph ∧ 𝑊 ∈ (ClWalks‘𝐺)) → ((𝐹 ∈ Word dom 𝐼 ∧ 𝑃:(0...(♯‘𝐹))⟶𝑉) ∧ ∀𝑘 ∈ (0..^(♯‘𝐹))(𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹)))) | ||
Theorem | clwlkcompbp 27571 | Basic properties of the components of a closed walk. (Contributed by AV, 23-May-2022.) |
⊢ 𝐹 = (1st ‘𝑊) & ⊢ 𝑃 = (2nd ‘𝑊) ⇒ ⊢ (𝑊 ∈ (ClWalks‘𝐺) → (𝐹(Walks‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹)))) | ||
Theorem | clwlkl1loop 27572 | A closed walk of length 1 is a loop. (Contributed by AV, 22-Apr-2021.) |
⊢ ((Fun (iEdg‘𝐺) ∧ 𝐹(ClWalks‘𝐺)𝑃 ∧ (♯‘𝐹) = 1) → ((𝑃‘0) = (𝑃‘1) ∧ {(𝑃‘0)} ∈ (Edg‘𝐺))) | ||
Syntax | ccrcts 27573 | Extend class notation with circuits (in a graph). |
class Circuits | ||
Syntax | ccycls 27574 | Extend class notation with cycles (in a graph). |
class Cycles | ||
Definition | df-crcts 27575* |
Define the set of all circuits (in an undirected graph).
According to Wikipedia ("Cycle (graph theory)", https://en.wikipedia.org/wiki/Cycle_(graph_theory), 3-Oct-2017): "A circuit can be a closed walk allowing repetitions of vertices but not edges"; according to Wikipedia ("Glossary of graph theory terms", https://en.wikipedia.org/wiki/Glossary_of_graph_theory_terms, 3-Oct-2017): "A circuit may refer to ... a trail (a closed tour without repeated edges), ...". Following Bollobas ("A trail whose endvertices coincide (a closed trail) is called a circuit.", see Definition of [Bollobas] p. 5.), a circuit is a closed trail without repeated edges. So the circuit is also represented by the following sequence: p(0) e(f(1)) p(1) e(f(2)) ... p(n-1) e(f(n)) p(n)=p(0). (Contributed by Alexander van der Vekens, 3-Oct-2017.) (Revised by AV, 31-Jan-2021.) |
⊢ Circuits = (𝑔 ∈ V ↦ {〈𝑓, 𝑝〉 ∣ (𝑓(Trails‘𝑔)𝑝 ∧ (𝑝‘0) = (𝑝‘(♯‘𝑓)))}) | ||
Definition | df-cycls 27576* |
Define the set of all (simple) cycles (in an undirected graph).
According to Wikipedia ("Cycle (graph theory)", https://en.wikipedia.org/wiki/Cycle_(graph_theory), 3-Oct-2017): "A simple cycle may be defined either as a closed walk with no repetitions of vertices and edges allowed, other than the repetition of the starting and ending vertex." According to Bollobas: "If a walk W = x0 x1 ... x(l) is such that l >= 3, x0=x(l), and the vertices x(i), 0 < i < l, are distinct from each other and x0, then W is said to be a cycle." See Definition of [Bollobas] p. 5. However, since a walk consisting of distinct vertices (except the first and the last vertex) is a path, a cycle can be defined as path whose first and last vertices coincide. So a cycle is represented by the following sequence: p(0) e(f(1)) p(1) ... p(n-1) e(f(n)) p(n)=p(0). (Contributed by Alexander van der Vekens, 3-Oct-2017.) (Revised by AV, 31-Jan-2021.) |
⊢ Cycles = (𝑔 ∈ V ↦ {〈𝑓, 𝑝〉 ∣ (𝑓(Paths‘𝑔)𝑝 ∧ (𝑝‘0) = (𝑝‘(♯‘𝑓)))}) | ||
Theorem | crcts 27577* | The set of circuits (in an undirected graph). (Contributed by Alexander van der Vekens, 30-Oct-2017.) (Revised by AV, 31-Jan-2021.) |
⊢ (Circuits‘𝐺) = {〈𝑓, 𝑝〉 ∣ (𝑓(Trails‘𝐺)𝑝 ∧ (𝑝‘0) = (𝑝‘(♯‘𝑓)))} | ||
Theorem | cycls 27578* | The set of cycles (in an undirected graph). (Contributed by Alexander van der Vekens, 30-Oct-2017.) (Revised by AV, 31-Jan-2021.) |
⊢ (Cycles‘𝐺) = {〈𝑓, 𝑝〉 ∣ (𝑓(Paths‘𝐺)𝑝 ∧ (𝑝‘0) = (𝑝‘(♯‘𝑓)))} | ||
Theorem | iscrct 27579 | Sufficient and necessary conditions for a pair of functions to be a circuit (in an undirected graph): A pair of function "is" (represents) a circuit iff it is a closed trail. (Contributed by Alexander van der Vekens, 30-Oct-2017.) (Revised by AV, 31-Jan-2021.) (Revised by AV, 30-Oct-2021.) |
⊢ (𝐹(Circuits‘𝐺)𝑃 ↔ (𝐹(Trails‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹)))) | ||
Theorem | iscycl 27580 | Sufficient and necessary conditions for a pair of functions to be a cycle (in an undirected graph): A pair of function "is" (represents) a cycle iff it is a closed path. (Contributed by Alexander van der Vekens, 30-Oct-2017.) (Revised by AV, 31-Jan-2021.) (Revised by AV, 30-Oct-2021.) |
⊢ (𝐹(Cycles‘𝐺)𝑃 ↔ (𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹)))) | ||
Theorem | crctprop 27581 | The properties of a circuit: A circuit is a closed trail. (Contributed by AV, 31-Jan-2021.) (Proof shortened by AV, 30-Oct-2021.) |
⊢ (𝐹(Circuits‘𝐺)𝑃 → (𝐹(Trails‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹)))) | ||
Theorem | cyclprop 27582 | The properties of a cycle: A cycle is a closed path. (Contributed by AV, 31-Jan-2021.) (Proof shortened by AV, 30-Oct-2021.) |
⊢ (𝐹(Cycles‘𝐺)𝑃 → (𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹)))) | ||
Theorem | crctisclwlk 27583 | A circuit is a closed walk. (Contributed by AV, 17-Feb-2021.) (Proof shortened by AV, 30-Oct-2021.) |
⊢ (𝐹(Circuits‘𝐺)𝑃 → 𝐹(ClWalks‘𝐺)𝑃) | ||
Theorem | crctistrl 27584 | A circuit is a trail. (Contributed by Alexander van der Vekens, 30-Oct-2017.) (Revised by AV, 31-Jan-2021.) |
⊢ (𝐹(Circuits‘𝐺)𝑃 → 𝐹(Trails‘𝐺)𝑃) | ||
Theorem | crctiswlk 27585 | A circuit is a walk. (Contributed by AV, 6-Apr-2021.) |
⊢ (𝐹(Circuits‘𝐺)𝑃 → 𝐹(Walks‘𝐺)𝑃) | ||
Theorem | cyclispth 27586 | A cycle is a path. (Contributed by Alexander van der Vekens, 30-Oct-2017.) (Revised by AV, 31-Jan-2021.) |
⊢ (𝐹(Cycles‘𝐺)𝑃 → 𝐹(Paths‘𝐺)𝑃) | ||
Theorem | cycliswlk 27587 | A cycle is a walk. (Contributed by Alexander van der Vekens, 7-Nov-2017.) (Revised by AV, 31-Jan-2021.) |
⊢ (𝐹(Cycles‘𝐺)𝑃 → 𝐹(Walks‘𝐺)𝑃) | ||
Theorem | cycliscrct 27588 | A cycle is a circuit. (Contributed by Alexander van der Vekens, 30-Oct-2017.) (Revised by AV, 31-Jan-2021.) (Proof shortened by AV, 30-Oct-2021.) |
⊢ (𝐹(Cycles‘𝐺)𝑃 → 𝐹(Circuits‘𝐺)𝑃) | ||
Theorem | cyclnspth 27589 | A (non-trivial) cycle is not a simple path. (Contributed by Alexander van der Vekens, 30-Oct-2017.) (Revised by AV, 31-Jan-2021.) (Proof shortened by AV, 30-Oct-2021.) |
⊢ (𝐹 ≠ ∅ → (𝐹(Cycles‘𝐺)𝑃 → ¬ 𝐹(SPaths‘𝐺)𝑃)) | ||
Theorem | cyclispthon 27590 | 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.) (Proof shortened by AV, 30-Oct-2021.) |
⊢ (𝐹(Cycles‘𝐺)𝑃 → 𝐹((𝑃‘0)(PathsOn‘𝐺)(𝑃‘0))𝑃) | ||
Theorem | lfgrn1cycl 27591* | 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 27592 | 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 27593 | 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 27594 | 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.) (Proof shortened by AV, 31-Oct-2021.) |
⊢ ((𝐺 ∈ USPGraph ∧ 𝐹(Circuits‘𝐺)𝑃) → (♯‘𝐹) ≠ 2) | ||
Theorem | usgrn2cycl 27595 | 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 | crctcshwlkn0lem1 27596 | Lemma for crctcshwlkn0 27607. (Contributed by AV, 13-Mar-2021.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℕ) → ((𝐴 − 𝐵) + 1) ≤ 𝐴) | ||
Theorem | crctcshwlkn0lem2 27597* | Lemma for crctcshwlkn0 27607. (Contributed by AV, 12-Mar-2021.) |
⊢ (𝜑 → 𝑆 ∈ (1..^𝑁)) & ⊢ 𝑄 = (𝑥 ∈ (0...𝑁) ↦ if(𝑥 ≤ (𝑁 − 𝑆), (𝑃‘(𝑥 + 𝑆)), (𝑃‘((𝑥 + 𝑆) − 𝑁)))) ⇒ ⊢ ((𝜑 ∧ 𝐽 ∈ (0...(𝑁 − 𝑆))) → (𝑄‘𝐽) = (𝑃‘(𝐽 + 𝑆))) | ||
Theorem | crctcshwlkn0lem3 27598* | Lemma for crctcshwlkn0 27607. (Contributed by AV, 12-Mar-2021.) |
⊢ (𝜑 → 𝑆 ∈ (1..^𝑁)) & ⊢ 𝑄 = (𝑥 ∈ (0...𝑁) ↦ if(𝑥 ≤ (𝑁 − 𝑆), (𝑃‘(𝑥 + 𝑆)), (𝑃‘((𝑥 + 𝑆) − 𝑁)))) ⇒ ⊢ ((𝜑 ∧ 𝐽 ∈ (((𝑁 − 𝑆) + 1)...𝑁)) → (𝑄‘𝐽) = (𝑃‘((𝐽 + 𝑆) − 𝑁))) | ||
Theorem | crctcshwlkn0lem4 27599* | Lemma for crctcshwlkn0 27607. (Contributed by AV, 12-Mar-2021.) |
⊢ (𝜑 → 𝑆 ∈ (1..^𝑁)) & ⊢ 𝑄 = (𝑥 ∈ (0...𝑁) ↦ if(𝑥 ≤ (𝑁 − 𝑆), (𝑃‘(𝑥 + 𝑆)), (𝑃‘((𝑥 + 𝑆) − 𝑁)))) & ⊢ 𝐻 = (𝐹 cyclShift 𝑆) & ⊢ 𝑁 = (♯‘𝐹) & ⊢ (𝜑 → 𝐹 ∈ Word 𝐴) & ⊢ (𝜑 → ∀𝑖 ∈ (0..^𝑁)if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖)))) ⇒ ⊢ (𝜑 → ∀𝑗 ∈ (0..^(𝑁 − 𝑆))if-((𝑄‘𝑗) = (𝑄‘(𝑗 + 1)), (𝐼‘(𝐻‘𝑗)) = {(𝑄‘𝑗)}, {(𝑄‘𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻‘𝑗)))) | ||
Theorem | crctcshwlkn0lem5 27600* | Lemma for crctcshwlkn0 27607. (Contributed by AV, 12-Mar-2021.) |
⊢ (𝜑 → 𝑆 ∈ (1..^𝑁)) & ⊢ 𝑄 = (𝑥 ∈ (0...𝑁) ↦ if(𝑥 ≤ (𝑁 − 𝑆), (𝑃‘(𝑥 + 𝑆)), (𝑃‘((𝑥 + 𝑆) − 𝑁)))) & ⊢ 𝐻 = (𝐹 cyclShift 𝑆) & ⊢ 𝑁 = (♯‘𝐹) & ⊢ (𝜑 → 𝐹 ∈ Word 𝐴) & ⊢ (𝜑 → ∀𝑖 ∈ (0..^𝑁)if-((𝑃‘𝑖) = (𝑃‘(𝑖 + 1)), (𝐼‘(𝐹‘𝑖)) = {(𝑃‘𝑖)}, {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ⊆ (𝐼‘(𝐹‘𝑖)))) ⇒ ⊢ (𝜑 → ∀𝑗 ∈ (((𝑁 − 𝑆) + 1)..^𝑁)if-((𝑄‘𝑗) = (𝑄‘(𝑗 + 1)), (𝐼‘(𝐻‘𝑗)) = {(𝑄‘𝑗)}, {(𝑄‘𝑗), (𝑄‘(𝑗 + 1))} ⊆ (𝐼‘(𝐻‘𝑗)))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |