Home | Metamath
Proof Explorer Theorem List (p. 264 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 | clwwlknndef 26301 | Conditions for ClWWalksN not being defined. (Contributed by Alexander van der Vekens, 15-Sep-2018.) |
⊢ ((𝑉 ∉ V ∨ 𝐸 ∉ V ∨ 𝑁 ∉ ℕ0) → ((𝑉 ClWWalksN 𝐸)‘𝑁) = ∅) | ||
Theorem | clwwlkn0 26302 | There is no closed walk of length 0 in an undirected simple graph. (Contributed by Alexander van der Vekens, 15-Sep-2018.) |
⊢ (𝑉 USGrph 𝐸 → ((𝑉 ClWWalksN 𝐸)‘0) = ∅) | ||
Theorem | clwwlkn2 26303 | In an undirected simple graph, a closed walk of length 2 represented as word is a word consisting of 2 symbols representing vertices connected by an edge. (Contributed by Alexander van der Vekens, 19-Sep-2018.) |
⊢ (𝑉 USGrph 𝐸 → (𝑊 ∈ ((𝑉 ClWWalksN 𝐸)‘2) ↔ ((#‘𝑊) = 2 ∧ 𝑊 ∈ Word 𝑉 ∧ {(𝑊‘0), (𝑊‘1)} ∈ ran 𝐸))) | ||
Theorem | clwwlknimp 26304* | Implications for a set being a closed walk (represented by a word). (Contributed by Alexander van der Vekens, 17-Jun-2018.) |
⊢ (𝑊 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) → ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = 𝑁) ∧ ∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ ran 𝐸)) | ||
Theorem | clwwlksswrd 26305 | Closed walks (represented by words) are words. (Contributed by Alexander van der Vekens, 25-Mar-2018.) |
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (𝑉 ClWWalks 𝐸) ⊆ Word 𝑉) | ||
Theorem | clwwlknfi 26306 | If there is only a finite number of vertices, the number of closed walk of fixed length (as words) is also finite. (Contributed by Alexander van der Vekens, 25-Mar-2018.) |
⊢ ((𝑉 ∈ Fin ∧ 𝐸 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0) → ((𝑉 ClWWalksN 𝐸)‘𝑁) ∈ Fin) | ||
Theorem | clwlkisclwwlklem2a1 26307* | Lemma 1 for clwlkisclwwlklem2a 26313. (Contributed by Alexander van der Vekens, 21-Jun-2018.) |
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) → ((( lastS ‘𝑃) = (𝑃‘0) ∧ (∀𝑖 ∈ (0..^((((#‘𝑃) − 1) − 0) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((#‘𝑃) − 2)), (𝑃‘0)} ∈ ran 𝐸)) → ∀𝑖 ∈ (0..^((#‘𝑃) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸)) | ||
Theorem | clwlkisclwwlklem2a2 26308* | Lemma 3 for clwlkisclwwlklem2a 26313. (Contributed by Alexander van der Vekens, 21-Jun-2018.) |
⊢ 𝐹 = (𝑥 ∈ (0..^((#‘𝑃) − 1)) ↦ if(𝑥 < ((#‘𝑃) − 2), (◡𝐸‘{(𝑃‘𝑥), (𝑃‘(𝑥 + 1))}), (◡𝐸‘{(𝑃‘𝑥), (𝑃‘0)}))) ⇒ ⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) → (#‘𝐹) = ((#‘𝑃) − 1)) | ||
Theorem | clwlkisclwwlklem2a3 26309* | Lemma 3 for clwlkisclwwlklem2a 26313. (Contributed by Alexander van der Vekens, 21-Jun-2018.) |
⊢ 𝐹 = (𝑥 ∈ (0..^((#‘𝑃) − 1)) ↦ if(𝑥 < ((#‘𝑃) − 2), (◡𝐸‘{(𝑃‘𝑥), (𝑃‘(𝑥 + 1))}), (◡𝐸‘{(𝑃‘𝑥), (𝑃‘0)}))) ⇒ ⊢ ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) → (𝑃‘(#‘𝐹)) = ( lastS ‘𝑃)) | ||
Theorem | clwlkisclwwlklem2fv1 26310* | Lemma 4a for clwlkisclwwlklem2a 26313. (Contributed by Alexander van der Vekens, 22-Jun-2018.) |
⊢ 𝐹 = (𝑥 ∈ (0..^((#‘𝑃) − 1)) ↦ if(𝑥 < ((#‘𝑃) − 2), (◡𝐸‘{(𝑃‘𝑥), (𝑃‘(𝑥 + 1))}), (◡𝐸‘{(𝑃‘𝑥), (𝑃‘0)}))) ⇒ ⊢ (((#‘𝑃) ∈ ℕ0 ∧ 𝐼 ∈ (0..^((#‘𝑃) − 2))) → (𝐹‘𝐼) = (◡𝐸‘{(𝑃‘𝐼), (𝑃‘(𝐼 + 1))})) | ||
Theorem | clwlkisclwwlklem2fv2 26311* | Lemma 4b for clwlkisclwwlklem2a 26313. (Contributed by Alexander van der Vekens, 22-Jun-2018.) |
⊢ 𝐹 = (𝑥 ∈ (0..^((#‘𝑃) − 1)) ↦ if(𝑥 < ((#‘𝑃) − 2), (◡𝐸‘{(𝑃‘𝑥), (𝑃‘(𝑥 + 1))}), (◡𝐸‘{(𝑃‘𝑥), (𝑃‘0)}))) ⇒ ⊢ (((#‘𝑃) ∈ ℕ0 ∧ 2 ≤ (#‘𝑃)) → (𝐹‘((#‘𝑃) − 2)) = (◡𝐸‘{(𝑃‘((#‘𝑃) − 2)), (𝑃‘0)})) | ||
Theorem | clwlkisclwwlklem2a4 26312* | Lemma 4 for clwlkisclwwlklem2a 26313. (Contributed by Alexander van der Vekens, 21-Jun-2018.) |
⊢ 𝐹 = (𝑥 ∈ (0..^((#‘𝑃) − 1)) ↦ if(𝑥 < ((#‘𝑃) − 2), (◡𝐸‘{(𝑃‘𝑥), (𝑃‘(𝑥 + 1))}), (◡𝐸‘{(𝑃‘𝑥), (𝑃‘0)}))) ⇒ ⊢ ((𝑉 USGrph 𝐸 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) → ((( lastS ‘𝑃) = (𝑃‘0) ∧ 𝐼 ∈ (0..^((#‘𝑃) − 1))) → ({(𝑃‘𝐼), (𝑃‘(𝐼 + 1))} ∈ ran 𝐸 → (𝐸‘(𝐹‘𝐼)) = {(𝑃‘𝐼), (𝑃‘(𝐼 + 1))}))) | ||
Theorem | clwlkisclwwlklem2a 26313* | Lemma 2 for clwlkisclwwlklem2 26314. (Contributed by Alexander van der Vekens, 22-Jun-2018.) |
⊢ 𝐹 = (𝑥 ∈ (0..^((#‘𝑃) − 1)) ↦ if(𝑥 < ((#‘𝑃) − 2), (◡𝐸‘{(𝑃‘𝑥), (𝑃‘(𝑥 + 1))}), (◡𝐸‘{(𝑃‘𝑥), (𝑃‘0)}))) ⇒ ⊢ ((𝑉 USGrph 𝐸 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) → ((( lastS ‘𝑃) = (𝑃‘0) ∧ (∀𝑖 ∈ (0..^((((#‘𝑃) − 1) − 0) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((#‘𝑃) − 2)), (𝑃‘0)} ∈ ran 𝐸)) → ((𝐹 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))))) | ||
Theorem | clwlkisclwwlklem2 26314* | Lemma for clwlkisclwwlk 26317. (Contributed by Alexander van der Vekens, 22-Jun-2018.) |
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) → ((( lastS ‘𝑃) = (𝑃‘0) ∧ (∀𝑖 ∈ (0..^((((#‘𝑃) − 1) − 0) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((#‘𝑃) − 2)), (𝑃‘0)} ∈ ran 𝐸)) → ∃𝑓((𝑓 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝑓))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(#‘𝑓))(𝐸‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) ∧ (𝑃‘0) = (𝑃‘(#‘𝑓))))) | ||
Theorem | clwlkisclwwlklem1 26315* | Lemma for clwlkisclwwlk 26317. (Contributed by Alexander van der Vekens, 22-Jun-2018.) |
⊢ (((𝑉 USGrph 𝐸 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (𝑃:(0...(#‘𝐹))⟶𝑉 ∧ 2 ≤ (#‘𝑃)) ∧ (∀𝑖 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∧ (𝑃‘0) = (𝑃‘(#‘𝐹)))) → (( lastS ‘𝑃) = (𝑃‘0) ∧ ∀𝑖 ∈ (0..^((#‘𝐹) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((#‘𝐹) − 1)), (𝑃‘0)} ∈ ran 𝐸)) | ||
Theorem | clwlkisclwwlklem0 26316* | Lemma for clwlkisclwwlk 26317. (Contributed by Alexander van der Vekens, 22-Jun-2018.) |
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) → (∃𝑓((𝑓 ∈ Word dom 𝐸 ∧ 𝑃:(0...(#‘𝑓))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(#‘𝑓))(𝐸‘(𝑓‘𝑖)) = {(𝑃‘𝑖), (𝑃‘(𝑖 + 1))}) ∧ (𝑃‘0) = (𝑃‘(#‘𝑓))) ↔ (( lastS ‘𝑃) = (𝑃‘0) ∧ (∀𝑖 ∈ (0..^((((#‘𝑃) − 1) − 0) − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((#‘𝑃) − 2)), (𝑃‘0)} ∈ ran 𝐸)))) | ||
Theorem | clwlkisclwwlk 26317* | A closed walk as word corresponds to a closed walk in an undirected graph. (Contributed by Alexander van der Vekens, 22-Jun-2018.) |
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑃)) → (∃𝑓 𝑓(𝑉 ClWalks 𝐸)𝑃 ↔ (( lastS ‘𝑃) = (𝑃‘0) ∧ (𝑃 substr 〈0, ((#‘𝑃) − 1)〉) ∈ (𝑉 ClWWalks 𝐸)))) | ||
Theorem | clwlkisclwwlk2 26318* | A closed walk corresponds to a closed walk as word in an undirected graph. (Contributed by Alexander van der Vekens, 22-Jun-2018.) |
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑃 ∈ Word 𝑉 ∧ 1 ≤ (#‘𝑃)) → (∃𝑓 𝑓(𝑉 ClWalks 𝐸)(𝑃 ++ 〈“(𝑃‘0)”〉) ↔ 𝑃 ∈ (𝑉 ClWWalks 𝐸))) | ||
Theorem | clwwlkisclwwlkn 26319 | 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.) |
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ0) → (𝑃 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) → 𝑃 ∈ (𝑉 ClWWalks 𝐸))) | ||
Theorem | clwwlkssclwwlkn 26320 | 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.) |
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ0) → ((𝑉 ClWWalksN 𝐸)‘𝑁) ⊆ (𝑉 ClWWalks 𝐸)) | ||
Theorem | clwwlkel 26321* | Obtaining a closed walk (as word) by appending the first symbol to the word representing a walk. (Contributed by AV, 28-Sep-2018.) (Proof shortened by AV, 20-Oct-2018.) |
⊢ 𝐷 = {𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ ( lastS ‘𝑤) = (𝑤‘0)} ⇒ ⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) ∧ (𝑃 ∈ Word 𝑉 ∧ (#‘𝑃) = 𝑁) ∧ (∀𝑖 ∈ (0..^(𝑁 − 1)){(𝑃‘𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑃), (𝑃‘0)} ∈ ran 𝐸)) → (𝑃 ++ 〈“(𝑃‘0)”〉) ∈ 𝐷) | ||
Theorem | clwwlkf 26322* | Lemma 1 for clwwlkbij 26327: F is a function. (Contributed by Alexander van der Vekens, 27-Sep-2018.) |
⊢ 𝐷 = {𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ ( lastS ‘𝑤) = (𝑤‘0)} & ⊢ 𝐹 = (𝑡 ∈ 𝐷 ↦ (𝑡 substr 〈0, 𝑁〉)) ⇒ ⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) → 𝐹:𝐷⟶((𝑉 ClWWalksN 𝐸)‘𝑁)) | ||
Theorem | clwwlkfv 26323* | Lemma 2 for clwwlkbij 26327: the value of function F. (Contributed by Alexander van der Vekens, 28-Sep-2018.) |
⊢ 𝐷 = {𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ ( lastS ‘𝑤) = (𝑤‘0)} & ⊢ 𝐹 = (𝑡 ∈ 𝐷 ↦ (𝑡 substr 〈0, 𝑁〉)) ⇒ ⊢ (𝑊 ∈ 𝐷 → (𝐹‘𝑊) = (𝑊 substr 〈0, 𝑁〉)) | ||
Theorem | clwwlkf1 26324* | Lemma 3 for clwwlkbij 26327: F is a 1-1 function. (Contributed by AV, 28-Sep-2018.) (Proof shortened by AV, 23-Oct-2018.) |
⊢ 𝐷 = {𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ ( lastS ‘𝑤) = (𝑤‘0)} & ⊢ 𝐹 = (𝑡 ∈ 𝐷 ↦ (𝑡 substr 〈0, 𝑁〉)) ⇒ ⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) → 𝐹:𝐷–1-1→((𝑉 ClWWalksN 𝐸)‘𝑁)) | ||
Theorem | clwwlkfo 26325* | Lemma 4 for clwwlkbij 26327: F is an onto function. (Contributed by Alexander van der Vekens, 29-Sep-2018.) |
⊢ 𝐷 = {𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ ( lastS ‘𝑤) = (𝑤‘0)} & ⊢ 𝐹 = (𝑡 ∈ 𝐷 ↦ (𝑡 substr 〈0, 𝑁〉)) ⇒ ⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) → 𝐹:𝐷–onto→((𝑉 ClWWalksN 𝐸)‘𝑁)) | ||
Theorem | clwwlkf1o 26326* | Lemma 5 for clwwlkbij 26327: F is a 1-1 onto function. (Contributed by Alexander van der Vekens, 29-Sep-2018.) |
⊢ 𝐷 = {𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ ( lastS ‘𝑤) = (𝑤‘0)} & ⊢ 𝐹 = (𝑡 ∈ 𝐷 ↦ (𝑡 substr 〈0, 𝑁〉)) ⇒ ⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) → 𝐹:𝐷–1-1-onto→((𝑉 ClWWalksN 𝐸)‘𝑁)) | ||
Theorem | clwwlkbij 26327* | 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.) |
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) → ∃𝑓 𝑓:{𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ ( lastS ‘𝑤) = (𝑤‘0)}–1-1-onto→((𝑉 ClWWalksN 𝐸)‘𝑁)) | ||
Theorem | clwwlknwwlkncl 26328* | 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.) |
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁)) → (𝑃 ++ 〈“(𝑃‘0)”〉) ∈ {𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ ( lastS ‘𝑤) = (𝑤‘0)}) | ||
Theorem | clwwlkvbij 26329* | 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.) |
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝑁 ∈ ℕ) → ∃𝑓 𝑓:{𝑤 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∣ (( lastS ‘𝑤) = (𝑤‘0) ∧ (𝑤‘0) = 𝑆)}–1-1-onto→{𝑤 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) ∣ (𝑤‘0) = 𝑆}) | ||
Theorem | clwwlkext2edg 26330 | 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.) |
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ (ℤ≥‘2)) ∧ (𝑊 ++ 〈“𝑍”〉) ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁)) → ({( lastS ‘𝑊), 𝑍} ∈ ran 𝐸 ∧ {𝑍, (𝑊‘0)} ∈ ran 𝐸)) | ||
Theorem | wwlkext2clwwlk 26331 | 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.) |
⊢ ((𝑊 ∈ ((𝑉 WWalksN 𝐸)‘𝑁) ∧ 𝑍 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → (({( lastS ‘𝑊), 𝑍} ∈ ran 𝐸 ∧ {𝑍, (𝑊‘0)} ∈ ran 𝐸) → (𝑊 ++ 〈“𝑍”〉) ∈ ((𝑉 ClWWalksN 𝐸)‘(𝑁 + 2)))) | ||
Theorem | wwlksubclwwlk 26332 | Any prefix of a word representing a closed walk represents a word. (Contributed by Alexander van der Vekens, 5-Oct-2018.) |
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘(𝑀 + 1))) → (𝑋 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) → (𝑋 substr 〈0, 𝑀〉) ∈ ((𝑉 WWalksN 𝐸)‘(𝑀 − 1)))) | ||
Theorem | clwwisshclwwlem1 26333* | Lemma 1 for clwwisshclwwlem 26334. (Contributed by Alexander van der Vekens, 23-Mar-2018.) |
⊢ (((𝐿 ∈ (ℤ≥‘2) ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ ∀𝑖 ∈ (0..^(𝐿 − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ 𝑅 ∧ {(𝑊‘(𝐿 − 1)), (𝑊‘0)} ∈ 𝑅) → {(𝑊‘((𝐴 + 𝐵) mod 𝐿)), (𝑊‘(((𝐴 + 1) + 𝐵) mod 𝐿))} ∈ 𝑅) | ||
Theorem | clwwisshclwwlem 26334* | Lemma for clwwisshclww 26335. (Contributed by AV, 24-Mar-2018.) (Revised by AV, 10-Jun-2018.) (Proof shortened by AV, 2-Nov-2018.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (1..^(#‘𝑊))) → ((∀𝑖 ∈ (0..^((#‘𝑊) − 1)){(𝑊‘𝑖), (𝑊‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {( lastS ‘𝑊), (𝑊‘0)} ∈ ran 𝐸) → ∀𝑗 ∈ (0..^((#‘(𝑊 cyclShift 𝑁)) − 1)){((𝑊 cyclShift 𝑁)‘𝑗), ((𝑊 cyclShift 𝑁)‘(𝑗 + 1))} ∈ ran 𝐸)) | ||
Theorem | clwwisshclww 26335 | 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 Alexander van der Vekens, 10-Jun-2018.) |
⊢ ((𝑊 ∈ (𝑉 ClWWalks 𝐸) ∧ 𝑁 ∈ (0..^(#‘𝑊))) → (𝑊 cyclShift 𝑁) ∈ (𝑉 ClWWalks 𝐸)) | ||
Theorem | clwwisshclwwn 26336 | 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.) |
⊢ ((𝑊 ∈ (𝑉 ClWWalks 𝐸) ∧ 𝑁 ∈ (0...(#‘𝑊))) → (𝑊 cyclShift 𝑁) ∈ (𝑉 ClWWalks 𝐸)) | ||
Theorem | clwwnisshclwwn 26337 | 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.) |
⊢ ((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁)) → (𝑀 ∈ (0...𝑁) → (𝑊 cyclShift 𝑀) ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁))) | ||
Theorem | erclwwlkrel 26338 | ∼ is a relation. (Contributed by Alexander van der Vekens, 25-Mar-2018.) |
⊢ ∼ = {〈𝑢, 𝑤〉 ∣ (𝑢 ∈ (𝑉 ClWWalks 𝐸) ∧ 𝑤 ∈ (𝑉 ClWWalks 𝐸) ∧ ∃𝑛 ∈ (0...(#‘𝑤))𝑢 = (𝑤 cyclShift 𝑛))} ⇒ ⊢ Rel ∼ | ||
Theorem | erclwwlkeq 26339* | 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 Alexander van der Vekens, 11-Jun-2018.) |
⊢ ∼ = {〈𝑢, 𝑤〉 ∣ (𝑢 ∈ (𝑉 ClWWalks 𝐸) ∧ 𝑤 ∈ (𝑉 ClWWalks 𝐸) ∧ ∃𝑛 ∈ (0...(#‘𝑤))𝑢 = (𝑤 cyclShift 𝑛))} ⇒ ⊢ ((𝑈 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌) → (𝑈 ∼ 𝑊 ↔ (𝑈 ∈ (𝑉 ClWWalks 𝐸) ∧ 𝑊 ∈ (𝑉 ClWWalks 𝐸) ∧ ∃𝑛 ∈ (0...(#‘𝑊))𝑈 = (𝑊 cyclShift 𝑛)))) | ||
Theorem | erclwwlkeqlen 26340* | 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 Alexander van der Vekens, 11-Jun-2018.) |
⊢ ∼ = {〈𝑢, 𝑤〉 ∣ (𝑢 ∈ (𝑉 ClWWalks 𝐸) ∧ 𝑤 ∈ (𝑉 ClWWalks 𝐸) ∧ ∃𝑛 ∈ (0...(#‘𝑤))𝑢 = (𝑤 cyclShift 𝑛))} ⇒ ⊢ ((𝑈 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌) → (𝑈 ∼ 𝑊 → (#‘𝑈) = (#‘𝑊))) | ||
Theorem | erclwwlkref 26341* | ∼ is a reflexive relation over the set of closed walks (defined as words). (Contributed by Alexander van der Vekens, 25-Mar-2018.) (Revised by Alexander van der Vekens, 11-Jun-2018.) |
⊢ ∼ = {〈𝑢, 𝑤〉 ∣ (𝑢 ∈ (𝑉 ClWWalks 𝐸) ∧ 𝑤 ∈ (𝑉 ClWWalks 𝐸) ∧ ∃𝑛 ∈ (0...(#‘𝑤))𝑢 = (𝑤 cyclShift 𝑛))} ⇒ ⊢ (𝑥 ∈ (𝑉 ClWWalks 𝐸) ↔ 𝑥 ∼ 𝑥) | ||
Theorem | erclwwlksym 26342* | ∼ is a symmetric relation over the set of closed walks (defined as words). (Contributed by Alexander van der Vekens, 8-Apr-2018.) (Revised by Alexander van der Vekens, 11-Jun-2018.) |
⊢ ∼ = {〈𝑢, 𝑤〉 ∣ (𝑢 ∈ (𝑉 ClWWalks 𝐸) ∧ 𝑤 ∈ (𝑉 ClWWalks 𝐸) ∧ ∃𝑛 ∈ (0...(#‘𝑤))𝑢 = (𝑤 cyclShift 𝑛))} ⇒ ⊢ (𝑥 ∼ 𝑦 → 𝑦 ∼ 𝑥) | ||
Theorem | erclwwlktr 26343* | ∼ is a transitive relation over the set of closed walks (defined as words). (Contributed by Alexander van der Vekens, 10-Apr-2018.) (Revised by Alexander van der Vekens, 11-Jun-2018.) |
⊢ ∼ = {〈𝑢, 𝑤〉 ∣ (𝑢 ∈ (𝑉 ClWWalks 𝐸) ∧ 𝑤 ∈ (𝑉 ClWWalks 𝐸) ∧ ∃𝑛 ∈ (0...(#‘𝑤))𝑢 = (𝑤 cyclShift 𝑛))} ⇒ ⊢ ((𝑥 ∼ 𝑦 ∧ 𝑦 ∼ 𝑧) → 𝑥 ∼ 𝑧) | ||
Theorem | erclwwlk 26344* | ∼ is an equivalence relation over the set of closed walks (defined as words). (Contributed by Alexander van der Vekens, 10-Apr-2018.) (Revised by Alexander van der Vekens, 11-Jun-2018.) (Proof shortened by AV, 1-May-2021.) |
⊢ ∼ = {〈𝑢, 𝑤〉 ∣ (𝑢 ∈ (𝑉 ClWWalks 𝐸) ∧ 𝑤 ∈ (𝑉 ClWWalks 𝐸) ∧ ∃𝑛 ∈ (0...(#‘𝑤))𝑢 = (𝑤 cyclShift 𝑛))} ⇒ ⊢ ∼ Er (𝑉 ClWWalks 𝐸) | ||
Theorem | eleclclwwlknlem1 26345* | Lemma 1 for eleclclwwlkn 26360. (Contributed by Alexander van der Vekens, 11-May-2018.) (Revised by Alexander van der Vekens, 14-Jun-2018.) |
⊢ 𝑊 = ((𝑉 ClWWalksN 𝐸)‘𝑁) ⇒ ⊢ ((𝐾 ∈ (0...𝑁) ∧ (𝑋 ∈ 𝑊 ∧ 𝑌 ∈ 𝑊)) → ((𝑋 = (𝑌 cyclShift 𝐾) ∧ ∃𝑚 ∈ (0...𝑁)𝑍 = (𝑌 cyclShift 𝑚)) → ∃𝑛 ∈ (0...𝑁)𝑍 = (𝑋 cyclShift 𝑛))) | ||
Theorem | eleclclwwlknlem2 26346* | Lemma 2 for eleclclwwlkn 26360. (Contributed by Alexander van der Vekens, 11-May-2018.) (Revised by Alexander van der Vekens, 14-Jun-2018.) |
⊢ 𝑊 = ((𝑉 ClWWalksN 𝐸)‘𝑁) ⇒ ⊢ (((𝑘 ∈ (0...𝑁) ∧ 𝑋 = (𝑥 cyclShift 𝑘)) ∧ (𝑋 ∈ 𝑊 ∧ 𝑥 ∈ 𝑊)) → (∃𝑚 ∈ (0...𝑁)𝑌 = (𝑥 cyclShift 𝑚) ↔ ∃𝑛 ∈ (0...𝑁)𝑌 = (𝑋 cyclShift 𝑛))) | ||
Theorem | clwwlknscsh 26347* | 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.) |
⊢ ((𝑁 ∈ ℕ0 ∧ 𝑊 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁)) → {𝑦 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁) ∣ ∃𝑛 ∈ (0...𝑁)𝑦 = (𝑊 cyclShift 𝑛)} = {𝑦 ∈ Word 𝑉 ∣ ∃𝑛 ∈ (0...𝑁)𝑦 = (𝑊 cyclShift 𝑛)}) | ||
Theorem | usg2cwwk2dif 26348 | 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.) |
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ (ℤ≥‘2) ∧ 𝑊 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁)) → (𝑊‘1) ≠ (𝑊‘0)) | ||
Theorem | usg2cwwkdifex 26349* | 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.) |
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ (ℤ≥‘2) ∧ 𝑊 ∈ ((𝑉 ClWWalksN 𝐸)‘𝑁)) → ∃𝑖 ∈ (0..^𝑁)(𝑊‘𝑖) ≠ (𝑊‘0)) | ||
Theorem | erclwwlknrel 26350 | ∼ is a relation. (Contributed by Alexander van der Vekens, 25-Mar-2018.) |
⊢ 𝑊 = ((𝑉 ClWWalksN 𝐸)‘𝑁) & ⊢ ∼ = {〈𝑡, 𝑢〉 ∣ (𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊 ∧ ∃𝑛 ∈ (0...𝑁)𝑡 = (𝑢 cyclShift 𝑛))} ⇒ ⊢ Rel ∼ | ||
Theorem | erclwwlkneq 26351* | 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 Alexander van der Vekens, 14-Jun-2018.) |
⊢ 𝑊 = ((𝑉 ClWWalksN 𝐸)‘𝑁) & ⊢ ∼ = {〈𝑡, 𝑢〉 ∣ (𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊 ∧ ∃𝑛 ∈ (0...𝑁)𝑡 = (𝑢 cyclShift 𝑛))} ⇒ ⊢ ((𝑇 ∈ 𝑋 ∧ 𝑈 ∈ 𝑌) → (𝑇 ∼ 𝑈 ↔ (𝑇 ∈ 𝑊 ∧ 𝑈 ∈ 𝑊 ∧ ∃𝑛 ∈ (0...𝑁)𝑇 = (𝑈 cyclShift 𝑛)))) | ||
Theorem | erclwwlkneqlen 26352* | 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 Alexander van der Vekens, 14-Jun-2018.) |
⊢ 𝑊 = ((𝑉 ClWWalksN 𝐸)‘𝑁) & ⊢ ∼ = {〈𝑡, 𝑢〉 ∣ (𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊 ∧ ∃𝑛 ∈ (0...𝑁)𝑡 = (𝑢 cyclShift 𝑛))} ⇒ ⊢ ((𝑇 ∈ 𝑋 ∧ 𝑈 ∈ 𝑌) → (𝑇 ∼ 𝑈 → (#‘𝑇) = (#‘𝑈))) | ||
Theorem | erclwwlknref 26353* | ∼ is a reflexive relation over the set of closed walks (defined as words). (Contributed by Alexander van der Vekens, 26-Mar-2018.) (Revised by Alexander van der Vekens, 14-Jun-2018.) |
⊢ 𝑊 = ((𝑉 ClWWalksN 𝐸)‘𝑁) & ⊢ ∼ = {〈𝑡, 𝑢〉 ∣ (𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊 ∧ ∃𝑛 ∈ (0...𝑁)𝑡 = (𝑢 cyclShift 𝑛))} ⇒ ⊢ (𝑥 ∈ 𝑊 ↔ 𝑥 ∼ 𝑥) | ||
Theorem | erclwwlknsym 26354* | ∼ is a symmetric relation over the set of closed walks (defined as words). (Contributed by Alexander van der Vekens, 10-Apr-2018.) (Revised by Alexander van der Vekens, 14-Jun-2018.) |
⊢ 𝑊 = ((𝑉 ClWWalksN 𝐸)‘𝑁) & ⊢ ∼ = {〈𝑡, 𝑢〉 ∣ (𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊 ∧ ∃𝑛 ∈ (0...𝑁)𝑡 = (𝑢 cyclShift 𝑛))} ⇒ ⊢ (𝑥 ∼ 𝑦 → 𝑦 ∼ 𝑥) | ||
Theorem | erclwwlkntr 26355* | ∼ is a transitive relation over the set of closed walks (defined as words). (Contributed by Alexander van der Vekens, 10-Apr-2018.) (Revised by Alexander van der Vekens, 14-Jun-2018.) |
⊢ 𝑊 = ((𝑉 ClWWalksN 𝐸)‘𝑁) & ⊢ ∼ = {〈𝑡, 𝑢〉 ∣ (𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊 ∧ ∃𝑛 ∈ (0...𝑁)𝑡 = (𝑢 cyclShift 𝑛))} ⇒ ⊢ ((𝑥 ∼ 𝑦 ∧ 𝑦 ∼ 𝑧) → 𝑥 ∼ 𝑧) | ||
Theorem | erclwwlkn 26356* | ∼ 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.) (Proof shortened by AV, 1-May-2021.) |
⊢ 𝑊 = ((𝑉 ClWWalksN 𝐸)‘𝑁) & ⊢ ∼ = {〈𝑡, 𝑢〉 ∣ (𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊 ∧ ∃𝑛 ∈ (0...𝑁)𝑡 = (𝑢 cyclShift 𝑛))} ⇒ ⊢ ∼ Er 𝑊 | ||
Theorem | qerclwwlknfi 26357* | 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.) |
⊢ 𝑊 = ((𝑉 ClWWalksN 𝐸)‘𝑁) & ⊢ ∼ = {〈𝑡, 𝑢〉 ∣ (𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊 ∧ ∃𝑛 ∈ (0...𝑁)𝑡 = (𝑢 cyclShift 𝑛))} ⇒ ⊢ ((𝑉 ∈ Fin ∧ 𝐸 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0) → (𝑊 / ∼ ) ∈ Fin) | ||
Theorem | hashclwwlkn0 26358* | 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.) |
⊢ 𝑊 = ((𝑉 ClWWalksN 𝐸)‘𝑁) & ⊢ ∼ = {〈𝑡, 𝑢〉 ∣ (𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊 ∧ ∃𝑛 ∈ (0...𝑁)𝑡 = (𝑢 cyclShift 𝑛))} ⇒ ⊢ ((𝑉 ∈ Fin ∧ 𝐸 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0) → (#‘𝑊) = Σ𝑥 ∈ (𝑊 / ∼ )(#‘𝑥)) | ||
Theorem | eclclwwlkn1 26359* | An equivalence class according to ∼. (Contributed by Alexander van der Vekens, 12-Apr-2018.) (Revised by Alexander van der Vekens, 15-Jun-2018.) |
⊢ 𝑊 = ((𝑉 ClWWalksN 𝐸)‘𝑁) & ⊢ ∼ = {〈𝑡, 𝑢〉 ∣ (𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊 ∧ ∃𝑛 ∈ (0...𝑁)𝑡 = (𝑢 cyclShift 𝑛))} ⇒ ⊢ (𝐵 ∈ 𝑋 → (𝐵 ∈ (𝑊 / ∼ ) ↔ ∃𝑥 ∈ 𝑊 𝐵 = {𝑦 ∈ 𝑊 ∣ ∃𝑛 ∈ (0...𝑁)𝑦 = (𝑥 cyclShift 𝑛)})) | ||
Theorem | eleclclwwlkn 26360* | A member of an equivalence class according to ∼. (Contributed by Alexander van der Vekens, 11-May-2018.) (Revised by Alexander van der Vekens, 15-Jun-2018.) |
⊢ 𝑊 = ((𝑉 ClWWalksN 𝐸)‘𝑁) & ⊢ ∼ = {〈𝑡, 𝑢〉 ∣ (𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊 ∧ ∃𝑛 ∈ (0...𝑁)𝑡 = (𝑢 cyclShift 𝑛))} ⇒ ⊢ ((𝐵 ∈ (𝑊 / ∼ ) ∧ 𝑋 ∈ 𝐵) → (𝑌 ∈ 𝐵 ↔ (𝑌 ∈ 𝑊 ∧ ∃𝑛 ∈ (0...𝑁)𝑌 = (𝑋 cyclShift 𝑛)))) | ||
Theorem | hashecclwwlkn1 26361* | 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.) |
⊢ 𝑊 = ((𝑉 ClWWalksN 𝐸)‘𝑁) & ⊢ ∼ = {〈𝑡, 𝑢〉 ∣ (𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊 ∧ ∃𝑛 ∈ (0...𝑁)𝑡 = (𝑢 cyclShift 𝑛))} ⇒ ⊢ ((𝑁 ∈ ℙ ∧ 𝑈 ∈ (𝑊 / ∼ )) → ((#‘𝑈) = 1 ∨ (#‘𝑈) = 𝑁)) | ||
Theorem | usghashecclwwlk 26362* | 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.) |
⊢ 𝑊 = ((𝑉 ClWWalksN 𝐸)‘𝑁) & ⊢ ∼ = {〈𝑡, 𝑢〉 ∣ (𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊 ∧ ∃𝑛 ∈ (0...𝑁)𝑡 = (𝑢 cyclShift 𝑛))} ⇒ ⊢ ((𝑉 USGrph 𝐸 ∧ 𝑁 ∈ ℙ) → (𝑈 ∈ (𝑊 / ∼ ) → (#‘𝑈) = 𝑁)) | ||
Theorem | hashclwwlkn 26363* | 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.) |
⊢ 𝑊 = ((𝑉 ClWWalksN 𝐸)‘𝑁) & ⊢ ∼ = {〈𝑡, 𝑢〉 ∣ (𝑡 ∈ 𝑊 ∧ 𝑢 ∈ 𝑊 ∧ ∃𝑛 ∈ (0...𝑁)𝑡 = (𝑢 cyclShift 𝑛))} ⇒ ⊢ ((𝑉 ∈ Fin ∧ 𝑉 USGrph 𝐸 ∧ 𝑁 ∈ ℙ) → (#‘𝑊) = ((#‘(𝑊 / ∼ )) · 𝑁)) | ||
Theorem | clwwlkndivn 26364 | 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.) |
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ ℙ) → 𝑁 ∥ (#‘((𝑉 ClWWalksN 𝐸)‘𝑁))) | ||
Theorem | wlklenvp1 26365 | The number of vertices of a walk (in an undirected graph) is the number of its edges plus 1. (Contributed by Alexander van der Vekens, 29-Jun-2018.) |
⊢ (𝐹(𝑉 Walks 𝐸)𝑃 → (#‘𝑃) = ((#‘𝐹) + 1)) | ||
Theorem | wlklenvclwlk 26366 | The number of vertices in a walk equals the length of the walk after it is "closed" (i.e. enhanced by an edge from its last vertex to its first vertex). (Contributed by Alexander van der Vekens, 29-Jun-2018.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 1 ≤ (#‘𝑊)) → (〈𝐹, (𝑊 ++ 〈“(𝑊‘0)”〉)〉 ∈ (𝑉 Walks 𝐸) → (#‘𝐹) = (#‘𝑊))) | ||
Theorem | clwlkfclwwlk2wrd 26367 | The second component of a closed walk is a word over the "vertices". (Contributed by Alexander van der Vekens, 25-Jun-2018.) |
⊢ 𝐴 = (1st ‘𝑐) & ⊢ 𝐵 = (2nd ‘𝑐) & ⊢ 𝐶 = {𝑐 ∈ (𝑉 ClWalks 𝐸) ∣ (#‘𝐴) = 𝑁} & ⊢ 𝐹 = (𝑐 ∈ 𝐶 ↦ (𝐵 substr 〈0, (#‘𝐴)〉)) ⇒ ⊢ (𝑐 ∈ 𝐶 → 𝐵 ∈ Word 𝑉) | ||
Theorem | clwlkfclwwlk1hashn 26368* | The size of the first component of a closed walk. (Contributed by Alexander van der Vekens, 5-Jul-2018.) |
⊢ 𝐴 = (1st ‘𝑐) & ⊢ 𝐵 = (2nd ‘𝑐) & ⊢ 𝐶 = {𝑐 ∈ (𝑉 ClWalks 𝐸) ∣ (#‘𝐴) = 𝑁} & ⊢ 𝐹 = (𝑐 ∈ 𝐶 ↦ (𝐵 substr 〈0, (#‘𝐴)〉)) ⇒ ⊢ (𝑊 ∈ 𝐶 → (#‘(1st ‘𝑊)) = 𝑁) | ||
Theorem | clwlkfclwwlk1hash 26369* | 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.) |
⊢ 𝐴 = (1st ‘𝑐) & ⊢ 𝐵 = (2nd ‘𝑐) & ⊢ 𝐶 = {𝑐 ∈ (𝑉 ClWalks 𝐸) ∣ (#‘𝐴) = 𝑁} & ⊢ 𝐹 = (𝑐 ∈ 𝐶 ↦ (𝐵 substr 〈0, (#‘𝐴)〉)) ⇒ ⊢ (𝑐 ∈ 𝐶 → (#‘𝐴) ∈ (0...(#‘𝐵))) | ||
Theorem | clwlkfclwwlk2sswd 26370* | 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.) |
⊢ 𝐴 = (1st ‘𝑐) & ⊢ 𝐵 = (2nd ‘𝑐) & ⊢ 𝐶 = {𝑐 ∈ (𝑉 ClWalks 𝐸) ∣ (#‘𝐴) = 𝑁} & ⊢ 𝐹 = (𝑐 ∈ 𝐶 ↦ (𝐵 substr 〈0, (#‘𝐴)〉)) ⇒ ⊢ (𝑐 ∈ 𝐶 → (#‘𝐴) = (#‘(𝐵 substr 〈0, (#‘𝐴)〉))) | ||
Theorem | clwlkfclwwlk 26371* | 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 (in an undirected simple graph). (Contributed by Alexander van der Vekens, 25-Jun-2018.) |
⊢ 𝐴 = (1st ‘𝑐) & ⊢ 𝐵 = (2nd ‘𝑐) & ⊢ 𝐶 = {𝑐 ∈ (𝑉 ClWalks 𝐸) ∣ (#‘𝐴) = 𝑁} & ⊢ 𝐹 = (𝑐 ∈ 𝐶 ↦ (𝐵 substr 〈0, (#‘𝐴)〉)) ⇒ ⊢ ((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ ℙ) → 𝐹:𝐶⟶((𝑉 ClWWalksN 𝐸)‘𝑁)) | ||
Theorem | clwlkfoclwwlk 26372* | 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 (in an undirected simple graph). (Contributed by Alexander van der Vekens, 30-Jun-2018.) |
⊢ 𝐴 = (1st ‘𝑐) & ⊢ 𝐵 = (2nd ‘𝑐) & ⊢ 𝐶 = {𝑐 ∈ (𝑉 ClWalks 𝐸) ∣ (#‘𝐴) = 𝑁} & ⊢ 𝐹 = (𝑐 ∈ 𝐶 ↦ (𝐵 substr 〈0, (#‘𝐴)〉)) ⇒ ⊢ ((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ ℙ) → 𝐹:𝐶–onto→((𝑉 ClWWalksN 𝐸)‘𝑁)) | ||
Theorem | clwlkf1clwwlklem1 26373* | Lemma 1 for clwlkf1clwwlklem 26376. (Contributed by Alexander van der Vekens, 5-Jul-2018.) |
⊢ 𝐴 = (1st ‘𝑐) & ⊢ 𝐵 = (2nd ‘𝑐) & ⊢ 𝐶 = {𝑐 ∈ (𝑉 ClWalks 𝐸) ∣ (#‘𝐴) = 𝑁} & ⊢ 𝐹 = (𝑐 ∈ 𝐶 ↦ (𝐵 substr 〈0, (#‘𝐴)〉)) ⇒ ⊢ (𝑊 ∈ 𝐶 → 𝑁 ≤ (#‘(2nd ‘𝑊))) | ||
Theorem | clwlkf1clwwlklem2 26374* | Lemma 2 for clwlkf1clwwlklem 26376. (Contributed by Alexander van der Vekens, 5-Jul-2018.) |
⊢ 𝐴 = (1st ‘𝑐) & ⊢ 𝐵 = (2nd ‘𝑐) & ⊢ 𝐶 = {𝑐 ∈ (𝑉 ClWalks 𝐸) ∣ (#‘𝐴) = 𝑁} & ⊢ 𝐹 = (𝑐 ∈ 𝐶 ↦ (𝐵 substr 〈0, (#‘𝐴)〉)) ⇒ ⊢ (𝑊 ∈ 𝐶 → ((2nd ‘𝑊)‘0) = ((2nd ‘𝑊)‘𝑁)) | ||
Theorem | clwlkf1clwwlklem3 26375* | Lemma 3 for clwlkf1clwwlklem 26376. (Contributed by Alexander van der Vekens, 5-Jul-2018.) |
⊢ 𝐴 = (1st ‘𝑐) & ⊢ 𝐵 = (2nd ‘𝑐) & ⊢ 𝐶 = {𝑐 ∈ (𝑉 ClWalks 𝐸) ∣ (#‘𝐴) = 𝑁} & ⊢ 𝐹 = (𝑐 ∈ 𝐶 ↦ (𝐵 substr 〈0, (#‘𝐴)〉)) ⇒ ⊢ (𝑊 ∈ 𝐶 → (2nd ‘𝑊) ∈ Word 𝑉) | ||
Theorem | clwlkf1clwwlklem 26376* | Lemma for clwlkf1clwwlk 26377. (Contributed by Alexander van der Vekens, 5-Jul-2018.) |
⊢ 𝐴 = (1st ‘𝑐) & ⊢ 𝐵 = (2nd ‘𝑐) & ⊢ 𝐶 = {𝑐 ∈ (𝑉 ClWalks 𝐸) ∣ (#‘𝐴) = 𝑁} & ⊢ 𝐹 = (𝑐 ∈ 𝐶 ↦ (𝐵 substr 〈0, (#‘𝐴)〉)) ⇒ ⊢ ((𝑁 ∈ ℕ ∧ 𝑈 ∈ 𝐶 ∧ 𝑊 ∈ 𝐶) → (((2nd ‘𝑈) substr 〈0, (#‘(1st ‘𝑈))〉) = ((2nd ‘𝑊) substr 〈0, (#‘(1st ‘𝑊))〉) → ∀𝑦 ∈ (0...𝑁)((2nd ‘𝑈)‘𝑦) = ((2nd ‘𝑊)‘𝑦))) | ||
Theorem | clwlkf1clwwlk 26377* | 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.) |
⊢ 𝐴 = (1st ‘𝑐) & ⊢ 𝐵 = (2nd ‘𝑐) & ⊢ 𝐶 = {𝑐 ∈ (𝑉 ClWalks 𝐸) ∣ (#‘𝐴) = 𝑁} & ⊢ 𝐹 = (𝑐 ∈ 𝐶 ↦ (𝐵 substr 〈0, (#‘𝐴)〉)) ⇒ ⊢ ((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ ℙ) → 𝐹:𝐶–1-1→((𝑉 ClWWalksN 𝐸)‘𝑁)) | ||
Theorem | clwlkf1oclwwlk 26378* | 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.) |
⊢ 𝐴 = (1st ‘𝑐) & ⊢ 𝐵 = (2nd ‘𝑐) & ⊢ 𝐶 = {𝑐 ∈ (𝑉 ClWalks 𝐸) ∣ (#‘𝐴) = 𝑁} & ⊢ 𝐹 = (𝑐 ∈ 𝐶 ↦ (𝐵 substr 〈0, (#‘𝐴)〉)) ⇒ ⊢ ((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ ℙ) → 𝐹:𝐶–1-1-onto→((𝑉 ClWWalksN 𝐸)‘𝑁)) | ||
Theorem | clwlksizeeq 26379* | 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.) (Proof shortened by AV, 4-May-2021.) |
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ ℙ) → (#‘((𝑉 ClWWalksN 𝐸)‘𝑁)) = (#‘{𝑐 ∈ (𝑉 ClWalks 𝐸) ∣ (#‘(1st ‘𝑐)) = 𝑁})) | ||
Theorem | clwlkndivn 26380* | 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.) |
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑉 ∈ Fin ∧ 𝑁 ∈ ℙ) → 𝑁 ∥ (#‘{𝑐 ∈ (𝑉 ClWalks 𝐸) ∣ (#‘(1st ‘𝑐)) = 𝑁})) | ||
Syntax | c2wlkot 26381 | Extend class notation with walks (of a graph) of length 2 as ordered triple. |
class 2WalksOt | ||
Syntax | c2wlkonot 26382 | Extend class notation with walks between two vertices (within a graph) of length 2 as ordered triple. |
class 2WalksOnOt | ||
Syntax | c2spthot 26383 | Extend class notation with paths (of a graph) of length 2 as ordered triple. |
class 2SPathsOt | ||
Syntax | c2pthonot 26384 | Extend class notation with simple paths between two vertices (within a graph) of length 2 as ordered triple. |
class 2SPathOnOt | ||
Definition | df-2wlkonot 26385* | Define the collection of walks of length 2 with particular endpoints as ordered triple (in a graph). (Contributed by Alexander van der Vekens, 15-Feb-2018.) |
⊢ 2WalksOnOt = (𝑣 ∈ V, 𝑒 ∈ V ↦ (𝑎 ∈ 𝑣, 𝑏 ∈ 𝑣 ↦ {𝑡 ∈ ((𝑣 × 𝑣) × 𝑣) ∣ ∃𝑓∃𝑝(𝑓(𝑎(𝑣 WalkOn 𝑒)𝑏)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st ‘𝑡)) = 𝑎 ∧ (2nd ‘(1st ‘𝑡)) = (𝑝‘1) ∧ (2nd ‘𝑡) = 𝑏))})) | ||
Definition | df-2wlksot 26386* | Define the collection of all walks of length 2 as ordered triple (in a graph). (Contributed by Alexander van der Vekens, 15-Feb-2018.) |
⊢ 2WalksOt = (𝑣 ∈ V, 𝑒 ∈ V ↦ {𝑡 ∈ ((𝑣 × 𝑣) × 𝑣) ∣ ∃𝑎 ∈ 𝑣 ∃𝑏 ∈ 𝑣 𝑡 ∈ (𝑎(𝑣 2WalksOnOt 𝑒)𝑏)}) | ||
Definition | df-2spthonot 26387* | Define the collection of simple paths of length 2 with particular endpoints as ordered triple (in a graph). (Contributed by Alexander van der Vekens, 1-Mar-2018.) |
⊢ 2SPathOnOt = (𝑣 ∈ V, 𝑒 ∈ V ↦ (𝑎 ∈ 𝑣, 𝑏 ∈ 𝑣 ↦ {𝑡 ∈ ((𝑣 × 𝑣) × 𝑣) ∣ ∃𝑓∃𝑝(𝑓(𝑎(𝑣 SPathOn 𝑒)𝑏)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st ‘𝑡)) = 𝑎 ∧ (2nd ‘(1st ‘𝑡)) = (𝑝‘1) ∧ (2nd ‘𝑡) = 𝑏))})) | ||
Definition | df-2spthsot 26388* | Define the collection of all simple paths of length 2 as ordered triple (in a graph). (Contributed by Alexander van der Vekens, 1-Mar-2018.) |
⊢ 2SPathsOt = (𝑣 ∈ V, 𝑒 ∈ V ↦ {𝑡 ∈ ((𝑣 × 𝑣) × 𝑣) ∣ ∃𝑎 ∈ 𝑣 ∃𝑏 ∈ 𝑣 𝑡 ∈ (𝑎(𝑣 2SPathOnOt 𝑒)𝑏)}) | ||
Theorem | el2wlkonotlem 26389 | Lemma for el2wlkonot 26396. (Contributed by Alexander van der Vekens, 15-Feb-2018.) |
⊢ ((𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2) → (𝑝‘1) ∈ 𝑉) | ||
Theorem | is2wlkonot 26390* | The set of walks of length 2 between two vertices (in a graph) as ordered triple. (Contributed by Alexander van der Vekens, 15-Feb-2018.) |
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (𝑉 2WalksOnOt 𝐸) = (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑓∃𝑝(𝑓(𝑎(𝑉 WalkOn 𝐸)𝑏)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st ‘𝑡)) = 𝑎 ∧ (2nd ‘(1st ‘𝑡)) = (𝑝‘1) ∧ (2nd ‘𝑡) = 𝑏))})) | ||
Theorem | is2spthonot 26391* | The set of simple paths of length 2 between two vertices (in a graph) as ordered triple. (Contributed by Alexander van der Vekens, 1-Mar-2018.) |
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (𝑉 2SPathOnOt 𝐸) = (𝑎 ∈ 𝑉, 𝑏 ∈ 𝑉 ↦ {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑓∃𝑝(𝑓(𝑎(𝑉 SPathOn 𝐸)𝑏)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st ‘𝑡)) = 𝑎 ∧ (2nd ‘(1st ‘𝑡)) = (𝑝‘1) ∧ (2nd ‘𝑡) = 𝑏))})) | ||
Theorem | 2wlkonot 26392* | The set of walks of length 2 between two vertices (in a graph) as ordered triple. (Contributed by Alexander van der Vekens, 15-Feb-2018.) |
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) → (𝐴(𝑉 2WalksOnOt 𝐸)𝐵) = {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑓∃𝑝(𝑓(𝐴(𝑉 WalkOn 𝐸)𝐵)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st ‘𝑡)) = 𝐴 ∧ (2nd ‘(1st ‘𝑡)) = (𝑝‘1) ∧ (2nd ‘𝑡) = 𝐵))}) | ||
Theorem | 2spthonot 26393* | The set of simple paths of length 2 between two vertices (in a graph) as ordered triple. (Contributed by Alexander van der Vekens, 1-Mar-2018.) |
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) → (𝐴(𝑉 2SPathOnOt 𝐸)𝐵) = {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑓∃𝑝(𝑓(𝐴(𝑉 SPathOn 𝐸)𝐵)𝑝 ∧ (#‘𝑓) = 2 ∧ ((1st ‘(1st ‘𝑡)) = 𝐴 ∧ (2nd ‘(1st ‘𝑡)) = (𝑝‘1) ∧ (2nd ‘𝑡) = 𝐵))}) | ||
Theorem | 2wlksot 26394* | The set of walks of length 2 (in a graph) as ordered triple. (Contributed by Alexander van der Vekens, 21-Feb-2018.) |
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (𝑉 2WalksOt 𝐸) = {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 𝑡 ∈ (𝑎(𝑉 2WalksOnOt 𝐸)𝑏)}) | ||
Theorem | 2spthsot 26395* | The set of simple paths of length 2 (in a graph) as ordered triple. (Contributed by Alexander van der Vekens, 28-Feb-2018.) |
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) → (𝑉 2SPathsOt 𝐸) = {𝑡 ∈ ((𝑉 × 𝑉) × 𝑉) ∣ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 𝑡 ∈ (𝑎(𝑉 2SPathOnOt 𝐸)𝑏)}) | ||
Theorem | el2wlkonot 26396* | A walk of length 2 between two vertices (in a graph) as ordered triple. (Contributed by Alexander van der Vekens, 15-Feb-2018.) |
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (𝑇 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐶) ↔ ∃𝑏 ∈ 𝑉 (𝑇 = 〈𝐴, 𝑏, 𝐶〉 ∧ ∃𝑓∃𝑝(𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)))))) | ||
Theorem | el2spthonot 26397* | A simple path of length 2 between two vertices (in a graph) as ordered triple. (Contributed by Alexander van der Vekens, 2-Mar-2018.) |
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (𝑇 ∈ (𝐴(𝑉 2SPathOnOt 𝐸)𝐶) ↔ ∃𝑏 ∈ 𝑉 (𝑇 = 〈𝐴, 𝑏, 𝐶〉 ∧ ∃𝑓∃𝑝(𝑓(𝑉 SPaths 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝑏 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)))))) | ||
Theorem | el2spthonot0 26398* | A simple path of length 2 between two vertices (in a graph) as ordered triple. (Contributed by Alexander van der Vekens, 9-Mar-2018.) |
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (𝑇 ∈ (𝐴(𝑉 2SPathOnOt 𝐸)𝐶) ↔ ∃𝑏 ∈ 𝑉 (𝑇 = 〈𝐴, 𝑏, 𝐶〉 ∧ 〈𝐴, 𝑏, 𝐶〉 ∈ (𝐴(𝑉 2SPathOnOt 𝐸)𝐶)))) | ||
Theorem | el2wlkonotot0 26399* | A walk of length 2 between two vertices (in a graph) as ordered triple. (Contributed by Alexander van der Vekens, 15-Feb-2018.) |
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑉)) → (〈𝐴, 𝐵, 𝐶〉 ∈ (𝑅(𝑉 2WalksOnOt 𝐸)𝑆) ↔ (𝐴 = 𝑅 ∧ 𝐶 = 𝑆 ∧ ∃𝑓∃𝑝(𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2)))))) | ||
Theorem | el2wlkonotot 26400* | A walk of length 2 between two vertices (in a graph) as ordered triple. (Contributed by Alexander van der Vekens, 15-Feb-2018.) |
⊢ (((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌) ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (〈𝐴, 𝐵, 𝐶〉 ∈ (𝐴(𝑉 2WalksOnOt 𝐸)𝐶) ↔ ∃𝑓∃𝑝(𝑓(𝑉 Walks 𝐸)𝑝 ∧ (#‘𝑓) = 2 ∧ (𝐴 = (𝑝‘0) ∧ 𝐵 = (𝑝‘1) ∧ 𝐶 = (𝑝‘2))))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |