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
Definition	df-word 14501*	Define the class of words over a set. A word (sometimes also called a string) is a finite sequence of symbols from a set (alphabet) 𝑆. Definition in Section 9.1 of [AhoHopUll] p. 318. The domain is forced to be an initial segment of ℕ0 so that two words with the same symbols in the same order be equal. The set Word 𝑆 is sometimes denoted by S*, using the Kleene star, although the Kleene star, or Kleene closure, is sometimes reserved to denote an operation on languages. The set Word 𝑆 equipped with concatenation is the free monoid over 𝑆, and the monoid unit is the empty word (see frmdval 18811). (Contributed by FL, 14-Jan-2014.) (Revised by Stefan O'Rear, 14-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.)
⊢ Word 𝑆 = {𝑤 ∣ ∃𝑙 ∈ ℕ0 𝑤:(0..^𝑙)⟶𝑆}
Theorem	iswrd 14502*	Property of being a word over a set with an existential quantifier over the length. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.) (Proof shortened by AV, 13-May-2020.)
⊢ (𝑊 ∈ Word 𝑆 ↔ ∃𝑙 ∈ ℕ0 𝑊:(0..^𝑙)⟶𝑆)
Theorem	wrdval 14503*	Value of the set of words over a set. (Contributed by Stefan O'Rear, 10-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.)
⊢ (𝑆 ∈ 𝑉 → Word 𝑆 = ∪ 𝑙 ∈ ℕ0 (𝑆 ↑m (0..^𝑙)))
Theorem	iswrdi 14504	A zero-based sequence is a word. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.)
⊢ (𝑊:(0..^𝐿)⟶𝑆 → 𝑊 ∈ Word 𝑆)
Theorem	wrdf 14505	A word is a zero-based sequence with a recoverable upper limit. (Contributed by Stefan O'Rear, 15-Aug-2015.)
⊢ (𝑊 ∈ Word 𝑆 → 𝑊:(0..^(♯‘𝑊))⟶𝑆)
Theorem	iswrdb 14506	A word over an alphabet is a function from an open range of nonnegative integers (of length equal to the length of the word) into the alphabet. (Contributed by Alexander van der Vekens, 30-Jul-2018.)
⊢ (𝑊 ∈ Word 𝑆 ↔ 𝑊:(0..^(♯‘𝑊))⟶𝑆)
Theorem	wrddm 14507	The indices of a word (i.e. its domain regarded as function) are elements of an open range of nonnegative integers (of length equal to the length of the word). (Contributed by AV, 2-May-2020.)
⊢ (𝑊 ∈ Word 𝑆 → dom 𝑊 = (0..^(♯‘𝑊)))
Theorem	sswrd 14508	The set of words respects ordering on the base set. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.) (Proof shortened by AV, 13-May-2020.)
⊢ (𝑆 ⊆ 𝑇 → Word 𝑆 ⊆ Word 𝑇)
Theorem	snopiswrd 14509	A singleton of an ordered pair (with 0 as first component) is a word. (Contributed by AV, 23-Nov-2018.) (Proof shortened by AV, 18-Apr-2021.)
⊢ (𝑆 ∈ 𝑉 → {⟨0, 𝑆⟩} ∈ Word 𝑉)
Theorem	wrdexg 14510	The set of words over a set is a set. (Contributed by Mario Carneiro, 26-Feb-2016.) (Proof shortened by JJ, 18-Nov-2022.)
⊢ (𝑆 ∈ 𝑉 → Word 𝑆 ∈ V)
Theorem	wrdexb 14511	The set of words over a set is a set, bidirectional version. (Contributed by Mario Carneiro, 26-Feb-2016.) (Proof shortened by AV, 23-Nov-2018.)
⊢ (𝑆 ∈ V ↔ Word 𝑆 ∈ V)
Theorem	wrdexi 14512	The set of words over a set is a set, inference form. (Contributed by AV, 23-May-2021.)
⊢ 𝑆 ∈ V    ⇒   ⊢ Word 𝑆 ∈ V
Theorem	wrdsymbcl 14513	A symbol within a word over an alphabet belongs to the alphabet. (Contributed by Alexander van der Vekens, 28-Jun-2018.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐼 ∈ (0..^(♯‘𝑊))) → (𝑊‘𝐼) ∈ 𝑉)
Theorem	wrdfn 14514	A word is a function with a zero-based sequence of integers as domain. (Contributed by Alexander van der Vekens, 13-Apr-2018.)
⊢ (𝑊 ∈ Word 𝑆 → 𝑊 Fn (0..^(♯‘𝑊)))
Theorem	wrdv 14515	A word over an alphabet is a word over the universal class. (Contributed by AV, 8-Feb-2021.) (Proof shortened by JJ, 18-Nov-2022.)
⊢ (𝑊 ∈ Word 𝑉 → 𝑊 ∈ Word V)
Theorem	wrdlndm 14516	The length of a word is not in the domain of the word (regarded as a function). (Contributed by AV, 3-Mar-2021.) (Proof shortened by JJ, 18-Nov-2022.)
⊢ (𝑊 ∈ Word 𝑉 → (♯‘𝑊) ∉ dom 𝑊)
Theorem	iswrdsymb 14517*	An arbitrary word is a word over an alphabet if all of its symbols belong to the alphabet. (Contributed by AV, 23-Jan-2021.)
⊢ ((𝑊 ∈ Word V ∧ ∀𝑖 ∈ (0..^(♯‘𝑊))(𝑊‘𝑖) ∈ 𝑉) → 𝑊 ∈ Word 𝑉)
Theorem	wrdfin 14518	A word is a finite set. (Contributed by Stefan O'Rear, 2-Nov-2015.) (Proof shortened by AV, 18-Nov-2018.)
⊢ (𝑊 ∈ Word 𝑆 → 𝑊 ∈ Fin)
Theorem	lencl 14519	The length of a word is a nonnegative integer. This corresponds to the definition in Section 9.1 of [AhoHopUll] p. 318. (Contributed by Stefan O'Rear, 27-Aug-2015.)
⊢ (𝑊 ∈ Word 𝑆 → (♯‘𝑊) ∈ ℕ0)
Theorem	lennncl 14520	The length of a nonempty word is a positive integer. (Contributed by Mario Carneiro, 1-Oct-2015.)
⊢ ((𝑊 ∈ Word 𝑆 ∧ 𝑊 ≠ ∅) → (♯‘𝑊) ∈ ℕ)
Theorem	wrdffz 14521	A word is a function from a finite interval of integers. (Contributed by AV, 10-Feb-2021.)
⊢ (𝑊 ∈ Word 𝑆 → 𝑊:(0...((♯‘𝑊) − 1))⟶𝑆)
Theorem	wrdeq 14522	Equality theorem for the set of words. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ (𝑆 = 𝑇 → Word 𝑆 = Word 𝑇)
Theorem	wrdeqi 14523	Equality theorem for the set of words, inference form. (Contributed by AV, 23-May-2021.)
⊢ 𝑆 = 𝑇    ⇒   ⊢ Word 𝑆 = Word 𝑇
Theorem	iswrddm0 14524	A function with empty domain is a word. (Contributed by AV, 13-Oct-2018.)
⊢ (𝑊:∅⟶𝑆 → 𝑊 ∈ Word 𝑆)
Theorem	wrd0 14525	The empty set is a word (the empty word, frequently denoted ε in this context). This corresponds to the definition in Section 9.1 of [AhoHopUll] p. 318. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Proof shortened by AV, 13-May-2020.)
⊢ ∅ ∈ Word 𝑆
Theorem	0wrd0 14526	The empty word is the only word over an empty alphabet. (Contributed by AV, 25-Oct-2018.)
⊢ (𝑊 ∈ Word ∅ ↔ 𝑊 = ∅)
Theorem	ffz0iswrd 14527	A sequence with zero-based indices is a word. (Contributed by AV, 31-Jan-2018.) (Proof shortened by AV, 13-Oct-2018.) (Proof shortened by JJ, 18-Nov-2022.)
⊢ (𝑊:(0...𝐿)⟶𝑆 → 𝑊 ∈ Word 𝑆)
Theorem	wrdsymb 14528	A word is a word over the symbols it consists of. (Contributed by AV, 1-Dec-2022.)
⊢ (𝑆 ∈ Word 𝐴 → 𝑆 ∈ Word (𝑆 “ (0..^(♯‘𝑆))))
Theorem	nfwrd 14529	Hypothesis builder for Word 𝑆. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ Ⅎ𝑥𝑆    ⇒   ⊢ Ⅎ𝑥Word 𝑆
Theorem	csbwrdg 14530*	Class substitution for the symbols of a word. (Contributed by Alexander van der Vekens, 15-Jul-2018.)
⊢ (𝑆 ∈ 𝑉 → ⦋𝑆 / 𝑥⦌Word 𝑥 = Word 𝑆)
Theorem	wrdnval 14531*	Words of a fixed length are mappings from a fixed half-open integer interval. (Contributed by Alexander van der Vekens, 25-Mar-2018.) (Proof shortened by AV, 13-May-2020.)
⊢ ((𝑉 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0) → {𝑤 ∈ Word 𝑉 ∣ (♯‘𝑤) = 𝑁} = (𝑉 ↑m (0..^𝑁)))
Theorem	wrdmap 14532	Words as a mapping. (Contributed by Thierry Arnoux, 4-Mar-2020.)
⊢ ((𝑉 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0) → ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = 𝑁) ↔ 𝑊 ∈ (𝑉 ↑m (0..^𝑁))))
Theorem	hashwrdn 14533*	If there is only a finite number of symbols, the number of words of a fixed length over these sysmbols is the number of these symbols raised to the power of the length. (Contributed by Alexander van der Vekens, 25-Mar-2018.)
⊢ ((𝑉 ∈ Fin ∧ 𝑁 ∈ ℕ0) → (♯‘{𝑤 ∈ Word 𝑉 ∣ (♯‘𝑤) = 𝑁}) = ((♯‘𝑉)↑𝑁))
Theorem	wrdnfi 14534*	If there is only a finite number of symbols, the number of words of a fixed length over these symbols is also finite. (Contributed by Alexander van der Vekens, 25-Mar-2018.) Remove unnecessary antecedent. (Revised by JJ, 18-Nov-2022.)
⊢ (𝑉 ∈ Fin → {𝑤 ∈ Word 𝑉 ∣ (♯‘𝑤) = 𝑁} ∈ Fin)
Theorem	wrdsymb0 14535	A symbol at a position "outside" of a word. (Contributed by Alexander van der Vekens, 26-May-2018.) (Proof shortened by AV, 2-May-2020.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐼 ∈ ℤ) → ((𝐼 < 0 ∨ (♯‘𝑊) ≤ 𝐼) → (𝑊‘𝐼) = ∅))
Theorem	wrdlenge1n0 14536	A word with length at least 1 is not empty. (Contributed by AV, 14-Oct-2018.)
⊢ (𝑊 ∈ Word 𝑉 → (𝑊 ≠ ∅ ↔ 1 ≤ (♯‘𝑊)))
Theorem	len0nnbi 14537	The length of a word is a positive integer iff the word is not empty. (Contributed by AV, 22-Mar-2022.)
⊢ (𝑊 ∈ Word 𝑆 → (𝑊 ≠ ∅ ↔ (♯‘𝑊) ∈ ℕ))
Theorem	wrdlenge2n0 14538	A word with length at least 2 is not empty. (Contributed by AV, 18-Jun-2018.) (Proof shortened by AV, 14-Oct-2018.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑊)) → 𝑊 ≠ ∅)
Theorem	wrdsymb1 14539	The first symbol of a nonempty word over an alphabet belongs to the alphabet. (Contributed by Alexander van der Vekens, 28-Jun-2018.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 1 ≤ (♯‘𝑊)) → (𝑊‘0) ∈ 𝑉)
Theorem	wrdlen1 14540*	A word of length 1 starts with a symbol. (Contributed by AV, 20-Jul-2018.) (Proof shortened by AV, 19-Oct-2018.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = 1) → ∃𝑣 ∈ 𝑉 (𝑊‘0) = 𝑣)
Theorem	fstwrdne 14541	The first symbol of a nonempty word is element of the alphabet for the word. (Contributed by AV, 28-Sep-2018.) (Proof shortened by AV, 14-Oct-2018.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → (𝑊‘0) ∈ 𝑉)
Theorem	fstwrdne0 14542	The first symbol of a nonempty word is element of the alphabet for the word. (Contributed by AV, 29-Sep-2018.) (Proof shortened by AV, 14-Oct-2018.)
⊢ ((𝑁 ∈ ℕ ∧ (𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = 𝑁)) → (𝑊‘0) ∈ 𝑉)
Theorem	eqwrd 14543*	Two words are equal iff they have the same length and the same symbol at each position. (Contributed by AV, 13-Apr-2018.) (Revised by JJ, 30-Dec-2023.)
⊢ ((𝑈 ∈ Word 𝑆 ∧ 𝑊 ∈ Word 𝑇) → (𝑈 = 𝑊 ↔ ((♯‘𝑈) = (♯‘𝑊) ∧ ∀𝑖 ∈ (0..^(♯‘𝑈))(𝑈‘𝑖) = (𝑊‘𝑖))))
Theorem	elovmpowrd 14544*	Implications for the value of an operation defined by the maps-to notation with a class abstraction of words as a result having an element. Note that 𝜑 may depend on 𝑧 as well as on 𝑣 and 𝑦. (Contributed by Alexander van der Vekens, 15-Jul-2018.)
⊢ 𝑂 = (𝑣 ∈ V, 𝑦 ∈ V ↦ {𝑧 ∈ Word 𝑣 ∣ 𝜑})    ⇒   ⊢ (𝑍 ∈ (𝑉𝑂𝑌) → (𝑉 ∈ V ∧ 𝑌 ∈ V ∧ 𝑍 ∈ Word 𝑉))
Theorem	elovmptnn0wrd 14545*	Implications for the value of an operation defined by the maps-to notation with a function of nonnegative integers into a class abstraction of words as a result having an element. Note that 𝜑 may depend on 𝑧 as well as on 𝑣 and 𝑦 and 𝑛. (Contributed by AV, 16-Jul-2018.) (Revised by AV, 16-May-2019.)
⊢ 𝑂 = (𝑣 ∈ V, 𝑦 ∈ V ↦ (𝑛 ∈ ℕ0 ↦ {𝑧 ∈ Word 𝑣 ∣ 𝜑}))    ⇒   ⊢ (𝑍 ∈ ((𝑉𝑂𝑌)‘𝑁) → ((𝑉 ∈ V ∧ 𝑌 ∈ V) ∧ (𝑁 ∈ ℕ0 ∧ 𝑍 ∈ Word 𝑉)))
Theorem	wrdred1 14546	A word truncated by a symbol is a word. (Contributed by AV, 29-Jan-2021.)
⊢ (𝐹 ∈ Word 𝑆 → (𝐹 ↾ (0..^((♯‘𝐹) − 1))) ∈ Word 𝑆)
Theorem	wrdred1hash 14547	The length of a word truncated by a symbol. (Contributed by Alexander van der Vekens, 1-Nov-2017.) (Revised by AV, 29-Jan-2021.)
⊢ ((𝐹 ∈ Word 𝑆 ∧ 1 ≤ (♯‘𝐹)) → (♯‘(𝐹 ↾ (0..^((♯‘𝐹) − 1)))) = ((♯‘𝐹) − 1))
5.7.2  Last symbol of a word
Syntax	clsw 14548	Extend class notation with the Last Symbol of a word.
class lastS
Definition	df-lsw 14549	Extract the last symbol of a word. May be not meaningful for other sets which are not words. The name lastS (as abbreviation of "lastSymbol") is a compromise between usually used names for corresponding functions in computer programs (as last() or lastChar()), the terminology used for words in set.mm ("symbol" instead of "character") and brevity ("lastS" is shorter than "lastChar" and "lastSymbol"). Labels of theorems about last symbols of a word will contain the abbreviation "lsw" (Last Symbol of a Word). (Contributed by Alexander van der Vekens, 18-Mar-2018.)
⊢ lastS = (𝑤 ∈ V ↦ (𝑤‘((♯‘𝑤) − 1)))
Theorem	lsw 14550	Extract the last symbol of a word. May be not meaningful for other sets which are not words. (Contributed by Alexander van der Vekens, 18-Mar-2018.)
⊢ (𝑊 ∈ 𝑋 → (lastS‘𝑊) = (𝑊‘((♯‘𝑊) − 1)))
Theorem	lsw0 14551	The last symbol of an empty word does not exist. (Contributed by Alexander van der Vekens, 19-Mar-2018.) (Proof shortened by AV, 2-May-2020.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = 0) → (lastS‘𝑊) = ∅)
Theorem	lsw0g 14552	The last symbol of an empty word does not exist. (Contributed by Alexander van der Vekens, 11-Nov-2018.)
⊢ (lastS‘∅) = ∅
Theorem	lsw1 14553	The last symbol of a word of length 1 is the first symbol of this word. (Contributed by Alexander van der Vekens, 19-Mar-2018.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = 1) → (lastS‘𝑊) = (𝑊‘0))
Theorem	lswcl 14554	Closure of the last symbol: the last symbol of a not empty word belongs to the alphabet for the word. (Contributed by AV, 2-Aug-2018.) (Proof shortened by AV, 29-Apr-2020.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → (lastS‘𝑊) ∈ 𝑉)
Theorem	lswlgt0cl 14555	The last symbol of a nonempty word is element of the alphabet for the word. (Contributed by Alexander van der Vekens, 1-Oct-2018.) (Proof shortened by AV, 29-Apr-2020.)
⊢ ((𝑁 ∈ ℕ ∧ (𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = 𝑁)) → (lastS‘𝑊) ∈ 𝑉)
5.7.3  Concatenations of words
Syntax	cconcat 14556	Syntax for the concatenation operator.
class ++
Definition	df-concat 14557*	Define the concatenation operator which combines two words. Definition in Section 9.1 of [AhoHopUll] p. 318. (Contributed by FL, 14-Jan-2014.) (Revised by Stefan O'Rear, 15-Aug-2015.)
⊢ ++ = (𝑠 ∈ V, 𝑡 ∈ V ↦ (𝑥 ∈ (0..^((♯‘𝑠) + (♯‘𝑡))) ↦ if(𝑥 ∈ (0..^(♯‘𝑠)), (𝑠‘𝑥), (𝑡‘(𝑥 − (♯‘𝑠))))))
Theorem	ccatfn 14558	The concatenation operator is a two-argument function. (Contributed by Mario Carneiro, 27-Sep-2015.) (Proof shortened by AV, 29-Apr-2020.)
⊢ ++ Fn (V × V)
Theorem	ccatfval 14559*	Value of the concatenation operator. (Contributed by Stefan O'Rear, 15-Aug-2015.)
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑊) → (𝑆 ++ 𝑇) = (𝑥 ∈ (0..^((♯‘𝑆) + (♯‘𝑇))) ↦ if(𝑥 ∈ (0..^(♯‘𝑆)), (𝑆‘𝑥), (𝑇‘(𝑥 − (♯‘𝑆))))))
Theorem	ccatcl 14560	The concatenation of two words is a word. (Contributed by FL, 2-Feb-2014.) (Proof shortened by Stefan O'Rear, 15-Aug-2015.) (Proof shortened by AV, 29-Apr-2020.)
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → (𝑆 ++ 𝑇) ∈ Word 𝐵)
Theorem	ccatlen 14561	The length of a concatenated word. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by JJ, 1-Jan-2024.)
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐵) → (♯‘(𝑆 ++ 𝑇)) = ((♯‘𝑆) + (♯‘𝑇)))
Theorem	ccat0 14562	The concatenation of two words is empty iff the two words are empty. (Contributed by AV, 4-Mar-2022.) (Revised by JJ, 18-Jan-2024.)
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐵) → ((𝑆 ++ 𝑇) = ∅ ↔ (𝑆 = ∅ ∧ 𝑇 = ∅)))
Theorem	ccatval1 14563	Value of a symbol in the left half of a concatenated word. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by Mario Carneiro, 22-Sep-2015.) (Proof shortened by AV, 30-Apr-2020.) (Revised by JJ, 18-Jan-2024.)
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝐼 ∈ (0..^(♯‘𝑆))) → ((𝑆 ++ 𝑇)‘𝐼) = (𝑆‘𝐼))
Theorem	ccatval2 14564	Value of a symbol in the right half of a concatenated word. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by Mario Carneiro, 22-Sep-2015.)
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝐼 ∈ ((♯‘𝑆)..^((♯‘𝑆) + (♯‘𝑇)))) → ((𝑆 ++ 𝑇)‘𝐼) = (𝑇‘(𝐼 − (♯‘𝑆))))
Theorem	ccatval3 14565	Value of a symbol in the right half of a concatenated word, using an index relative to the subword. (Contributed by Stefan O'Rear, 16-Aug-2015.) (Proof shortened by AV, 30-Apr-2020.)
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝐼 ∈ (0..^(♯‘𝑇))) → ((𝑆 ++ 𝑇)‘(𝐼 + (♯‘𝑆))) = (𝑇‘𝐼))
Theorem	elfzelfzccat 14566	An element of a finite set of sequential integers up to the length of a word is an element of an extended finite set of sequential integers up to the length of a concatenation of this word with another word. (Contributed by Alexander van der Vekens, 28-Mar-2018.)
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → (𝑁 ∈ (0...(♯‘𝐴)) → 𝑁 ∈ (0...(♯‘(𝐴 ++ 𝐵)))))
Theorem	ccatvalfn 14567	The concatenation of two words is a function over the half-open integer range having the sum of the lengths of the word as length. (Contributed by Alexander van der Vekens, 30-Mar-2018.)
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉) → (𝐴 ++ 𝐵) Fn (0..^((♯‘𝐴) + (♯‘𝐵))))
Theorem	ccatsymb 14568	The symbol at a given position in a concatenated word. (Contributed by AV, 26-May-2018.) (Proof shortened by AV, 24-Nov-2018.)
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝐼 ∈ ℤ) → ((𝐴 ++ 𝐵)‘𝐼) = if(𝐼 < (♯‘𝐴), (𝐴‘𝐼), (𝐵‘(𝐼 − (♯‘𝐴)))))
Theorem	ccatfv0 14569	The first symbol of a concatenation of two words is the first symbol of the first word if the first word is not empty. (Contributed by Alexander van der Vekens, 22-Sep-2018.)
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 0 < (♯‘𝐴)) → ((𝐴 ++ 𝐵)‘0) = (𝐴‘0))
Theorem	ccatval1lsw 14570	The last symbol of the left (nonempty) half of a concatenated word. (Contributed by Alexander van der Vekens, 3-Oct-2018.) (Proof shortened by AV, 1-May-2020.)
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝐴 ≠ ∅) → ((𝐴 ++ 𝐵)‘((♯‘𝐴) − 1)) = (lastS‘𝐴))
Theorem	ccatval21sw 14571	The first symbol of the right (nonempty) half of a concatenated word. (Contributed by AV, 23-Apr-2022.)
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝐵 ≠ ∅) → ((𝐴 ++ 𝐵)‘(♯‘𝐴)) = (𝐵‘0))
Theorem	ccatlid 14572	Concatenation of a word by the empty word on the left. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Proof shortened by AV, 1-May-2020.)
⊢ (𝑆 ∈ Word 𝐵 → (∅ ++ 𝑆) = 𝑆)
Theorem	ccatrid 14573	Concatenation of a word by the empty word on the right. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Proof shortened by AV, 1-May-2020.)
⊢ (𝑆 ∈ Word 𝐵 → (𝑆 ++ ∅) = 𝑆)
Theorem	ccatass 14574	Associative law for concatenation of words. (Contributed by Stefan O'Rear, 15-Aug-2015.)
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵) → ((𝑆 ++ 𝑇) ++ 𝑈) = (𝑆 ++ (𝑇 ++ 𝑈)))
Theorem	ccatrn 14575	The range of a concatenated word. (Contributed by Stefan O'Rear, 15-Aug-2015.)
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → ran (𝑆 ++ 𝑇) = (ran 𝑆 ∪ ran 𝑇))
Theorem	ccatidid 14576	Concatenation of the empty word by the empty word. (Contributed by AV, 26-Mar-2022.)
⊢ (∅ ++ ∅) = ∅
Theorem	lswccatn0lsw 14577	The last symbol of a word concatenated with a nonempty word is the last symbol of the nonempty word. (Contributed by AV, 22-Oct-2018.) (Proof shortened by AV, 1-May-2020.)
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝐵 ≠ ∅) → (lastS‘(𝐴 ++ 𝐵)) = (lastS‘𝐵))
Theorem	lswccat0lsw 14578	The last symbol of a word concatenated with the empty word is the last symbol of the word. (Contributed by AV, 22-Oct-2018.) (Proof shortened by AV, 1-May-2020.)
⊢ (𝑊 ∈ Word 𝑉 → (lastS‘(𝑊 ++ ∅)) = (lastS‘𝑊))
Theorem	ccatalpha 14579	A concatenation of two arbitrary words is a word over an alphabet iff the symbols of both words belong to the alphabet. (Contributed by AV, 28-Feb-2021.)
⊢ ((𝐴 ∈ Word V ∧ 𝐵 ∈ Word V) → ((𝐴 ++ 𝐵) ∈ Word 𝑆 ↔ (𝐴 ∈ Word 𝑆 ∧ 𝐵 ∈ Word 𝑆)))
Theorem	ccatrcl1 14580	Reverse closure of a concatenation: If the concatenation of two arbitrary words is a word over an alphabet then the symbols of the first word belong to the alphabet. (Contributed by AV, 3-Mar-2021.)
⊢ ((𝐴 ∈ Word 𝑋 ∧ 𝐵 ∈ Word 𝑌 ∧ (𝑊 = (𝐴 ++ 𝐵) ∧ 𝑊 ∈ Word 𝑆)) → 𝐴 ∈ Word 𝑆)
5.7.4  Singleton words
Syntax	cs1 14581	Syntax for the singleton word constructor.
class ⟨“𝐴”⟩
Definition	df-s1 14582	Define the canonical injection from symbols to words. Although not required, 𝐴 should usually be a set. Otherwise, the singleton word ⟨“𝐴”⟩ would be the singleton word consisting of the empty set, see s1prc 14590, and not, as maybe expected, the empty word, see also s1nz 14593. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.)
⊢ ⟨“𝐴”⟩ = {⟨0, ( I ‘𝐴)⟩}
Theorem	ids1 14583	Identity function protection for a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ ⟨“𝐴”⟩ = ⟨“( I ‘𝐴)”⟩
Theorem	s1val 14584	Value of a singleton word. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.)
⊢ (𝐴 ∈ 𝑉 → ⟨“𝐴”⟩ = {⟨0, 𝐴⟩})
Theorem	s1rn 14585	The range of a singleton word. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ (𝐴 ∈ 𝑉 → ran ⟨“𝐴”⟩ = {𝐴})
Theorem	s1eq 14586	Equality theorem for a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ (𝐴 = 𝐵 → ⟨“𝐴”⟩ = ⟨“𝐵”⟩)
Theorem	s1eqd 14587	Equality theorem for a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → ⟨“𝐴”⟩ = ⟨“𝐵”⟩)
Theorem	s1cl 14588	A singleton word is a word. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.) (Proof shortened by AV, 23-Nov-2018.)
⊢ (𝐴 ∈ 𝐵 → ⟨“𝐴”⟩ ∈ Word 𝐵)
Theorem	s1cld 14589	A singleton word is a word. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ (𝜑 → 𝐴 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ⟨“𝐴”⟩ ∈ Word 𝐵)
Theorem	s1prc 14590	Value of a singleton word if the symbol is a proper class. (Contributed by AV, 26-Mar-2022.)
⊢ (¬ 𝐴 ∈ V → ⟨“𝐴”⟩ = ⟨“∅”⟩)
Theorem	s1cli 14591	A singleton word is a word. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ ⟨“𝐴”⟩ ∈ Word V
Theorem	s1len 14592	Length of a singleton word. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.)
⊢ (♯‘⟨“𝐴”⟩) = 1
Theorem	s1nz 14593	A singleton word is not the empty string. (Contributed by Mario Carneiro, 27-Feb-2016.) (Proof shortened by Kyle Wyonch, 18-Jul-2021.)
⊢ ⟨“𝐴”⟩ ≠ ∅
Theorem	s1dm 14594	The domain of a singleton word is a singleton. (Contributed by AV, 9-Jan-2020.)
⊢ dom ⟨“𝐴”⟩ = {0}
Theorem	s1dmALT 14595	Alternate version of s1dm 14594, having a shorter proof, but requiring that 𝐴 is a set. (Contributed by AV, 9-Jan-2020.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐴 ∈ 𝑆 → dom ⟨“𝐴”⟩ = {0})
Theorem	s1fv 14596	Sole symbol of a singleton word. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.)
⊢ (𝐴 ∈ 𝐵 → (⟨“𝐴”⟩‘0) = 𝐴)
Theorem	lsws1 14597	The last symbol of a singleton word is its symbol. (Contributed by AV, 22-Oct-2018.)
⊢ (𝐴 ∈ 𝑉 → (lastS‘⟨“𝐴”⟩) = 𝐴)
Theorem	eqs1 14598	A word of length 1 is a singleton word. (Contributed by Stefan O'Rear, 23-Aug-2015.) (Proof shortened by AV, 1-May-2020.)
⊢ ((𝑊 ∈ Word 𝐴 ∧ (♯‘𝑊) = 1) → 𝑊 = ⟨“(𝑊‘0)”⟩)
Theorem	wrdl1exs1 14599*	A word of length 1 is a singleton word. (Contributed by AV, 24-Jan-2021.)
⊢ ((𝑊 ∈ Word 𝑆 ∧ (♯‘𝑊) = 1) → ∃𝑠 ∈ 𝑆 𝑊 = ⟨“𝑠”⟩)
Theorem	wrdl1s1 14600	A word of length 1 is a singleton word consisting of the first symbol of the word. (Contributed by AV, 22-Jul-2018.) (Proof shortened by AV, 14-Oct-2018.)
⊢ (𝑆 ∈ 𝑉 → (𝑊 = ⟨“𝑆”⟩ ↔ (𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = 1 ∧ (𝑊‘0) = 𝑆)))