P. 147 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 14601-14700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	ccatidid 14601	Concatenation of the empty word by the empty word. (Contributed by AV, 26-Mar-2022.)
⊢ (∅ ++ ∅) = ∅
Theorem	lswccatn0lsw 14602	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 14603	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 14604	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 14605	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 14606	Syntax for the singleton word constructor.
class ⟨“𝐴”⟩
Definition	df-s1 14607	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 14615, and not, as maybe expected, the empty word, see also s1nz 14618. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.)
⊢ ⟨“𝐴”⟩ = {⟨0, ( I ‘𝐴)⟩}
Theorem	ids1 14608	Identity function protection for a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ ⟨“𝐴”⟩ = ⟨“( I ‘𝐴)”⟩
Theorem	s1val 14609	Value of a singleton word. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.)
⊢ (𝐴 ∈ 𝑉 → ⟨“𝐴”⟩ = {⟨0, 𝐴⟩})
Theorem	s1rn 14610	The range of a singleton word. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ (𝐴 ∈ 𝑉 → ran ⟨“𝐴”⟩ = {𝐴})
Theorem	s1eq 14611	Equality theorem for a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ (𝐴 = 𝐵 → ⟨“𝐴”⟩ = ⟨“𝐵”⟩)
Theorem	s1eqd 14612	Equality theorem for a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ (𝜑 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → ⟨“𝐴”⟩ = ⟨“𝐵”⟩)
Theorem	s1cl 14613	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 14614	A singleton word is a word. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ (𝜑 → 𝐴 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ⟨“𝐴”⟩ ∈ Word 𝐵)
Theorem	s1prc 14615	Value of a singleton word if the symbol is a proper class. (Contributed by AV, 26-Mar-2022.)
⊢ (¬ 𝐴 ∈ V → ⟨“𝐴”⟩ = ⟨“∅”⟩)
Theorem	s1cli 14616	A singleton word is a word. (Contributed by Mario Carneiro, 26-Feb-2016.)
⊢ ⟨“𝐴”⟩ ∈ Word V
Theorem	s1len 14617	Length of a singleton word. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.)
⊢ (♯‘⟨“𝐴”⟩) = 1
Theorem	s1nz 14618	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 14619	The domain of a singleton word is a singleton. (Contributed by AV, 9-Jan-2020.)
⊢ dom ⟨“𝐴”⟩ = {0}
Theorem	s1dmALT 14620	Alternate version of s1dm 14619, 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 14621	Sole symbol of a singleton word. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.)
⊢ (𝐴 ∈ 𝐵 → (⟨“𝐴”⟩‘0) = 𝐴)
Theorem	lsws1 14622	The last symbol of a singleton word is its symbol. (Contributed by AV, 22-Oct-2018.)
⊢ (𝐴 ∈ 𝑉 → (lastS‘⟨“𝐴”⟩) = 𝐴)
Theorem	eqs1 14623	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 14624*	A word of length 1 is a singleton word. (Contributed by AV, 24-Jan-2021.)
⊢ ((𝑊 ∈ Word 𝑆 ∧ (♯‘𝑊) = 1) → ∃𝑠 ∈ 𝑆 𝑊 = ⟨“𝑠”⟩)
Theorem	wrdl1s1 14625	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) = 𝑆)))
Theorem	s111 14626	The singleton word function is injective. (Contributed by Mario Carneiro, 1-Oct-2015.) (Revised by Mario Carneiro, 26-Feb-2016.)
⊢ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) → (⟨“𝑆”⟩ = ⟨“𝑇”⟩ ↔ 𝑆 = 𝑇))
5.7.5  Concatenations with singleton words
Theorem	ccatws1cl 14627	The concatenation of a word with a singleton word is a word. (Contributed by Alexander van der Vekens, 22-Sep-2018.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑋 ∈ 𝑉) → (𝑊 ++ ⟨“𝑋”⟩) ∈ Word 𝑉)
Theorem	ccatws1clv 14628	The concatenation of a word with a singleton word (which can be over a different alphabet) is a word. (Contributed by AV, 5-Mar-2022.)
⊢ (𝑊 ∈ Word 𝑉 → (𝑊 ++ ⟨“𝑋”⟩) ∈ Word V)
Theorem	ccat2s1cl 14629	The concatenation of two singleton words is a word. (Contributed by Alexander van der Vekens, 22-Sep-2018.)
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (⟨“𝑋”⟩ ++ ⟨“𝑌”⟩) ∈ Word 𝑉)
Theorem	ccats1alpha 14630	A concatenation of a word with a singleton word is a word over an alphabet 𝑆 iff the symbols of both words belong to the alphabet 𝑆. (Contributed by AV, 27-Mar-2022.)
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝑋 ∈ 𝑈) → ((𝐴 ++ ⟨“𝑋”⟩) ∈ Word 𝑆 ↔ (𝐴 ∈ Word 𝑆 ∧ 𝑋 ∈ 𝑆)))
Theorem	ccatws1len 14631	The length of the concatenation of a word with a singleton word. (Contributed by Alexander van der Vekens, 22-Sep-2018.) (Revised by AV, 4-Mar-2022.)
⊢ (𝑊 ∈ Word 𝑉 → (♯‘(𝑊 ++ ⟨“𝑋”⟩)) = ((♯‘𝑊) + 1))
Theorem	ccatws1lenp1b 14632	The length of a word is 𝑁 iff the length of the concatenation of the word with a singleton word is 𝑁 + 1. (Contributed by AV, 4-Mar-2022.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ0) → ((♯‘(𝑊 ++ ⟨“𝑋”⟩)) = (𝑁 + 1) ↔ (♯‘𝑊) = 𝑁))
Theorem	wrdlenccats1lenm1 14633	The length of a word is the length of the word concatenated with a singleton word minus 1. (Contributed by AV, 28-Jun-2018.) (Revised by AV, 5-Mar-2022.)
⊢ (𝑊 ∈ Word 𝑉 → ((♯‘(𝑊 ++ ⟨“𝑆”⟩)) − 1) = (♯‘𝑊))
Theorem	ccat2s1len 14634	The length of the concatenation of two singleton words. (Contributed by Alexander van der Vekens, 22-Sep-2018.) (Revised by JJ, 14-Jan-2024.)
⊢ (♯‘(⟨“𝑋”⟩ ++ ⟨“𝑌”⟩)) = 2
Theorem	ccatw2s1cl 14635	The concatenation of a word with two singleton words is a word. (Contributed by Alexander van der Vekens, 22-Sep-2018.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → ((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩) ∈ Word 𝑉)
Theorem	ccatw2s1len 14636	The length of the concatenation of a word with two singleton words. (Contributed by Alexander van der Vekens, 22-Sep-2018.) (Revised by AV, 5-Mar-2022.)
⊢ (𝑊 ∈ Word 𝑉 → (♯‘((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)) = ((♯‘𝑊) + 2))
Theorem	ccats1val1 14637	Value of a symbol in the left half of a word concatenated with a single symbol. (Contributed by Alexander van der Vekens, 5-Aug-2018.) (Revised by JJ, 20-Jan-2024.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐼 ∈ (0..^(♯‘𝑊))) → ((𝑊 ++ ⟨“𝑆”⟩)‘𝐼) = (𝑊‘𝐼))
Theorem	ccats1val2 14638	Value of the symbol concatenated with a word. (Contributed by Alexander van der Vekens, 5-Aug-2018.) (Proof shortened by Alexander van der Vekens, 14-Oct-2018.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑆 ∈ 𝑉 ∧ 𝐼 = (♯‘𝑊)) → ((𝑊 ++ ⟨“𝑆”⟩)‘𝐼) = 𝑆)
Theorem	ccat1st1st 14639	The first symbol of a word concatenated with its first symbol is the first symbol of the word. This theorem holds even if 𝑊 is the empty word. (Contributed by AV, 26-Mar-2022.)
⊢ (𝑊 ∈ Word 𝑉 → ((𝑊 ++ ⟨“(𝑊‘0)”⟩)‘0) = (𝑊‘0))
Theorem	ccat2s1p1 14640	Extract the first of two concatenated singleton words. (Contributed by Alexander van der Vekens, 22-Sep-2018.) (Revised by JJ, 20-Jan-2024.)
⊢ (𝑋 ∈ 𝑉 → ((⟨“𝑋”⟩ ++ ⟨“𝑌”⟩)‘0) = 𝑋)
Theorem	ccat2s1p2 14641	Extract the second of two concatenated singleton words. (Contributed by Alexander van der Vekens, 22-Sep-2018.) (Revised by JJ, 20-Jan-2024.)
⊢ (𝑌 ∈ 𝑉 → ((⟨“𝑋”⟩ ++ ⟨“𝑌”⟩)‘1) = 𝑌)
Theorem	ccatw2s1ass 14642	Associative law for a concatenation of a word with two singleton words. (Contributed by Alexander van der Vekens, 22-Sep-2018.)
⊢ (𝑊 ∈ Word 𝑉 → ((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩) = (𝑊 ++ (⟨“𝑋”⟩ ++ ⟨“𝑌”⟩)))
Theorem	ccatws1n0 14643	The concatenation of a word with a singleton word is not the empty set. (Contributed by Alexander van der Vekens, 29-Sep-2018.) (Revised by AV, 5-Mar-2022.)
⊢ (𝑊 ∈ Word 𝑉 → (𝑊 ++ ⟨“𝑋”⟩) ≠ ∅)
Theorem	ccatws1ls 14644	The last symbol of the concatenation of a word with a singleton word is the symbol of the singleton word. (Contributed by AV, 29-Sep-2018.) (Proof shortened by AV, 14-Oct-2018.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑋 ∈ 𝑉) → ((𝑊 ++ ⟨“𝑋”⟩)‘(♯‘𝑊)) = 𝑋)
Theorem	lswccats1 14645	The last symbol of a word concatenated with a singleton word is the symbol of the singleton word. (Contributed by AV, 6-Aug-2018.) (Proof shortened by AV, 22-Oct-2018.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑆 ∈ 𝑉) → (lastS‘(𝑊 ++ ⟨“𝑆”⟩)) = 𝑆)
Theorem	lswccats1fst 14646	The last symbol of a nonempty word concatenated with its first symbol is the first symbol. (Contributed by AV, 28-Jun-2018.) (Proof shortened by AV, 1-May-2020.)
⊢ ((𝑃 ∈ Word 𝑉 ∧ 1 ≤ (♯‘𝑃)) → (lastS‘(𝑃 ++ ⟨“(𝑃‘0)”⟩)) = ((𝑃 ++ ⟨“(𝑃‘0)”⟩)‘0))
Theorem	ccatw2s1p1 14647	Extract the symbol of the first singleton word of a word concatenated with this singleton word and another singleton word. (Contributed by Alexander van der Vekens, 22-Sep-2018.) (Proof shortened by AV, 1-May-2020.) (Revised by AV, 1-May-2020.) (Revised by AV, 29-Jan-2024.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = 𝑁 ∧ 𝑋 ∈ 𝑉) → (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘𝑁) = 𝑋)
Theorem	ccatw2s1p2 14648	Extract the second of two single symbols concatenated with a word. (Contributed by Alexander van der Vekens, 22-Sep-2018.) (Proof shortened by AV, 1-May-2020.)
⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = 𝑁) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘(𝑁 + 1)) = 𝑌)
Theorem	ccat2s1fvw 14649	Extract a symbol of a word from the concatenation of the word with two single symbols. (Contributed by AV, 22-Sep-2018.) (Revised by AV, 13-Jan-2020.) (Proof shortened by AV, 1-May-2020.) (Revised by AV, 28-Jan-2024.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐼 ∈ ℕ0 ∧ 𝐼 < (♯‘𝑊)) → (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘𝐼) = (𝑊‘𝐼))
Theorem	ccat2s1fst 14650	The first symbol of the concatenation of a word with two single symbols. (Contributed by Alexander van der Vekens, 22-Sep-2018.) (Revised by AV, 28-Jan-2024.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 0 < (♯‘𝑊)) → (((𝑊 ++ ⟨“𝑋”⟩) ++ ⟨“𝑌”⟩)‘0) = (𝑊‘0))
5.7.6  Subwords/substrings
Syntax	csubstr 14651	Syntax for the subword operator.
class substr
Definition	df-substr 14652*	Define an operation which extracts portions (called subwords or substrings) of words. Definition in Section 9.1 of [AhoHopUll] p. 318. (Contributed by Stefan O'Rear, 15-Aug-2015.)
⊢ substr = (𝑠 ∈ V, 𝑏 ∈ (ℤ × ℤ) ↦ if(((1st ‘𝑏)..^(2nd ‘𝑏)) ⊆ dom 𝑠, (𝑥 ∈ (0..^((2nd ‘𝑏) − (1st ‘𝑏))) ↦ (𝑠‘(𝑥 + (1st ‘𝑏)))), ∅))
Theorem	swrdnznd 14653	The value of a subword operation for noninteger arguments is the empty set. (This is due to our definition of function values for out-of-domain arguments, see ndmfv 6895). (Contributed by AV, 2-Dec-2022.) (New usage is discouraged.)
⊢ (¬ (𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ) → (𝑆 substr ⟨𝐹, 𝐿⟩) = ∅)
Theorem	swrdval 14654*	Value of a subword. (Contributed by Stefan O'Rear, 15-Aug-2015.)
⊢ ((𝑆 ∈ 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ) → (𝑆 substr ⟨𝐹, 𝐿⟩) = if((𝐹..^𝐿) ⊆ dom 𝑆, (𝑥 ∈ (0..^(𝐿 − 𝐹)) ↦ (𝑆‘(𝑥 + 𝐹))), ∅))
Theorem	swrd00 14655	A zero length substring. (Contributed by Stefan O'Rear, 27-Aug-2015.)
⊢ (𝑆 substr ⟨𝑋, 𝑋⟩) = ∅
Theorem	swrdcl 14656	Closure of the subword extractor. (Contributed by Stefan O'Rear, 16-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.)
⊢ (𝑆 ∈ Word 𝐴 → (𝑆 substr ⟨𝐹, 𝐿⟩) ∈ Word 𝐴)
Theorem	swrdval2 14657*	Value of the subword extractor in its intended domain. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Proof shortened by AV, 2-May-2020.)
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝐹 ∈ (0...𝐿) ∧ 𝐿 ∈ (0...(♯‘𝑆))) → (𝑆 substr ⟨𝐹, 𝐿⟩) = (𝑥 ∈ (0..^(𝐿 − 𝐹)) ↦ (𝑆‘(𝑥 + 𝐹))))
Theorem	swrdlen 14658	Length of an extracted subword. (Contributed by Stefan O'Rear, 16-Aug-2015.)
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝐹 ∈ (0...𝐿) ∧ 𝐿 ∈ (0...(♯‘𝑆))) → (♯‘(𝑆 substr ⟨𝐹, 𝐿⟩)) = (𝐿 − 𝐹))
Theorem	swrdfv 14659	A symbol in an extracted subword, indexed using the subword's indices. (Contributed by Stefan O'Rear, 16-Aug-2015.)
⊢ (((𝑆 ∈ Word 𝐴 ∧ 𝐹 ∈ (0...𝐿) ∧ 𝐿 ∈ (0...(♯‘𝑆))) ∧ 𝑋 ∈ (0..^(𝐿 − 𝐹))) → ((𝑆 substr ⟨𝐹, 𝐿⟩)‘𝑋) = (𝑆‘(𝑋 + 𝐹)))
Theorem	swrdfv0 14660	The first symbol in an extracted subword. (Contributed by AV, 27-Apr-2022.)
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝐹 ∈ (0..^𝐿) ∧ 𝐿 ∈ (0...(♯‘𝑆))) → ((𝑆 substr ⟨𝐹, 𝐿⟩)‘0) = (𝑆‘𝐹))
Theorem	swrdf 14661	A subword of a word is a function from a half-open range of nonnegative integers of the same length as the subword to the set of symbols for the original word. (Contributed by AV, 13-Nov-2018.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) → (𝑊 substr ⟨𝑀, 𝑁⟩):(0..^(𝑁 − 𝑀))⟶𝑉)
Theorem	swrdvalfn 14662	Value of the subword extractor as function with domain. (Contributed by Alexander van der Vekens, 28-Mar-2018.) (Proof shortened by AV, 2-May-2020.)
⊢ ((𝑆 ∈ Word 𝑉 ∧ 𝐹 ∈ (0...𝐿) ∧ 𝐿 ∈ (0...(♯‘𝑆))) → (𝑆 substr ⟨𝐹, 𝐿⟩) Fn (0..^(𝐿 − 𝐹)))
Theorem	swrdrn 14663	The range of a subword of a word is a subset of the set of symbols for the word. (Contributed by AV, 13-Nov-2018.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) → ran (𝑊 substr ⟨𝑀, 𝑁⟩) ⊆ 𝑉)
Theorem	swrdlend 14664	The value of the subword extractor is the empty set (undefined) if the range is not valid. (Contributed by Alexander van der Vekens, 16-Mar-2018.) (Proof shortened by AV, 2-May-2020.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ) → (𝐿 ≤ 𝐹 → (𝑊 substr ⟨𝐹, 𝐿⟩) = ∅))
Theorem	swrdnd 14665	The value of the subword extractor is the empty set (undefined) if the range is not valid. (Contributed by Alexander van der Vekens, 16-Mar-2018.) (Proof shortened by AV, 2-May-2020.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ) → ((𝐹 < 0 ∨ 𝐿 ≤ 𝐹 ∨ (♯‘𝑊) < 𝐿) → (𝑊 substr ⟨𝐹, 𝐿⟩) = ∅))
Theorem	swrdnd2 14666	Value of the subword extractor outside its intended domain. (Contributed by Alexander van der Vekens, 24-May-2018.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝐵 ≤ 𝐴 ∨ (♯‘𝑊) ≤ 𝐴 ∨ 𝐵 ≤ 0) → (𝑊 substr ⟨𝐴, 𝐵⟩) = ∅))
Theorem	swrdnnn0nd 14667	The value of a subword operation for arguments not being nonnegative integers is the empty set. (Contributed by AV, 2-Dec-2022.)
⊢ ((𝑆 ∈ Word 𝑉 ∧ ¬ (𝐹 ∈ ℕ0 ∧ 𝐿 ∈ ℕ0)) → (𝑆 substr ⟨𝐹, 𝐿⟩) = ∅)
Theorem	swrdnd0 14668	The value of a subword operation for inproper arguments is the empty set. (Contributed by AV, 2-Dec-2022.)
⊢ (𝑆 ∈ Word 𝑉 → (¬ (𝐹 ∈ (0...𝐿) ∧ 𝐿 ∈ (0...(♯‘𝑆))) → (𝑆 substr ⟨𝐹, 𝐿⟩) = ∅))
Theorem	swrd0 14669	A subword of an empty set is always the empty set. (Contributed by AV, 31-Mar-2018.) (Revised by AV, 20-Oct-2018.) (Proof shortened by AV, 2-May-2020.)
⊢ (∅ substr ⟨𝐹, 𝐿⟩) = ∅
Theorem	swrdrlen 14670	Length of a right-anchored subword. (Contributed by Alexander van der Vekens, 5-Apr-2018.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐼 ∈ (0...(♯‘𝑊))) → (♯‘(𝑊 substr ⟨𝐼, (♯‘𝑊)⟩)) = ((♯‘𝑊) − 𝐼))
Theorem	swrdlen2 14671	Length of an extracted subword. (Contributed by AV, 5-May-2020.)
⊢ ((𝑆 ∈ Word 𝑉 ∧ (𝐹 ∈ ℕ0 ∧ 𝐿 ∈ (ℤ≥‘𝐹)) ∧ 𝐿 ≤ (♯‘𝑆)) → (♯‘(𝑆 substr ⟨𝐹, 𝐿⟩)) = (𝐿 − 𝐹))
Theorem	swrdfv2 14672	A symbol in an extracted subword, indexed using the word's indices. (Contributed by AV, 5-May-2020.)
⊢ (((𝑆 ∈ Word 𝑉 ∧ (𝐹 ∈ ℕ0 ∧ 𝐿 ∈ (ℤ≥‘𝐹)) ∧ 𝐿 ≤ (♯‘𝑆)) ∧ 𝑋 ∈ (𝐹..^𝐿)) → ((𝑆 substr ⟨𝐹, 𝐿⟩)‘(𝑋 − 𝐹)) = (𝑆‘𝑋))
Theorem	swrdwrdsymb 14673	A subword is a word over the symbols it consists of. (Contributed by AV, 2-Dec-2022.)
⊢ (𝑆 ∈ Word 𝐴 → (𝑆 substr ⟨𝑀, 𝑁⟩) ∈ Word (𝑆 “ (𝑀..^𝑁)))
Theorem	swrdsb0eq 14674	Two subwords with the same bounds are equal if the range is not valid. (Contributed by AV, 4-May-2020.)
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ 𝑁 ≤ 𝑀) → (𝑊 substr ⟨𝑀, 𝑁⟩) = (𝑈 substr ⟨𝑀, 𝑁⟩))
Theorem	swrdsbslen 14675	Two subwords with the same bounds have the same length. (Contributed by AV, 4-May-2020.)
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) → (♯‘(𝑊 substr ⟨𝑀, 𝑁⟩)) = (♯‘(𝑈 substr ⟨𝑀, 𝑁⟩)))
Theorem	swrdspsleq 14676*	Two words have a common subword (starting at the same position with the same length) iff they have the same symbols at each position. (Contributed by Alexander van der Vekens, 7-Aug-2018.) (Proof shortened by AV, 7-May-2020.)
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) → ((𝑊 substr ⟨𝑀, 𝑁⟩) = (𝑈 substr ⟨𝑀, 𝑁⟩) ↔ ∀𝑖 ∈ (𝑀..^𝑁)(𝑊‘𝑖) = (𝑈‘𝑖)))
Theorem	swrds1 14677	Extract a single symbol from a word. (Contributed by Stefan O'Rear, 23-Aug-2015.)
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ (0..^(♯‘𝑊))) → (𝑊 substr ⟨𝐼, (𝐼 + 1)⟩) = ⟨“(𝑊‘𝐼)”⟩)
Theorem	swrdlsw 14678	Extract the last single symbol from a word. (Contributed by Alexander van der Vekens, 23-Sep-2018.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅) → (𝑊 substr ⟨((♯‘𝑊) − 1), (♯‘𝑊)⟩) = ⟨“(lastS‘𝑊)”⟩)
Theorem	ccatswrd 14679	Joining two adjacent subwords makes a longer subword. (Contributed by Stefan O'Rear, 20-Aug-2015.)
⊢ ((𝑆 ∈ Word 𝐴 ∧ (𝑋 ∈ (0...𝑌) ∧ 𝑌 ∈ (0...𝑍) ∧ 𝑍 ∈ (0...(♯‘𝑆)))) → ((𝑆 substr ⟨𝑋, 𝑌⟩) ++ (𝑆 substr ⟨𝑌, 𝑍⟩)) = (𝑆 substr ⟨𝑋, 𝑍⟩))
Theorem	swrdccat2 14680	Recover the right half of a concatenated word. (Contributed by Mario Carneiro, 27-Sep-2015.)
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → ((𝑆 ++ 𝑇) substr ⟨(♯‘𝑆), ((♯‘𝑆) + (♯‘𝑇))⟩) = 𝑇)
5.7.7  Prefixes of a word
Syntax	cpfx 14681	Syntax for the prefix operator.
class prefix
Definition	df-pfx 14682*	Define an operation which extracts prefixes of words, i.e. subwords (or substrings) starting at the beginning of a word (or string). In other words, (𝑆 prefix 𝐿) is the prefix of the word 𝑆 of length 𝐿. Definition in Section 9.1 of [AhoHopUll] p. 318. See also Wikipedia "Substring" https://en.wikipedia.org/wiki/Substring#Prefix. (Contributed by AV, 2-May-2020.)
⊢ prefix = (𝑠 ∈ V, 𝑙 ∈ ℕ0 ↦ (𝑠 substr ⟨0, 𝑙⟩))
Theorem	pfxnndmnd 14683	The value of a prefix operation for out-of-domain arguments. (This is due to our definition of function values for out-of-domain arguments, see ndmfv 6895). (Contributed by AV, 3-Dec-2022.) (New usage is discouraged.)
⊢ (¬ (𝑆 ∈ V ∧ 𝐿 ∈ ℕ0) → (𝑆 prefix 𝐿) = ∅)
Theorem	pfxval 14684	Value of a prefix operation. (Contributed by AV, 2-May-2020.)
⊢ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) → (𝑆 prefix 𝐿) = (𝑆 substr ⟨0, 𝐿⟩))
Theorem	pfx00 14685	The zero length prefix is the empty set. (Contributed by AV, 2-May-2020.)
⊢ (𝑆 prefix 0) = ∅
Theorem	pfx0 14686	A prefix of an empty set is always the empty set. (Contributed by AV, 3-May-2020.)
⊢ (∅ prefix 𝐿) = ∅
Theorem	pfxval0 14687	Value of a prefix operation. This theorem should only be used in proofs if 𝐿 ∈ ℕ0 is not available. Otherwise (and usually), pfxval 14684 should be used. (Contributed by AV, 3-Dec-2022.) (New usage is discouraged.)
⊢ (𝑆 ∈ Word 𝐴 → (𝑆 prefix 𝐿) = (𝑆 substr ⟨0, 𝐿⟩))
Theorem	pfxcl 14688	Closure of the prefix extractor. (Contributed by AV, 2-May-2020.)
⊢ (𝑆 ∈ Word 𝐴 → (𝑆 prefix 𝐿) ∈ Word 𝐴)
Theorem	pfxmpt 14689*	Value of the prefix extractor as a mapping. (Contributed by AV, 2-May-2020.)
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝐿 ∈ (0...(♯‘𝑆))) → (𝑆 prefix 𝐿) = (𝑥 ∈ (0..^𝐿) ↦ (𝑆‘𝑥)))
Theorem	pfxres 14690	Value of the prefix extractor as the restriction of a word. (Contributed by Stefan O'Rear, 24-Aug-2015.) (Revised by AV, 2-May-2020.)
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝐿 ∈ (0...(♯‘𝑆))) → (𝑆 prefix 𝐿) = (𝑆 ↾ (0..^𝐿)))
Theorem	pfxf 14691	A prefix of a word is a function from a half-open range of nonnegative integers of the same length as the prefix to the set of symbols for the original word. (Contributed by AV, 2-May-2020.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊))) → (𝑊 prefix 𝐿):(0..^𝐿)⟶𝑉)
Theorem	pfxfn 14692	Value of the prefix extractor as function with domain. (Contributed by AV, 2-May-2020.)
⊢ ((𝑆 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑆))) → (𝑆 prefix 𝐿) Fn (0..^𝐿))
Theorem	pfxfv 14693	A symbol in a prefix of a word, indexed using the prefix' indices. (Contributed by Alexander van der Vekens, 16-Jun-2018.) (Revised by AV, 3-May-2020.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊)) ∧ 𝐼 ∈ (0..^𝐿)) → ((𝑊 prefix 𝐿)‘𝐼) = (𝑊‘𝐼))
Theorem	pfxlen 14694	Length of a prefix. (Contributed by Stefan O'Rear, 24-Aug-2015.) (Revised by AV, 2-May-2020.)
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝐿 ∈ (0...(♯‘𝑆))) → (♯‘(𝑆 prefix 𝐿)) = 𝐿)
Theorem	pfxid 14695	A word is a prefix of itself. (Contributed by Stefan O'Rear, 16-Aug-2015.) (Revised by AV, 2-May-2020.)
⊢ (𝑆 ∈ Word 𝐴 → (𝑆 prefix (♯‘𝑆)) = 𝑆)
Theorem	pfxrn 14696	The range of a prefix of a word is a subset of the set of symbols for the word. (Contributed by AV, 2-May-2020.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(♯‘𝑊))) → ran (𝑊 prefix 𝐿) ⊆ 𝑉)
Theorem	pfxn0 14697	A prefix consisting of at least one symbol is not empty. (Contributed by Alexander van der Vekens, 4-Aug-2018.) (Revised by AV, 2-May-2020.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℕ ∧ 𝐿 ≤ (♯‘𝑊)) → (𝑊 prefix 𝐿) ≠ ∅)
Theorem	pfxnd 14698	The value of a prefix operation for a length argument larger than the word length is the empty set. (This is due to our definition of function values for out-of-domain arguments, see ndmfv 6895). (Contributed by AV, 3-May-2020.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℕ0 ∧ (♯‘𝑊) < 𝐿) → (𝑊 prefix 𝐿) = ∅)
Theorem	pfxnd0 14699	The value of a prefix operation for a length argument not in the range of the word length is the empty set. (This is due to our definition of function values for out-of-domain arguments, see ndmfv 6895). (Contributed by AV, 3-Dec-2022.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∉ (0...(♯‘𝑊))) → (𝑊 prefix 𝐿) = ∅)
Theorem	pfxwrdsymb 14700	A prefix of a word is a word over the symbols it consists of. (Contributed by AV, 3-Dec-2022.)
⊢ (𝑆 ∈ Word 𝐴 → (𝑆 prefix 𝐿) ∈ Word (𝑆 “ (0..^𝐿)))