Home | Metamath
Proof Explorer Theorem List (p. 413 of 424) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-27159) |
Hilbert Space Explorer
(27160-28684) |
Users' Mathboxes
(28685-42360) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | clwlkclwwlklem2a1 41201* | Lemma 1 for clwlkclwwlklem2a 41207. (Contributed by Alexander van der Vekens, 21-Jun-2018.) (Revised by AV, 11-Apr-2021.) |
⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) → ((( lastS ‘𝑃) = (𝑃‘0) ∧ (∀𝑖 ∈ (0..^((((#‘𝑃) − 1) − 0) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((#‘𝑃) − 2)), (𝑃‘0)} ∈ ran 𝐸)) → ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸)) | ||
Theorem | clwlkclwwlklem2a2 41202* | Lemma 2 for clwlkclwwlklem2a 41207. (Contributed by Alexander van der Vekens, 21-Jun-2018.) |
⊢ 𝐹 = (𝑥 ∈ (0..^((#‘𝑃) − 1)) ↦ if(𝑥 < ((#‘𝑃) − 2), (◡𝐸‘{(𝑃‘𝑥), (𝑃‘(𝑥 + 1))}), (◡𝐸‘{(𝑃‘𝑥), (𝑃‘0)}))) ⇒ ⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) → (#‘𝐹) = ((#‘𝑃) − 1)) | ||
Theorem | clwlkclwwlklem2a3 41203* | Lemma 3 for clwlkclwwlklem2a 41207. (Contributed by Alexander van der Vekens, 21-Jun-2018.) |
⊢ 𝐹 = (𝑥 ∈ (0..^((#‘𝑃) − 1)) ↦ if(𝑥 < ((#‘𝑃) − 2), (◡𝐸‘{(𝑃‘𝑥), (𝑃‘(𝑥 + 1))}), (◡𝐸‘{(𝑃‘𝑥), (𝑃‘0)}))) ⇒ ⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) → (𝑃‘(#‘𝐹)) = ( lastS ‘𝑃)) | ||
Theorem | clwlkclwwlklem2fv1 41204* | Lemma 4a for clwlkclwwlklem2a 41207. (Contributed by Alexander van der Vekens, 22-Jun-2018.) |
⊢ 𝐹 = (𝑥 ∈ (0..^((#‘𝑃) − 1)) ↦ if(𝑥 < ((#‘𝑃) − 2), (◡𝐸‘{(𝑃‘𝑥), (𝑃‘(𝑥 + 1))}), (◡𝐸‘{(𝑃‘𝑥), (𝑃‘0)}))) ⇒ ⊢ (((#‘𝑃) ∈ ℕ0 ∧ 𝐼 ∈ (0..^((#‘𝑃) − 2))) → (𝐹‘𝐼) = (◡𝐸‘{(𝑃‘𝐼), (𝑃‘(𝐼 + 1))})) | ||
Theorem | clwlkclwwlklem2fv2 41205* | Lemma 4b for clwlkclwwlklem2a 41207. (Contributed by Alexander van der Vekens, 22-Jun-2018.) |
⊢ 𝐹 = (𝑥 ∈ (0..^((#‘𝑃) − 1)) ↦ if(𝑥 < ((#‘𝑃) − 2), (◡𝐸‘{(𝑃‘𝑥), (𝑃‘(𝑥 + 1))}), (◡𝐸‘{(𝑃‘𝑥), (𝑃‘0)}))) ⇒ ⊢ (((#‘𝑃) ∈ ℕ0 ∧ 2 ≤ (#‘𝑃)) → (𝐹‘((#‘𝑃) − 2)) = (◡𝐸‘{(𝑃‘((#‘𝑃) − 2)), (𝑃‘0)})) | ||
Theorem | clwlkclwwlklem2a4 41206* | Lemma 4 for clwlkclwwlklem2a 41207. (Contributed by Alexander van der Vekens, 21-Jun-2018.) (Revised by AV, 11-Apr-2021.) |
⊢ 𝐹 = (𝑥 ∈ (0..^((#‘𝑃) − 1)) ↦ if(𝑥 < ((#‘𝑃) − 2), (◡𝐸‘{(𝑃‘𝑥), (𝑃‘(𝑥 + 1))}), (◡𝐸‘{(𝑃‘𝑥), (𝑃‘0)}))) ⇒ ⊢ ((𝐸:dom 𝐸–1-1→𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) → ((( lastS ‘𝑃) = (𝑃‘0) ∧ 𝐼 ∈ (0..^((#‘𝑃) − 1))) → ({(𝑃‘𝐼), (𝑃‘(𝐼 + 1))} ∈ ran 𝐸 → (𝐸‘(𝐹‘𝐼)) = {(𝑃‘𝐼), (𝑃‘(𝐼 + 1))}))) | ||
Theorem | clwlkclwwlklem2a 41207* | Lemma for clwlkclwwlklem2 41209. (Contributed by Alexander van der Vekens, 22-Jun-2018.) (Revised by AV, 11-Apr-2021.) |
⊢ 𝐹 = (𝑥 ∈ (0..^((#‘𝑃) − 1)) ↦ if(𝑥 < ((#‘𝑃) − 2), (◡𝐸‘{(𝑃‘𝑥), (𝑃‘(𝑥 + 1))}), (◡𝐸‘{(𝑃‘𝑥), (𝑃‘0)}))) ⇒ ⊢ ((𝐸:dom 𝐸–1-1→𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) → ((( lastS ‘𝑃) = (𝑃‘0) ∧ (∀𝑖 ∈ (0..^((((#‘𝑃) − 1) − 0) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((#‘𝑃) − 2)), (𝑃‘0)} ∈ ran 𝐸)) → ((𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))))) | ||
Theorem | clwlkclwwlklem1 41208* | Lemma 1 for clwlkclwwlk 41211. (Contributed by Alexander van der Vekens, 22-Jun-2018.) (Revised by AV, 11-Apr-2021.) |
⊢ ((𝐸:dom 𝐸–1-1→𝑅 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) → ((( lastS ‘𝑃) = (𝑃‘0) ∧ (∀𝑖 ∈ (0..^((((#‘𝑃) − 1) − 0) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((#‘𝑃) − 2)), (𝑃‘0)} ∈ ran 𝐸)) → ∃𝑓((𝑓 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝑓))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(#‘𝑓))(𝐸‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) ∧ (𝑃‘0) = (𝑃‘(#‘𝑓))))) | ||
Theorem | clwlkclwwlklem2 41209* | Lemma 2 for clwlkclwwlk 41211. (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 41210* | Lemma 3 for clwlkclwwlk 41211. (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 41211* | 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 41212* | 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 | clwwlksgt0 41213 | 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 41214 | 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 41215 | A closed walk of length 1 is a loop. See also clwlkl1loop 40989. (Contributed by AV, 24-Apr-2021.) |
⊢ ((𝑊 ∈ (ClWWalkS‘𝐺) ∧ (#‘𝑊) = 1) → {(𝑊‘0), (𝑊‘0)} ∈ (Edg‘𝐺)) | ||
Theorem | clwwlksn1loop 41216 | A closed walk of length 1 is a loop. (Contributed by AV, 24-Apr-2021.) |
⊢ (𝑊 ∈ (1 ClWWalkSN 𝐺) → ((#‘𝑊) = 1 ∧ {(𝑊‘0), (𝑊‘0)} ∈ (Edg‘𝐺))) | ||
Theorem | clwwlksn2 41217 | 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 41218 | 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 41219 | 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 41220 | 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 41221* | 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 41222* | Lemma 1 for clwwlksbij 41227: 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 41223* | Lemma 2 for clwwlksbij 41227: 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 41224* | Lemma 3 for clwwlksbij 41227: 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 41225* | Lemma 4 for clwwlksbij 41227: 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 41226* | Lemma 5 for clwwlksbij 41227: 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 41227* | 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 41228* | 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 41229* | 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 41230 | 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 41231 | 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 41232 | Any prefix of a word representing a closed walk represents a word. (Contributed by Alexander van der Vekens, 5-Oct-2018.) (Revised by AV, 28-Apr-2021.) |
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → (𝑋 ∈ (𝑁 ClWWalkSN 𝐺) → (𝑋 substr 〈0, 𝑀〉) ∈ ((𝑀 − 1) WWalkSN 𝐺))) | ||
Theorem | clwwisshclwwslemlem 41233* | Lemma for clwwisshclwwlem 26334. (Contributed by Alexander van der Vekens, 23-Mar-2018.) |
⊢ (((𝐿 ∈ (ℤ≥‘2) ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ ∀𝑖 ∈ (0..^(𝐿 − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝑅 ∧ {(𝑊‘(𝐿 − 1)), (𝑊‘0)} ∈ 𝑅) → {(𝑊‘((𝐴 + 𝐵) mod 𝐿)), (𝑊‘(((𝐴 + 1) + 𝐵) mod 𝐿))} ∈ 𝑅) | ||
Theorem | clwwisshclwwslem 41234* | Lemma for clwwisshclww 26335. (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 41235 | 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 41236 | 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 41237 | 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 41238 | ∼ 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 41239* | 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 41240* | 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 41241* | ∼ 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 41242* | ∼ 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 41243* | ∼ 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 41244* | ∼ 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 41245* | Lemma 1 for eleclclwwlksn 41260. (Contributed by Alexander van der Vekens, 11-May-2018.) (Revised by AV, 30-Apr-2021.) |
⊢ 𝑊 = (𝑁 ClWWalkSN 𝐺) ⇒ ⊢ ((𝐾 ∈ (0...𝑁) ∧ (𝑋 ∈ 𝑊 ∧ 𝑌 ∈ 𝑊)) → ((𝑋 = (𝑌 cyclShift 𝐾) ∧ ∃𝑚 ∈ (0...𝑁)𝑍 = (𝑌 cyclShift 𝑚)) → ∃𝑛 ∈ (0...𝑁)𝑍 = (𝑋 cyclShift 𝑛))) | ||
Theorem | eleclclwwlksnlem2 41246* | Lemma 2 for eleclclwwlksn 41260. (Contributed by Alexander van der Vekens, 11-May-2018.) (Revised by AV, 30-Apr-2021.) |
⊢ 𝑊 = (𝑁 ClWWalkSN 𝐺) ⇒ ⊢ (((𝑘 ∈ (0...𝑁) ∧ 𝑋 = (𝑥 cyclShift 𝑘)) ∧ (𝑋 ∈ 𝑊 ∧ 𝑥 ∈ 𝑊)) → (∃𝑚 ∈ (0...𝑁)𝑌 = (𝑥 cyclShift 𝑚) ↔ ∃𝑛 ∈ (0...𝑁)𝑌 = (𝑋 cyclShift 𝑛))) | ||
Theorem | clwwlksnscsh 41247* | 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 41248 | 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 41249* | 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 41250 | ∼ is a relation. (Contributed by Alexander van der Vekens, 25-Mar-2018.) (Revised by AV, 30-Apr-2021.) |
⊢ 𝑊 = (𝑁 ClWWalkSN 𝐺) & ⊢ ∼ = {〈𝑡, 𝑢〉 ∣ (𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊 ∧ ∃𝑛 ∈ (0...𝑁)𝑡 = (𝑢 cyclShift 𝑛))} ⇒ ⊢ Rel ∼ | ||
Theorem | erclwwlksneq 41251* | 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 41252* | 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 41253* | ∼ 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 41254* | ∼ 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 41255* | ∼ 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 41256* | ∼ 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 41257* | 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 41258* | 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 41259* | 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 41260* | 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 41261* | 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 41262* | 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 41263* | 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 41264 | 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 41265* | 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 41266* | 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 41267* | 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 41268* | 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 41269* | 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 41270* | 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 41271* | Lemma 1 for clwlksf1clwwlklem 41275. (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 41272* | Lemma 1 for clwlksf1clwwlklem 41275. (Contributed by Alexander van der Vekens, 5-Jul-2018.) (Revised by AV, 3-May-2021.) |
⊢ 𝐴 = (1st ‘𝑐) & ⊢ 𝐵 = (2nd ‘𝑐) & ⊢ 𝐶 = {𝑐 ∈ (ClWalkS‘𝐺) ∣ (#‘𝐴) = 𝑁} & ⊢ 𝐹 = (𝑐 ∈ 𝐶 ↦ (𝐵 substr 〈0, (#‘𝐴)〉)) ⇒ ⊢ (𝑊 ∈ 𝐶 → 𝑁 ≤ (#‘(2nd ‘𝑊))) | ||
Theorem | clwlksf1clwwlklem2 41273* | Lemma 2 for clwlksf1clwwlklem 41275. (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 41274* | Lemma 3 for clwlksf1clwwlklem 41275. (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 41275* | Lemma for clwlksf1clwwlk 41276. (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 41276* | 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 41277* | 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 41278* | 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 41279* | 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 41280* | 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 41281* | 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 41282 | 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 41283 | 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 | 01wlk 41284 | 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.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ ((𝐺 ∈ 𝑈 ∧ 𝑃 ∈ 𝑍) → (∅(1Walks‘𝐺)𝑃 ↔ 𝑃:(0...0)⟶𝑉)) | ||
Theorem | is01wlk 41285 | 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.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ ((𝑃 = {〈0, 𝑁〉} ∧ 𝑁 ∈ 𝑉) → ∅(1Walks‘𝐺)𝑃) | ||
Theorem | 0wlkOnlem1 41286 | Lemma 1 for 0wlkOn 41288 and 0TrlOn 41292. (Contributed by AV, 3-Jan-2021.) (Revised by AV, 23-Mar-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ ((𝑃:(0...0)⟶𝑉 ∧ (𝑃‘0) = 𝑁) → (𝑁 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉)) | ||
Theorem | 0wlkOnlem2 41287 | Lemma 2 for 0wlkOn 41288 and 0TrlOn 41292. (Contributed by AV, 3-Jan-2021.) (Revised by AV, 23-Mar-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ ((𝑃:(0...0)⟶𝑉 ∧ (𝑃‘0) = 𝑁) → 𝑃 ∈ (𝑉 ↑pm (0...0))) | ||
Theorem | 0wlkOn 41288 | 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.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ ((𝑃:(0...0)⟶𝑉 ∧ (𝑃‘0) = 𝑁) → ∅(𝑁(WalksOn‘𝐺)𝑁)𝑃) | ||
Theorem | 0wlkOns1 41289 | A walk of length 0 from a vertex to itself. (Contributed by AV, 17-Apr-2021.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ (𝑁 ∈ 𝑉 → ∅(𝑁(WalksOn‘𝐺)𝑁)〈“𝑁”〉) | ||
Theorem | 0Trl 41290 | 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.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ ((𝐺 ∈ 𝑈 ∧ 𝑃 ∈ 𝑍) → (∅(TrailS‘𝐺)𝑃 ↔ 𝑃:(0...0)⟶𝑉)) | ||
Theorem | is0Trl 41291 | 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.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ ((𝑃 = {〈0, 𝑁〉} ∧ 𝑁 ∈ 𝑉) → ∅(TrailS‘𝐺)𝑃) | ||
Theorem | 0TrlOn 41292 | 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.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ ((𝑃:(0...0)⟶𝑉 ∧ (𝑃‘0) = 𝑁) → ∅(𝑁(TrailsOn‘𝐺)𝑁)𝑃) | ||
Theorem | 0pth-av 41293 | 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.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ ((𝐺 ∈ 𝑊 ∧ 𝑃 ∈ 𝑍) → (∅(PathS‘𝐺)𝑃 ↔ 𝑃:(0...0)⟶𝑉)) | ||
Theorem | 0spth-av 41294 | 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.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ ((𝐺 ∈ 𝑊 ∧ 𝑃 ∈ 𝑍) → (∅(SPathS‘𝐺)𝑃 ↔ 𝑃:(0...0)⟶𝑉)) | ||
Theorem | 0pthon-av 41295 | 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‘𝐺) ⇒ ⊢ (𝑁 ∈ 𝑉 → ((𝑃:(0...0)⟶𝑉 ∧ (𝑃‘0) = 𝑁) → ∅(𝑁(PathsOn‘𝐺)𝑁)𝑃)) | ||
Theorem | 0pthon1-av 41296 | 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-av 41297* | 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 41298 | 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.) |
⊢ 𝑉 = (Vtx‘𝐺) ⇒ ⊢ ((𝐺 ∈ 𝑋 ∧ 𝑃 ∈ 𝑍) → (∅(ClWalkS‘𝐺)𝑃 ↔ 𝑃:(0...0)⟶𝑉)) | ||
Theorem | 0clwlk0 41299 | 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 41300 | 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.) |
⊢ ((𝐺 ∈ 𝑊 ∧ 𝑃 ∈ 𝑍) → (∅(CircuitS‘𝐺)𝑃 ↔ 𝑃:(0...0)⟶(Vtx‘𝐺))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |