Home | Metamath
Proof Explorer Theorem List (p. 270 of 426) | < 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-27775) |
Hilbert Space Explorer
(27776-29300) |
Users' Mathboxes
(29301-42551) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | clwlkclwwlklem2 26901* | Lemma 2 for clwlkclwwlk 26903. (Contributed by Alexander van der Vekens, 22-Jun-2018.) (Revised by AV, 11-Apr-2021.) |
⊢ (((𝐸:dom 𝐸–1-1→𝑅 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (𝑃:(0...(#‘𝐹))⟶𝑉 ∧ 2 ≤ (#‘𝑃)) ∧ (∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∧ (𝑃‘0) = (𝑃‘(#‘𝐹)))) → (( lastS ‘𝑃) = (𝑃‘0) ∧ ∀𝑖 ∈ (0..^((#‘𝐹) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((#‘𝐹) − 1)), (𝑃‘0)} ∈ ran 𝐸)) | ||
Theorem | clwlkclwwlklem3 26902* | Lemma 3 for clwlkclwwlk 26903. (Contributed by Alexander van der Vekens, 22-Jun-2018.) (Revised by AV, 11-Apr-2021.) |
⊢ ((𝐸:dom 𝐸–1-1→𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) → (∃𝑓((𝑓 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝑓))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(#‘𝑓))(𝐸‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) ∧ (𝑃‘0) = (𝑃‘(#‘𝑓))) ↔ (( lastS ‘𝑃) = (𝑃‘0) ∧ (∀𝑖 ∈ (0..^((((#‘𝑃) − 1) − 0) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((#‘𝑃) − 2)), (𝑃‘0)} ∈ ran 𝐸)))) | ||
Theorem | clwlkclwwlk 26903* | A closed walk as word of length at least 2 corresponds to a closed walk in a simple pseudograph. (Contributed by Alexander van der Vekens, 22-Jun-2018.) (Revised by AV, 24-Apr-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (iEdg‘𝐺) ⇒ ⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) → (∃𝑓 𝑓(ClWalks‘𝐺)𝑃 ↔ (( lastS ‘𝑃) = (𝑃‘0) ∧ (𝑃 substr 〈0, ((#‘𝑃) − 1)〉) ∈ (ClWWalks‘𝐺)))) | ||
Theorem | clwlkclwwlk2 26904* | A closed walk corresponds to a closed walk as word in a simple pseudograph. (Contributed by Alexander van der Vekens, 22-Jun-2018.) (Revised by AV, 24-Apr-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (iEdg‘𝐺) ⇒ ⊢ ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ (#‘𝑃)) → (∃𝑓 𝑓(ClWalks‘𝐺)(𝑃 ++ 〈“(𝑃‘0)”〉) ↔ 𝑃 ∈ (ClWWalks‘𝐺))) | ||
Theorem | clwwlkinwwlk 26905 | 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.) |
⊢ (((𝑁 ∈ ℕ ∧ 𝑀 ∈ (ℤ≥‘𝑁)) ∧ 𝑊 ∈ (𝑀 WWalksN 𝐺) ∧ (𝑊‘𝑁) = (𝑊‘0)) → (𝑊 substr 〈0, 𝑁〉) ∈ (𝑁 ClWWalksN 𝐺)) | ||
Theorem | clwwlksgt0 26906 | There is no empty closed walk (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.) |
⊢ (𝑊 ∈ (ClWWalks‘𝐺) → 0 < (#‘𝑊)) | ||
Theorem | clwwlksn0 26907 | 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 | clwwlks1loop 26908 | A closed walk of length 1 is a loop. See also clwlkl1loop 26678. (Contributed by AV, 24-Apr-2021.) |
⊢ ((𝑊 ∈ (ClWWalks‘𝐺) ∧ (#‘𝑊) = 1) → {(𝑊‘0), (𝑊‘0)} ∈ (Edg‘𝐺)) | ||
Theorem | clwwlksn1loop 26909 | A closed walk of length 1 is a loop. (Contributed by AV, 24-Apr-2021.) |
⊢ (𝑊 ∈ (1 ClWWalksN 𝐺) → ((#‘𝑊) = 1 ∧ {(𝑊‘0), (𝑊‘0)} ∈ (Edg‘𝐺))) | ||
Theorem | clwwlksn2 26910 | 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 | clwwlkssswrd 26911 | Closed walks (represented by words) are words. (Contributed by Alexander van der Vekens, 25-Mar-2018.) (Revised by AV, 25-Apr-2021.) |
⊢ (ClWWalks‘𝐺) ⊆ Word (Vtx‘𝐺) | ||
Theorem | umgrclwwlksge2 26912 | A closed walk in a multigraph has a length of at least 2 (because it cannot have a loop). (Contributed by Alexander van der Vekens, 16-Sep-2018.) (Revised by AV, 24-Apr-2021.) |
⊢ (𝐺 ∈ UMGraph → (𝑃 ∈ (ClWWalks‘𝐺) → 2 ≤ (#‘𝑃))) | ||
Theorem | clwwlksnfi 26913 | 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.) |
⊢ ((Vtx‘𝐺) ∈ Fin → (𝑁 ClWWalksN 𝐺) ∈ Fin) | ||
Theorem | clwwlksel 26914* | 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 | clwwlksf 26915* | Lemma 1 for clwwlksbij 26920: F is a function. (Contributed by Alexander van der Vekens, 27-Sep-2018.) (Revised by AV, 26-Apr-2021.) |
⊢ 𝐷 = {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ ( lastS ‘𝑤) = (𝑤‘0)} & ⊢ 𝐹 = (𝑡 ∈ 𝐷 ↦ (𝑡 substr 〈0, 𝑁〉)) ⇒ ⊢ (𝑁 ∈ ℕ → 𝐹:𝐷⟶(𝑁 ClWWalksN 𝐺)) | ||
Theorem | clwwlksfv 26916* | Lemma 2 for clwwlksbij 26920: the value of function F. (Contributed by Alexander van der Vekens, 28-Sep-2018.) (Revised by AV, 26-Apr-2021.) |
⊢ 𝐷 = {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ ( lastS ‘𝑤) = (𝑤‘0)} & ⊢ 𝐹 = (𝑡 ∈ 𝐷 ↦ (𝑡 substr 〈0, 𝑁〉)) ⇒ ⊢ (𝑊 ∈ 𝐷 → (𝐹‘𝑊) = (𝑊 substr 〈0, 𝑁〉)) | ||
Theorem | clwwlksf1 26917* | Lemma 3 for clwwlksbij 26920: F is a 1-1 function. (Contributed by AV, 28-Sep-2018.) (Revised by AV, 26-Apr-2021.) |
⊢ 𝐷 = {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ ( lastS ‘𝑤) = (𝑤‘0)} & ⊢ 𝐹 = (𝑡 ∈ 𝐷 ↦ (𝑡 substr 〈0, 𝑁〉)) ⇒ ⊢ (𝑁 ∈ ℕ → 𝐹:𝐷–1-1→(𝑁 ClWWalksN 𝐺)) | ||
Theorem | clwwlksfo 26918* | Lemma 4 for clwwlksbij 26920: F is an onto function. (Contributed by Alexander van der Vekens, 29-Sep-2018.) (Revised by AV, 26-Apr-2021.) |
⊢ 𝐷 = {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ ( lastS ‘𝑤) = (𝑤‘0)} & ⊢ 𝐹 = (𝑡 ∈ 𝐷 ↦ (𝑡 substr 〈0, 𝑁〉)) ⇒ ⊢ (𝑁 ∈ ℕ → 𝐹:𝐷–onto→(𝑁 ClWWalksN 𝐺)) | ||
Theorem | clwwlksf1o 26919* | Lemma 5 for clwwlksbij 26920: F is a 1-1 onto function. (Contributed by Alexander van der Vekens, 29-Sep-2018.) (Revised by AV, 26-Apr-2021.) |
⊢ 𝐷 = {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ ( lastS ‘𝑤) = (𝑤‘0)} & ⊢ 𝐹 = (𝑡 ∈ 𝐷 ↦ (𝑡 substr 〈0, 𝑁〉)) ⇒ ⊢ (𝑁 ∈ ℕ → 𝐹:𝐷–1-1-onto→(𝑁 ClWWalksN 𝐺)) | ||
Theorem | clwwlksbij 26920* | There is a bijection between the set of closed walks of a fixed length represented by walks (as word) and the set of closed walks (as words) of a 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.) |
⊢ (𝑁 ∈ ℕ → ∃𝑓 𝑓:{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ ( lastS ‘𝑤) = (𝑤‘0)}–1-1-onto→(𝑁 ClWWalksN 𝐺)) | ||
Theorem | clwwlksnwwlkncl 26921* | 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.) |
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (𝑁 ClWWalksN 𝐺)) → (𝑃 ++ 〈“(𝑃‘0)”〉) ∈ {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ ( lastS ‘𝑤) = (𝑤‘0)}) | ||
Theorem | clwwlksvbij 26922* | There is a bijection between the set of closed walks of a fixed length starting at a fixed vertex represented by walks (as word) and the set of closed walks (as words) of a fixed length starting at a fixed vertex. 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.) |
⊢ (𝑁 ∈ ℕ → ∃𝑓 𝑓:{𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (( lastS ‘𝑤) = (𝑤‘0) ∧ (𝑤‘0) = 𝑆)}–1-1-onto→{𝑤 ∈ (𝑁 ClWWalksN 𝐺) ∣ (𝑤‘0) = 𝑆}) | ||
Theorem | clwwlksext2edg 26923 | 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.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2)) ∧ (𝑊 ++ 〈“𝑍”〉) ∈ (𝑁 ClWWalksN 𝐺)) → ({( lastS ‘𝑊), 𝑍} ∈ 𝐸 ∧ {𝑍, (𝑊‘0)} ∈ 𝐸)) | ||
Theorem | wwlksext2clwwlk 26924 | 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.) |
⊢ 𝑉 = (Vtx‘𝐺) & ⊢ 𝐸 = (Edg‘𝐺) ⇒ ⊢ ((𝑊 ∈ (𝑁 WWalksN 𝐺) ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → (({( lastS ‘𝑊), 𝑍} ∈ 𝐸 ∧ {𝑍, (𝑊‘0)} ∈ 𝐸) → (𝑊 ++ 〈“𝑍”〉) ∈ ((𝑁 + 2) ClWWalksN 𝐺))) | ||
Theorem | wwlksubclwwlks 26925 | 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.) |
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → (𝑋 ∈ (𝑁 ClWWalksN 𝐺) → (𝑋 substr 〈0, 𝑀〉) ∈ ((𝑀 − 1) WWalksN 𝐺))) | ||
Theorem | clwwisshclwwslemlem 26926* | Lemma for clwwisshclwwslem 26927. (Contributed by Alexander van der Vekens, 23-Mar-2018.) |
⊢ (((𝐿 ∈ (ℤ≥‘2) ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ ∀𝑖 ∈ (0..^(𝐿 − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝑅 ∧ {(𝑊‘(𝐿 − 1)), (𝑊‘0)} ∈ 𝑅) → {(𝑊‘((𝐴 + 𝐵) mod 𝐿)), (𝑊‘(((𝐴 + 1) + 𝐵) mod 𝐿))} ∈ 𝑅) | ||
Theorem | clwwisshclwwslem 26927* | Lemma for clwwisshclwws 26928. (Contributed by AV, 24-Mar-2018.) (Revised by AV, 28-Apr-2021.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (1..^(#‘𝑊))) → ((∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ 𝐸) → ∀𝑗 ∈ (0..^((#‘(𝑊 cyclShift 𝑁)) − 1)){((𝑊 cyclShift 𝑁)‘𝑗), ((𝑊 cyclShift 𝑁)‘(𝑗 + 1))} ∈ 𝐸)) | ||
Theorem | clwwisshclwws 26928 | Cyclically shifting a closed walk as word results in a closed walk as word (in an undirected graph). (Contributed by Alexander van der Vekens, 24-Mar-2018.) (Revised by AV, 28-Apr-2021.) |
⊢ ((𝑊 ∈ (ClWWalks‘𝐺) ∧ 𝑁 ∈ (0..^(#‘𝑊))) → (𝑊 cyclShift 𝑁) ∈ (ClWWalks‘𝐺)) | ||
Theorem | clwwisshclwwsn 26929 | Cyclically shifting a closed walk as word results in a closed walk as word (in an undirected graph). (Contributed by Alexander van der Vekens, 15-Jun-2018.) (Revised by AV, 29-Apr-2021.) |
⊢ ((𝑊 ∈ (ClWWalks‘𝐺) ∧ 𝑁 ∈ (0...(#‘𝑊))) → (𝑊 cyclShift 𝑁) ∈ (ClWWalks‘𝐺)) | ||
Theorem | clwwnisshclwwsn 26930 | 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.) |
⊢ ((𝑊 ∈ (𝑁 ClWWalksN 𝐺) ∧ 𝑀 ∈ (0...𝑁)) → (𝑊 cyclShift 𝑀) ∈ (𝑁 ClWWalksN 𝐺)) | ||
Theorem | erclwwlksrel 26931 | ∼ is a relation. (Contributed by Alexander van der Vekens, 25-Mar-2018.) (Revised by AV, 29-Apr-2021.) |
⊢ ∼ = {〈𝑢, 𝑤〉 ∣ (𝑢 ∈ (ClWWalks‘𝐺) ∧ 𝑤 ∈ (ClWWalks‘𝐺) ∧ ∃𝑛 ∈ (0...(#‘𝑤))𝑢 = (𝑤 cyclShift 𝑛))} ⇒ ⊢ Rel ∼ | ||
Theorem | erclwwlkseq 26932* | Two classes are equivalent regarding ∼ if both are words and one is the other cyclically shifted. (Contributed by Alexander van der Vekens, 25-Mar-2018.) (Revised by AV, 29-Apr-2021.) |
⊢ ∼ = {〈𝑢, 𝑤〉 ∣ (𝑢 ∈ (ClWWalks‘𝐺) ∧ 𝑤 ∈ (ClWWalks‘𝐺) ∧ ∃𝑛 ∈ (0...(#‘𝑤))𝑢 = (𝑤 cyclShift 𝑛))} ⇒ ⊢ ((𝑈 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌) → (𝑈 ∼ 𝑊 ↔ (𝑈 ∈ (ClWWalks‘𝐺) ∧ 𝑊 ∈ (ClWWalks‘𝐺) ∧ ∃𝑛 ∈ (0...(#‘𝑊))𝑈 = (𝑊 cyclShift 𝑛)))) | ||
Theorem | erclwwlkseqlen 26933* | 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, 29-Apr-2021.) |
⊢ ∼ = {〈𝑢, 𝑤〉 ∣ (𝑢 ∈ (ClWWalks‘𝐺) ∧ 𝑤 ∈ (ClWWalks‘𝐺) ∧ ∃𝑛 ∈ (0...(#‘𝑤))𝑢 = (𝑤 cyclShift 𝑛))} ⇒ ⊢ ((𝑈 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌) → (𝑈 ∼ 𝑊 → (#‘𝑈) = (#‘𝑊))) | ||
Theorem | erclwwlksref 26934* | ∼ is a reflexive relation over the set of closed walks (defined as words). (Contributed by Alexander van der Vekens, 25-Mar-2018.) (Revised by AV, 29-Apr-2021.) |
⊢ ∼ = {〈𝑢, 𝑤〉 ∣ (𝑢 ∈ (ClWWalks‘𝐺) ∧ 𝑤 ∈ (ClWWalks‘𝐺) ∧ ∃𝑛 ∈ (0...(#‘𝑤))𝑢 = (𝑤 cyclShift 𝑛))} ⇒ ⊢ (𝑥 ∈ (ClWWalks‘𝐺) ↔ 𝑥 ∼ 𝑥) | ||
Theorem | erclwwlkssym 26935* | ∼ is a symmetric relation over the set of closed walks (defined as words). (Contributed by Alexander van der Vekens, 8-Apr-2018.) (Revised by AV, 29-Apr-2021.) |
⊢ ∼ = {〈𝑢, 𝑤〉 ∣ (𝑢 ∈ (ClWWalks‘𝐺) ∧ 𝑤 ∈ (ClWWalks‘𝐺) ∧ ∃𝑛 ∈ (0...(#‘𝑤))𝑢 = (𝑤 cyclShift 𝑛))} ⇒ ⊢ (𝑥 ∼ 𝑦 → 𝑦 ∼ 𝑥) | ||
Theorem | erclwwlkstr 26936* | ∼ 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.) |
⊢ ∼ = {〈𝑢, 𝑤〉 ∣ (𝑢 ∈ (ClWWalks‘𝐺) ∧ 𝑤 ∈ (ClWWalks‘𝐺) ∧ ∃𝑛 ∈ (0...(#‘𝑤))𝑢 = (𝑤 cyclShift 𝑛))} ⇒ ⊢ ((𝑥 ∼ 𝑦 ∧ 𝑦 ∼ 𝑧) → 𝑥 ∼ 𝑧) | ||
Theorem | erclwwlks 26937* | ∼ is an equivalence 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.) |
⊢ ∼ = {〈𝑢, 𝑤〉 ∣ (𝑢 ∈ (ClWWalks‘𝐺) ∧ 𝑤 ∈ (ClWWalks‘𝐺) ∧ ∃𝑛 ∈ (0...(#‘𝑤))𝑢 = (𝑤 cyclShift 𝑛))} ⇒ ⊢ ∼ Er (ClWWalks‘𝐺) | ||
Theorem | eleclclwwlksnlem1 26938* | Lemma 1 for eleclclwwlksn 26953. (Contributed by Alexander van der Vekens, 11-May-2018.) (Revised by AV, 30-Apr-2021.) |
⊢ 𝑊 = (𝑁 ClWWalksN 𝐺) ⇒ ⊢ ((𝐾 ∈ (0...𝑁) ∧ (𝑋 ∈ 𝑊 ∧ 𝑌 ∈ 𝑊)) → ((𝑋 = (𝑌 cyclShift 𝐾) ∧ ∃𝑚 ∈ (0...𝑁)𝑍 = (𝑌 cyclShift 𝑚)) → ∃𝑛 ∈ (0...𝑁)𝑍 = (𝑋 cyclShift 𝑛))) | ||
Theorem | eleclclwwlksnlem2 26939* | Lemma 2 for eleclclwwlksn 26953. (Contributed by Alexander van der Vekens, 11-May-2018.) (Revised by AV, 30-Apr-2021.) |
⊢ 𝑊 = (𝑁 ClWWalksN 𝐺) ⇒ ⊢ (((𝑘 ∈ (0...𝑁) ∧ 𝑋 = (𝑥 cyclShift 𝑘)) ∧ (𝑋 ∈ 𝑊 ∧ 𝑥 ∈ 𝑊)) → (∃𝑚 ∈ (0...𝑁)𝑌 = (𝑥 cyclShift 𝑚) ↔ ∃𝑛 ∈ (0...𝑁)𝑌 = (𝑋 cyclShift 𝑛))) | ||
Theorem | clwwlksnscsh 26940* | 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 | umgr2cwwk2dif 26941 | 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 26942* | 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 | erclwwlksnrel 26943 | ∼ is a relation. (Contributed by Alexander van der Vekens, 25-Mar-2018.) (Revised by AV, 30-Apr-2021.) |
⊢ 𝑊 = (𝑁 ClWWalksN 𝐺) & ⊢ ∼ = {〈𝑡, 𝑢〉 ∣ (𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊 ∧ ∃𝑛 ∈ (0...𝑁)𝑡 = (𝑢 cyclShift 𝑛))} ⇒ ⊢ Rel ∼ | ||
Theorem | erclwwlksneq 26944* | 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 | erclwwlksneqlen 26945* | 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 | erclwwlksnref 26946* | ∼ 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.) |
⊢ 𝑊 = (𝑁 ClWWalksN 𝐺) & ⊢ ∼ = {〈𝑡, 𝑢〉 ∣ (𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊 ∧ ∃𝑛 ∈ (0...𝑁)𝑡 = (𝑢 cyclShift 𝑛))} ⇒ ⊢ (𝑥 ∈ 𝑊 ↔ 𝑥 ∼ 𝑥) | ||
Theorem | erclwwlksnsym 26947* | ∼ 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 | erclwwlksntr 26948* | ∼ 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 | erclwwlksn 26949* | ∼ 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 | qerclwwlksnfi 26950* | 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 | hashclwwlksn0 26951* | 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 | eclclwwlksn1 26952* | 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 | eleclclwwlksn 26953* | 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 | hashecclwwlksn1 26954* | 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 26955* | 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 26956* | 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 | clwwlksndivn 26957 | The size of the set of closed walks (defined as words) of length n is divisible by n. (Contributed by Alexander van der Vekens, 17-Jun-2018.) (Revised by AV, 2-May-2021.) |
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → 𝑁 ∥ (#‘(𝑁 ClWWalksN 𝐺))) | ||
Theorem | clwlksfclwwlk2wrd 26958* | The second component of a closed walk is a word over the "vertices". (Contributed by Alexander van der Vekens, 25-Jun-2018.) (Revised by AV, 2-May-2021.) |
⊢ 𝐴 = (1st ‘𝑐) & ⊢ 𝐵 = (2nd ‘𝑐) & ⊢ 𝐶 = {𝑐 ∈ (ClWalks‘𝐺) ∣ (#‘𝐴) = 𝑁} & ⊢ 𝐹 = (𝑐 ∈ 𝐶 ↦ (𝐵 substr 〈0, (#‘𝐴)〉)) ⇒ ⊢ (𝑐 ∈ 𝐶 → 𝐵 ∈ Word (Vtx‘𝐺)) | ||
Theorem | clwlksfclwwlk1hashn 26959* | The size of the first component of a closed walk. (Contributed by Alexander van der Vekens, 5-Jul-2018.) (Revised by AV, 2-May-2021.) |
⊢ 𝐴 = (1st ‘𝑐) & ⊢ 𝐵 = (2nd ‘𝑐) & ⊢ 𝐶 = {𝑐 ∈ (ClWalks‘𝐺) ∣ (#‘𝐴) = 𝑁} & ⊢ 𝐹 = (𝑐 ∈ 𝐶 ↦ (𝐵 substr 〈0, (#‘𝐴)〉)) ⇒ ⊢ (𝑊 ∈ 𝐶 → (#‘(1st ‘𝑊)) = 𝑁) | ||
Theorem | clwlksfclwwlk1hash 26960* | The size of the first component of a closed walk is an integer in the range between 0 and the size of the second component. (Contributed by Alexander van der Vekens, 25-Jun-2018.) (Revised by AV, 2-May-2021.) |
⊢ 𝐴 = (1st ‘𝑐) & ⊢ 𝐵 = (2nd ‘𝑐) & ⊢ 𝐶 = {𝑐 ∈ (ClWalks‘𝐺) ∣ (#‘𝐴) = 𝑁} & ⊢ 𝐹 = (𝑐 ∈ 𝐶 ↦ (𝐵 substr 〈0, (#‘𝐴)〉)) ⇒ ⊢ (𝑐 ∈ 𝐶 → (#‘𝐴) ∈ (0...(#‘𝐵))) | ||
Theorem | clwlksfclwwlk2sswd 26961* | The size of a subword of the second component of a closed walk with length of the size of the second component. (Contributed by Alexander van der Vekens, 25-Jun-2018.) (Revised by AV, 2-May-2021.) |
⊢ 𝐴 = (1st ‘𝑐) & ⊢ 𝐵 = (2nd ‘𝑐) & ⊢ 𝐶 = {𝑐 ∈ (ClWalks‘𝐺) ∣ (#‘𝐴) = 𝑁} & ⊢ 𝐹 = (𝑐 ∈ 𝐶 ↦ (𝐵 substr 〈0, (#‘𝐴)〉)) ⇒ ⊢ (𝑐 ∈ 𝐶 → (#‘𝐴) = (#‘(𝐵 substr 〈0, (#‘𝐴)〉))) | ||
Theorem | clwlksfclwwlk 26962* | There is a function between the set of closed walks (defined as words) of length n and the set of closed walks of length n. (Contributed by Alexander van der Vekens, 25-Jun-2018.) (Revised by AV, 2-May-2021.) |
⊢ 𝐴 = (1st ‘𝑐) & ⊢ 𝐵 = (2nd ‘𝑐) & ⊢ 𝐶 = {𝑐 ∈ (ClWalks‘𝐺) ∣ (#‘𝐴) = 𝑁} & ⊢ 𝐹 = (𝑐 ∈ 𝐶 ↦ (𝐵 substr 〈0, (#‘𝐴)〉)) ⇒ ⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → 𝐹:𝐶⟶(𝑁 ClWWalksN 𝐺)) | ||
Theorem | clwlksfoclwwlk 26963* | There is an onto function between the set of closed walks (defined as words) of length n and the set of closed walks of length n. (Contributed by Alexander van der Vekens, 30-Jun-2018.) (Revised by AV, 2-May-2021.) |
⊢ 𝐴 = (1st ‘𝑐) & ⊢ 𝐵 = (2nd ‘𝑐) & ⊢ 𝐶 = {𝑐 ∈ (ClWalks‘𝐺) ∣ (#‘𝐴) = 𝑁} & ⊢ 𝐹 = (𝑐 ∈ 𝐶 ↦ (𝐵 substr 〈0, (#‘𝐴)〉)) ⇒ ⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → 𝐹:𝐶–onto→(𝑁 ClWWalksN 𝐺)) | ||
Theorem | clwlksf1clwwlklem0 26964* | Lemma 1 for clwlksf1clwwlklem 26968. (Contributed by AV, 3-May-2021.) |
⊢ 𝐴 = (1st ‘𝑐) & ⊢ 𝐵 = (2nd ‘𝑐) & ⊢ 𝐶 = {𝑐 ∈ (ClWalks‘𝐺) ∣ (#‘𝐴) = 𝑁} & ⊢ 𝐹 = (𝑐 ∈ 𝐶 ↦ (𝐵 substr 〈0, (#‘𝐴)〉)) ⇒ ⊢ (𝑊 ∈ 𝐶 → (((1st ‘𝑊) ∈ Word dom (iEdg‘𝐺) ∧ (2nd ‘𝑊):(0...(#‘(1st ‘𝑊)))⟶(Vtx‘𝐺) ∧ ((2nd ‘𝑊)‘0) = ((2nd ‘𝑊)‘(#‘(1st ‘𝑊)))) ∧ (#‘(1st ‘𝑊)) = 𝑁)) | ||
Theorem | clwlksf1clwwlklem1 26965* | Lemma 1 for clwlksf1clwwlklem 26968. (Contributed by Alexander van der Vekens, 5-Jul-2018.) (Revised by AV, 3-May-2021.) |
⊢ 𝐴 = (1st ‘𝑐) & ⊢ 𝐵 = (2nd ‘𝑐) & ⊢ 𝐶 = {𝑐 ∈ (ClWalks‘𝐺) ∣ (#‘𝐴) = 𝑁} & ⊢ 𝐹 = (𝑐 ∈ 𝐶 ↦ (𝐵 substr 〈0, (#‘𝐴)〉)) ⇒ ⊢ (𝑊 ∈ 𝐶 → 𝑁 ≤ (#‘(2nd ‘𝑊))) | ||
Theorem | clwlksf1clwwlklem2 26966* | Lemma 2 for clwlksf1clwwlklem 26968. (Contributed by Alexander van der Vekens, 5-Jul-2018.) (Revised by AV, 3-May-2021.) |
⊢ 𝐴 = (1st ‘𝑐) & ⊢ 𝐵 = (2nd ‘𝑐) & ⊢ 𝐶 = {𝑐 ∈ (ClWalks‘𝐺) ∣ (#‘𝐴) = 𝑁} & ⊢ 𝐹 = (𝑐 ∈ 𝐶 ↦ (𝐵 substr 〈0, (#‘𝐴)〉)) ⇒ ⊢ (𝑊 ∈ 𝐶 → ((2nd ‘𝑊)‘0) = ((2nd ‘𝑊)‘𝑁)) | ||
Theorem | clwlksf1clwwlklem3 26967* | Lemma 3 for clwlksf1clwwlklem 26968. (Contributed by Alexander van der Vekens, 5-Jul-2018.) (Revised by AV, 3-May-2021.) |
⊢ 𝐴 = (1st ‘𝑐) & ⊢ 𝐵 = (2nd ‘𝑐) & ⊢ 𝐶 = {𝑐 ∈ (ClWalks‘𝐺) ∣ (#‘𝐴) = 𝑁} & ⊢ 𝐹 = (𝑐 ∈ 𝐶 ↦ (𝐵 substr 〈0, (#‘𝐴)〉)) ⇒ ⊢ (𝑊 ∈ 𝐶 → (2nd ‘𝑊) ∈ Word (Vtx‘𝐺)) | ||
Theorem | clwlksf1clwwlklem 26968* | Lemma for clwlksf1clwwlk 26969. (Contributed by Alexander van der Vekens, 5-Jul-2018.) (Revised by AV, 3-May-2021.) |
⊢ 𝐴 = (1st ‘𝑐) & ⊢ 𝐵 = (2nd ‘𝑐) & ⊢ 𝐶 = {𝑐 ∈ (ClWalks‘𝐺) ∣ (#‘𝐴) = 𝑁} & ⊢ 𝐹 = (𝑐 ∈ 𝐶 ↦ (𝐵 substr 〈0, (#‘𝐴)〉)) ⇒ ⊢ ((𝑁 ∈ ℕ ∧ 𝑈 ∈ 𝐶 ∧ 𝑊 ∈ 𝐶) → (((2nd ‘𝑈) substr 〈0, (#‘(1st ‘𝑈))〉) = ((2nd ‘𝑊) substr 〈0, (#‘(1st ‘𝑊))〉) → ∀𝑦 ∈ (0...𝑁)((2nd ‘𝑈)‘𝑦) = ((2nd ‘𝑊)‘𝑦))) | ||
Theorem | clwlksf1clwwlk 26969* | There is a one-to-one function between the set of closed walks (defined as words) of length n and the set of closed walks of length n (in an undirected simple graph). (Contributed by Alexander van der Vekens, 5-Jul-2018.) (Revised by AV, 3-May-2021.) |
⊢ 𝐴 = (1st ‘𝑐) & ⊢ 𝐵 = (2nd ‘𝑐) & ⊢ 𝐶 = {𝑐 ∈ (ClWalks‘𝐺) ∣ (#‘𝐴) = 𝑁} & ⊢ 𝐹 = (𝑐 ∈ 𝐶 ↦ (𝐵 substr 〈0, (#‘𝐴)〉)) ⇒ ⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → 𝐹:𝐶–1-1→(𝑁 ClWWalksN 𝐺)) | ||
Theorem | clwlksf1oclwwlk 26970* | There is a one-to-one onto function between the set of closed walks (defined as words) of length n and the set of closed walks of length n (in an undirected simple graph). (Contributed by Alexander van der Vekens, 5-Jul-2018.) (Revised by AV, 3-May-2021.) |
⊢ 𝐴 = (1st ‘𝑐) & ⊢ 𝐵 = (2nd ‘𝑐) & ⊢ 𝐶 = {𝑐 ∈ (ClWalks‘𝐺) ∣ (#‘𝐴) = 𝑁} & ⊢ 𝐹 = (𝑐 ∈ 𝐶 ↦ (𝐵 substr 〈0, (#‘𝐴)〉)) ⇒ ⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → 𝐹:𝐶–1-1-onto→(𝑁 ClWWalksN 𝐺)) | ||
Theorem | clwlkssizeeq 26971* | The size of the set of closed walks (defined as words) of length n corresponds to the size of the set of closed walks of length n (in an undirected simple graph). (Contributed by Alexander van der Vekens, 6-Jul-2018.) (Revised by AV, 4-May-2021.) |
⊢ ((𝐺 ∈ FinUSGraph ∧ 𝑁 ∈ ℙ) → (#‘(𝑁 ClWWalksN 𝐺)) = (#‘{𝑐 ∈ (ClWalks‘𝐺) ∣ (#‘(1st ‘𝑐)) = 𝑁})) | ||
Theorem | clwlksndivn 26972* | The size of the set of closed walks of length n is divisible by n. 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 ‘𝑐)) = 𝑁})) | ||
Theorem | clwwlksndisj 26973* | The sets of closed walks starting at different vertices are disjunct. (Contributed by Alexander van der Vekens, 7-Oct-2018.) (Revised by AV, 28-May-2021.) |
⊢ Disj 𝑥 ∈ 𝑉 {𝑤 ∈ (𝑁 ClWWalksN 𝐺) ∣ (𝑤‘0) = 𝑥} | ||
Theorem | clwwlksnun 26974* | The set of closed walks of fixed length in a simple graph is the union of the closed walks of the fixed length starting at each of the vertices. (Contributed by Alexander van der Vekens, 7-Oct-2018.) (Revised by AV, 28-May-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ ((𝐺 ∈ USGraph ∧ 𝑁 ∈ ℕ0) → (𝑁 ClWWalksN 𝐺) = ∪ 𝑥 ∈ 𝑉 {𝑤 ∈ (𝑁 ClWWalksN 𝐺) ∣ (𝑤‘0) = 𝑥}) | ||
Theorem | 0ewlk 26975 | 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 26976 | 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 26977 | 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 26978 | 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 26979 | Lemma 1 for 0wlkon 26981 and 0trlon 26985. (Contributed by AV, 3-Jan-2021.) (Revised by AV, 23-Mar-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ ((𝑃:(0...0)⟶𝑉 ∧ (𝑃‘0) = 𝑁) → (𝑁 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉)) | ||
Theorem | 0wlkonlem2 26980 | Lemma 2 for 0wlkon 26981 and 0trlon 26985. (Contributed by AV, 3-Jan-2021.) (Revised by AV, 23-Mar-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ ((𝑃:(0...0)⟶𝑉 ∧ (𝑃‘0) = 𝑁) → 𝑃 ∈ (𝑉 ↑pm (0...0))) | ||
Theorem | 0wlkon 26981 | 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 26982 | A walk of length 0 from a vertex to itself. (Contributed by AV, 17-Apr-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝑁 ∈ 𝑉 → ∅(𝑁(WalksOn‘𝐺)𝑁)〈“𝑁”〉) | ||
Theorem | 0trl 26983 | 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 26984 | 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 26985 | 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 26986 | 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 26987 | 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 26988 | A path of length 0 from a vertex to itself. (Contributed by Alexander van der Vekens, 3-Dec-2017.) (Revised by AV, 20-Jan-2021.) (Revised by AV, 30-Oct-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ ((𝑃:(0...0)⟶𝑉 ∧ (𝑃‘0) = 𝑁) → ∅(𝑁(PathsOn‘𝐺)𝑁)𝑃) | ||
Theorem | 0pthon1 26989 | A path of length 0 from a vertex to itself. (Contributed by Alexander van der Vekens, 3-Dec-2017.) (Revised by AV, 20-Jan-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝑁 ∈ 𝑉 → ∅(𝑁(PathsOn‘𝐺)𝑁){〈0, 𝑁〉}) | ||
Theorem | 0pthonv 26990* | For each vertex there is a path of length 0 from the vertex to itself. (Contributed by Alexander van der Vekens, 3-Dec-2017.) (Revised by AV, 21-Jan-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝑁 ∈ 𝑉 → ∃𝑓∃𝑝 𝑓(𝑁(PathsOn‘𝐺)𝑁)𝑝) | ||
Theorem | 0clwlk 26991 | A pair of an empty set (of edges) and a second set (of vertices) is a closed walk if and only if the second set contains exactly one vertex (in an undirected graph). (Contributed by Alexander van der Vekens, 15-Mar-2018.) (Revised by AV, 17-Feb-2021.) (Revised by AV, 30-Oct-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝐺 ∈ 𝑋 → (∅(ClWalks‘𝐺)𝑃 ↔ 𝑃:(0...0)⟶𝑉)) | ||
Theorem | 0clwlk0 26992 | There is no closed walk in the empty set (i.e. the null graph). (Contributed by Alexander van der Vekens, 2-Sep-2018.) (Revised by AV, 5-Mar-2021.) |
⊢ (ClWalks‘∅) = ∅ | ||
Theorem | 0crct 26993 | A pair of an empty set (of edges) and a second set (of vertices) is a circuit if and only if the second set contains exactly one vertex (in an undirected graph). (Contributed by Alexander van der Vekens, 30-Oct-2017.) (Revised by AV, 31-Jan-2021.) (Revised by AV, 30-Oct-2021.) |
⊢ (𝐺 ∈ 𝑊 → (∅(Circuits‘𝐺)𝑃 ↔ 𝑃:(0...0)⟶(Vtx‘𝐺))) | ||
Theorem | 0cycl 26994 | A pair of an empty set (of edges) and a second set (of vertices) is a cycle if and only if the second set contains exactly one vertex (in an undirected graph). (Contributed by Alexander van der Vekens, 30-Oct-2017.) (Revised by AV, 31-Jan-2021.) (Revised by AV, 30-Oct-2021.) |
⊢ (𝐺 ∈ 𝑊 → (∅(Cycles‘𝐺)𝑃 ↔ 𝑃:(0...0)⟶(Vtx‘𝐺))) | ||
Theorem | 1pthdlem1 26995 | Lemma 1 for 1pthd 27003. (Contributed by Alexander van der Vekens, 4-Dec-2017.) (Revised by AV, 22-Jan-2021.) |
⊢ 𝑃 = 〈“𝑋𝑌”〉 & ⊢ 𝐹 = 〈“𝐽”〉 ⇒ ⊢ Fun ◡(𝑃 ↾ (1..^(#‘𝐹))) | ||
Theorem | 1pthdlem2 26996 | Lemma 2 for 1pthd 27003. (Contributed by Alexander van der Vekens, 4-Dec-2017.) (Revised by AV, 22-Jan-2021.) |
⊢ 𝑃 = 〈“𝑋𝑌”〉 & ⊢ 𝐹 = 〈“𝐽”〉 ⇒ ⊢ ((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅ | ||
Theorem | 1wlkdlem1 26997 | Lemma 1 for 1wlkd 27001. (Contributed by AV, 22-Jan-2021.) |
⊢ 𝑃 = 〈“𝑋𝑌”〉 & ⊢ 𝐹 = 〈“𝐽”〉 & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) ⇒ ⊢ (𝜑 → 𝑃:(0...(#‘𝐹))⟶𝑉) | ||
Theorem | 1wlkdlem2 26998 | Lemma 2 for 1wlkd 27001. (Contributed by AV, 22-Jan-2021.) |
⊢ 𝑃 = 〈“𝑋𝑌”〉 & ⊢ 𝐹 = 〈“𝐽”〉 & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑋 = 𝑌) → (𝐼‘𝐽) = {𝑋}) & ⊢ ((𝜑 ∧ 𝑋 ≠ 𝑌) → {𝑋, 𝑌} ⊆ (𝐼‘𝐽)) ⇒ ⊢ (𝜑 → 𝑋 ∈ (𝐼‘𝐽)) | ||
Theorem | 1wlkdlem3 26999 | Lemma 3 for 1wlkd 27001. (Contributed by AV, 22-Jan-2021.) |
⊢ 𝑃 = 〈“𝑋𝑌”〉 & ⊢ 𝐹 = 〈“𝐽”〉 & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑋 = 𝑌) → (𝐼‘𝐽) = {𝑋}) & ⊢ ((𝜑 ∧ 𝑋 ≠ 𝑌) → {𝑋, 𝑌} ⊆ (𝐼‘𝐽)) ⇒ ⊢ (𝜑 → 𝐹 ∈ Word dom 𝐼) | ||
Theorem | 1wlkdlem4 27000* | Lemma 4 for 1wlkd 27001. (Contributed by AV, 22-Jan-2021.) |
⊢ 𝑃 = 〈“𝑋𝑌”〉 & ⊢ 𝐹 = 〈“𝐽”〉 & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑋 = 𝑌) → (𝐼‘𝐽) = {𝑋}) & ⊢ ((𝜑 ∧ 𝑋 ≠ 𝑌) → {𝑋, 𝑌} ⊆ (𝐼‘𝐽)) ⇒ ⊢ (𝜑 → ∀𝑘 ∈ (0..^(#‘𝐹))if-((𝑃‘𝑘) = (𝑃‘(𝑘 + 1)), (𝐼‘(𝐹‘𝑘)) = {(𝑃‘𝑘)}, {(𝑃‘𝑘), (𝑃‘(𝑘 + 1))} ⊆ (𝐼‘(𝐹‘𝑘)))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |