P. 148 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 14701-14800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	2cshw 14701	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 14702	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 14703	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 14704	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 14705	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 14706	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 14707	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 14708	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 14709*	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 14710*	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 14711	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 14712*	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.) (Proof shortened by SN, 15-Jan-2025.)
⊢ {𝑤 ∈ Word 𝑉 ∣ ∃𝑛 ∈ (0..^(♯‘𝑊))(𝑊 cyclShift 𝑛) = 𝑤} ∈ V
Theorem	cshwsexaOLD 14713*	Obsolete version of cshwsexa 14712 as of 15-Jan-2025. (Contributed by AV, 8-Jun-2018.) (Revised by Mario Carneiro/AV, 25-Oct-2018.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ {𝑤 ∈ Word 𝑉 ∣ ∃𝑛 ∈ (0..^(♯‘𝑊))(𝑊 cyclShift 𝑛) = 𝑤} ∈ V
Theorem	2cshwcshw 14714*	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 14715*	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 14716*	A cyclically shifted word can be reconstructed by cyclically shifting it again. Lemma for erclwwlksym 28965 and erclwwlknsym 29014. (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 14717*	A cyclically shifted word can be reconstructed by cyclically shifting it again twice. Lemma for erclwwlktr 28966 and erclwwlkntr 29015. (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 14718	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 14719	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 14720	Mapping a word by a function. (Contributed by Stefan O'Rear, 27-Aug-2015.)
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (𝐹 ∘ 𝑊) ∈ Word 𝐵)
Theorem	lenco 14721	Length of a mapped word is unchanged. (Contributed by Stefan O'Rear, 27-Aug-2015.)
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (♯‘(𝐹 ∘ 𝑊)) = (♯‘𝑊))
Theorem	s1co 14722	Mapping of a singleton word. (Contributed by Mario Carneiro, 27-Sep-2015.) (Revised by Mario Carneiro, 26-Feb-2016.)
⊢ ((𝑆 ∈ 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (𝐹 ∘ ⟨“𝑆”⟩) = ⟨“(𝐹‘𝑆)”⟩)
Theorem	revco 14723	Mapping of words (i.e., a letterwise mapping) commutes with reversal. (Contributed by Stefan O'Rear, 27-Aug-2015.)
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (𝐹 ∘ (reverse‘𝑊)) = (reverse‘(𝐹 ∘ 𝑊)))
Theorem	ccatco 14724	Mapping of words commutes with concatenation. (Contributed by Stefan O'Rear, 27-Aug-2015.)
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (𝐹 ∘ (𝑆 ++ 𝑇)) = ((𝐹 ∘ 𝑆) ++ (𝐹 ∘ 𝑇)))
Theorem	cshco 14725	Mapping of words commutes with the "cyclical shift" operation. (Contributed by AV, 12-Nov-2018.)
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝑁 ∈ ℤ ∧ 𝐹:𝐴⟶𝐵) → (𝐹 ∘ (𝑊 cyclShift 𝑁)) = ((𝐹 ∘ 𝑊) cyclShift 𝑁))
Theorem	swrdco 14726	Mapping of words commutes with the substring operation. (Contributed by AV, 11-Nov-2018.)
⊢ ((𝑊 ∈ Word 𝐴 ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ 𝐹:𝐴⟶𝐵) → (𝐹 ∘ (𝑊 substr ⟨𝑀, 𝑁⟩)) = ((𝐹 ∘ 𝑊) substr ⟨𝑀, 𝑁⟩))
Theorem	pfxco 14727	Mapping of words commutes with the prefix operation. (Contributed by AV, 15-May-2020.)
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝑁 ∈ (0...(♯‘𝑊)) ∧ 𝐹:𝐴⟶𝐵) → (𝐹 ∘ (𝑊 prefix 𝑁)) = ((𝐹 ∘ 𝑊) prefix 𝑁))
Theorem	lswco 14728	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 14729	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 14730	Syntax for the length 2 word constructor.
class ⟨“𝐴𝐵”⟩
Syntax	cs3 14731	Syntax for the length 3 word constructor.
class ⟨“𝐴𝐵𝐶”⟩
Syntax	cs4 14732	Syntax for the length 4 word constructor.
class ⟨“𝐴𝐵𝐶𝐷”⟩
Syntax	cs5 14733	Syntax for the length 5 word constructor.
class ⟨“𝐴𝐵𝐶𝐷𝐸”⟩
Syntax	cs6 14734	Syntax for the length 6 word constructor.
class ⟨“𝐴𝐵𝐶𝐷𝐸𝐹”⟩
Syntax	cs7 14735	Syntax for the length 7 word constructor.
class ⟨“𝐴𝐵𝐶𝐷𝐸𝐹𝐺”⟩
Syntax	cs8 14736	Syntax for the length 8 word constructor.
class ⟨“𝐴𝐵𝐶𝐷𝐸𝐹𝐺𝐻”⟩
Definition	df-s2 14737	Define the length 2 word constructor. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ ⟨“𝐴𝐵”⟩ = (⟨“𝐴”⟩ ++ ⟨“𝐵”⟩)
Definition	df-s3 14738	Define the length 3 word constructor. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ ⟨“𝐴𝐵𝐶”⟩ = (⟨“𝐴𝐵”⟩ ++ ⟨“𝐶”⟩)
Definition	df-s4 14739	Define the length 4 word constructor. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ ⟨“𝐴𝐵𝐶𝐷”⟩ = (⟨“𝐴𝐵𝐶”⟩ ++ ⟨“𝐷”⟩)
Definition	df-s5 14740	Define the length 5 word constructor. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ ⟨“𝐴𝐵𝐶𝐷𝐸”⟩ = (⟨“𝐴𝐵𝐶𝐷”⟩ ++ ⟨“𝐸”⟩)
Definition	df-s6 14741	Define the length 6 word constructor. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ ⟨“𝐴𝐵𝐶𝐷𝐸𝐹”⟩ = (⟨“𝐴𝐵𝐶𝐷𝐸”⟩ ++ ⟨“𝐹”⟩)
Definition	df-s7 14742	Define the length 7 word constructor. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ ⟨“𝐴𝐵𝐶𝐷𝐸𝐹𝐺”⟩ = (⟨“𝐴𝐵𝐶𝐷𝐸𝐹”⟩ ++ ⟨“𝐺”⟩)
Definition	df-s8 14743	Define the length 8 word constructor. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ ⟨“𝐴𝐵𝐶𝐷𝐸𝐹𝐺𝐻”⟩ = (⟨“𝐴𝐵𝐶𝐷𝐸𝐹𝐺”⟩ ++ ⟨“𝐻”⟩)
Theorem	cats1cld 14744	Closure of concatenation with a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ 𝑇 = (𝑆 ++ ⟨“𝑋”⟩)    &   ⊢ (𝜑 → 𝑆 ∈ Word 𝐴)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    ⇒   ⊢ (𝜑 → 𝑇 ∈ Word 𝐴)
Theorem	cats1co 14745	Closure of concatenation with a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ 𝑇 = (𝑆 ++ ⟨“𝑋”⟩)    &   ⊢ (𝜑 → 𝑆 ∈ Word 𝐴)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    &   ⊢ (𝜑 → (𝐹 ∘ 𝑆) = 𝑈)    &   ⊢ 𝑉 = (𝑈 ++ ⟨“(𝐹‘𝑋)”⟩)    ⇒   ⊢ (𝜑 → (𝐹 ∘ 𝑇) = 𝑉)
Theorem	cats1cli 14746	Closure of concatenation with a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ 𝑇 = (𝑆 ++ ⟨“𝑋”⟩)    &   ⊢ 𝑆 ∈ Word V    ⇒   ⊢ 𝑇 ∈ Word V
Theorem	cats1fvn 14747	The last symbol of a concatenation with a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ 𝑇 = (𝑆 ++ ⟨“𝑋”⟩)    &   ⊢ 𝑆 ∈ Word V    &   ⊢ (♯‘𝑆) = 𝑀    ⇒   ⊢ (𝑋 ∈ 𝑉 → (𝑇‘𝑀) = 𝑋)
Theorem	cats1fv 14748	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 14749	The length of concatenation with a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ 𝑇 = (𝑆 ++ ⟨“𝑋”⟩)    &   ⊢ 𝑆 ∈ Word V    &   ⊢ (♯‘𝑆) = 𝑀    &   ⊢ (𝑀 + 1) = 𝑁    ⇒   ⊢ (♯‘𝑇) = 𝑁
Theorem	cats1cat 14750	Closure of concatenation with a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ 𝑇 = (𝑆 ++ ⟨“𝑋”⟩)    &   ⊢ 𝐴 ∈ Word V    &   ⊢ 𝑆 ∈ Word V    &   ⊢ 𝐶 = (𝐵 ++ ⟨“𝑋”⟩)    &   ⊢ 𝐵 = (𝐴 ++ 𝑆)    ⇒   ⊢ 𝐶 = (𝐴 ++ 𝑇)
Theorem	cats2cat 14751	Closure of concatenation of concatenations with singleton words. (Contributed by AV, 1-Mar-2021.)
⊢ 𝐵 ∈ Word V    &   ⊢ 𝐷 ∈ Word V    &   ⊢ 𝐴 = (𝐵 ++ ⟨“𝑋”⟩)    &   ⊢ 𝐶 = (⟨“𝑌”⟩ ++ 𝐷)    ⇒   ⊢ (𝐴 ++ 𝐶) = ((𝐵 ++ ⟨“𝑋𝑌”⟩) ++ 𝐷)
Theorem	s2eqd 14752	Equality theorem for a doubleton word. (Contributed by Mario Carneiro, 27-Feb-2016.)
⊢ (𝜑 → 𝐴 = 𝑁)    &   ⊢ (𝜑 → 𝐵 = 𝑂)    ⇒   ⊢ (𝜑 → ⟨“𝐴𝐵”⟩ = ⟨“𝑁𝑂”⟩)
Theorem	s3eqd 14753	Equality theorem for a length 3 word. (Contributed by Mario Carneiro, 27-Feb-2016.)
⊢ (𝜑 → 𝐴 = 𝑁)    &   ⊢ (𝜑 → 𝐵 = 𝑂)    &   ⊢ (𝜑 → 𝐶 = 𝑃)    ⇒   ⊢ (𝜑 → ⟨“𝐴𝐵𝐶”⟩ = ⟨“𝑁𝑂𝑃”⟩)
Theorem	s4eqd 14754	Equality theorem for a length 4 word. (Contributed by Mario Carneiro, 27-Feb-2016.)
⊢ (𝜑 → 𝐴 = 𝑁)    &   ⊢ (𝜑 → 𝐵 = 𝑂)    &   ⊢ (𝜑 → 𝐶 = 𝑃)    &   ⊢ (𝜑 → 𝐷 = 𝑄)    ⇒   ⊢ (𝜑 → ⟨“𝐴𝐵𝐶𝐷”⟩ = ⟨“𝑁𝑂𝑃𝑄”⟩)
Theorem	s5eqd 14755	Equality theorem for a length 5 word. (Contributed by Mario Carneiro, 27-Feb-2016.)
⊢ (𝜑 → 𝐴 = 𝑁)    &   ⊢ (𝜑 → 𝐵 = 𝑂)    &   ⊢ (𝜑 → 𝐶 = 𝑃)    &   ⊢ (𝜑 → 𝐷 = 𝑄)    &   ⊢ (𝜑 → 𝐸 = 𝑅)    ⇒   ⊢ (𝜑 → ⟨“𝐴𝐵𝐶𝐷𝐸”⟩ = ⟨“𝑁𝑂𝑃𝑄𝑅”⟩)
Theorem	s6eqd 14756	Equality theorem for a length 6 word. (Contributed by Mario Carneiro, 27-Feb-2016.)
⊢ (𝜑 → 𝐴 = 𝑁)    &   ⊢ (𝜑 → 𝐵 = 𝑂)    &   ⊢ (𝜑 → 𝐶 = 𝑃)    &   ⊢ (𝜑 → 𝐷 = 𝑄)    &   ⊢ (𝜑 → 𝐸 = 𝑅)    &   ⊢ (𝜑 → 𝐹 = 𝑆)    ⇒   ⊢ (𝜑 → ⟨“𝐴𝐵𝐶𝐷𝐸𝐹”⟩ = ⟨“𝑁𝑂𝑃𝑄𝑅𝑆”⟩)
Theorem	s7eqd 14757	Equality theorem for a length 7 word. (Contributed by Mario Carneiro, 27-Feb-2016.)
⊢ (𝜑 → 𝐴 = 𝑁)    &   ⊢ (𝜑 → 𝐵 = 𝑂)    &   ⊢ (𝜑 → 𝐶 = 𝑃)    &   ⊢ (𝜑 → 𝐷 = 𝑄)    &   ⊢ (𝜑 → 𝐸 = 𝑅)    &   ⊢ (𝜑 → 𝐹 = 𝑆)    &   ⊢ (𝜑 → 𝐺 = 𝑇)    ⇒   ⊢ (𝜑 → ⟨“𝐴𝐵𝐶𝐷𝐸𝐹𝐺”⟩ = ⟨“𝑁𝑂𝑃𝑄𝑅𝑆𝑇”⟩)
Theorem	s8eqd 14758	Equality theorem for a length 8 word. (Contributed by Mario Carneiro, 27-Feb-2016.)
⊢ (𝜑 → 𝐴 = 𝑁)    &   ⊢ (𝜑 → 𝐵 = 𝑂)    &   ⊢ (𝜑 → 𝐶 = 𝑃)    &   ⊢ (𝜑 → 𝐷 = 𝑄)    &   ⊢ (𝜑 → 𝐸 = 𝑅)    &   ⊢ (𝜑 → 𝐹 = 𝑆)    &   ⊢ (𝜑 → 𝐺 = 𝑇)    &   ⊢ (𝜑 → 𝐻 = 𝑈)    ⇒   ⊢ (𝜑 → ⟨“𝐴𝐵𝐶𝐷𝐸𝐹𝐺𝐻”⟩ = ⟨“𝑁𝑂𝑃𝑄𝑅𝑆𝑇𝑈”⟩)
Theorem	s3eq2 14759	Equality theorem for a length 3 word for the second symbol. (Contributed by AV, 4-Jan-2022.)
⊢ (𝐵 = 𝐷 → ⟨“𝐴𝐵𝐶”⟩ = ⟨“𝐴𝐷𝐶”⟩)
Theorem	s2cld 14760	A doubleton word is a word. (Contributed by Mario Carneiro, 27-Feb-2016.)
⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑋)    ⇒   ⊢ (𝜑 → ⟨“𝐴𝐵”⟩ ∈ Word 𝑋)
Theorem	s3cld 14761	A length 3 string is a word. (Contributed by Mario Carneiro, 27-Feb-2016.)
⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑋)    ⇒   ⊢ (𝜑 → ⟨“𝐴𝐵𝐶”⟩ ∈ Word 𝑋)
Theorem	s4cld 14762	A length 4 string is a word. (Contributed by Mario Carneiro, 27-Feb-2016.)
⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑋)    ⇒   ⊢ (𝜑 → ⟨“𝐴𝐵𝐶𝐷”⟩ ∈ Word 𝑋)
Theorem	s5cld 14763	A length 5 string is a word. (Contributed by Mario Carneiro, 27-Feb-2016.)
⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑋)    ⇒   ⊢ (𝜑 → ⟨“𝐴𝐵𝐶𝐷𝐸”⟩ ∈ Word 𝑋)
Theorem	s6cld 14764	A length 6 string is a word. (Contributed by Mario Carneiro, 27-Feb-2016.)
⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑋)    ⇒   ⊢ (𝜑 → ⟨“𝐴𝐵𝐶𝐷𝐸𝐹”⟩ ∈ Word 𝑋)
Theorem	s7cld 14765	A length 7 string is a word. (Contributed by Mario Carneiro, 27-Feb-2016.)
⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑋)    ⇒   ⊢ (𝜑 → ⟨“𝐴𝐵𝐶𝐷𝐸𝐹𝐺”⟩ ∈ Word 𝑋)
Theorem	s8cld 14766	A length 7 string is a word. (Contributed by Mario Carneiro, 27-Feb-2016.)
⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐸 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐻 ∈ 𝑋)    ⇒   ⊢ (𝜑 → ⟨“𝐴𝐵𝐶𝐷𝐸𝐹𝐺𝐻”⟩ ∈ Word 𝑋)
Theorem	s2cl 14767	A doubleton word is a word. (Contributed by Stefan O'Rear, 23-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.)
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ⟨“𝐴𝐵”⟩ ∈ Word 𝑋)
Theorem	s3cl 14768	A length 3 string is a word. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋) → ⟨“𝐴𝐵𝐶”⟩ ∈ Word 𝑋)
Theorem	s2cli 14769	A doubleton word is a word. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ ⟨“𝐴𝐵”⟩ ∈ Word V
Theorem	s3cli 14770	A length 3 string is a word. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ ⟨“𝐴𝐵𝐶”⟩ ∈ Word V
Theorem	s4cli 14771	A length 4 string is a word. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ ⟨“𝐴𝐵𝐶𝐷”⟩ ∈ Word V
Theorem	s5cli 14772	A length 5 string is a word. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ ⟨“𝐴𝐵𝐶𝐷𝐸”⟩ ∈ Word V
Theorem	s6cli 14773	A length 6 string is a word. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ ⟨“𝐴𝐵𝐶𝐷𝐸𝐹”⟩ ∈ Word V
Theorem	s7cli 14774	A length 7 string is a word. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ ⟨“𝐴𝐵𝐶𝐷𝐸𝐹𝐺”⟩ ∈ Word V
Theorem	s8cli 14775	A length 8 string is a word. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ ⟨“𝐴𝐵𝐶𝐷𝐸𝐹𝐺𝐻”⟩ ∈ Word V
Theorem	s2fv0 14776	Extract the first symbol from a doubleton word. (Contributed by Stefan O'Rear, 23-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.)
⊢ (𝐴 ∈ 𝑉 → (⟨“𝐴𝐵”⟩‘0) = 𝐴)
Theorem	s2fv1 14777	Extract the second symbol from a doubleton word. (Contributed by Stefan O'Rear, 23-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.)
⊢ (𝐵 ∈ 𝑉 → (⟨“𝐴𝐵”⟩‘1) = 𝐵)
Theorem	s2len 14778	The length of a doubleton word. (Contributed by Stefan O'Rear, 23-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.)
⊢ (♯‘⟨“𝐴𝐵”⟩) = 2
Theorem	s2dm 14779	The domain of a doubleton word is an unordered pair. (Contributed by AV, 9-Jan-2020.)
⊢ dom ⟨“𝐴𝐵”⟩ = {0, 1}
Theorem	s3fv0 14780	Extract the first symbol from a length 3 string. (Contributed by Mario Carneiro, 13-Jan-2017.)
⊢ (𝐴 ∈ 𝑉 → (⟨“𝐴𝐵𝐶”⟩‘0) = 𝐴)
Theorem	s3fv1 14781	Extract the second symbol from a length 3 string. (Contributed by Mario Carneiro, 13-Jan-2017.)
⊢ (𝐵 ∈ 𝑉 → (⟨“𝐴𝐵𝐶”⟩‘1) = 𝐵)
Theorem	s3fv2 14782	Extract the third symbol from a length 3 string. (Contributed by Mario Carneiro, 13-Jan-2017.)
⊢ (𝐶 ∈ 𝑉 → (⟨“𝐴𝐵𝐶”⟩‘2) = 𝐶)
Theorem	s3len 14783	The length of a length 3 string. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ (♯‘⟨“𝐴𝐵𝐶”⟩) = 3
Theorem	s4fv0 14784	Extract the first symbol from a length 4 string. (Contributed by Thierry Arnoux, 8-Oct-2020.)
⊢ (𝐴 ∈ 𝑉 → (⟨“𝐴𝐵𝐶𝐷”⟩‘0) = 𝐴)
Theorem	s4fv1 14785	Extract the second symbol from a length 4 string. (Contributed by Thierry Arnoux, 8-Oct-2020.)
⊢ (𝐵 ∈ 𝑉 → (⟨“𝐴𝐵𝐶𝐷”⟩‘1) = 𝐵)
Theorem	s4fv2 14786	Extract the third symbol from a length 4 string. (Contributed by Thierry Arnoux, 8-Oct-2020.)
⊢ (𝐶 ∈ 𝑉 → (⟨“𝐴𝐵𝐶𝐷”⟩‘2) = 𝐶)
Theorem	s4fv3 14787	Extract the fourth symbol from a length 4 string. (Contributed by Thierry Arnoux, 8-Oct-2020.)
⊢ (𝐷 ∈ 𝑉 → (⟨“𝐴𝐵𝐶𝐷”⟩‘3) = 𝐷)
Theorem	s4len 14788	The length of a length 4 string. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ (♯‘⟨“𝐴𝐵𝐶𝐷”⟩) = 4
Theorem	s5len 14789	The length of a length 5 string. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ (♯‘⟨“𝐴𝐵𝐶𝐷𝐸”⟩) = 5
Theorem	s6len 14790	The length of a length 6 string. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ (♯‘⟨“𝐴𝐵𝐶𝐷𝐸𝐹”⟩) = 6
Theorem	s7len 14791	The length of a length 7 string. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ (♯‘⟨“𝐴𝐵𝐶𝐷𝐸𝐹𝐺”⟩) = 7
Theorem	s8len 14792	The length of a length 8 string. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ (♯‘⟨“𝐴𝐵𝐶𝐷𝐸𝐹𝐺𝐻”⟩) = 8
Theorem	lsws2 14793	The last symbol of a doubleton word is its second symbol. (Contributed by AV, 8-Feb-2021.)
⊢ (𝐵 ∈ 𝑉 → (lastS‘⟨“𝐴𝐵”⟩) = 𝐵)
Theorem	lsws3 14794	The last symbol of a 3 letter word is its third symbol. (Contributed by AV, 8-Feb-2021.)
⊢ (𝐶 ∈ 𝑉 → (lastS‘⟨“𝐴𝐵𝐶”⟩) = 𝐶)
Theorem	lsws4 14795	The last symbol of a 4 letter word is its fourth symbol. (Contributed by AV, 8-Feb-2021.)
⊢ (𝐷 ∈ 𝑉 → (lastS‘⟨“𝐴𝐵𝐶𝐷”⟩) = 𝐷)
Theorem	s2prop 14796	A length 2 word is an unordered pair of ordered pairs. (Contributed by Alexander van der Vekens, 14-Aug-2017.)
⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → ⟨“𝐴𝐵”⟩ = {⟨0, 𝐴⟩, ⟨1, 𝐵⟩})
Theorem	s2dmALT 14797	Alternate version of s2dm 14779, having a shorter proof, but requiring that 𝐴 and 𝐵 are sets. (Contributed by AV, 9-Jan-2020.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → dom ⟨“𝐴𝐵”⟩ = {0, 1})
Theorem	s3tpop 14798	A length 3 word is an unordered triple of ordered pairs. (Contributed by AV, 23-Jan-2021.)
⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) → ⟨“𝐴𝐵𝐶”⟩ = {⟨0, 𝐴⟩, ⟨1, 𝐵⟩, ⟨2, 𝐶⟩})
Theorem	s4prop 14799	A length 4 word is a union of two unordered pairs of ordered pairs. (Contributed by Alexander van der Vekens, 14-Aug-2017.)
⊢ (((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) → ⟨“𝐴𝐵𝐶𝐷”⟩ = ({⟨0, 𝐴⟩, ⟨1, 𝐵⟩} ∪ {⟨2, 𝐶⟩, ⟨3, 𝐷⟩}))
Theorem	s3fn 14800	A length 3 word is a function with a triple as domain. (Contributed by Alexander van der Vekens, 5-Dec-2017.) (Revised by AV, 23-Jan-2021.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → ⟨“𝐴𝐵𝐶”⟩ Fn {0, 1, 2})