![]() |
Metamath
Proof Explorer Theorem List (p. 138 of 443) | < 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-28474) |
![]() (28475-29999) |
![]() (30000-44271) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | 0wrd0 13701 | The empty word is the only word over an empty alphabet. (Contributed by AV, 25-Oct-2018.) |
⊢ (𝑊 ∈ Word ∅ ↔ 𝑊 = ∅) | ||
Theorem | ffz0iswrd 13702 | 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 | ffz0iswrdOLD 13703 | Obsolete proof of ffz0iswrd 13702 as of 1-May-2023. (Contributed by AV, 31-Jan-2018.) (Proof shortened by AV, 13-Oct-2018.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (𝑊:(0...𝐿)⟶𝑆 → 𝑊 ∈ Word 𝑆) | ||
Theorem | wrdsymb 13704 | A word is a word over the symbols it consists of. (Contributed by AV, 1-Dec-2022.) |
⊢ (𝑆 ∈ Word 𝐴 → 𝑆 ∈ Word (𝑆 “ (0..^(♯‘𝑆)))) | ||
Theorem | nfwrd 13705 | Hypothesis builder for Word 𝑆. (Contributed by Mario Carneiro, 26-Feb-2016.) |
⊢ Ⅎ𝑥𝑆 ⇒ ⊢ Ⅎ𝑥Word 𝑆 | ||
Theorem | csbwrdg 13706* | Class substitution for the symbols of a word. (Contributed by Alexander van der Vekens, 15-Jul-2018.) |
⊢ (𝑆 ∈ 𝑉 → ⦋𝑆 / 𝑥⦌Word 𝑥 = Word 𝑆) | ||
Theorem | wrdnval 13707* | 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 𝑉 ∣ (♯‘𝑤) = 𝑁} = (𝑉 ↑𝑚 (0..^𝑁))) | ||
Theorem | wrdmap 13708 | Words as a mapping. (Contributed by Thierry Arnoux, 4-Mar-2020.) |
⊢ ((𝑉 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0) → ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = 𝑁) ↔ 𝑊 ∈ (𝑉 ↑𝑚 (0..^𝑁)))) | ||
Theorem | hashwrdn 13709* | 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 13710* | 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 | wrdnfiOLD 13711* | Obsolete version of wrdnfi 13710 as of 4-May-2023. (Contributed by Alexander van der Vekens, 25-Mar-2018.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ ((𝑉 ∈ Fin ∧ 𝑁 ∈ ℕ0) → {𝑤 ∈ Word 𝑉 ∣ (♯‘𝑤) = 𝑁} ∈ Fin) | ||
Theorem | wrdsymb0 13712 | 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 13713 | A word with length at least 1 is not empty. (Contributed by AV, 14-Oct-2018.) |
⊢ (𝑊 ∈ Word 𝑉 → (𝑊 ≠ ∅ ↔ 1 ≤ (♯‘𝑊))) | ||
Theorem | len0nnbi 13714 | The length of a word is a positive integer iff the word is not empty. (Contributed by AV, 22-Mar-2022.) |
⊢ (𝑊 ∈ Word 𝑆 → (𝑊 ≠ ∅ ↔ (♯‘𝑊) ∈ ℕ)) | ||
Theorem | wrdlenge2n0 13715 | 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 13716 | 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 13717* | 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 13718 | 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 13719 | 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 13720* | Two words are equal iff they have the same length and the same symbol at each position. (Contributed by AV, 13-Apr-2018.) |
⊢ ((𝑈 ∈ Word 𝑉 ∧ 𝑊 ∈ Word 𝑉) → (𝑈 = 𝑊 ↔ ((♯‘𝑈) = (♯‘𝑊) ∧ ∀𝑖 ∈ (0..^(♯‘𝑈))(𝑈‘𝑖) = (𝑊‘𝑖)))) | ||
Theorem | elovmpowrd 13721* | Implications for the value of an operation defined by the maps-to notation with a class abstration 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 13722* | 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 13723 | A word truncated by a symbol is a word. (Contributed by AV, 29-Jan-2021.) |
⊢ (𝐹 ∈ Word 𝑆 → (𝐹 ↾ (0..^((♯‘𝐹) − 1))) ∈ Word 𝑆) | ||
Theorem | wrdred1hash 13724 | 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)) | ||
Syntax | clsw 13725 | Extend class notation with the Last Symbol of a word. |
class lastS | ||
Definition | df-lsw 13726 | 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 13727 | 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 13728 | 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 13729 | The last symbol of an empty word does not exist. (Contributed by Alexander van der Vekens, 11-Nov-2018.) |
⊢ (lastS‘∅) = ∅ | ||
Theorem | lsw1 13730 | 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 13731 | 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 13732 | 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 13733 | Syntax for the concatenation operator. |
class ++ | ||
Definition | df-concat 13734* | 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 13735 | 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 13736* | Value of the concatenation operator. (Contributed by Stefan O'Rear, 15-Aug-2015.) |
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑊) → (𝑆 ++ 𝑇) = (𝑥 ∈ (0..^((♯‘𝑆) + (♯‘𝑇))) ↦ if(𝑥 ∈ (0..^(♯‘𝑆)), (𝑆‘𝑥), (𝑇‘(𝑥 − (♯‘𝑆)))))) | ||
Theorem | ccatcl 13737 | 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 13738 | The length of a concatenated word. (Contributed by Stefan O'Rear, 15-Aug-2015.) |
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → (♯‘(𝑆 ++ 𝑇)) = ((♯‘𝑆) + (♯‘𝑇))) | ||
Theorem | ccat0 13739 | The concatenation of two words is empty iff the two words are empty. (Contributed by AV, 4-Mar-2022.) |
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → ((𝑆 ++ 𝑇) = ∅ ↔ (𝑆 = ∅ ∧ 𝑇 = ∅))) | ||
Theorem | ccatval1 13740 | 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.) |
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝐼 ∈ (0..^(♯‘𝑆))) → ((𝑆 ++ 𝑇)‘𝐼) = (𝑆‘𝐼)) | ||
Theorem | ccatval2 13741 | 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 13742 | 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 13743 | 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 13744 | 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 13745 | 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 13746 | 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 13747 | 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 13748 | The first symbol of the right (nonempty) half of a concatenated word. (Contributed by AV, 23-Apr-2022.) |
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝐵 ≠ ∅) → ((𝐴 ++ 𝐵)‘(♯‘𝐴)) = (𝐵‘0)) | ||
Theorem | ccatlid 13749 | 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 13750 | 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 13751 | Associative law for concatenation of words. (Contributed by Stefan O'Rear, 15-Aug-2015.) |
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵) → ((𝑆 ++ 𝑇) ++ 𝑈) = (𝑆 ++ (𝑇 ++ 𝑈))) | ||
Theorem | ccatrn 13752 | The range of a concatenated word. (Contributed by Stefan O'Rear, 15-Aug-2015.) |
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → ran (𝑆 ++ 𝑇) = (ran 𝑆 ∪ ran 𝑇)) | ||
Theorem | ccatidid 13753 | Concatenation of the empty word by the empty word. (Contributed by AV, 26-Mar-2022.) |
⊢ (∅ ++ ∅) = ∅ | ||
Theorem | lswccatn0lsw 13754 | 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 13755 | 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 13756 | 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 13757 | 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 13758 | Syntax for the singleton word constructor. |
class 〈“𝐴”〉 | ||
Definition | df-s1 13759 | 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 13767, and not, as maybe expected, the empty word, see also s1nz 13770. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.) |
⊢ 〈“𝐴”〉 = {〈0, ( I ‘𝐴)〉} | ||
Theorem | ids1 13760 | Identity function protection for a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016.) |
⊢ 〈“𝐴”〉 = 〈“( I ‘𝐴)”〉 | ||
Theorem | s1val 13761 | Value of a singleton word. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.) |
⊢ (𝐴 ∈ 𝑉 → 〈“𝐴”〉 = {〈0, 𝐴〉}) | ||
Theorem | s1rn 13762 | The range of a singleton word. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ (𝐴 ∈ 𝑉 → ran 〈“𝐴”〉 = {𝐴}) | ||
Theorem | s1eq 13763 | Equality theorem for a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016.) |
⊢ (𝐴 = 𝐵 → 〈“𝐴”〉 = 〈“𝐵”〉) | ||
Theorem | s1eqd 13764 | Equality theorem for a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → 〈“𝐴”〉 = 〈“𝐵”〉) | ||
Theorem | s1cl 13765 | 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 13766 | A singleton word is a word. (Contributed by Mario Carneiro, 26-Feb-2016.) |
⊢ (𝜑 → 𝐴 ∈ 𝐵) ⇒ ⊢ (𝜑 → 〈“𝐴”〉 ∈ Word 𝐵) | ||
Theorem | s1prc 13767 | Value of a singleton word if the symbol is a proper class. (Contributed by AV, 26-Mar-2022.) |
⊢ (¬ 𝐴 ∈ V → 〈“𝐴”〉 = 〈“∅”〉) | ||
Theorem | s1cli 13768 | A singleton word is a word. (Contributed by Mario Carneiro, 26-Feb-2016.) |
⊢ 〈“𝐴”〉 ∈ Word V | ||
Theorem | s1len 13769 | Length of a singleton word. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.) |
⊢ (♯‘〈“𝐴”〉) = 1 | ||
Theorem | s1nz 13770 | 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 13771 | The domain of a singleton word is a singleton. (Contributed by AV, 9-Jan-2020.) |
⊢ dom 〈“𝐴”〉 = {0} | ||
Theorem | s1dmALT 13772 | Alternate version of s1dm 13771, 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 13773 | Sole symbol of a singleton word. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.) |
⊢ (𝐴 ∈ 𝐵 → (〈“𝐴”〉‘0) = 𝐴) | ||
Theorem | lsws1 13774 | The last symbol of a singleton word is its symbol. (Contributed by AV, 22-Oct-2018.) |
⊢ (𝐴 ∈ 𝑉 → (lastS‘〈“𝐴”〉) = 𝐴) | ||
Theorem | eqs1 13775 | 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 13776* | A word of length 1 is a singleton word. (Contributed by AV, 24-Jan-2021.) |
⊢ ((𝑊 ∈ Word 𝑆 ∧ (♯‘𝑊) = 1) → ∃𝑠 ∈ 𝑆 𝑊 = 〈“𝑠”〉) | ||
Theorem | wrdl1s1 13777 | 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 13778 | The singleton word function is injective. (Contributed by Mario Carneiro, 1-Oct-2015.) (Revised by Mario Carneiro, 26-Feb-2016.) |
⊢ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) → (〈“𝑆”〉 = 〈“𝑇”〉 ↔ 𝑆 = 𝑇)) | ||
Theorem | ccatws1cl 13779 | 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 13780 | 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 13781 | The concatenation of two singleton words is a word. (Contributed by Alexander van der Vekens, 22-Sep-2018.) |
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (〈“𝑋”〉 ++ 〈“𝑌”〉) ∈ Word 𝑉) | ||
Theorem | ccats1alpha 13782 | 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 13783 | 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 13784 | 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 13785 | 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 13786 | The length of the concatenation of two singleton words. (Contributed by Alexander van der Vekens, 22-Sep-2018.) |
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (♯‘(〈“𝑋”〉 ++ 〈“𝑌”〉)) = 2) | ||
Theorem | ccatw2s1cl 13787 | 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 13788 | 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 13789 | 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.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑆 ∈ 𝑉 ∧ 𝐼 ∈ (0..^(♯‘𝑊))) → ((𝑊 ++ 〈“𝑆”〉)‘𝐼) = (𝑊‘𝐼)) | ||
Theorem | ccats1val2 13790 | 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 13791 | 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 13792 | Extract the first of two concatenated singleton words. (Contributed by Alexander van der Vekens, 22-Sep-2018.) |
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → ((〈“𝑋”〉 ++ 〈“𝑌”〉)‘0) = 𝑋) | ||
Theorem | ccat2s1p2 13793 | Extract the second of two concatenated singleton words. (Contributed by Alexander van der Vekens, 22-Sep-2018.) |
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → ((〈“𝑋”〉 ++ 〈“𝑌”〉)‘1) = 𝑌) | ||
Theorem | ccatw2s1ass 13794 | Associative law for a concatenation of a word with two singleton words. (Contributed by Alexander van der Vekens, 22-Sep-2018.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → ((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉) = (𝑊 ++ (〈“𝑋”〉 ++ 〈“𝑌”〉))) | ||
Theorem | ccatws1n0 13795 | 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 13796 | 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 13797 | 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 13798 | 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 13799 | 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.) |
⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = 𝑁) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘𝑁) = 𝑋) | ||
Theorem | ccatw2s1p2 13800 | 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)) = 𝑌) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |