P. 146 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 14501-14600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	repswsymball 14501*	All the symbols of a "repeated symbol word" are the same. (Contributed by AV, 10-Nov-2018.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑆 ∈ 𝑉) → (𝑊 = (𝑆 repeatS (♯‘𝑊)) → ∀𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) = 𝑆))
Theorem	repswsymballbi 14502*	A word is a "repeated symbol word" iff each of its symbols equals the first symbol of the word. (Contributed by AV, 10-Nov-2018.)
⊢ (𝑊 ∈ Word 𝑉 → (𝑊 = ((𝑊‘0) repeatS (♯‘𝑊)) ↔ ∀𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0)))
Theorem	repswfsts 14503	The first symbol of a nonempty "repeated symbol word". (Contributed by AV, 4-Nov-2018.)
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → ((𝑆 repeatS 𝑁)‘0) = 𝑆)
Theorem	repswlsw 14504	The last symbol of a nonempty "repeated symbol word". (Contributed by AV, 4-Nov-2018.)
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ) → (lastS‘(𝑆 repeatS 𝑁)) = 𝑆)
Theorem	repsw1 14505	The "repeated symbol word" of length 1. (Contributed by AV, 4-Nov-2018.)
⊢ (𝑆 ∈ 𝑉 → (𝑆 repeatS 1) = ⟨“𝑆”⟩)
Theorem	repswswrd 14506	A subword of a "repeated symbol word" is again a "repeated symbol word". The assumption 𝑁 ≤ 𝐿 is required, because otherwise (𝐿 < 𝑁): ((𝑆 repeatS 𝐿) substr ⟨𝑀, 𝑁⟩) = ∅, but for M < N (𝑆 repeatS (𝑁 − 𝑀))) ≠ ∅! The proof is relatively long because the border cases (𝑀 = 𝑁, ¬ (𝑀..^𝑁) ⊆ (0..^𝐿) must have been considered. (Contributed by AV, 6-Nov-2018.)
⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝐿) → ((𝑆 repeatS 𝐿) substr ⟨𝑀, 𝑁⟩) = (𝑆 repeatS (𝑁 − 𝑀)))
Theorem	repswpfx 14507	A prefix of a repeated symbol word is a repeated symbol word. (Contributed by AV, 11-May-2020.)
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝐿 ∈ (0...𝑁)) → ((𝑆 repeatS 𝑁) prefix 𝐿) = (𝑆 repeatS 𝐿))
Theorem	repswccat 14508	The concatenation of two "repeated symbol words" with the same symbol is again a "repeated symbol word". (Contributed by AV, 4-Nov-2018.)
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0) → ((𝑆 repeatS 𝑁) ++ (𝑆 repeatS 𝑀)) = (𝑆 repeatS (𝑁 + 𝑀)))
Theorem	repswrevw 14509	The reverse of a "repeated symbol word". (Contributed by AV, 6-Nov-2018.)
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → (reverse‘(𝑆 repeatS 𝑁)) = (𝑆 repeatS 𝑁))
5.7.14  Cyclical shifts of words A word/string can be regarded as "necklace" by connecting the two ends of the word/string together (see Wikipedia "Necklace (combinatorics)", https://en.wikipedia.org/wiki/Necklace_(combinatorics)). Two strings are regarded as the same necklace if one string can be rotated/circularly shifted/cyclically shifted to obtain the second string. To cope with words in the sense of necklaces, the rotation/cyclic shift cyclShift is defined as the basic operation, see df-csh 14511. The main theorems in this section are about counting the number of different necklaces resulting from cyclically shifting a given word, see cshwrepswhash1 16813 for words consisting of identical symbols and cshwshash 16815 for words having lengths which are prime numbers.
Syntax	ccsh 14510	Extend class notation with Cyclical Shifts.
class cyclShift
Definition	df-csh 14511*	Perform a cyclical shift for an arbitrary class. Meaningful only for words 𝑤 ∈ Word 𝑆 or at least functions over half-open ranges of nonnegative integers. (Contributed by Alexander van der Vekens, 20-May-2018.) (Revised by Mario Carneiro/Alexander van der Vekens/ Gerard Lang, 17-Nov-2018.) (Revised by AV, 4-Nov-2022.)
⊢ cyclShift = (𝑤 ∈ {𝑓 ∣ ∃𝑙 ∈ ℕ0 𝑓 Fn (0..^𝑙)}, 𝑛 ∈ ℤ ↦ if(𝑤 = ∅, ∅, ((𝑤 substr ⟨(𝑛 mod (♯‘𝑤)), (♯‘𝑤)⟩) ++ (𝑤 prefix (𝑛 mod (♯‘𝑤))))))
Theorem	cshfn 14512*	Perform a cyclical shift for a function over a half-open range of nonnegative integers. (Contributed by AV, 20-May-2018.) (Revised by AV, 17-Nov-2018.) (Revised by AV, 4-Nov-2022.)
⊢ ((𝑊 ∈ {𝑓 ∣ ∃𝑙 ∈ ℕ0 𝑓 Fn (0..^𝑙)} ∧ 𝑁 ∈ ℤ) → (𝑊 cyclShift 𝑁) = if(𝑊 = ∅, ∅, ((𝑊 substr ⟨(𝑁 mod (♯‘𝑊)), (♯‘𝑊)⟩) ++ (𝑊 prefix (𝑁 mod (♯‘𝑊))))))
Theorem	cshword 14513	Perform a cyclical shift for a word. (Contributed by Alexander van der Vekens, 20-May-2018.) (Revised by AV, 12-Oct-2022.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ) → (𝑊 cyclShift 𝑁) = ((𝑊 substr ⟨(𝑁 mod (♯‘𝑊)), (♯‘𝑊)⟩) ++ (𝑊 prefix (𝑁 mod (♯‘𝑊)))))
Theorem	cshnz 14514	A cyclical shift is the empty set if the number of shifts is not an integer. (Contributed by Alexander van der Vekens, 21-May-2018.) (Revised by AV, 17-Nov-2018.)
⊢ (¬ 𝑁 ∈ ℤ → (𝑊 cyclShift 𝑁) = ∅)
Theorem	0csh0 14515	Cyclically shifting an empty set/word always results in the empty word/set. (Contributed by AV, 25-Oct-2018.) (Revised by AV, 17-Nov-2018.)
⊢ (∅ cyclShift 𝑁) = ∅
Theorem	cshw0 14516	A word cyclically shifted by 0 is the word itself. (Contributed by AV, 16-May-2018.) (Revised by AV, 20-May-2018.) (Revised by AV, 26-Oct-2018.)
⊢ (𝑊 ∈ Word 𝑉 → (𝑊 cyclShift 0) = 𝑊)
Theorem	cshwmodn 14517	Cyclically shifting a word is invariant regarding modulo the word's length. (Contributed by AV, 26-Oct-2018.) (Proof shortened by AV, 16-Oct-2022.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ) → (𝑊 cyclShift 𝑁) = (𝑊 cyclShift (𝑁 mod (♯‘𝑊))))
Theorem	cshwsublen 14518	Cyclically shifting a word is invariant regarding subtraction of the word's length. (Contributed by AV, 3-Nov-2018.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ) → (𝑊 cyclShift 𝑁) = (𝑊 cyclShift (𝑁 − (♯‘𝑊))))
Theorem	cshwn 14519	A word cyclically shifted by its length is the word itself. (Contributed by AV, 16-May-2018.) (Revised by AV, 20-May-2018.) (Revised by AV, 26-Oct-2018.)
⊢ (𝑊 ∈ Word 𝑉 → (𝑊 cyclShift (♯‘𝑊)) = 𝑊)
Theorem	cshwcl 14520	A cyclically shifted word is a word over the same set as for the original word. (Contributed by AV, 16-May-2018.) (Revised by AV, 21-May-2018.) (Revised by AV, 27-Oct-2018.)
⊢ (𝑊 ∈ Word 𝑉 → (𝑊 cyclShift 𝑁) ∈ Word 𝑉)
Theorem	cshwlen 14521	The length of a cyclically shifted word is the same as the length of the original word. (Contributed by AV, 16-May-2018.) (Revised by AV, 20-May-2018.) (Revised by AV, 27-Oct-2018.) (Proof shortened by AV, 16-Oct-2022.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ) → (♯‘(𝑊 cyclShift 𝑁)) = (♯‘𝑊))
Theorem	cshwf 14522	A cyclically shifted word is a function from a half-open range of integers of the same length as the word as domain to the set of symbols for the word. (Contributed by AV, 12-Nov-2018.)
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝑁 ∈ ℤ) → (𝑊 cyclShift 𝑁):(0..^(♯‘𝑊))⟶𝐴)
Theorem	cshwfn 14523	A cyclically shifted word is a function with a half-open range of integers of the same length as the word as domain. (Contributed by AV, 12-Nov-2018.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ) → (𝑊 cyclShift 𝑁) Fn (0..^(♯‘𝑊)))
Theorem	cshwrn 14524	The range of a cyclically shifted word is a subset of the set of symbols for the word. (Contributed by AV, 12-Nov-2018.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ) → ran (𝑊 cyclShift 𝑁) ⊆ 𝑉)
Theorem	cshwidxmod 14525	The symbol at a given index of a cyclically shifted nonempty word is the symbol at the shifted index of the original word. (Contributed by AV, 13-May-2018.) (Revised by AV, 21-May-2018.) (Revised by AV, 30-Oct-2018.) (Proof shortened by AV, 12-Oct-2022.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))) → ((𝑊 cyclShift 𝑁)‘𝐼) = (𝑊‘((𝐼 + 𝑁) mod (♯‘𝑊))))
Theorem	cshwidxmodr 14526	The symbol at a given index of a cyclically shifted nonempty word is the symbol at the shifted index of the original word. (Contributed by AV, 17-Mar-2021.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(♯‘𝑊))) → ((𝑊 cyclShift 𝑁)‘((𝐼 − 𝑁) mod (♯‘𝑊))) = (𝑊‘𝐼))
Theorem	cshwidx0mod 14527	The symbol at index 0 of a cyclically shifted nonempty word is the symbol at index N (modulo the length of the word) of the original word. (Contributed by AV, 30-Oct-2018.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ∧ 𝑁 ∈ ℤ) → ((𝑊 cyclShift 𝑁)‘0) = (𝑊‘(𝑁 mod (♯‘𝑊))))
Theorem	cshwidx0 14528	The symbol at index 0 of a cyclically shifted nonempty word is the symbol at index N of the original word. (Contributed by AV, 15-May-2018.) (Revised by AV, 21-May-2018.) (Revised by AV, 30-Oct-2018.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0..^(♯‘𝑊))) → ((𝑊 cyclShift 𝑁)‘0) = (𝑊‘𝑁))
Theorem	cshwidxm1 14529	The symbol at index ((n-N)-1) of a word of length n (not 0) cyclically shifted by N positions is the symbol at index (n-1) of the original word. (Contributed by AV, 23-Mar-2018.) (Revised by AV, 21-May-2018.) (Revised by AV, 30-Oct-2018.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0..^(♯‘𝑊))) → ((𝑊 cyclShift 𝑁)‘(((♯‘𝑊) − 𝑁) − 1)) = (𝑊‘((♯‘𝑊) − 1)))
Theorem	cshwidxm 14530	The symbol at index (n-N) of a word of length n (not 0) cyclically shifted by N positions (not 0) is the symbol at index 0 of the original word. (Contributed by AV, 18-May-2018.) (Revised by AV, 21-May-2018.) (Revised by AV, 30-Oct-2018.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (1...(♯‘𝑊))) → ((𝑊 cyclShift 𝑁)‘((♯‘𝑊) − 𝑁)) = (𝑊‘0))
Theorem	cshwidxn 14531	The symbol at index (n-1) of a word of length n (not 0) cyclically shifted by N positions (not 0) is the symbol at index (N-1) of the original word. (Contributed by AV, 18-May-2018.) (Revised by AV, 21-May-2018.) (Revised by AV, 30-Oct-2018.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (1...(♯‘𝑊))) → ((𝑊 cyclShift 𝑁)‘((♯‘𝑊) − 1)) = (𝑊‘(𝑁 − 1)))
Theorem	cshf1 14532	Cyclically shifting a word which contains a symbol at most once results in a word which contains a symbol at most once. (Contributed by AV, 14-Mar-2021.)
⊢ ((𝐹:(0..^(♯‘𝐹))–1-1→𝐴 ∧ 𝑆 ∈ ℤ ∧ 𝐺 = (𝐹 cyclShift 𝑆)) → 𝐺:(0..^(♯‘𝐹))–1-1→𝐴)
Theorem	cshinj 14533	If a word is injectiv (regarded as function), the cyclically shifted word is also injective. (Contributed by AV, 14-Mar-2021.)
⊢ ((𝐹 ∈ Word 𝐴 ∧ Fun ◡𝐹 ∧ 𝑆 ∈ ℤ) → (𝐺 = (𝐹 cyclShift 𝑆) → Fun ◡𝐺))
Theorem	repswcshw 14534	A cyclically shifted "repeated symbol word". (Contributed by Alexander van der Vekens, 7-Nov-2018.) (Proof shortened by AV, 16-Oct-2022.)
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝐼 ∈ ℤ) → ((𝑆 repeatS 𝑁) cyclShift 𝐼) = (𝑆 repeatS 𝑁))
Theorem	2cshw 14535	Cyclically shifting a word two times. (Contributed by AV, 7-Apr-2018.) (Revised by AV, 4-Jun-2018.) (Revised by AV, 31-Oct-2018.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑊 cyclShift 𝑀) cyclShift 𝑁) = (𝑊 cyclShift (𝑀 + 𝑁)))
Theorem	2cshwid 14536	Cyclically shifting a word two times resulting in the word itself. (Contributed by AV, 7-Apr-2018.) (Revised by AV, 5-Jun-2018.) (Revised by AV, 1-Nov-2018.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ) → ((𝑊 cyclShift 𝑁) cyclShift ((♯‘𝑊) − 𝑁)) = 𝑊)
Theorem	lswcshw 14537	The last symbol of a word cyclically shifted by N positions is the symbol at index (N-1) of the original word. (Contributed by AV, 21-Mar-2018.) (Revised by AV, 5-Jun-2018.) (Revised by AV, 1-Nov-2018.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (1...(♯‘𝑊))) → (lastS‘(𝑊 cyclShift 𝑁)) = (𝑊‘(𝑁 − 1)))
Theorem	2cshwcom 14538	Cyclically shifting a word two times is commutative. (Contributed by AV, 21-Apr-2018.) (Revised by AV, 5-Jun-2018.) (Revised by Mario Carneiro/AV, 1-Nov-2018.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((𝑊 cyclShift 𝑁) cyclShift 𝑀) = ((𝑊 cyclShift 𝑀) cyclShift 𝑁))
Theorem	cshwleneq 14539	If the results of cyclically shifting two words are equal, the length of the two words was equal. (Contributed by AV, 21-Apr-2018.) (Revised by AV, 5-Jun-2018.) (Revised by AV, 1-Nov-2018.)
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ) ∧ (𝑊 cyclShift 𝑁) = (𝑈 cyclShift 𝑀)) → (♯‘𝑊) = (♯‘𝑈))
Theorem	3cshw 14540	Cyclically shifting a word three times results in a once cyclically shifted word under certain circumstances. (Contributed by AV, 6-Jun-2018.) (Revised by AV, 1-Nov-2018.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑊 cyclShift 𝑁) = (((𝑊 cyclShift 𝑀) cyclShift 𝑁) cyclShift ((♯‘𝑊) − 𝑀)))
Theorem	cshweqdif2 14541	If cyclically shifting two words (of the same length) results in the same word, cyclically shifting one of the words by the difference of the numbers of shifts results in the other word. (Contributed by AV, 21-Apr-2018.) (Revised by AV, 6-Jun-2018.) (Revised by AV, 1-Nov-2018.)
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ)) → ((𝑊 cyclShift 𝑁) = (𝑈 cyclShift 𝑀) → (𝑈 cyclShift (𝑀 − 𝑁)) = 𝑊))
Theorem	cshweqdifid 14542	If cyclically shifting a word by two positions results in the same word, cyclically shifting the word by the difference of these two positions results in the original word itself. (Contributed by AV, 21-Apr-2018.) (Revised by AV, 7-Jun-2018.) (Revised by AV, 1-Nov-2018.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((𝑊 cyclShift 𝑁) = (𝑊 cyclShift 𝑀) → (𝑊 cyclShift (𝑀 − 𝑁)) = 𝑊))
Theorem	cshweqrep 14543*	If cyclically shifting a word by L position results in the word itself, the symbol at any position is repeated at multiples of L (modulo the length of the word) positions in the word. (Contributed by AV, 13-May-2018.) (Revised by AV, 7-Jun-2018.) (Revised by AV, 1-Nov-2018.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℤ) → (((𝑊 cyclShift 𝐿) = 𝑊 ∧ 𝐼 ∈ (0..^(♯‘𝑊))) → ∀𝑗 ∈ ℕ0 (𝑊‘𝐼) = (𝑊‘((𝐼 + (𝑗 · 𝐿)) mod (♯‘𝑊)))))
Theorem	cshw1 14544*	If cyclically shifting a word by 1 position results in the word itself, the word is build of identical symbols. Remark: also "valid" for an empty word! (Contributed by AV, 13-May-2018.) (Revised by AV, 7-Jun-2018.) (Proof shortened by AV, 1-Nov-2018.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ (𝑊 cyclShift 1) = 𝑊) → ∀𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) = (𝑊‘0))
Theorem	cshw1repsw 14545	If cyclically shifting a word by 1 position results in the word itself, the word is a "repeated symbol word". Remark: also "valid" for an empty word! (Contributed by AV, 8-Nov-2018.) (Proof shortened by AV, 10-Nov-2018.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ (𝑊 cyclShift 1) = 𝑊) → 𝑊 = ((𝑊‘0) repeatS (♯‘𝑊)))
Theorem	cshwsexa 14546*	The class of (different!) words resulting by cyclically shifting something (not necessarily a word) is a set. (Contributed by AV, 8-Jun-2018.) (Revised by Mario Carneiro/AV, 25-Oct-2018.)
⊢ {𝑤 ∈ Word 𝑉 ∣ ∃𝑛 ∈ (0..^(♯‘𝑊))(𝑊 cyclShift 𝑛) = 𝑤} ∈ V
Theorem	2cshwcshw 14547*	If a word is a cyclically shifted word, and a second word is the result of cyclically shifting the same word, then the second word is the result of cyclically shifting the first word. (Contributed by AV, 11-May-2018.) (Revised by AV, 12-Jun-2018.) (Proof shortened by AV, 3-Nov-2018.)
⊢ ((𝑌 ∈ Word 𝑉 ∧ (♯‘𝑌) = 𝑁) → ((𝐾 ∈ (0...𝑁) ∧ 𝑋 = (𝑌 cyclShift 𝐾) ∧ ∃𝑚 ∈ (0...𝑁)𝑍 = (𝑌 cyclShift 𝑚)) → ∃𝑛 ∈ (0...𝑁)𝑍 = (𝑋 cyclShift 𝑛)))
Theorem	scshwfzeqfzo 14548*	For a nonempty word the sets of shifted words, expressd by a finite interval of integers or by a half-open integer range are identical. (Contributed by Alexander van der Vekens, 15-Jun-2018.)
⊢ ((𝑋 ∈ Word 𝑉 ∧ 𝑋 ≠ ∅ ∧ 𝑁 = (♯‘𝑋)) → {𝑦 ∈ Word 𝑉 ∣ ∃𝑛 ∈ (0...𝑁)𝑦 = (𝑋 cyclShift 𝑛)} = {𝑦 ∈ Word 𝑉 ∣ ∃𝑛 ∈ (0..^𝑁)𝑦 = (𝑋 cyclShift 𝑛)})
Theorem	cshwcshid 14549*	A cyclically shifted word can be reconstructed by cyclically shifting it again. Lemma for erclwwlksym 28394 and erclwwlknsym 28443. (Contributed by AV, 8-Apr-2018.) (Revised by AV, 11-Jun-2018.) (Proof shortened by AV, 3-Nov-2018.)
⊢ (𝜑 → 𝑦 ∈ Word 𝑉)    &   ⊢ (𝜑 → (♯‘𝑥) = (♯‘𝑦))    ⇒   ⊢ (𝜑 → ((𝑚 ∈ (0...(♯‘𝑦)) ∧ 𝑥 = (𝑦 cyclShift 𝑚)) → ∃𝑛 ∈ (0...(♯‘𝑥))𝑦 = (𝑥 cyclShift 𝑛)))
Theorem	cshwcsh2id 14550*	A cyclically shifted word can be reconstructed by cyclically shifting it again twice. Lemma for erclwwlktr 28395 and erclwwlkntr 28444. (Contributed by AV, 9-Apr-2018.) (Revised by AV, 11-Jun-2018.) (Proof shortened by AV, 3-Nov-2018.)
⊢ (𝜑 → 𝑧 ∈ Word 𝑉)    &   ⊢ (𝜑 → ((♯‘𝑦) = (♯‘𝑧) ∧ (♯‘𝑥) = (♯‘𝑦)))    ⇒   ⊢ (𝜑 → (((𝑚 ∈ (0...(♯‘𝑦)) ∧ 𝑥 = (𝑦 cyclShift 𝑚)) ∧ (𝑘 ∈ (0...(♯‘𝑧)) ∧ 𝑦 = (𝑧 cyclShift 𝑘))) → ∃𝑛 ∈ (0...(♯‘𝑧))𝑥 = (𝑧 cyclShift 𝑛)))
Theorem	cshimadifsn 14551	The image of a cyclically shifted word under its domain without its left bound is the image of a cyclically shifted word under its domain without the number of shifted symbols. (Contributed by AV, 19-Mar-2021.)
⊢ ((𝐹 ∈ Word 𝑆 ∧ 𝑁 = (♯‘𝐹) ∧ 𝐽 ∈ (0..^𝑁)) → (𝐹 “ ((0..^𝑁) ∖ {𝐽})) = ((𝐹 cyclShift 𝐽) “ (1..^𝑁)))
Theorem	cshimadifsn0 14552	The image of a cyclically shifted word under its domain without its upper bound is the image of a cyclically shifted word under its domain without the number of shifted symbols. (Contributed by AV, 19-Mar-2021.)
⊢ ((𝐹 ∈ Word 𝑆 ∧ 𝑁 = (♯‘𝐹) ∧ 𝐽 ∈ (0..^𝑁)) → (𝐹 “ ((0..^𝑁) ∖ {𝐽})) = ((𝐹 cyclShift (𝐽 + 1)) “ (0..^(𝑁 − 1))))
5.7.15  Mapping words by a function
Theorem	wrdco 14553	Mapping a word by a function. (Contributed by Stefan O'Rear, 27-Aug-2015.)
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (𝐹 ∘ 𝑊) ∈ Word 𝐵)
Theorem	lenco 14554	Length of a mapped word is unchanged. (Contributed by Stefan O'Rear, 27-Aug-2015.)
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (♯‘(𝐹 ∘ 𝑊)) = (♯‘𝑊))
Theorem	s1co 14555	Mapping of a singleton word. (Contributed by Mario Carneiro, 27-Sep-2015.) (Revised by Mario Carneiro, 26-Feb-2016.)
⊢ ((𝑆 ∈ 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (𝐹 ∘ ⟨“𝑆”⟩) = ⟨“(𝐹‘𝑆)”⟩)
Theorem	revco 14556	Mapping of words (i.e., a letterwise mapping) commutes with reversal. (Contributed by Stefan O'Rear, 27-Aug-2015.)
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (𝐹 ∘ (reverse‘𝑊)) = (reverse‘(𝐹 ∘ 𝑊)))
Theorem	ccatco 14557	Mapping of words commutes with concatenation. (Contributed by Stefan O'Rear, 27-Aug-2015.)
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (𝐹 ∘ (𝑆 ++ 𝑇)) = ((𝐹 ∘ 𝑆) ++ (𝐹 ∘ 𝑇)))
Theorem	cshco 14558	Mapping of words commutes with the "cyclical shift" operation. (Contributed by AV, 12-Nov-2018.)
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝑁 ∈ ℤ ∧ 𝐹:𝐴⟶𝐵) → (𝐹 ∘ (𝑊 cyclShift 𝑁)) = ((𝐹 ∘ 𝑊) cyclShift 𝑁))
Theorem	swrdco 14559	Mapping of words commutes with the substring operation. (Contributed by AV, 11-Nov-2018.)
⊢ ((𝑊 ∈ Word 𝐴 ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ 𝐹:𝐴⟶𝐵) → (𝐹 ∘ (𝑊 substr ⟨𝑀, 𝑁⟩)) = ((𝐹 ∘ 𝑊) substr ⟨𝑀, 𝑁⟩))
Theorem	pfxco 14560	Mapping of words commutes with the prefix operation. (Contributed by AV, 15-May-2020.)
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝑁 ∈ (0...(♯‘𝑊)) ∧ 𝐹:𝐴⟶𝐵) → (𝐹 ∘ (𝑊 prefix 𝑁)) = ((𝐹 ∘ 𝑊) prefix 𝑁))
Theorem	lswco 14561	Mapping of (nonempty) words commutes with the "last symbol" operation. This theorem would not hold if 𝑊 = ∅, (𝐹‘∅) ≠ ∅ and ∅ ∈ 𝐴, because then (lastS‘(𝐹 ∘ 𝑊)) = (lastS‘∅) = ∅ ≠ (𝐹‘∅) = (𝐹(lastS‘𝑊)). (Contributed by AV, 11-Nov-2018.)
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝑊 ≠ ∅ ∧ 𝐹:𝐴⟶𝐵) → (lastS‘(𝐹 ∘ 𝑊)) = (𝐹‘(lastS‘𝑊)))
Theorem	repsco 14562	Mapping of words commutes with the "repeated symbol" operation. (Contributed by AV, 11-Nov-2018.)
⊢ ((𝑆 ∈ 𝐴 ∧ 𝑁 ∈ ℕ0 ∧ 𝐹:𝐴⟶𝐵) → (𝐹 ∘ (𝑆 repeatS 𝑁)) = ((𝐹‘𝑆) repeatS 𝑁))
5.7.16  Longer string literals
Syntax	cs2 14563	Syntax for the length 2 word constructor.
class ⟨“𝐴𝐵”⟩
Syntax	cs3 14564	Syntax for the length 3 word constructor.
class ⟨“𝐴𝐵𝐶”⟩
Syntax	cs4 14565	Syntax for the length 4 word constructor.
class ⟨“𝐴𝐵𝐶𝐷”⟩
Syntax	cs5 14566	Syntax for the length 5 word constructor.
class ⟨“𝐴𝐵𝐶𝐷𝐸”⟩
Syntax	cs6 14567	Syntax for the length 6 word constructor.
class ⟨“𝐴𝐵𝐶𝐷𝐸𝐹”⟩
Syntax	cs7 14568	Syntax for the length 7 word constructor.
class ⟨“𝐴𝐵𝐶𝐷𝐸𝐹𝐺”⟩
Syntax	cs8 14569	Syntax for the length 8 word constructor.
class ⟨“𝐴𝐵𝐶𝐷𝐸𝐹𝐺𝐻”⟩
Definition	df-s2 14570	Define the length 2 word constructor. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ ⟨“𝐴𝐵”⟩ = (⟨“𝐴”⟩ ++ ⟨“𝐵”⟩)
Definition	df-s3 14571	Define the length 3 word constructor. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ ⟨“𝐴𝐵𝐶”⟩ = (⟨“𝐴𝐵”⟩ ++ ⟨“𝐶”⟩)
Definition	df-s4 14572	Define the length 4 word constructor. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ ⟨“𝐴𝐵𝐶𝐷”⟩ = (⟨“𝐴𝐵𝐶”⟩ ++ ⟨“𝐷”⟩)
Definition	df-s5 14573	Define the length 5 word constructor. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ ⟨“𝐴𝐵𝐶𝐷𝐸”⟩ = (⟨“𝐴𝐵𝐶𝐷”⟩ ++ ⟨“𝐸”⟩)
Definition	df-s6 14574	Define the length 6 word constructor. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ ⟨“𝐴𝐵𝐶𝐷𝐸𝐹”⟩ = (⟨“𝐴𝐵𝐶𝐷𝐸”⟩ ++ ⟨“𝐹”⟩)
Definition	df-s7 14575	Define the length 7 word constructor. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ ⟨“𝐴𝐵𝐶𝐷𝐸𝐹𝐺”⟩ = (⟨“𝐴𝐵𝐶𝐷𝐸𝐹”⟩ ++ ⟨“𝐺”⟩)
Definition	df-s8 14576	Define the length 8 word constructor. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ ⟨“𝐴𝐵𝐶𝐷𝐸𝐹𝐺𝐻”⟩ = (⟨“𝐴𝐵𝐶𝐷𝐸𝐹𝐺”⟩ ++ ⟨“𝐻”⟩)
Theorem	cats1cld 14577	Closure of concatenation with a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ 𝑇 = (𝑆 ++ ⟨“𝑋”⟩)    &   ⊢ (𝜑 → 𝑆 ∈ Word 𝐴)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    ⇒   ⊢ (𝜑 → 𝑇 ∈ Word 𝐴)
Theorem	cats1co 14578	Closure of concatenation with a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ 𝑇 = (𝑆 ++ ⟨“𝑋”⟩)    &   ⊢ (𝜑 → 𝑆 ∈ Word 𝐴)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ (𝜑 → (𝐹 ∘ 𝑆) = 𝑈)    &   ⊢ 𝑉 = (𝑈 ++ ⟨“(𝐹‘𝑋)”⟩)    ⇒   ⊢ (𝜑 → (𝐹 ∘ 𝑇) = 𝑉)
Theorem	cats1cli 14579	Closure of concatenation with a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ 𝑇 = (𝑆 ++ ⟨“𝑋”⟩)    &   ⊢ 𝑆 ∈ Word V    ⇒   ⊢ 𝑇 ∈ Word V
Theorem	cats1fvn 14580	The last symbol of a concatenation with a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ 𝑇 = (𝑆 ++ ⟨“𝑋”⟩)    &   ⊢ 𝑆 ∈ Word V    &   ⊢ (♯‘𝑆) = 𝑀    ⇒   ⊢ (𝑋 ∈ 𝑉 → (𝑇‘𝑀) = 𝑋)
Theorem	cats1fv 14581	A symbol other than the last in a concatenation with a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ 𝑇 = (𝑆 ++ ⟨“𝑋”⟩)    &   ⊢ 𝑆 ∈ Word V    &   ⊢ (♯‘𝑆) = 𝑀    &   ⊢ (𝑌 ∈ 𝑉 → (𝑆‘𝑁) = 𝑌)    &   ⊢ 𝑁 ∈ ℕ0    &   ⊢ 𝑁 < 𝑀    ⇒   ⊢ (𝑌 ∈ 𝑉 → (𝑇‘𝑁) = 𝑌)
Theorem	cats1len 14582	The length of concatenation with a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ 𝑇 = (𝑆 ++ ⟨“𝑋”⟩)    &   ⊢ 𝑆 ∈ Word V    &   ⊢ (♯‘𝑆) = 𝑀    &   ⊢ (𝑀 + 1) = 𝑁    ⇒   ⊢ (♯‘𝑇) = 𝑁
Theorem	cats1cat 14583	Closure of concatenation with a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ 𝑇 = (𝑆 ++ ⟨“𝑋”⟩)    &   ⊢ 𝐴 ∈ Word V    &   ⊢ 𝑆 ∈ Word V    &   ⊢ 𝐶 = (𝐵 ++ ⟨“𝑋”⟩)    &   ⊢ 𝐵 = (𝐴 ++ 𝑆)    ⇒   ⊢ 𝐶 = (𝐴 ++ 𝑇)
Theorem	cats2cat 14584	Closure of concatenation of concatenations with singleton words. (Contributed by AV, 1-Mar-2021.)
⊢ 𝐵 ∈ Word V    &   ⊢ 𝐷 ∈ Word V    &   ⊢ 𝐴 = (𝐵 ++ ⟨“𝑋”⟩)    &   ⊢ 𝐶 = (⟨“𝑌”⟩ ++ 𝐷)    ⇒   ⊢ (𝐴 ++ 𝐶) = ((𝐵 ++ ⟨“𝑋𝑌”⟩) ++ 𝐷)
Theorem	s2eqd 14585	Equality theorem for a doubleton word. (Contributed by Mario Carneiro, 27-Feb-2016.)
⊢ (𝜑 → 𝐴 = 𝑁)    &   ⊢ (𝜑 → 𝐵 = 𝑂)    ⇒   ⊢ (𝜑 → ⟨“𝐴𝐵”⟩ = ⟨“𝑁𝑂”⟩)
Theorem	s3eqd 14586	Equality theorem for a length 3 word. (Contributed by Mario Carneiro, 27-Feb-2016.)
⊢ (𝜑 → 𝐴 = 𝑁)    &   ⊢ (𝜑 → 𝐵 = 𝑂)    &   ⊢ (𝜑 → 𝐶 = 𝑃)    ⇒   ⊢ (𝜑 → ⟨“𝐴𝐵𝐶”⟩ = ⟨“𝑁𝑂𝑃”⟩)
Theorem	s4eqd 14587	Equality theorem for a length 4 word. (Contributed by Mario Carneiro, 27-Feb-2016.)
⊢ (𝜑 → 𝐴 = 𝑁)    &   ⊢ (𝜑 → 𝐵 = 𝑂)    &   ⊢ (𝜑 → 𝐶 = 𝑃)    &   ⊢ (𝜑 → 𝐷 = 𝑄)    ⇒   ⊢ (𝜑 → ⟨“𝐴𝐵𝐶𝐷”⟩ = ⟨“𝑁𝑂𝑃𝑄”⟩)
Theorem	s5eqd 14588	Equality theorem for a length 5 word. (Contributed by Mario Carneiro, 27-Feb-2016.)
⊢ (𝜑 → 𝐴 = 𝑁)    &   ⊢ (𝜑 → 𝐵 = 𝑂)    &   ⊢ (𝜑 → 𝐶 = 𝑃)    &   ⊢ (𝜑 → 𝐷 = 𝑄)    &   ⊢ (𝜑 → 𝐸 = 𝑅)    ⇒   ⊢ (𝜑 → ⟨“𝐴𝐵𝐶𝐷𝐸”⟩ = ⟨“𝑁𝑂𝑃𝑄𝑅”⟩)
Theorem	s6eqd 14589	Equality theorem for a length 6 word. (Contributed by Mario Carneiro, 27-Feb-2016.)
⊢ (𝜑 → 𝐴 = 𝑁)    &   ⊢ (𝜑 → 𝐵 = 𝑂)    &   ⊢ (𝜑 → 𝐶 = 𝑃)    &   ⊢ (𝜑 → 𝐷 = 𝑄)    &   ⊢ (𝜑 → 𝐸 = 𝑅)    &   ⊢ (𝜑 → 𝐹 = 𝑆)    ⇒   ⊢ (𝜑 → ⟨“𝐴𝐵𝐶𝐷𝐸𝐹”⟩ = ⟨“𝑁𝑂𝑃𝑄𝑅𝑆”⟩)
Theorem	s7eqd 14590	Equality theorem for a length 7 word. (Contributed by Mario Carneiro, 27-Feb-2016.)
⊢ (𝜑 → 𝐴 = 𝑁)    &   ⊢ (𝜑 → 𝐵 = 𝑂)    &   ⊢ (𝜑 → 𝐶 = 𝑃)    &   ⊢ (𝜑 → 𝐷 = 𝑄)    &   ⊢ (𝜑 → 𝐸 = 𝑅)    &   ⊢ (𝜑 → 𝐹 = 𝑆)    &   ⊢ (𝜑 → 𝐺 = 𝑇)    ⇒   ⊢ (𝜑 → ⟨“𝐴𝐵𝐶𝐷𝐸𝐹𝐺”⟩ = ⟨“𝑁𝑂𝑃𝑄𝑅𝑆𝑇”⟩)
Theorem	s8eqd 14591	Equality theorem for a length 8 word. (Contributed by Mario Carneiro, 27-Feb-2016.)
⊢ (𝜑 → 𝐴 = 𝑁)    &   ⊢ (𝜑 → 𝐵 = 𝑂)    &   ⊢ (𝜑 → 𝐶 = 𝑃)    &   ⊢ (𝜑 → 𝐷 = 𝑄)    &   ⊢ (𝜑 → 𝐸 = 𝑅)    &   ⊢ (𝜑 → 𝐹 = 𝑆)    &   ⊢ (𝜑 → 𝐺 = 𝑇)    &   ⊢ (𝜑 → 𝐻 = 𝑈)    ⇒   ⊢ (𝜑 → ⟨“𝐴𝐵𝐶𝐷𝐸𝐹𝐺𝐻”⟩ = ⟨“𝑁𝑂𝑃𝑄𝑅𝑆𝑇𝑈”⟩)
Theorem	s3eq2 14592	Equality theorem for a length 3 word for the second symbol. (Contributed by AV, 4-Jan-2022.)
⊢ (𝐵 = 𝐷 → ⟨“𝐴𝐵𝐶”⟩ = ⟨“𝐴𝐷𝐶”⟩)
Theorem	s2cld 14593	A doubleton word is a word. (Contributed by Mario Carneiro, 27-Feb-2016.)
⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑋)    ⇒   ⊢ (𝜑 → ⟨“𝐴𝐵”⟩ ∈ Word 𝑋)
Theorem	s3cld 14594	A length 3 string is a word. (Contributed by Mario Carneiro, 27-Feb-2016.)
⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑋)    ⇒   ⊢ (𝜑 → ⟨“𝐴𝐵𝐶”⟩ ∈ Word 𝑋)
Theorem	s4cld 14595	A length 4 string is a word. (Contributed by Mario Carneiro, 27-Feb-2016.)
⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑋)    ⇒   ⊢ (𝜑 → ⟨“𝐴𝐵𝐶𝐷”⟩ ∈ Word 𝑋)
Theorem	s5cld 14596	A length 5 string is a word. (Contributed by Mario Carneiro, 27-Feb-2016.)
⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑋)    ⇒   ⊢ (𝜑 → ⟨“𝐴𝐵𝐶𝐷𝐸”⟩ ∈ Word 𝑋)
Theorem	s6cld 14597	A length 6 string is a word. (Contributed by Mario Carneiro, 27-Feb-2016.)
⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑋)    ⇒   ⊢ (𝜑 → ⟨“𝐴𝐵𝐶𝐷𝐸𝐹”⟩ ∈ Word 𝑋)
Theorem	s7cld 14598	A length 7 string is a word. (Contributed by Mario Carneiro, 27-Feb-2016.)
⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑋)    ⇒   ⊢ (𝜑 → ⟨“𝐴𝐵𝐶𝐷𝐸𝐹𝐺”⟩ ∈ Word 𝑋)
Theorem	s8cld 14599	A length 7 string is a word. (Contributed by Mario Carneiro, 27-Feb-2016.)
⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐻 ∈ 𝑋)    ⇒   ⊢ (𝜑 → ⟨“𝐴𝐵𝐶𝐷𝐸𝐹𝐺𝐻”⟩ ∈ Word 𝑋)
Theorem	s2cl 14600	A doubleton word is a word. (Contributed by Stefan O'Rear, 23-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.)
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ⟨“𝐴𝐵”⟩ ∈ Word 𝑋)