![]() |
Metamath
Proof Explorer Theorem List (p. 147 of 491) | < 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: | ![]() (1-30946) |
![]() (30947-32469) |
![]() (32470-49035) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | lsw1 14601 | 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 14602 | 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 14603 | 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‘𝑊) ∈ 𝑉) | ||
Syntax | cconcat 14604 | Syntax for the concatenation operator. |
class ++ | ||
Definition | df-concat 14605* | 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 14606 | 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 14607* | Value of the concatenation operator. (Contributed by Stefan O'Rear, 15-Aug-2015.) |
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑊) → (𝑆 ++ 𝑇) = (𝑥 ∈ (0..^((♯‘𝑆) + (♯‘𝑇))) ↦ if(𝑥 ∈ (0..^(♯‘𝑆)), (𝑆‘𝑥), (𝑇‘(𝑥 − (♯‘𝑆)))))) | ||
Theorem | ccatcl 14608 | 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 14609 | The length of a concatenated word. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by JJ, 1-Jan-2024.) |
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐵) → (♯‘(𝑆 ++ 𝑇)) = ((♯‘𝑆) + (♯‘𝑇))) | ||
Theorem | ccat0 14610 | 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 14611 | 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 14612 | 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 14613 | 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 14614 | 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 14615 | 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 14616 | 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 14617 | 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 14618 | 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 14619 | The first symbol of the right (nonempty) half of a concatenated word. (Contributed by AV, 23-Apr-2022.) |
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝐵 ≠ ∅) → ((𝐴 ++ 𝐵)‘(♯‘𝐴)) = (𝐵‘0)) | ||
Theorem | ccatlid 14620 | 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 14621 | 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 14622 | Associative law for concatenation of words. (Contributed by Stefan O'Rear, 15-Aug-2015.) |
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵) → ((𝑆 ++ 𝑇) ++ 𝑈) = (𝑆 ++ (𝑇 ++ 𝑈))) | ||
Theorem | ccatrn 14623 | The range of a concatenated word. (Contributed by Stefan O'Rear, 15-Aug-2015.) |
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → ran (𝑆 ++ 𝑇) = (ran 𝑆 ∪ ran 𝑇)) | ||
Theorem | ccatidid 14624 | Concatenation of the empty word by the empty word. (Contributed by AV, 26-Mar-2022.) |
⊢ (∅ ++ ∅) = ∅ | ||
Theorem | lswccatn0lsw 14625 | 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 14626 | 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 14627 | 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 14628 | 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 𝑆) | ||
Syntax | cs1 14629 | Syntax for the singleton word constructor. |
class 〈“𝐴”〉 | ||
Definition | df-s1 14630 | 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 14638, and not, as maybe expected, the empty word, see also s1nz 14641. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.) |
⊢ 〈“𝐴”〉 = {〈0, ( I ‘𝐴)〉} | ||
Theorem | ids1 14631 | Identity function protection for a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016.) |
⊢ 〈“𝐴”〉 = 〈“( I ‘𝐴)”〉 | ||
Theorem | s1val 14632 | Value of a singleton word. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.) |
⊢ (𝐴 ∈ 𝑉 → 〈“𝐴”〉 = {〈0, 𝐴〉}) | ||
Theorem | s1rn 14633 | The range of a singleton word. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ (𝐴 ∈ 𝑉 → ran 〈“𝐴”〉 = {𝐴}) | ||
Theorem | s1eq 14634 | Equality theorem for a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016.) |
⊢ (𝐴 = 𝐵 → 〈“𝐴”〉 = 〈“𝐵”〉) | ||
Theorem | s1eqd 14635 | Equality theorem for a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → 〈“𝐴”〉 = 〈“𝐵”〉) | ||
Theorem | s1cl 14636 | 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 14637 | A singleton word is a word. (Contributed by Mario Carneiro, 26-Feb-2016.) |
⊢ (𝜑 → 𝐴 ∈ 𝐵) ⇒ ⊢ (𝜑 → 〈“𝐴”〉 ∈ Word 𝐵) | ||
Theorem | s1prc 14638 | Value of a singleton word if the symbol is a proper class. (Contributed by AV, 26-Mar-2022.) |
⊢ (¬ 𝐴 ∈ V → 〈“𝐴”〉 = 〈“∅”〉) | ||
Theorem | s1cli 14639 | A singleton word is a word. (Contributed by Mario Carneiro, 26-Feb-2016.) |
⊢ 〈“𝐴”〉 ∈ Word V | ||
Theorem | s1len 14640 | Length of a singleton word. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.) |
⊢ (♯‘〈“𝐴”〉) = 1 | ||
Theorem | s1nz 14641 | 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 14642 | The domain of a singleton word is a singleton. (Contributed by AV, 9-Jan-2020.) |
⊢ dom 〈“𝐴”〉 = {0} | ||
Theorem | s1dmALT 14643 | Alternate version of s1dm 14642, 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 14644 | Sole symbol of a singleton word. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.) |
⊢ (𝐴 ∈ 𝐵 → (〈“𝐴”〉‘0) = 𝐴) | ||
Theorem | lsws1 14645 | The last symbol of a singleton word is its symbol. (Contributed by AV, 22-Oct-2018.) |
⊢ (𝐴 ∈ 𝑉 → (lastS‘〈“𝐴”〉) = 𝐴) | ||
Theorem | eqs1 14646 | 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 14647* | A word of length 1 is a singleton word. (Contributed by AV, 24-Jan-2021.) |
⊢ ((𝑊 ∈ Word 𝑆 ∧ (♯‘𝑊) = 1) → ∃𝑠 ∈ 𝑆 𝑊 = 〈“𝑠”〉) | ||
Theorem | wrdl1s1 14648 | 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 14649 | The singleton word function is injective. (Contributed by Mario Carneiro, 1-Oct-2015.) (Revised by Mario Carneiro, 26-Feb-2016.) |
⊢ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) → (〈“𝑆”〉 = 〈“𝑇”〉 ↔ 𝑆 = 𝑇)) | ||
Theorem | ccatws1cl 14650 | 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 14651 | 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 14652 | The concatenation of two singleton words is a word. (Contributed by Alexander van der Vekens, 22-Sep-2018.) |
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (〈“𝑋”〉 ++ 〈“𝑌”〉) ∈ Word 𝑉) | ||
Theorem | ccats1alpha 14653 | 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 14654 | 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 14655 | 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 14656 | 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 14657 | 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 14658 | 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 14659 | 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 14660 | 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 14661 | 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 14662 | 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 14663 | 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 14664 | 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 14665 | Associative law for a concatenation of a word with two singleton words. (Contributed by Alexander van der Vekens, 22-Sep-2018.) |
⊢ (𝑊 ∈ Word 𝑉 → ((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉) = (𝑊 ++ (〈“𝑋”〉 ++ 〈“𝑌”〉))) | ||
Theorem | ccatws1n0 14666 | 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 14667 | 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 14668 | 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 14669 | 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 14670 | 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 14671 | 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 14672 | 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 14673 | 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)) | ||
Syntax | csubstr 14674 | Syntax for the subword operator. |
class substr | ||
Definition | df-substr 14675* | 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 14676 | 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 6941). (Contributed by AV, 2-Dec-2022.) (New usage is discouraged.) |
⊢ (¬ (𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ) → (𝑆 substr 〈𝐹, 𝐿〉) = ∅) | ||
Theorem | swrdval 14677* | Value of a subword. (Contributed by Stefan O'Rear, 15-Aug-2015.) |
⊢ ((𝑆 ∈ 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ) → (𝑆 substr 〈𝐹, 𝐿〉) = if((𝐹..^𝐿) ⊆ dom 𝑆, (𝑥 ∈ (0..^(𝐿 − 𝐹)) ↦ (𝑆‘(𝑥 + 𝐹))), ∅)) | ||
Theorem | swrd00 14678 | A zero length substring. (Contributed by Stefan O'Rear, 27-Aug-2015.) |
⊢ (𝑆 substr 〈𝑋, 𝑋〉) = ∅ | ||
Theorem | swrdcl 14679 | 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 14680* | 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 14681 | Length of an extracted subword. (Contributed by Stefan O'Rear, 16-Aug-2015.) |
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝐹 ∈ (0...𝐿) ∧ 𝐿 ∈ (0...(♯‘𝑆))) → (♯‘(𝑆 substr 〈𝐹, 𝐿〉)) = (𝐿 − 𝐹)) | ||
Theorem | swrdfv 14682 | 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 14683 | The first symbol in an extracted subword. (Contributed by AV, 27-Apr-2022.) |
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝐹 ∈ (0..^𝐿) ∧ 𝐿 ∈ (0...(♯‘𝑆))) → ((𝑆 substr 〈𝐹, 𝐿〉)‘0) = (𝑆‘𝐹)) | ||
Theorem | swrdf 14684 | 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 14685 | 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 14686 | 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 14687 | 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 14688 | 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 14689 | Value of the subword extractor outside its intended domain. (Contributed by Alexander van der Vekens, 24-May-2018.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝐵 ≤ 𝐴 ∨ (♯‘𝑊) ≤ 𝐴 ∨ 𝐵 ≤ 0) → (𝑊 substr 〈𝐴, 𝐵〉) = ∅)) | ||
Theorem | swrdnnn0nd 14690 | 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 14691 | 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 14692 | 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 14693 | Length of a right-anchored subword. (Contributed by Alexander van der Vekens, 5-Apr-2018.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐼 ∈ (0...(♯‘𝑊))) → (♯‘(𝑊 substr 〈𝐼, (♯‘𝑊)〉)) = ((♯‘𝑊) − 𝐼)) | ||
Theorem | swrdlen2 14694 | Length of an extracted subword. (Contributed by AV, 5-May-2020.) |
⊢ ((𝑆 ∈ Word 𝑉 ∧ (𝐹 ∈ ℕ0 ∧ 𝐿 ∈ (ℤ≥‘𝐹)) ∧ 𝐿 ≤ (♯‘𝑆)) → (♯‘(𝑆 substr 〈𝐹, 𝐿〉)) = (𝐿 − 𝐹)) | ||
Theorem | swrdfv2 14695 | A symbol in an extracted subword, indexed using the word's indices. (Contributed by AV, 5-May-2020.) |
⊢ (((𝑆 ∈ Word 𝑉 ∧ (𝐹 ∈ ℕ0 ∧ 𝐿 ∈ (ℤ≥‘𝐹)) ∧ 𝐿 ≤ (♯‘𝑆)) ∧ 𝑋 ∈ (𝐹..^𝐿)) → ((𝑆 substr 〈𝐹, 𝐿〉)‘(𝑋 − 𝐹)) = (𝑆‘𝑋)) | ||
Theorem | swrdwrdsymb 14696 | A subword is a word over the symbols it consists of. (Contributed by AV, 2-Dec-2022.) |
⊢ (𝑆 ∈ Word 𝐴 → (𝑆 substr 〈𝑀, 𝑁〉) ∈ Word (𝑆 “ (𝑀..^𝑁))) | ||
Theorem | swrdsb0eq 14697 | 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 14698 | Two subwords with the same bounds have the same length. (Contributed by AV, 4-May-2020.) |
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ (𝑁 ≤ (♯‘𝑊) ∧ 𝑁 ≤ (♯‘𝑈))) → (♯‘(𝑊 substr 〈𝑀, 𝑁〉)) = (♯‘(𝑈 substr 〈𝑀, 𝑁〉))) | ||
Theorem | swrdspsleq 14699* | 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 14700 | Extract a single symbol from a word. (Contributed by Stefan O'Rear, 23-Aug-2015.) |
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐼 ∈ (0..^(♯‘𝑊))) → (𝑊 substr 〈𝐼, (𝐼 + 1)〉) = 〈“(𝑊‘𝐼)”〉) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |