Home | Metamath
Proof Explorer Theorem List (p. 285 of 466) | < 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-29289) |
Hilbert Space Explorer
(29290-30812) |
Users' Mathboxes
(30813-46532) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | clwwlkn0 28401 | There is no closed walk of length 0 (i.e. a closed walk without any edge) represented by a word of vertices. (Contributed by Alexander van der Vekens, 15-Sep-2018.) (Revised by AV, 24-Apr-2021.) |
⊢ (0 ClWWalksN 𝐺) = ∅ | ||
Theorem | clwwlkneq0 28402 | Sufficient conditions for ClWWalksN to be empty. (Contributed by Alexander van der Vekens, 15-Sep-2018.) (Revised by AV, 24-Apr-2021.) (Proof shortened by AV, 24-Feb-2022.) |
⊢ ((𝐺 ∉ V ∨ 𝑁 ∉ ℕ) → (𝑁 ClWWalksN 𝐺) = ∅) | ||
Theorem | clwwlkclwwlkn 28403 | A closed walk of a fixed length as word is a closed walk (in an undirected graph) as word. (Contributed by Alexander van der Vekens, 15-Mar-2018.) (Revised by AV, 24-Apr-2021.) (Proof shortened by AV, 22-Mar-2022.) |
⊢ (𝑊 ∈ (𝑁 ClWWalksN 𝐺) → 𝑊 ∈ (ClWWalks‘𝐺)) | ||
Theorem | clwwlksclwwlkn 28404 | The closed walks of a fixed length as words are closed walks (in an undirected graph) as words. (Contributed by Alexander van der Vekens, 15-Mar-2018.) (Revised by AV, 12-Apr-2021.) |
⊢ (𝑁 ClWWalksN 𝐺) ⊆ (ClWWalks‘𝐺) | ||
Theorem | clwwlknlen 28405 | The length of a word representing a closed walk of a fixed length is this fixed length. (Contributed by AV, 22-Mar-2022.) |
⊢ (𝑊 ∈ (𝑁 ClWWalksN 𝐺) → (♯‘𝑊) = 𝑁) | ||
Theorem | clwwlknnn 28406 | The length of a closed walk of a fixed length as word is a positive integer. (Contributed by AV, 22-Mar-2022.) |
⊢ (𝑊 ∈ (𝑁 ClWWalksN 𝐺) → 𝑁 ∈ ℕ) | ||
Theorem | clwwlknwrd 28407 | A closed walk of a fixed length as word is a word over the vertices. (Contributed by AV, 30-Apr-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝑊 ∈ (𝑁 ClWWalksN 𝐺) → 𝑊 ∈ Word 𝑉) | ||
Theorem | clwwlknbp 28408 | Basic properties of a closed walk of a fixed length as word. (Contributed by AV, 30-Apr-2021.) (Proof shortened by AV, 22-Mar-2022.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝑊 ∈ (𝑁 ClWWalksN 𝐺) → (𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = 𝑁)) | ||
Theorem | isclwwlknx 28409* | Characterization of a word representing a closed walk of a fixed length, definition of ClWWalks expanded. (Contributed by AV, 25-Apr-2021.) (Proof shortened by AV, 22-Mar-2022.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ (𝑁 ∈ ℕ → (𝑊 ∈ (𝑁 ClWWalksN 𝐺) ↔ ((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (♯‘𝑊) = 𝑁))) | ||
Theorem | clwwlknp 28410* | Properties of a set being a closed walk (represented by a word). (Contributed by Alexander van der Vekens, 17-Jun-2018.) (Revised by AV, 24-Apr-2021.) (Proof shortened by AV, 23-Mar-2022.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ (𝑊 ∈ (𝑁 ClWWalksN 𝐺) → ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸)) | ||
Theorem | clwwlknwwlksn 28411 | A word representing a closed walk of length 𝑁 also represents a walk of length 𝑁 − 1. The walk is one edge shorter than the closed walk, because the last edge connecting the last with the first vertex is missing. For example, if 〈“𝑎𝑏𝑐”〉 ∈ (3 ClWWalksN 𝐺) represents a closed walk "abca" of length 3, then 〈“𝑎𝑏𝑐”〉 ∈ (2 WWalksN 𝐺) represents a walk "abc" (not closed if 𝑎 ≠ 𝑐) of length 2, and 〈“𝑎𝑏𝑐𝑎”〉 ∈ (3 WWalksN 𝐺) represents also a closed walk "abca" of length 3. (Contributed by AV, 24-Jan-2022.) (Revised by AV, 22-Mar-2022.) |
⊢ (𝑊 ∈ (𝑁 ClWWalksN 𝐺) → 𝑊 ∈ ((𝑁 − 1) WWalksN 𝐺)) | ||
Theorem | clwwlknlbonbgr1 28412 | The last but one vertex in a closed walk is a neighbor of the first vertex of the closed walk. (Contributed by AV, 17-Feb-2022.) |
⊢ ((𝐺 ∈ USGraph ∧ 𝑊 ∈ (𝑁 ClWWalksN 𝐺)) → (𝑊‘(𝑁 − 1)) ∈ (𝐺 NeighbVtx (𝑊‘0))) | ||
Theorem | clwwlkinwwlk 28413 | If the initial vertex of a walk occurs another time in the walk, the walk starts with a closed walk. Since the walk is expressed as a word over vertices, the closed walk can be expressed as a subword of this word. (Contributed by Alexander van der Vekens, 15-Sep-2018.) (Revised by AV, 23-Jan-2022.) (Revised by AV, 30-Oct-2022.) |
⊢ (((𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ≥‘𝑁)) ∧ 𝑊 ∈ (𝑀 WWalksN 𝐺) ∧ (𝑊‘𝑁) = (𝑊‘0)) → (𝑊 prefix 𝑁) ∈ (𝑁 ClWWalksN 𝐺)) | ||
Theorem | clwwlkn1 28414 | A closed walk of length 1 represented as word is a word consisting of 1 symbol representing a vertex connected to itself by (at least) one edge, that is, a loop. (Contributed by AV, 24-Apr-2021.) (Revised by AV, 11-Feb-2022.) |
⊢ (𝑊 ∈ (1 ClWWalksN 𝐺) ↔ ((♯‘𝑊) = 1 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ {(𝑊‘0)} ∈ (Edg‘𝐺))) | ||
Theorem | loopclwwlkn1b 28415 | The singleton word consisting of a vertex 𝑉 represents a closed walk of length 1 iff there is a loop at vertex 𝑉. (Contributed by AV, 11-Feb-2022.) |
⊢ (𝑉 ∈ (Vtx‘𝐺) → ({𝑉} ∈ (Edg‘𝐺) ↔ 〈“𝑉”〉 ∈ (1 ClWWalksN 𝐺))) | ||
Theorem | clwwlkn1loopb 28416* | A word represents a closed walk of length 1 iff this word is a singleton word consisting of a vertex with an attached loop. (Contributed by AV, 11-Feb-2022.) |
⊢ (𝑊 ∈ (1 ClWWalksN 𝐺) ↔ ∃𝑣 ∈ (Vtx‘𝐺)(𝑊 = 〈“𝑣”〉 ∧ {𝑣} ∈ (Edg‘𝐺))) | ||
Theorem | clwwlkn2 28417 | A closed walk of length 2 represented as word is a word consisting of 2 symbols representing (not necessarily different) vertices connected by (at least) one edge. (Contributed by Alexander van der Vekens, 19-Sep-2018.) (Revised by AV, 25-Apr-2021.) |
⊢ (𝑊 ∈ (2 ClWWalksN 𝐺) ↔ ((♯‘𝑊) = 2 ∧ 𝑊 ∈ Word (Vtx‘𝐺) ∧ {(𝑊‘0), (𝑊‘1)} ∈ (Edg‘𝐺))) | ||
Theorem | clwwlknfi 28418 | If there is only a finite number of vertices, the number of closed walks of fixed length (as words) is also finite. (Contributed by Alexander van der Vekens, 25-Mar-2018.) (Revised by AV, 25-Apr-2021.) (Proof shortened by AV, 22-Mar-2022.) (Proof shortened by JJ, 18-Nov-2022.) |
⊢ ((Vtx‘𝐺) ∈ Fin → (𝑁 ClWWalksN 𝐺) ∈ Fin) | ||
Theorem | clwwlkel 28419* | Obtaining a closed walk (as word) by appending the first symbol to the word representing a walk. (Contributed by AV, 28-Sep-2018.) (Revised by AV, 25-Apr-2021.) |
⊢ 𝐷 = {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (lastS‘𝑤) = (𝑤‘0)} ⇒ ⊢ ((𝑁 ∈ ℕ ∧ (𝑃 ∈ Word (Vtx‘𝐺) ∧ (♯‘𝑃) = 𝑁) ∧ (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘𝑃), (𝑃‘0)} ∈ (Edg‘𝐺))) → (𝑃 ++ 〈“(𝑃‘0)”〉) ∈ 𝐷) | ||
Theorem | clwwlkf 28420* | Lemma 1 for clwwlkf1o 28424: F is a function. (Contributed by Alexander van der Vekens, 27-Sep-2018.) (Revised by AV, 26-Apr-2021.) (Revised by AV, 1-Nov-2022.) |
⊢ 𝐷 = {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (lastS‘𝑤) = (𝑤‘0)} & ⊢ 𝐹 = (𝑡 ∈ 𝐷 ↦ (𝑡 prefix 𝑁)) ⇒ ⊢ (𝑁 ∈ ℕ → 𝐹:𝐷⟶(𝑁 ClWWalksN 𝐺)) | ||
Theorem | clwwlkfv 28421* | Lemma 2 for clwwlkf1o 28424: the value of function 𝐹. (Contributed by Alexander van der Vekens, 28-Sep-2018.) (Revised by AV, 26-Apr-2021.) (Revised by AV, 1-Nov-2022.) |
⊢ 𝐷 = {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (lastS‘𝑤) = (𝑤‘0)} & ⊢ 𝐹 = (𝑡 ∈ 𝐷 ↦ (𝑡 prefix 𝑁)) ⇒ ⊢ (𝑊 ∈ 𝐷 → (𝐹‘𝑊) = (𝑊 prefix 𝑁)) | ||
Theorem | clwwlkf1 28422* | Lemma 3 for clwwlkf1o 28424: 𝐹 is a 1-1 function. (Contributed by AV, 28-Sep-2018.) (Revised by AV, 26-Apr-2021.) (Revised by AV, 1-Nov-2022.) |
⊢ 𝐷 = {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (lastS‘𝑤) = (𝑤‘0)} & ⊢ 𝐹 = (𝑡 ∈ 𝐷 ↦ (𝑡 prefix 𝑁)) ⇒ ⊢ (𝑁 ∈ ℕ → 𝐹:𝐷–1-1→(𝑁 ClWWalksN 𝐺)) | ||
Theorem | clwwlkfo 28423* | Lemma 4 for clwwlkf1o 28424: F is an onto function. (Contributed by Alexander van der Vekens, 29-Sep-2018.) (Revised by AV, 26-Apr-2021.) (Revised by AV, 1-Nov-2022.) |
⊢ 𝐷 = {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (lastS‘𝑤) = (𝑤‘0)} & ⊢ 𝐹 = (𝑡 ∈ 𝐷 ↦ (𝑡 prefix 𝑁)) ⇒ ⊢ (𝑁 ∈ ℕ → 𝐹:𝐷–onto→(𝑁 ClWWalksN 𝐺)) | ||
Theorem | clwwlkf1o 28424* | F is a 1-1 onto function, that means that there is a bijection between the set of closed walks of a fixed length represented by walks (as words) and the set of closed walks (as words) of the fixed length. The difference between these two representations is that in the first case the starting vertex is repeated at the end of the word, and in the second case it is not. (Contributed by Alexander van der Vekens, 29-Sep-2018.) (Revised by AV, 26-Apr-2021.) (Revised by AV, 1-Nov-2022.) |
⊢ 𝐷 = {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (lastS‘𝑤) = (𝑤‘0)} & ⊢ 𝐹 = (𝑡 ∈ 𝐷 ↦ (𝑡 prefix 𝑁)) ⇒ ⊢ (𝑁 ∈ ℕ → 𝐹:𝐷–1-1-onto→(𝑁 ClWWalksN 𝐺)) | ||
Theorem | clwwlken 28425* | The set of closed walks of a fixed length represented by walks (as words) and the set of closed walks (as words) of the fixed length are equinumerous. (Contributed by AV, 5-Jun-2022.) (Proof shortened by AV, 2-Nov-2022.) |
⊢ (𝑁 ∈ ℕ → {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (lastS‘𝑤) = (𝑤‘0)} ≈ (𝑁 ClWWalksN 𝐺)) | ||
Theorem | clwwlknwwlkncl 28426* | Obtaining a closed walk (as word) by appending the first symbol to the word representing a walk. (Contributed by Alexander van der Vekens, 29-Sep-2018.) (Revised by AV, 26-Apr-2021.) (Revised by AV, 22-Mar-2022.) |
⊢ (𝑊 ∈ (𝑁 ClWWalksN 𝐺) → (𝑊 ++ 〈“(𝑊‘0)”〉) ∈ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (lastS‘𝑤) = (𝑤‘0)}) | ||
Theorem | clwwlkwwlksb 28427 | A nonempty word over vertices represents a closed walk iff the word concatenated with its first symbol represents a walk. (Contributed by AV, 4-Mar-2022.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → (𝑊 ∈ (ClWWalks‘𝐺) ↔ (𝑊 ++ 〈“(𝑊‘0)”〉) ∈ (WWalks‘𝐺))) | ||
Theorem | clwwlknwwlksnb 28428 | A word over vertices represents a closed walk of a fixed length 𝑁 greater than zero iff the word concatenated with its first symbol represents a walk of length 𝑁. This theorem would not hold for 𝑁 = 0 and 𝑊 = ∅, because (𝑊 ++ 〈“(𝑊‘0)”〉) = 〈“∅”〉 ∈ (0 WWalksN 𝐺) could be true, but not 𝑊 ∈ (0 ClWWalksN 𝐺) ↔ ∅ ∈ ∅. (Contributed by AV, 4-Mar-2022.) (Proof shortened by AV, 22-Mar-2022.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ) → (𝑊 ∈ (𝑁 ClWWalksN 𝐺) ↔ (𝑊 ++ 〈“(𝑊‘0)”〉) ∈ (𝑁 WWalksN 𝐺))) | ||
Theorem | clwwlkext2edg 28429 | If a word concatenated with a vertex represents a closed walk in (in a graph), there is an edge between this vertex and the last vertex of the word, and between this vertex and the first vertex of the word. (Contributed by Alexander van der Vekens, 3-Oct-2018.) (Revised by AV, 27-Apr-2021.) (Proof shortened by AV, 22-Mar-2022.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2)) ∧ (𝑊 ++ 〈“𝑍”〉) ∈ (𝑁 ClWWalksN 𝐺)) → ({(lastS‘𝑊), 𝑍} ∈ 𝐸 ∧ {𝑍, (𝑊‘0)} ∈ 𝐸)) | ||
Theorem | wwlksext2clwwlk 28430 | If a word represents a walk in (in a graph) and there are edges between the last vertex of the word and another vertex and between this other vertex and the first vertex of the word, then the concatenation of the word representing the walk with this other vertex represents a closed walk. (Contributed by Alexander van der Vekens, 3-Oct-2018.) (Revised by AV, 27-Apr-2021.) (Revised by AV, 14-Mar-2022.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ ((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ 𝑍 ∈ 𝑉) → (({(lastS‘𝑊), 𝑍} ∈ 𝐸 ∧ {𝑍, (𝑊‘0)} ∈ 𝐸) → (𝑊 ++ 〈“𝑍”〉) ∈ ((𝑁 + 2) ClWWalksN 𝐺))) | ||
Theorem | wwlksubclwwlk 28431 | Any prefix of a word representing a closed walk represents a walk. (Contributed by Alexander van der Vekens, 5-Oct-2018.) (Revised by AV, 28-Apr-2021.) (Revised by AV, 1-Nov-2022.) |
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → (𝑋 ∈ (𝑁 ClWWalksN 𝐺) → (𝑋 prefix 𝑀) ∈ ((𝑀 − 1) WWalksN 𝐺))) | ||
Theorem | clwwnisshclwwsn 28432 | Cyclically shifting a closed walk as word of fixed length results in a closed walk as word of the same length (in an undirected graph). (Contributed by Alexander van der Vekens, 10-Jun-2018.) (Revised by AV, 29-Apr-2021.) (Proof shortened by AV, 22-Mar-2022.) |
⊢ ((𝑊 ∈ (𝑁 ClWWalksN 𝐺) ∧ 𝑀 ∈ (0...𝑁)) → (𝑊 cyclShift 𝑀) ∈ (𝑁 ClWWalksN 𝐺)) | ||
Theorem | eleclclwwlknlem1 28433* | Lemma 1 for eleclclwwlkn 28449. (Contributed by Alexander van der Vekens, 11-May-2018.) (Revised by AV, 30-Apr-2021.) |
⊢ 𝑊 = (𝑁 ClWWalksN 𝐺) ⇒ ⊢ ((𝐾 ∈ (0...𝑁) ∧ (𝑋 ∈ 𝑊 ∧ 𝑌 ∈ 𝑊)) → ((𝑋 = (𝑌 cyclShift 𝐾) ∧ ∃𝑚 ∈ (0...𝑁)𝑍 = (𝑌 cyclShift 𝑚)) → ∃𝑛 ∈ (0...𝑁)𝑍 = (𝑋 cyclShift 𝑛))) | ||
Theorem | eleclclwwlknlem2 28434* | Lemma 2 for eleclclwwlkn 28449. (Contributed by Alexander van der Vekens, 11-May-2018.) (Revised by AV, 30-Apr-2021.) |
⊢ 𝑊 = (𝑁 ClWWalksN 𝐺) ⇒ ⊢ (((𝑘 ∈ (0...𝑁) ∧ 𝑋 = (𝑥 cyclShift 𝑘)) ∧ (𝑋 ∈ 𝑊 ∧ 𝑥 ∈ 𝑊)) → (∃𝑚 ∈ (0...𝑁)𝑌 = (𝑥 cyclShift 𝑚) ↔ ∃𝑛 ∈ (0...𝑁)𝑌 = (𝑋 cyclShift 𝑛))) | ||
Theorem | clwwlknscsh 28435* | The set of cyclical shifts of a word representing a closed walk is the set of closed walks represented by cyclical shifts of a word. (Contributed by Alexander van der Vekens, 15-Jun-2018.) (Revised by AV, 30-Apr-2021.) |
⊢ ((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ (𝑁 ClWWalksN 𝐺)) → {𝑦 ∈ (𝑁 ClWWalksN 𝐺) ∣ ∃𝑛 ∈ (0...𝑁)𝑦 = (𝑊 cyclShift 𝑛)} = {𝑦 ∈ Word (Vtx‘𝐺) ∣ ∃𝑛 ∈ (0...𝑁)𝑦 = (𝑊 cyclShift 𝑛)}) | ||
Theorem | clwwlknccat 28436 | The concatenation of two words representing closed walks anchored at the same vertex represents a closed walk with a length which is the sum of the lengths of the two walks. The resulting walk is a "double loop", starting at the common vertex, coming back to the common vertex by the first walk, following the second walk and finally coming back to the common vertex again. (Contributed by AV, 24-Apr-2022.) |
⊢ ((𝐴 ∈ (𝑀 ClWWalksN 𝐺) ∧ 𝐵 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝐴‘0) = (𝐵‘0)) → (𝐴 ++ 𝐵) ∈ ((𝑀 + 𝑁) ClWWalksN 𝐺)) | ||
Theorem | umgr2cwwk2dif 28437 | If a word represents a closed walk of length at least 2 in a multigraph, the first two symbols of the word must be different. (Contributed by Alexander van der Vekens, 17-Jun-2018.) (Revised by AV, 30-Apr-2021.) |
⊢ ((𝐺 ∈ UMGraph ∧ 𝑁 ∈ (ℤ≥‘2) ∧ 𝑊 ∈ (𝑁 ClWWalksN 𝐺)) → (𝑊‘1) ≠ (𝑊‘0)) | ||
Theorem | umgr2cwwkdifex 28438* | If a word represents a closed walk of length at least 2 in a undirected simple graph, the first two symbols of the word must be different. (Contributed by Alexander van der Vekens, 17-Jun-2018.) (Revised by AV, 30-Apr-2021.) |
⊢ ((𝐺 ∈ UMGraph ∧ 𝑁 ∈ (ℤ≥‘2) ∧ 𝑊 ∈ (𝑁 ClWWalksN 𝐺)) → ∃𝑖 ∈ (0..^𝑁)(𝑊‘𝑖) ≠ (𝑊‘0)) | ||
Theorem | erclwwlknrel 28439 | ∼ is a relation. (Contributed by Alexander van der Vekens, 25-Mar-2018.) (Revised by AV, 30-Apr-2021.) |
⊢ 𝑊 = (𝑁 ClWWalksN 𝐺) & ⊢ ∼ = {〈𝑡, 𝑢〉 ∣ (𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊 ∧ ∃𝑛 ∈ (0...𝑁)𝑡 = (𝑢 cyclShift 𝑛))} ⇒ ⊢ Rel ∼ | ||
Theorem | erclwwlkneq 28440* | Two classes are equivalent regarding ∼ if both are words of the same fixed length and one is the other cyclically shifted. (Contributed by Alexander van der Vekens, 25-Mar-2018.) (Revised by AV, 30-Apr-2021.) |
⊢ 𝑊 = (𝑁 ClWWalksN 𝐺) & ⊢ ∼ = {〈𝑡, 𝑢〉 ∣ (𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊 ∧ ∃𝑛 ∈ (0...𝑁)𝑡 = (𝑢 cyclShift 𝑛))} ⇒ ⊢ ((𝑇 ∈ 𝑋 ∧ 𝑈 ∈ 𝑌) → (𝑇 ∼ 𝑈 ↔ (𝑇 ∈ 𝑊 ∧ 𝑈 ∈ 𝑊 ∧ ∃𝑛 ∈ (0...𝑁)𝑇 = (𝑈 cyclShift 𝑛)))) | ||
Theorem | erclwwlkneqlen 28441* | If two classes are equivalent regarding ∼, then they are words of the same length. (Contributed by Alexander van der Vekens, 8-Apr-2018.) (Revised by AV, 30-Apr-2021.) |
⊢ 𝑊 = (𝑁 ClWWalksN 𝐺) & ⊢ ∼ = {〈𝑡, 𝑢〉 ∣ (𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊 ∧ ∃𝑛 ∈ (0...𝑁)𝑡 = (𝑢 cyclShift 𝑛))} ⇒ ⊢ ((𝑇 ∈ 𝑋 ∧ 𝑈 ∈ 𝑌) → (𝑇 ∼ 𝑈 → (♯‘𝑇) = (♯‘𝑈))) | ||
Theorem | erclwwlknref 28442* | ∼ is a reflexive relation over the set of closed walks (defined as words). (Contributed by Alexander van der Vekens, 26-Mar-2018.) (Revised by AV, 30-Apr-2021.) (Proof shortened by AV, 23-Mar-2022.) |
⊢ 𝑊 = (𝑁 ClWWalksN 𝐺) & ⊢ ∼ = {〈𝑡, 𝑢〉 ∣ (𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊 ∧ ∃𝑛 ∈ (0...𝑁)𝑡 = (𝑢 cyclShift 𝑛))} ⇒ ⊢ (𝑥 ∈ 𝑊 ↔ 𝑥 ∼ 𝑥) | ||
Theorem | erclwwlknsym 28443* | ∼ is a symmetric relation over the set of closed walks (defined as words). (Contributed by Alexander van der Vekens, 10-Apr-2018.) (Revised by AV, 30-Apr-2021.) |
⊢ 𝑊 = (𝑁 ClWWalksN 𝐺) & ⊢ ∼ = {〈𝑡, 𝑢〉 ∣ (𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊 ∧ ∃𝑛 ∈ (0...𝑁)𝑡 = (𝑢 cyclShift 𝑛))} ⇒ ⊢ (𝑥 ∼ 𝑦 → 𝑦 ∼ 𝑥) | ||
Theorem | erclwwlkntr 28444* | ∼ is a transitive relation over the set of closed walks (defined as words). (Contributed by Alexander van der Vekens, 10-Apr-2018.) (Revised by AV, 30-Apr-2021.) |
⊢ 𝑊 = (𝑁 ClWWalksN 𝐺) & ⊢ ∼ = {〈𝑡, 𝑢〉 ∣ (𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊 ∧ ∃𝑛 ∈ (0...𝑁)𝑡 = (𝑢 cyclShift 𝑛))} ⇒ ⊢ ((𝑥 ∼ 𝑦 ∧ 𝑦 ∼ 𝑧) → 𝑥 ∼ 𝑧) | ||
Theorem | erclwwlkn 28445* | ∼ is an equivalence relation over the set of closed walks (defined as words) with a fixed length. (Contributed by Alexander van der Vekens, 10-Apr-2018.) (Revised by AV, 30-Apr-2021.) |
⊢ 𝑊 = (𝑁 ClWWalksN 𝐺) & ⊢ ∼ = {〈𝑡, 𝑢〉 ∣ (𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊 ∧ ∃𝑛 ∈ (0...𝑁)𝑡 = (𝑢 cyclShift 𝑛))} ⇒ ⊢ ∼ Er 𝑊 | ||
Theorem | qerclwwlknfi 28446* | The quotient set of the set of closed walks (defined as words) with a fixed length according to the equivalence relation ∼ is finite. (Contributed by Alexander van der Vekens, 10-Apr-2018.) (Revised by AV, 30-Apr-2021.) |
⊢ 𝑊 = (𝑁 ClWWalksN 𝐺) & ⊢ ∼ = {〈𝑡, 𝑢〉 ∣ (𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊 ∧ ∃𝑛 ∈ (0...𝑁)𝑡 = (𝑢 cyclShift 𝑛))} ⇒ ⊢ ((Vtx‘𝐺) ∈ Fin → (𝑊 / ∼ ) ∈ Fin) | ||
Theorem | hashclwwlkn0 28447* | The number of closed walks (defined as words) with a fixed length is the sum of the sizes of all equivalence classes according to ∼. (Contributed by Alexander van der Vekens, 10-Apr-2018.) (Revised by AV, 30-Apr-2021.) |
⊢ 𝑊 = (𝑁 ClWWalksN 𝐺) & ⊢ ∼ = {〈𝑡, 𝑢〉 ∣ (𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊 ∧ ∃𝑛 ∈ (0...𝑁)𝑡 = (𝑢 cyclShift 𝑛))} ⇒ ⊢ ((Vtx‘𝐺) ∈ Fin → (♯‘𝑊) = Σ𝑥 ∈ (𝑊 / ∼ )(♯‘𝑥)) | ||
Theorem | eclclwwlkn1 28448* | An equivalence class according to ∼. (Contributed by Alexander van der Vekens, 12-Apr-2018.) (Revised by AV, 30-Apr-2021.) |
⊢ 𝑊 = (𝑁 ClWWalksN 𝐺) & ⊢ ∼ = {〈𝑡, 𝑢〉 ∣ (𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊 ∧ ∃𝑛 ∈ (0...𝑁)𝑡 = (𝑢 cyclShift 𝑛))} ⇒ ⊢ (𝐵 ∈ 𝑋 → (𝐵 ∈ (𝑊 / ∼ ) ↔ ∃𝑥 ∈ 𝑊 𝐵 = {𝑦 ∈ 𝑊 ∣ ∃𝑛 ∈ (0...𝑁)𝑦 = (𝑥 cyclShift 𝑛)})) | ||
Theorem | eleclclwwlkn 28449* | A member of an equivalence class according to ∼. (Contributed by Alexander van der Vekens, 11-May-2018.) (Revised by AV, 1-May-2021.) |
⊢ 𝑊 = (𝑁 ClWWalksN 𝐺) & ⊢ ∼ = {〈𝑡, 𝑢〉 ∣ (𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊 ∧ ∃𝑛 ∈ (0...𝑁)𝑡 = (𝑢 cyclShift 𝑛))} ⇒ ⊢ ((𝐵 ∈ (𝑊 / ∼ ) ∧ 𝑋 ∈ 𝐵) → (𝑌 ∈ 𝐵 ↔ (𝑌 ∈ 𝑊 ∧ ∃𝑛 ∈ (0...𝑁)𝑌 = (𝑋 cyclShift 𝑛)))) | ||
Theorem | hashecclwwlkn1 28450* | The size of every equivalence class of the equivalence relation over the set of closed walks (defined as words) with a fixed length which is a prime number is 1 or equals this length. (Contributed by Alexander van der Vekens, 17-Jun-2018.) (Revised by AV, 1-May-2021.) |
⊢ 𝑊 = (𝑁 ClWWalksN 𝐺) & ⊢ ∼ = {〈𝑡, 𝑢〉 ∣ (𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊 ∧ ∃𝑛 ∈ (0...𝑁)𝑡 = (𝑢 cyclShift 𝑛))} ⇒ ⊢ ((𝑁 ∈ ℙ ∧ 𝑈 ∈ (𝑊 / ∼ )) → ((♯‘𝑈) = 1 ∨ (♯‘𝑈) = 𝑁)) | ||
Theorem | umgrhashecclwwlk 28451* | The size of every equivalence class of the equivalence relation over the set of closed walks (defined as words) with a fixed length which is a prime number equals this length (in an undirected simple graph). (Contributed by Alexander van der Vekens, 17-Jun-2018.) (Revised by AV, 1-May-2021.) |
⊢ 𝑊 = (𝑁 ClWWalksN 𝐺) & ⊢ ∼ = {〈𝑡, 𝑢〉 ∣ (𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊 ∧ ∃𝑛 ∈ (0...𝑁)𝑡 = (𝑢 cyclShift 𝑛))} ⇒ ⊢ ((𝐺 ∈ UMGraph ∧ 𝑁 ∈ ℙ) → (𝑈 ∈ (𝑊 / ∼ ) → (♯‘𝑈) = 𝑁)) | ||
Theorem | fusgrhashclwwlkn 28452* | The size of the set of closed walks (defined as words) with a fixed length which is a prime number is the product of the number of equivalence classes for ∼ over the set of closed walks and the fixed length. (Contributed by Alexander van der Vekens, 17-Jun-2018.) (Revised by AV, 1-May-2021.) |
⊢ 𝑊 = (𝑁 ClWWalksN 𝐺) & ⊢ ∼ = {〈𝑡, 𝑢〉 ∣ (𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊 ∧ ∃𝑛 ∈ (0...𝑁)𝑡 = (𝑢 cyclShift 𝑛))} ⇒ ⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (♯‘𝑊) = ((♯‘(𝑊 / ∼ )) · 𝑁)) | ||
Theorem | clwwlkndivn 28453 | The size of the set of closed walks (defined as words) of length 𝑁 is divisible by 𝑁 if 𝑁 is a prime number. (Contributed by Alexander van der Vekens, 17-Jun-2018.) (Revised by AV, 2-May-2021.) |
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → 𝑁 ∥ (♯‘(𝑁 ClWWalksN 𝐺))) | ||
Theorem | clwlknf1oclwwlknlem1 28454 | Lemma 1 for clwlknf1oclwwlkn 28457. (Contributed by AV, 26-May-2022.) (Revised by AV, 1-Nov-2022.) |
⊢ ((𝐶 ∈ (ClWalks‘𝐺) ∧ 1 ≤ (♯‘(1st ‘𝐶))) → (♯‘((2nd ‘𝐶) prefix ((♯‘(2nd ‘𝐶)) − 1))) = (♯‘(1st ‘𝐶))) | ||
Theorem | clwlknf1oclwwlknlem2 28455* | Lemma 2 for clwlknf1oclwwlkn 28457: The closed walks of a positive length are nonempty closed walks of this length. (Contributed by AV, 26-May-2022.) |
⊢ (𝑁 ∈ ℕ → {𝑤 ∈ (ClWalks‘𝐺) ∣ (♯‘(1st ‘𝑤)) = 𝑁} = {𝑐 ∈ (ClWalks‘𝐺) ∣ (1 ≤ (♯‘(1st ‘𝑐)) ∧ (♯‘(1st ‘𝑐)) = 𝑁)}) | ||
Theorem | clwlknf1oclwwlknlem3 28456* | Lemma 3 for clwlknf1oclwwlkn 28457: The bijective function of clwlknf1oclwwlkn 28457 is the bijective function of clwlkclwwlkf1o 28384 restricted to the closed walks with a fixed positive length. (Contributed by AV, 26-May-2022.) (Revised by AV, 1-Nov-2022.) |
⊢ 𝐴 = (1st ‘𝑐) & ⊢ 𝐵 = (2nd ‘𝑐) & ⊢ 𝐶 = {𝑤 ∈ (ClWalks‘𝐺) ∣ (♯‘(1st ‘𝑤)) = 𝑁} & ⊢ 𝐹 = (𝑐 ∈ 𝐶 ↦ (𝐵 prefix (♯‘𝐴))) ⇒ ⊢ ((𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ) → 𝐹 = ((𝑐 ∈ {𝑤 ∈ (ClWalks‘𝐺) ∣ 1 ≤ (♯‘(1st ‘𝑤))} ↦ (𝐵 prefix (♯‘𝐴))) ↾ 𝐶)) | ||
Theorem | clwlknf1oclwwlkn 28457* | There is a one-to-one onto function between the set of closed walks as words of length 𝑁 and the set of closed walks of length 𝑁 in a simple pseudograph. (Contributed by Alexander van der Vekens, 5-Jul-2018.) (Revised by AV, 3-May-2021.) (Revised by AV, 1-Nov-2022.) |
⊢ 𝐴 = (1st ‘𝑐) & ⊢ 𝐵 = (2nd ‘𝑐) & ⊢ 𝐶 = {𝑤 ∈ (ClWalks‘𝐺) ∣ (♯‘(1st ‘𝑤)) = 𝑁} & ⊢ 𝐹 = (𝑐 ∈ 𝐶 ↦ (𝐵 prefix (♯‘𝐴))) ⇒ ⊢ ((𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ) → 𝐹:𝐶–1-1-onto→(𝑁 ClWWalksN 𝐺)) | ||
Theorem | clwlkssizeeq 28458* | The size of the set of closed walks as words of length 𝑁 corresponds to the size of the set of closed walks of length 𝑁 in a simple pseudograph. (Contributed by Alexander van der Vekens, 6-Jul-2018.) (Revised by AV, 4-May-2021.) (Revised by AV, 26-May-2022.) (Proof shortened by AV, 3-Nov-2022.) |
⊢ ((𝐺 ∈ USPGraph ∧ 𝑁 ∈ ℕ) → (♯‘(𝑁 ClWWalksN 𝐺)) = (♯‘{𝑤 ∈ (ClWalks‘𝐺) ∣ (♯‘(1st ‘𝑤)) = 𝑁})) | ||
Theorem | clwlksndivn 28459* | The size of the set of closed walks of prime length 𝑁 is divisible by 𝑁. This corresponds to statement 9 in [Huneke] p. 2: "It follows that, if p is a prime number, then the number of closed walks of length p is divisible by p". (Contributed by Alexander van der Vekens, 6-Jul-2018.) (Revised by AV, 4-May-2021.) |
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → 𝑁 ∥ (♯‘{𝑐 ∈ (ClWalks‘𝐺) ∣ (♯‘(1st ‘𝑐)) = 𝑁})) | ||
Syntax | cclwwlknon 28460 | Extend class notation with closed walks (in an undirected graph) anchored at a fixed vertex and of a fixed length as word over the set of vertices. |
class ClWWalksNOn | ||
Definition | df-clwwlknon 28461* | Define the set of all closed walks a graph 𝑔, anchored at a fixed vertex 𝑣 (i.e., a walk starting and ending at the fixed vertex 𝑣, also called "a closed walk on vertex 𝑣") and having a fixed length 𝑛 as words over the set of vertices. Such a word corresponds to the sequence v=p(0) p(1) ... p(n-1) of the vertices in a closed walk p(0) e(f(1)) p(1) e(f(2)) ... p(n-1) e(f(n)) p(n)=p(0)=v as defined in df-clwlks 28148. The set ((𝑣(ClWWalksNOn‘𝑔)𝑛) corresponds to the set of "walks from v to v of length n" in a statement of [Huneke] p. 2. (Contributed by AV, 24-Feb-2022.) |
⊢ ClWWalksNOn = (𝑔 ∈ V ↦ (𝑣 ∈ (Vtx‘𝑔), 𝑛 ∈ ℕ0 ↦ {𝑤 ∈ (𝑛 ClWWalksN 𝑔) ∣ (𝑤‘0) = 𝑣})) | ||
Theorem | clwwlknonmpo 28462* | (ClWWalksNOn‘𝐺) is an operator mapping a vertex 𝑣 and a nonnegative integer 𝑛 to the set of closed walks on 𝑣 of length 𝑛 as words over the set of vertices in a graph 𝐺. (Contributed by AV, 25-Feb-2022.) (Proof shortened by AV, 2-Mar-2024.) |
⊢ (ClWWalksNOn‘𝐺) = (𝑣 ∈ (Vtx‘𝐺), 𝑛 ∈ ℕ0 ↦ {𝑤 ∈ (𝑛 ClWWalksN 𝐺) ∣ (𝑤‘0) = 𝑣}) | ||
Theorem | clwwlknon 28463* | The set of closed walks on vertex 𝑋 of length 𝑁 in a graph 𝐺 as words over the set of vertices. (Contributed by Alexander van der Vekens, 14-Sep-2018.) (Revised by AV, 28-May-2021.) (Revised by AV, 24-Mar-2022.) |
⊢ (𝑋(ClWWalksNOn‘𝐺)𝑁) = {𝑤 ∈ (𝑁 ClWWalksN 𝐺) ∣ (𝑤‘0) = 𝑋} | ||
Theorem | isclwwlknon 28464 | A word over the set of vertices representing a closed walk on vertex 𝑋 of length 𝑁 in a graph 𝐺. (Contributed by AV, 25-Feb-2022.) (Revised by AV, 24-Mar-2022.) |
⊢ (𝑊 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ↔ (𝑊 ∈ (𝑁 ClWWalksN 𝐺) ∧ (𝑊‘0) = 𝑋)) | ||
Theorem | clwwlk0on0 28465 | There is no word over the set of vertices representing a closed walk on vertex 𝑋 of length 0 in a graph 𝐺. (Contributed by AV, 17-Feb-2022.) (Revised by AV, 25-Feb-2022.) |
⊢ (𝑋(ClWWalksNOn‘𝐺)0) = ∅ | ||
Theorem | clwwlknon0 28466 | Sufficient conditions for ClWWalksNOn to be empty. (Contributed by AV, 25-Mar-2022.) |
⊢ (¬ (𝑋 ∈ (Vtx‘𝐺) ∧ 𝑁 ∈ ℕ) → (𝑋(ClWWalksNOn‘𝐺)𝑁) = ∅) | ||
Theorem | clwwlknonfin 28467 | In a finite graph 𝐺, the set of closed walks on vertex 𝑋 of length 𝑁 is also finite. (Contributed by Alexander van der Vekens, 26-Sep-2018.) (Revised by AV, 25-Feb-2022.) (Proof shortened by AV, 24-Mar-2022.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝑉 ∈ Fin → (𝑋(ClWWalksNOn‘𝐺)𝑁) ∈ Fin) | ||
Theorem | clwwlknonel 28468* | Characterization of a word over the set of vertices representing a closed walk on vertex 𝑋 of (nonzero) length 𝑁 in a graph 𝐺. This theorem would not hold for 𝑁 = 0 if 𝑊 = 𝑋 = ∅. (Contributed by Alexander van der Vekens, 20-Sep-2018.) (Revised by AV, 28-May-2021.) (Revised by AV, 24-Mar-2022.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ (𝑁 ≠ 0 → (𝑊 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ↔ ((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (♯‘𝑊) = 𝑁 ∧ (𝑊‘0) = 𝑋))) | ||
Theorem | clwwlknonccat 28469 | The concatenation of two words representing closed walks on a vertex 𝑋 represents a closed walk on vertex 𝑋. The resulting walk is a "double loop", starting at vertex 𝑋, coming back to 𝑋 by the first walk, following the second walk and finally coming back to 𝑋 again. (Contributed by AV, 24-Apr-2022.) |
⊢ ((𝐴 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑀) ∧ 𝐵 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁)) → (𝐴 ++ 𝐵) ∈ (𝑋(ClWWalksNOn‘𝐺)(𝑀 + 𝑁))) | ||
Theorem | clwwlknon1 28470* | The set of closed walks on vertex 𝑋 of length 1 in a graph 𝐺 as words over the set of vertices. (Contributed by AV, 11-Feb-2022.) (Revised by AV, 25-Feb-2022.) (Proof shortened by AV, 24-Mar-2022.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐶 = (ClWWalksNOn‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ (𝑋 ∈ 𝑉 → (𝑋𝐶1) = {𝑤 ∈ Word 𝑉 ∣ (𝑤 = 〈“𝑋”〉 ∧ {𝑋} ∈ 𝐸)}) | ||
Theorem | clwwlknon1loop 28471 | If there is a loop at vertex 𝑋, the set of (closed) walks on 𝑋 of length 1 as words over the set of vertices is a singleton containing the singleton word consisting of 𝑋. (Contributed by AV, 11-Feb-2022.) (Revised by AV, 25-Feb-2022.) (Proof shortened by AV, 25-Mar-2022.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐶 = (ClWWalksNOn‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ ((𝑋 ∈ 𝑉 ∧ {𝑋} ∈ 𝐸) → (𝑋𝐶1) = {〈“𝑋”〉}) | ||
Theorem | clwwlknon1nloop 28472 | If there is no loop at vertex 𝑋, the set of (closed) walks on 𝑋 of length 1 as words over the set of vertices is empty. (Contributed by AV, 11-Feb-2022.) (Revised by AV, 25-Mar-2022.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐶 = (ClWWalksNOn‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ ({𝑋} ∉ 𝐸 → (𝑋𝐶1) = ∅) | ||
Theorem | clwwlknon1sn 28473 | The set of (closed) walks on vertex 𝑋 of length 1 as words over the set of vertices is a singleton containing the singleton word consisting of 𝑋 iff there is a loop at 𝑋. (Contributed by AV, 11-Feb-2022.) (Revised by AV, 25-Feb-2022.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐶 = (ClWWalksNOn‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ (𝑋 ∈ 𝑉 → ((𝑋𝐶1) = {〈“𝑋”〉} ↔ {𝑋} ∈ 𝐸)) | ||
Theorem | clwwlknon1le1 28474 | There is at most one (closed) walk on vertex 𝑋 of length 1 as word over the set of vertices. (Contributed by AV, 11-Feb-2022.) (Revised by AV, 25-Mar-2022.) |
⊢ (♯‘(𝑋(ClWWalksNOn‘𝐺)1)) ≤ 1 | ||
Theorem | clwwlknon2 28475* | The set of closed walks on vertex 𝑋 of length 2 in a graph 𝐺 as words over the set of vertices. (Contributed by AV, 5-Mar-2022.) (Revised by AV, 25-Mar-2022.) |
⊢ 𝐶 = (ClWWalksNOn‘𝐺) ⇒ ⊢ (𝑋𝐶2) = {𝑤 ∈ (2 ClWWalksN 𝐺) ∣ (𝑤‘0) = 𝑋} | ||
Theorem | clwwlknon2x 28476* | The set of closed walks on vertex 𝑋 of length 2 in a graph 𝐺 as words over the set of vertices, definition of ClWWalksN expanded. (Contributed by Alexander van der Vekens, 19-Sep-2018.) (Revised by AV, 25-Mar-2022.) |
⊢ 𝐶 = (ClWWalksNOn‘𝐺) & ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ (𝑋𝐶2) = {𝑤 ∈ Word 𝑉 ∣ ((♯‘𝑤) = 2 ∧ {(𝑤‘0), (𝑤‘1)} ∈ 𝐸 ∧ (𝑤‘0) = 𝑋)} | ||
Theorem | s2elclwwlknon2 28477 | Sufficient conditions of a doubleton word to represent a closed walk on vertex 𝑋 of length 2. (Contributed by AV, 11-May-2022.) |
⊢ 𝐶 = (ClWWalksNOn‘𝐺) & ⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ {𝑋, 𝑌} ∈ 𝐸) → 〈“𝑋𝑌”〉 ∈ (𝑋𝐶2)) | ||
Theorem | clwwlknon2num 28478 | In a 𝐾-regular graph 𝐺, there are 𝐾 closed walks on vertex 𝑋 of length 2. (Contributed by Alexander van der Vekens, 19-Sep-2018.) (Revised by AV, 28-May-2021.) (Revised by AV, 25-Feb-2022.) (Proof shortened by AV, 25-Mar-2022.) |
⊢ ((𝐺 RegUSGraph 𝐾 ∧ 𝑋 ∈ (Vtx‘𝐺)) → (♯‘(𝑋(ClWWalksNOn‘𝐺)2)) = 𝐾) | ||
Theorem | clwwlknonwwlknonb 28479 | A word over vertices represents a closed walk of a fixed length 𝑁 on vertex 𝑋 iff the word concatenated with 𝑋 represents a walk of length 𝑁 on 𝑋 and 𝑋. This theorem would not hold for 𝑁 = 0 and 𝑊 = ∅, see clwwlknwwlksnb 28428. (Contributed by AV, 4-Mar-2022.) (Revised by AV, 27-Mar-2022.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ) → (𝑊 ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁) ↔ (𝑊 ++ 〈“𝑋”〉) ∈ (𝑋(𝑁 WWalksNOn 𝐺)𝑋))) | ||
Theorem | clwwlknonex2lem1 28480 | Lemma 1 for clwwlknonex2 28482: Transformation of a special half-open integer range into a union of a smaller half-open integer range and an unordered pair. This Lemma would not hold for 𝑁 = 2, i.e., (♯‘𝑊) = 0, because (0..^(((♯‘𝑊) + 2) − 1)) = (0..^((0 + 2) − 1)) = (0..^1) = {0} ≠ {-1, 0} = (∅ ∪ {-1, 0}) = ((0..^(0 − 1)) ∪ {(0 − 1), 0}) = ((0..^((♯‘𝑊) − 1)) ∪ {((♯‘𝑊) − 1), (♯‘𝑊)}). (Contributed by AV, 22-Sep-2018.) (Revised by AV, 26-Jan-2022.) |
⊢ ((𝑁 ∈ (ℤ≥‘3) ∧ (♯‘𝑊) = (𝑁 − 2)) → (0..^(((♯‘𝑊) + 2) − 1)) = ((0..^((♯‘𝑊) − 1)) ∪ {((♯‘𝑊) − 1), (♯‘𝑊)})) | ||
Theorem | clwwlknonex2lem2 28481* | Lemma 2 for clwwlknonex2 28482: Transformation of a walk and two edges into a walk extended by two vertices/edges. (Contributed by AV, 22-Sep-2018.) (Revised by AV, 27-Jan-2022.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ ((((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)) ∧ ((𝑊 ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {(lastS‘𝑊), (𝑊‘0)} ∈ 𝐸) ∧ (♯‘𝑊) = (𝑁 − 2) ∧ (𝑊‘0) = 𝑋)) ∧ {𝑋, 𝑌} ∈ 𝐸) → ∀𝑖 ∈ ((0..^((♯‘𝑊) − 1)) ∪ {((♯‘𝑊) − 1), (♯‘𝑊)}){(((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘𝑖), (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘(𝑖 + 1))} ∈ 𝐸) | ||
Theorem | clwwlknonex2 28482 | Extending a closed walk 𝑊 on vertex 𝑋 by an additional edge (forth and back) results in a closed walk. (Contributed by AV, 22-Sep-2018.) (Revised by AV, 25-Feb-2022.) (Proof shortened by AV, 28-Mar-2022.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ (((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)) ∧ {𝑋, 𝑌} ∈ 𝐸 ∧ 𝑊 ∈ (𝑋(ClWWalksNOn‘𝐺)(𝑁 − 2))) → ((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉) ∈ (𝑁 ClWWalksN 𝐺)) | ||
Theorem | clwwlknonex2e 28483 | Extending a closed walk 𝑊 on vertex 𝑋 by an additional edge (forth and back) results in a closed walk on vertex 𝑋. (Contributed by AV, 17-Apr-2022.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ (((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘3)) ∧ {𝑋, 𝑌} ∈ 𝐸 ∧ 𝑊 ∈ (𝑋(ClWWalksNOn‘𝐺)(𝑁 − 2))) → ((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉) ∈ (𝑋(ClWWalksNOn‘𝐺)𝑁)) | ||
Theorem | clwwlknondisj 28484* | The sets of closed walks on different vertices are disjunct. (Contributed by Alexander van der Vekens, 7-Oct-2018.) (Revised by AV, 28-May-2021.) (Revised by AV, 3-Mar-2022.) (Proof shortened by AV, 28-Mar-2022.) |
⊢ Disj 𝑥 ∈ 𝑉 (𝑥(ClWWalksNOn‘𝐺)𝑁) | ||
Theorem | clwwlknun 28485* | The set of closed walks of fixed length 𝑁 in a simple graph 𝐺 is the union of the closed walks of the fixed length 𝑁 on each of the vertices of graph 𝐺. (Contributed by Alexander van der Vekens, 7-Oct-2018.) (Revised by AV, 28-May-2021.) (Revised by AV, 3-Mar-2022.) (Proof shortened by AV, 28-Mar-2022.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝐺 ∈ USGraph → (𝑁 ClWWalksN 𝐺) = ∪ 𝑥 ∈ 𝑉 (𝑥(ClWWalksNOn‘𝐺)𝑁)) | ||
Theorem | clwwlkvbij 28486* | There is a bijection between the set of closed walks of a fixed length 𝑁 on a fixed vertex 𝑋 represented by walks (as word) and the set of closed walks (as words) of the fixed length 𝑁 on the fixed vertex 𝑋. The difference between these two representations is that in the first case the fixed vertex is repeated at the end of the word, and in the second case it is not. (Contributed by Alexander van der Vekens, 29-Sep-2018.) (Revised by AV, 26-Apr-2021.) (Revised by AV, 7-Jul-2022.) (Proof shortened by AV, 2-Nov-2022.) |
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → ∃𝑓 𝑓:{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ ((lastS‘𝑤) = (𝑤‘0) ∧ (𝑤‘0) = 𝑋)}–1-1-onto→(𝑋(ClWWalksNOn‘𝐺)𝑁)) | ||
Theorem | 0ewlk 28487 | The empty set (empty sequence of edges) is an s-walk of edges for all s. (Contributed by AV, 4-Jan-2021.) |
⊢ ((𝐺 ∈ V ∧ 𝑆 ∈ ℕ0*) → ∅ ∈ (𝐺 EdgWalks 𝑆)) | ||
Theorem | 1ewlk 28488 | A sequence of 1 edge is an s-walk of edges for all s. (Contributed by AV, 5-Jan-2021.) |
⊢ ((𝐺 ∈ V ∧ 𝑆 ∈ ℕ0* ∧ 𝐼 ∈ dom (iEdg‘𝐺)) → 〈“𝐼”〉 ∈ (𝐺 EdgWalks 𝑆)) | ||
Theorem | 0wlk 28489 | A pair of an empty set (of edges) and a second set (of vertices) is a walk iff the second set contains exactly one vertex. (Contributed by Alexander van der Vekens, 30-Oct-2017.) (Revised by AV, 3-Jan-2021.) (Revised by AV, 30-Oct-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝐺 ∈ 𝑈 → (∅(Walks‘𝐺)𝑃 ↔ 𝑃:(0...0)⟶𝑉)) | ||
Theorem | is0wlk 28490 | A pair of an empty set (of edges) and a sequence of one vertex is a walk (of length 0). (Contributed by AV, 3-Jan-2021.) (Revised by AV, 23-Mar-2021.) (Proof shortened by AV, 30-Oct-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ ((𝑃 = {〈0, 𝑁〉} ∧ 𝑁 ∈ 𝑉) → ∅(Walks‘𝐺)𝑃) | ||
Theorem | 0wlkonlem1 28491 | Lemma 1 for 0wlkon 28493 and 0trlon 28497. (Contributed by AV, 3-Jan-2021.) (Revised by AV, 23-Mar-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ ((𝑃:(0...0)⟶𝑉 ∧ (𝑃‘0) = 𝑁) → (𝑁 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉)) | ||
Theorem | 0wlkonlem2 28492 | Lemma 2 for 0wlkon 28493 and 0trlon 28497. (Contributed by AV, 3-Jan-2021.) (Revised by AV, 23-Mar-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ ((𝑃:(0...0)⟶𝑉 ∧ (𝑃‘0) = 𝑁) → 𝑃 ∈ (𝑉 ↑pm (0...0))) | ||
Theorem | 0wlkon 28493 | A walk of length 0 from a vertex to itself. (Contributed by Alexander van der Vekens, 2-Dec-2017.) (Revised by AV, 3-Jan-2021.) (Revised by AV, 23-Mar-2021.) (Proof shortened by AV, 30-Oct-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ ((𝑃:(0...0)⟶𝑉 ∧ (𝑃‘0) = 𝑁) → ∅(𝑁(WalksOn‘𝐺)𝑁)𝑃) | ||
Theorem | 0wlkons1 28494 | A walk of length 0 from a vertex to itself. (Contributed by AV, 17-Apr-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝑁 ∈ 𝑉 → ∅(𝑁(WalksOn‘𝐺)𝑁)〈“𝑁”〉) | ||
Theorem | 0trl 28495 | A pair of an empty set (of edges) and a second set (of vertices) is a trail iff the second set contains exactly one vertex. (Contributed by Alexander van der Vekens, 30-Oct-2017.) (Revised by AV, 7-Jan-2021.) (Revised by AV, 30-Oct-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝐺 ∈ 𝑈 → (∅(Trails‘𝐺)𝑃 ↔ 𝑃:(0...0)⟶𝑉)) | ||
Theorem | is0trl 28496 | A pair of an empty set (of edges) and a sequence of one vertex is a trail (of length 0). (Contributed by AV, 7-Jan-2021.) (Revised by AV, 23-Mar-2021.) (Proof shortened by AV, 30-Oct-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ ((𝑃 = {〈0, 𝑁〉} ∧ 𝑁 ∈ 𝑉) → ∅(Trails‘𝐺)𝑃) | ||
Theorem | 0trlon 28497 | A trail of length 0 from a vertex to itself. (Contributed by Alexander van der Vekens, 2-Dec-2017.) (Revised by AV, 8-Jan-2021.) (Revised by AV, 23-Mar-2021.) (Proof shortened by AV, 30-Oct-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ ((𝑃:(0...0)⟶𝑉 ∧ (𝑃‘0) = 𝑁) → ∅(𝑁(TrailsOn‘𝐺)𝑁)𝑃) | ||
Theorem | 0pth 28498 | A pair of an empty set (of edges) and a second set (of vertices) is a path iff the second set contains exactly one vertex. (Contributed by Alexander van der Vekens, 30-Oct-2017.) (Revised by AV, 19-Jan-2021.) (Revised by AV, 30-Oct-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝐺 ∈ 𝑊 → (∅(Paths‘𝐺)𝑃 ↔ 𝑃:(0...0)⟶𝑉)) | ||
Theorem | 0spth 28499 | A pair of an empty set (of edges) and a second set (of vertices) is a simple path iff the second set contains exactly one vertex. (Contributed by Alexander van der Vekens, 30-Oct-2017.) (Revised by AV, 18-Jan-2021.) (Revised by AV, 30-Oct-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝐺 ∈ 𝑊 → (∅(SPaths‘𝐺)𝑃 ↔ 𝑃:(0...0)⟶𝑉)) | ||
Theorem | 0pthon 28500 | A path of length 0 from a vertex to itself. (Contributed by Alexander van der Vekens, 3-Dec-2017.) (Revised by AV, 20-Jan-2021.) (Revised by AV, 30-Oct-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ ((𝑃:(0...0)⟶𝑉 ∧ (𝑃‘0) = 𝑁) → ∅(𝑁(PathsOn‘𝐺)𝑁)𝑃) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |