HomeTheorem List (p. 134 of 426)
GIF version.
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List
| Home |
Metamath
Proof Explorer Theorem List (p. 134 of 426) | < 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: | Metamath Proof Explorer
(1-27775) |
Hilbert Space Explorer
(27776-29300) |
Users' Mathboxes
(29301-42551) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Definition | df-concat 13301* | 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..^(#‘𝑠)), (𝑠‘𝑥), (𝑡‘(𝑥 − (#‘𝑠)))))) | ||
| Definition | df-s1 13302 | Define the canonical injection from symbols to words. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.) |
| ⊢ ⟨“𝐴”⟩ = {⟨0, ( I ‘𝐴)⟩} | ||
| Definition | df-substr 13303* | Define an operation which extracts portions 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 ‘𝑏)))), ∅)) | ||
| Definition | df-splice 13304* | Define an operation which replaces portions of words. (Contributed by Stefan O'Rear, 15-Aug-2015.) |
| ⊢ splice = (𝑠 ∈ V, 𝑏 ∈ V ↦ (((𝑠 substr ⟨0, (1st ‘(1st ‘𝑏))⟩) ++ (2nd ‘𝑏)) ++ (𝑠 substr ⟨(2nd ‘(1st ‘𝑏)), (#‘𝑠)⟩))) | ||
| Definition | df-reverse 13305* | Define an operation which reverses the order of symbols in a word. (Contributed by Stefan O'Rear, 26-Aug-2015.) |
| ⊢ reverse = (𝑠 ∈ V ↦ (𝑥 ∈ (0..^(#‘𝑠)) ↦ (𝑠‘(((#‘𝑠) − 1) − 𝑥)))) | ||
| Definition | df-reps 13306* | Definition to construct a word consisting of one repeated symbol, often called "repeated symbol word" for short in the following. (Contributed by Alexander van der Vekens, 4-Nov-2018.) |
| ⊢ repeatS = (𝑠 ∈ V, 𝑛 ∈ ℕ0 ↦ (𝑥 ∈ (0..^𝑛) ↦ 𝑠)) | ||
| Theorem | iswrd 13307* | Property of being a word over a set with a 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 13308* | 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 (𝑆 ↑𝑚 (0..^𝑙))) | ||
| Theorem | iswrdi 13309 | 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 13310 | A word is a zero-based sequence with a recoverable upper limit. (Contributed by Stefan O'Rear, 15-Aug-2015.) |
| ⊢ (𝑊 ∈ Word 𝑆 → 𝑊:(0..^(#‘𝑊))⟶𝑆) | ||
| Theorem | iswrdb 13311 | A word over an alphabet is a function of 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 13312 | 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 13313 | 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 13314 | 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 13315 | The set of words over a set is a set. (Contributed by Mario Carneiro, 26-Feb-2016.) |
| ⊢ (𝑆 ∈ 𝑉 → Word 𝑆 ∈ V) | ||
| Theorem | wrdexb 13316 | 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 13317 | The set of words over a set is a set, inference form. (Contributed by AV, 23-May-2021.) |
| ⊢ 𝑆 ∈ V ⇒ ⊢ Word 𝑆 ∈ V | ||
| Theorem | wrdsymbcl 13318 | 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 13319 | 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 13320 | A word over an alphabet is a word over the universal class. (Contributed by AV, 8-Feb-2021.) |
| ⊢ (𝑊 ∈ Word 𝑉 → 𝑊 ∈ Word V) | ||
| Theorem | wrdlndm 13321 | The length of a word is not in the domain of the word (regarded as function). (Contributed by AV, 3-Mar-2021.) |
| ⊢ (𝑊 ∈ Word 𝑉 → (#‘𝑊) ∉ dom 𝑊) | ||
| Theorem | iswrdsymb 13322* | 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 13323 | 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 13324 | 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 13325 | The length of a nonempty word is a positive integer. (Contributed by Mario Carneiro, 1-Oct-2015.) |
| ⊢ ((𝑊 ∈ Word 𝑆 ∧ 𝑊 ≠ ∅) → (#‘𝑊) ∈ ℕ) | ||
| Theorem | wrdffz 13326 | A word is a function from a finite interval of integers. (Contributed by AV, 10-Feb-2021.) |
| ⊢ (𝑊 ∈ Word 𝑆 → 𝑊:(0...((#‘𝑊) − 1))⟶𝑆) | ||
| Theorem | wrdeq 13327 | Equality theorem for the set of words. (Contributed by Mario Carneiro, 26-Feb-2016.) |
| ⊢ (𝑆 = 𝑇 → Word 𝑆 = Word 𝑇) | ||
| Theorem | wrdeqi 13328 | Equality theorem for the set of words, inference form. (Contributed by AV, 23-May-2021.) |
| ⊢ 𝑆 = 𝑇 ⇒ ⊢ Word 𝑆 = Word 𝑇 | ||
| Theorem | iswrddm0 13329 | A function with empty domain is a word. (Contributed by AV, 13-Oct-2018.) |
| ⊢ (𝑊:∅⟶𝑆 → 𝑊 ∈ Word 𝑆) | ||
| Theorem | wrd0 13330 | 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 13331 | The empty word is the only word over an empty alphabet. (Contributed by AV, 25-Oct-2018.) |
| ⊢ (𝑊 ∈ Word ∅ ↔ 𝑊 = ∅) | ||
| Theorem | ffz0iswrd 13332 | A sequence with zero-based indices is a word. (Contributed by AV, 31-Jan-2018.) (Proof shortened by AV, 13-Oct-2018.) |
| ⊢ (𝑊:(0...𝐿)⟶𝑆 → 𝑊 ∈ Word 𝑆) | ||
| Theorem | nfwrd 13333 | Hypothesis builder for Word 𝑆. (Contributed by Mario Carneiro, 26-Feb-2016.) |
| ⊢ Ⅎ𝑥𝑆 ⇒ ⊢ Ⅎ𝑥Word 𝑆 | ||
| Theorem | csbwrdg 13334* | Class substitution for the symbols of a word. (Contributed by Alexander van der Vekens, 15-Jul-2018.) |
| ⊢ (𝑆 ∈ 𝑉 → ⦋𝑆 / 𝑥⦌Word 𝑥 = Word 𝑆) | ||
| Theorem | wrdnval 13335* | 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 13336 | Words as a mapping. (Contributed by Thierry Arnoux, 4-Mar-2020.) |
| ⊢ ((𝑉 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0) → ((𝑊 ∈ Word 𝑉 ∧ (#‘𝑊) = 𝑁) ↔ 𝑊 ∈ (𝑉 ↑𝑚 (0..^𝑁)))) | ||
| Theorem | hashwrdn 13337* | 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 13338* | 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.) |
| ⊢ ((𝑉 ∈ Fin ∧ 𝑁 ∈ ℕ0) → {𝑤 ∈ Word 𝑉 ∣ (#‘𝑤) = 𝑁} ∈ Fin) | ||
| Theorem | wrdsymb0 13339 | 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 13340 | A word with length at least 1 is not empty. (Contributed by AV, 14-Oct-2018.) |
| ⊢ (𝑊 ∈ Word 𝑉 → (𝑊 ≠ ∅ ↔ 1 ≤ (#‘𝑊))) | ||
| Theorem | wrdlenge2n0 13341 | 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 13342 | 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 13343* | 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 13344 | 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 13345 | 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 13346* | 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 | elovmpt2wrd 13347* | 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 13348* | 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 13349 | A word truncated by a symbol is a word. (Contributed by AV, 29-Jan-2021.) |
| ⊢ (𝐹 ∈ Word 𝑆 → (𝐹 ↾ (0..^((#‘𝐹) − 1))) ∈ Word 𝑆) | ||
| Theorem | wrdred1hash 13350 | 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)) | ||
| Theorem | lsw 13351 | 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 13352 | 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 13353 | The last symbol of an empty word does not exist. (Contributed by Alexander van der Vekens, 11-Nov-2018.) |
| ⊢ ( lastS ‘∅) = ∅ | ||
| Theorem | lsw1 13354 | 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 13355 | 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 13356 | 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 ‘𝑊) ∈ 𝑉) | ||
| Theorem | ccatfn 13357 | 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 13358* | Value of the concatenation operator. (Contributed by Stefan O'Rear, 15-Aug-2015.) |
| ⊢ ((𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑊) → (𝑆 ++ 𝑇) = (𝑥 ∈ (0..^((#‘𝑆) + (#‘𝑇))) ↦ if(𝑥 ∈ (0..^(#‘𝑆)), (𝑆‘𝑥), (𝑇‘(𝑥 − (#‘𝑆)))))) | ||
| Theorem | ccatcl 13359 | 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 13360 | The length of a concatenated word. (Contributed by Stefan O'Rear, 15-Aug-2015.) |
| ⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → (#‘(𝑆 ++ 𝑇)) = ((#‘𝑆) + (#‘𝑇))) | ||
| Theorem | ccatval1 13361 | 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 13362 | 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 13363 | 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 13364 | 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 13365 | 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 13366 | 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 13367 | 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 13368 | 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 | ccatlid 13369 | 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 13370 | 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 13371 | Associative law for concatenation of words. (Contributed by Stefan O'Rear, 15-Aug-2015.) |
| ⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵) → ((𝑆 ++ 𝑇) ++ 𝑈) = (𝑆 ++ (𝑇 ++ 𝑈))) | ||
| Theorem | ccatrn 13372 | The range of a concatenated word. (Contributed by Stefan O'Rear, 15-Aug-2015.) |
| ⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → ran (𝑆 ++ 𝑇) = (ran 𝑆 ∪ ran 𝑇)) | ||
| Theorem | lswccatn0lsw 13373 | 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 13374 | 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 13375 | 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 13376 | 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 𝑆) | ||
| Theorem | ids1 13377 | Identity function protection for a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016.) |
| ⊢ ⟨“𝐴”⟩ = ⟨“( I ‘𝐴)”⟩ | ||
| Theorem | s1val 13378 | Value of a single-symbol word. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.) |
| ⊢ (𝐴 ∈ 𝑉 → ⟨“𝐴”⟩ = {⟨0, 𝐴⟩}) | ||
| Theorem | s1rn 13379 | The range of a single-symbol word. (Contributed by Mario Carneiro, 18-Jul-2016.) |
| ⊢ (𝐴 ∈ 𝑉 → ran ⟨“𝐴”⟩ = {𝐴}) | ||
| Theorem | s1eq 13380 | Equality theorem for a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016.) |
| ⊢ (𝐴 = 𝐵 → ⟨“𝐴”⟩ = ⟨“𝐵”⟩) | ||
| Theorem | s1eqd 13381 | Equality theorem for a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016.) |
| ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → ⟨“𝐴”⟩ = ⟨“𝐵”⟩) | ||
| Theorem | s1cl 13382 | 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 13383 | A singleton word is a word. (Contributed by Mario Carneiro, 26-Feb-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ 𝐵) ⇒ ⊢ (𝜑 → ⟨“𝐴”⟩ ∈ Word 𝐵) | ||
| Theorem | s1cli 13384 | A singleton word is a word. (Contributed by Mario Carneiro, 26-Feb-2016.) |
| ⊢ ⟨“𝐴”⟩ ∈ Word V | ||
| Theorem | s1len 13385 | Length of a singleton word. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.) |
| ⊢ (#‘⟨“𝐴”⟩) = 1 | ||
| Theorem | s1nz 13386 | A singleton word is not the empty string. (Contributed by Mario Carneiro, 27-Feb-2016.) (Proof shortened by Kyle Wyonch, 18-Jul-2021.) |
| ⊢ ⟨“𝐴”⟩ ≠ ∅ | ||
| Theorem | s1nzOLD 13387 | Obsolete proof of s1nz 13386 as of 18-Jul-2021. A singleton word is not the empty string. (Contributed by Mario Carneiro, 27-Feb-2016.) (New usage is discouraged.) (Proof modification is discouraged.) |
| ⊢ ⟨“𝐴”⟩ ≠ ∅ | ||
| Theorem | s1dm 13388 | The domain of a singleton word is a singleton. (Contributed by AV, 9-Jan-2020.) |
| ⊢ dom ⟨“𝐴”⟩ = {0} | ||
| Theorem | s1dmALT 13389 | Alternate version of s1dm 13388, having a shorter proof, but requiring that 𝐴 ia a set. (Contributed by AV, 9-Jan-2020.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (𝐴 ∈ 𝑆 → dom ⟨“𝐴”⟩ = {0}) | ||
| Theorem | s1fv 13390 | Sole symbol of a singleton word. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.) |
| ⊢ (𝐴 ∈ 𝐵 → (⟨“𝐴”⟩‘0) = 𝐴) | ||
| Theorem | lsws1 13391 | The last symbol of a singleton word is its symbol. (Contributed by AV, 22-Oct-2018.) |
| ⊢ (𝐴 ∈ 𝑉 → ( lastS ‘⟨“𝐴”⟩) = 𝐴) | ||
| Theorem | eqs1 13392 | 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 13393* | A word of length 1 is a singleton word. (Contributed by AV, 24-Jan-2021.) |
| ⊢ ((𝑊 ∈ Word 𝑆 ∧ (#‘𝑊) = 1) → ∃𝑠 ∈ 𝑆 𝑊 = ⟨“𝑠”⟩) | ||
| Theorem | wrdl1s1 13394 | 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 13395 | The singleton word function is injective. (Contributed by Mario Carneiro, 1-Oct-2015.) (Revised by Mario Carneiro, 26-Feb-2016.) |
| ⊢ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) → (⟨“𝑆”⟩ = ⟨“𝑇”⟩ ↔ 𝑆 = 𝑇)) | ||
| Theorem | ccatws1cl 13396 | The concatenation of a word with a singleton word is a word. (Contributed by Alexander van der Vekens, 22-Sep-2018.) |
| ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑋 ∈ 𝑉) → (𝑊 ++ ⟨“𝑋”⟩) ∈ Word 𝑉) | ||
| Theorem | ccat2s1cl 13397 | The concatenation of two singleton words is a word. (Contributed by Alexander van der Vekens, 22-Sep-2018.) |
| ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (⟨“𝑋”⟩ ++ ⟨“𝑌”⟩) ∈ Word 𝑉) | ||
| Theorem | ccatws1len 13398 | The length of the concatenation of a word with a singleton word. (Contributed by Alexander van der Vekens, 22-Sep-2018.) |
| ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑋 ∈ 𝑉) → (#‘(𝑊 ++ ⟨“𝑋”⟩)) = ((#‘𝑊) + 1)) | ||
| Theorem | wrdlenccats1lenm1 13399 | The length of a word is the length of the word concatenated with a singleton word minus 1. (Contributed by AV, 28-Jun-2018.) (Proof shortened by AV, 1-May-2020.) |
| ⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑆 ∈ 𝑉) → (#‘𝑊) = ((#‘(𝑊 ++ ⟨“𝑆”⟩)) − 1)) | ||
| Theorem | ccat2s1len 13400 | The length of the concatenation of two singleton words. (Contributed by Alexander van der Vekens, 22-Sep-2018.) |
| ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (#‘(⟨“𝑋”⟩ ++ ⟨“𝑌”⟩)) = 2) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |