Home | Metamath
Proof Explorer Theorem List (p. 135 of 424) | < 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-27159) |
Hilbert Space Explorer
(27160-28684) |
Users' Mathboxes
(28685-42360) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | cshwidxmodr 13401 | The symbol at a given index of a cyclically shifted nonempty word is the symbol at the shifted index of the original word. (Contributed by AV, 17-Mar-2021.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ∧ 𝐼 ∈ (0..^(#‘𝑊))) → ((𝑊 cyclShift 𝑁)‘((𝐼 − 𝑁) mod (#‘𝑊))) = (𝑊‘𝐼)) | ||
Theorem | cshwidx0mod 13402 | The symbol at index 0 of a cyclically shifted nonempty word is the symbol at index N (modulo the length of the word) of the original word. (Contributed by AV, 30-Oct-2018.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ∧ 𝑁 ∈ ℤ) → ((𝑊 cyclShift 𝑁)‘0) = (𝑊‘(𝑁 mod (#‘𝑊)))) | ||
Theorem | cshwidx0 13403 | The symbol at index 0 of a cyclically shifted nonempty word is the symbol at index N of the original word. (Contributed by AV, 15-May-2018.) (Revised by AV, 21-May-2018.) (Revised by AV, 30-Oct-2018.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0..^(#‘𝑊))) → ((𝑊 cyclShift 𝑁)‘0) = (𝑊‘𝑁)) | ||
Theorem | cshwidxm1 13404 | The symbol at index ((n-N)-1) of a word of length n (not 0) cyclically shifted by N positions is the symbol at index (n-1) of the original word. (Contributed by AV, 23-May-2018.) (Revised by AV, 21-May-2018.) (Revised by AV, 30-Oct-2018.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0..^(#‘𝑊))) → ((𝑊 cyclShift 𝑁)‘(((#‘𝑊) − 𝑁) − 1)) = (𝑊‘((#‘𝑊) − 1))) | ||
Theorem | cshwidxm 13405 | The symbol at index (n-N) of a word of length n (not 0) cyclically shifted by N positions (not 0) is the symbol at index 0 of the original word. (Contributed by AV, 18-May-2018.) (Revised by AV, 21-May-2018.) (Revised by AV, 30-Oct-2018.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (1...(#‘𝑊))) → ((𝑊 cyclShift 𝑁)‘((#‘𝑊) − 𝑁)) = (𝑊‘0)) | ||
Theorem | cshwidxn 13406 | The symbol at index (n-1) of a word of length n (not 0) cyclically shifted by N positions (not 0) is the symbol at index (N-1) of the original word. (Contributed by AV, 18-May-2018.) (Revised by AV, 21-May-2018.) (Revised by AV, 30-Oct-2018.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (1...(#‘𝑊))) → ((𝑊 cyclShift 𝑁)‘((#‘𝑊) − 1)) = (𝑊‘(𝑁 − 1))) | ||
Theorem | cshf1 13407 | Cyclically shifting a word which contains a symbol at most once results in a word which contains a symbol at most once. (Contributed by AV, 14-Mar-2021.) |
⊢ ((𝐹:(0..^(#‘𝐹))–1-1→𝐴 ∧ 𝑆 ∈ ℤ ∧ 𝐺 = (𝐹 cyclShift 𝑆)) → 𝐺:(0..^(#‘𝐹))–1-1→𝐴) | ||
Theorem | cshinj 13408 | If a word is injectiv (regarded as function), the cyclically shifted word is also injective. (Contributed by AV, 14-Mar-2021.) |
⊢ ((𝐹 ∈ Word 𝐴 ∧ Fun ◡𝐹 ∧ 𝑆 ∈ ℤ) → (𝐺 = (𝐹 cyclShift 𝑆) → Fun ◡𝐺)) | ||
Theorem | repswcshw 13409 | A cyclically shifted "repeated symbol word". (Contributed by Alexander van der Vekens, 7-Nov-2018.) |
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ 𝐼 ∈ ℤ) → ((𝑆 repeatS 𝑁) cyclShift 𝐼) = (𝑆 repeatS 𝑁)) | ||
Theorem | 2cshw 13410 | Cyclically shifting a word two times. (Contributed by AV, 7-Apr-2018.) (Revised by AV, 4-Jun-2018.) (Revised by AV, 31-Oct-2018.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑊 cyclShift 𝑀) cyclShift 𝑁) = (𝑊 cyclShift (𝑀 + 𝑁))) | ||
Theorem | 2cshwid 13411 | Cyclically shifting a word two times resulting in the word itself. (Contributed by AV, 7-Apr-2018.) (Revised by AV, 5-Jun-2018.) (Revised by AV, 1-Nov-2018.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ) → ((𝑊 cyclShift 𝑁) cyclShift ((#‘𝑊) − 𝑁)) = 𝑊) | ||
Theorem | lswcshw 13412 | The last symbol of a word cyclically shifted by N positions is the symbol at index (N-1) of the original word. (Contributed by AV, 21-Mar-2018.) (Revised by AV, 5-Jun-2018.) (Revised by AV, 1-Nov-2018.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (1...(#‘𝑊))) → ( lastS ‘(𝑊 cyclShift 𝑁)) = (𝑊‘(𝑁 − 1))) | ||
Theorem | 2cshwcom 13413 | Cyclically shifting a word two times is commutative. (Contributed by AV, 21-Apr-2018.) (Revised by AV, 5-Jun-2018.) (Revised by Mario Carneiro/AV, 1-Nov-2018.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((𝑊 cyclShift 𝑁) cyclShift 𝑀) = ((𝑊 cyclShift 𝑀) cyclShift 𝑁)) | ||
Theorem | cshwleneq 13414 | If the results of cyclically shifting two words are equal, the length of the two words was equal. (Contributed by AV, 21-Apr-2018.) (Revised by AV, 5-Jun-2018.) (Revised by AV, 1-Nov-2018.) |
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ) ∧ (𝑊 cyclShift 𝑁) = (𝑈 cyclShift 𝑀)) → (#‘𝑊) = (#‘𝑈)) | ||
Theorem | 3cshw 13415 | Cyclically shifting a word three times results in a once cyclically shifted word under certain circumstances. (Contributed by AV, 6-Jun-2018.) (Revised by AV, 1-Nov-2018.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑊 cyclShift 𝑁) = (((𝑊 cyclShift 𝑀) cyclShift 𝑁) cyclShift ((#‘𝑊) − 𝑀))) | ||
Theorem | cshweqdif2 13416 | If cyclically shifting two words (of the same length) results in the same word, cyclically shifting one of the words by the difference of the numbers of shifts results in the other word. (Contributed by AV, 21-Apr-2018.) (Revised by AV, 6-Jun-2018.) (Revised by AV, 1-Nov-2018.) |
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ)) → ((𝑊 cyclShift 𝑁) = (𝑈 cyclShift 𝑀) → (𝑈 cyclShift (𝑀 − 𝑁)) = 𝑊)) | ||
Theorem | cshweqdifid 13417 | If cyclically shifting a word by two positions results in the same word, cyclically shifting the word by the difference of these two positions results in the original word itself. (Contributed by AV, 21-Apr-2018.) (Revised by AV, 7-Jun-2018.) (Revised by AV, 1-Nov-2018.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((𝑊 cyclShift 𝑁) = (𝑊 cyclShift 𝑀) → (𝑊 cyclShift (𝑀 − 𝑁)) = 𝑊)) | ||
Theorem | cshweqrep 13418* | If cyclically shifting a word by L position results in the word itself, the symbol at any position is repeated at multiples of L (modulo the length of the word) positions in the word. (Contributed by AV, 13-May-2018.) (Revised by AV, 7-Jun-2018.) (Revised by AV, 1-Nov-2018.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ ℤ) → (((𝑊 cyclShift 𝐿) = 𝑊 ∧ 𝐼 ∈ (0..^(#‘𝑊))) → ∀𝑗 ∈ ℕ0 (𝑊‘𝐼) = (𝑊‘((𝐼 + (𝑗 · 𝐿)) mod (#‘𝑊))))) | ||
Theorem | cshw1 13419* | If cyclically shifting a word by 1 position results in the word itself, the word is build of identical symbols. Remark: also "valid" for an empty word! (Contributed by AV, 13-May-2018.) (Revised by AV, 7-Jun-2018.) (Proof shortened by AV, 1-Nov-2018.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ (𝑊 cyclShift 1) = 𝑊) → ∀𝑖 ∈ (0..^(#‘𝑊))(𝑊‘𝑖) = (𝑊‘0)) | ||
Theorem | cshw1repsw 13420 | If cyclically shifting a word by 1 position results in the word itself, the word is a "repeated symbol word". Remark: also "valid" for an empty word! (Contributed by AV, 8-Nov-2018.) (Proof shortened by AV, 10-Nov-2018.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ (𝑊 cyclShift 1) = 𝑊) → 𝑊 = ((𝑊‘0) repeatS (#‘𝑊))) | ||
Theorem | cshwsexa 13421* | The class of (different!) words resulting by cyclically shifting something (not necessarily a word) is a set. (Contributed by AV, 8-Jun-2018.) (Revised by Mario Carneiro/AV, 25-Oct-2018.) |
⊢ {𝑤 ∈ Word 𝑉 ∣ ∃𝑛 ∈ (0..^(#‘𝑊))(𝑊 cyclShift 𝑛) = 𝑤} ∈ V | ||
Theorem | 2cshwcshw 13422* | If a word is a cyclically shifted word, and a second word is the result of cyclically shifting the same word, then the second word is the result of cyclically shifting the first word. (Contributed by AV, 11-May-2018.) (Revised by AV, 12-Jun-2018.) (Proof shortened by AV, 3-Nov-2018.) |
⊢ ((𝑌 ∈ Word 𝑉 ∧ (#‘𝑌) = 𝑁) → ((𝐾 ∈ (0...𝑁) ∧ 𝑋 = (𝑌 cyclShift 𝐾) ∧ ∃𝑚 ∈ (0...𝑁)𝑍 = (𝑌 cyclShift 𝑚)) → ∃𝑛 ∈ (0...𝑁)𝑍 = (𝑋 cyclShift 𝑛))) | ||
Theorem | scshwfzeqfzo 13423* | For a nonempty word the sets of shifted words, expressd by a finite interval of integers or by a half-open integer range are identical. (Contributed by Alexander van der Vekens, 15-Jun-2018.) |
⊢ ((𝑋 ∈ Word 𝑉 ∧ 𝑋 ≠ ∅ ∧ 𝑁 = (#‘𝑋)) → {𝑦 ∈ Word 𝑉 ∣ ∃𝑛 ∈ (0...𝑁)𝑦 = (𝑋 cyclShift 𝑛)} = {𝑦 ∈ Word 𝑉 ∣ ∃𝑛 ∈ (0..^𝑁)𝑦 = (𝑋 cyclShift 𝑛)}) | ||
Theorem | cshwcshid 13424* | A cyclically shifted word can be reconstructed by cyclically shifting it again. Lemma for erclwwlktr 26343 and erclwwlkntr 26355. (Contributed by AV, 8-Apr-2018.) (Revised by AV, 11-Jun-2018.) (Proof shortened by AV, 3-Nov-2018.) |
⊢ (𝜑 → 𝑦 ∈ Word 𝑉) & ⊢ (𝜑 → (#‘𝑥) = (#‘𝑦)) ⇒ ⊢ (𝜑 → ((𝑚 ∈ (0...(#‘𝑦)) ∧ 𝑥 = (𝑦 cyclShift 𝑚)) → ∃𝑛 ∈ (0...(#‘𝑥))𝑦 = (𝑥 cyclShift 𝑛))) | ||
Theorem | cshwcsh2id 13425* | A cyclically shifted word can be reconstructed by cyclically shifting it again twice. Lemma for erclwwlktr 26343 and erclwwlkntr 26355. (Contributed by AV, 9-Apr-2018.) (Revised by AV, 11-Jun-2018.) (Proof shortened by AV, 3-Nov-2018.) |
⊢ (𝜑 → 𝑧 ∈ Word 𝑉) & ⊢ (𝜑 → ((#‘𝑦) = (#‘𝑧) ∧ (#‘𝑥) = (#‘𝑦))) ⇒ ⊢ (𝜑 → (((𝑚 ∈ (0...(#‘𝑦)) ∧ 𝑥 = (𝑦 cyclShift 𝑚)) ∧ (𝑘 ∈ (0...(#‘𝑧)) ∧ 𝑦 = (𝑧 cyclShift 𝑘))) → ∃𝑛 ∈ (0...(#‘𝑧))𝑥 = (𝑧 cyclShift 𝑛))) | ||
Theorem | cshimadifsn 13426 | The image of a cyclically shifted word under its domain without its left bound is the image of a cyclically shifted word under its domain without the number of shifted symbols. (Contributed by AV, 19-Mar-2021.) |
⊢ ((𝐹 ∈ Word 𝑆 ∧ 𝑁 = (#‘𝐹) ∧ 𝐽 ∈ (0..^𝑁)) → (𝐹 “ ((0..^𝑁) ∖ {𝐽})) = ((𝐹 cyclShift 𝐽) “ (1..^𝑁))) | ||
Theorem | cshimadifsn0 13427 | The image of a cyclically shifted word under its domain without its upper bound is the image of a cyclically shifted word under its domain without the number of shifted symbols. (Contributed by AV, 19-Mar-2021.) |
⊢ ((𝐹 ∈ Word 𝑆 ∧ 𝑁 = (#‘𝐹) ∧ 𝐽 ∈ (0..^𝑁)) → (𝐹 “ ((0..^𝑁) ∖ {𝐽})) = ((𝐹 cyclShift (𝐽 + 1)) “ (0..^(𝑁 − 1)))) | ||
Theorem | wrdco 13428 | Mapping a word by a function. (Contributed by Stefan O'Rear, 27-Aug-2015.) |
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (𝐹 ∘ 𝑊) ∈ Word 𝐵) | ||
Theorem | lenco 13429 | Length of a mapped word is unchanged. (Contributed by Stefan O'Rear, 27-Aug-2015.) |
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (#‘(𝐹 ∘ 𝑊)) = (#‘𝑊)) | ||
Theorem | s1co 13430 | Mapping of a singleton word. (Contributed by Mario Carneiro, 27-Sep-2015.) (Revised by Mario Carneiro, 26-Feb-2016.) |
⊢ ((𝑆 ∈ 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (𝐹 ∘ 〈“𝑆”〉) = 〈“(𝐹‘𝑆)”〉) | ||
Theorem | revco 13431 | Mapping of words commutes with reversal. (Contributed by Stefan O'Rear, 27-Aug-2015.) |
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (𝐹 ∘ (reverse‘𝑊)) = (reverse‘(𝐹 ∘ 𝑊))) | ||
Theorem | ccatco 13432 | Mapping of words commutes with concatenation. (Contributed by Stefan O'Rear, 27-Aug-2015.) |
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐴 ∧ 𝐹:𝐴⟶𝐵) → (𝐹 ∘ (𝑆 ++ 𝑇)) = ((𝐹 ∘ 𝑆) ++ (𝐹 ∘ 𝑇))) | ||
Theorem | cshco 13433 | Mapping of words commutes with the "cyclical shift" operation. (Contributed by AV, 12-Nov-2018.) |
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝑁 ∈ ℤ ∧ 𝐹:𝐴⟶𝐵) → (𝐹 ∘ (𝑊 cyclShift 𝑁)) = ((𝐹 ∘ 𝑊) cyclShift 𝑁)) | ||
Theorem | swrdco 13434 | Mapping of words commutes with the substring operation. (Contributed by AV, 11-Nov-2018.) |
⊢ ((𝑊 ∈ Word 𝐴 ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(#‘𝑊))) ∧ 𝐹:𝐴⟶𝐵) → (𝐹 ∘ (𝑊 substr 〈𝑀, 𝑁〉)) = ((𝐹 ∘ 𝑊) substr 〈𝑀, 𝑁〉)) | ||
Theorem | lswco 13435 | Mapping of (nonempty) words commutes with the "last symbol" operation. This theorem would not hold if 𝑊 = ∅, (𝐹‘∅) ≠ ∅ and ∅ ∈ 𝐴, because then ( lastS ‘(𝐹 ∘ 𝑊)) = ( lastS ‘∅) = ∅ ≠ (𝐹‘∅) = (𝐹( lastS ‘𝑊)). (Contributed by AV, 11-Nov-2018.) |
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝑊 ≠ ∅ ∧ 𝐹:𝐴⟶𝐵) → ( lastS ‘(𝐹 ∘ 𝑊)) = (𝐹‘( lastS ‘𝑊))) | ||
Theorem | repsco 13436 | Mapping of words commutes with the "repeated symbol" operation. (Contributed by AV, 11-Nov-2018.) |
⊢ ((𝑆 ∈ 𝐴 ∧ 𝑁 ∈ ℕ0 ∧ 𝐹:𝐴⟶𝐵) → (𝐹 ∘ (𝑆 repeatS 𝑁)) = ((𝐹‘𝑆) repeatS 𝑁)) | ||
Syntax | cs2 13437 | Syntax for the length 2 word constructor. |
class 〈“𝐴𝐵”〉 | ||
Syntax | cs3 13438 | Syntax for the length 3 word constructor. |
class 〈“𝐴𝐵𝐶”〉 | ||
Syntax | cs4 13439 | Syntax for the length 4 word constructor. |
class 〈“𝐴𝐵𝐶𝐷”〉 | ||
Syntax | cs5 13440 | Syntax for the length 5 word constructor. |
class 〈“𝐴𝐵𝐶𝐷𝐸”〉 | ||
Syntax | cs6 13441 | Syntax for the length 6 word constructor. |
class 〈“𝐴𝐵𝐶𝐷𝐸𝐹”〉 | ||
Syntax | cs7 13442 | Syntax for the length 7 word constructor. |
class 〈“𝐴𝐵𝐶𝐷𝐸𝐹𝐺”〉 | ||
Syntax | cs8 13443 | Syntax for the length 8 word constructor. |
class 〈“𝐴𝐵𝐶𝐷𝐸𝐹𝐺𝐻”〉 | ||
Definition | df-s2 13444 | Define the length 2 word constructor. (Contributed by Mario Carneiro, 26-Feb-2016.) |
⊢ 〈“𝐴𝐵”〉 = (〈“𝐴”〉 ++ 〈“𝐵”〉) | ||
Definition | df-s3 13445 | Define the length 3 word constructor. (Contributed by Mario Carneiro, 26-Feb-2016.) |
⊢ 〈“𝐴𝐵𝐶”〉 = (〈“𝐴𝐵”〉 ++ 〈“𝐶”〉) | ||
Definition | df-s4 13446 | Define the length 4 word constructor. (Contributed by Mario Carneiro, 26-Feb-2016.) |
⊢ 〈“𝐴𝐵𝐶𝐷”〉 = (〈“𝐴𝐵𝐶”〉 ++ 〈“𝐷”〉) | ||
Definition | df-s5 13447 | Define the length 5 word constructor. (Contributed by Mario Carneiro, 26-Feb-2016.) |
⊢ 〈“𝐴𝐵𝐶𝐷𝐸”〉 = (〈“𝐴𝐵𝐶𝐷”〉 ++ 〈“𝐸”〉) | ||
Definition | df-s6 13448 | Define the length 6 word constructor. (Contributed by Mario Carneiro, 26-Feb-2016.) |
⊢ 〈“𝐴𝐵𝐶𝐷𝐸𝐹”〉 = (〈“𝐴𝐵𝐶𝐷𝐸”〉 ++ 〈“𝐹”〉) | ||
Definition | df-s7 13449 | Define the length 7 word constructor. (Contributed by Mario Carneiro, 26-Feb-2016.) |
⊢ 〈“𝐴𝐵𝐶𝐷𝐸𝐹𝐺”〉 = (〈“𝐴𝐵𝐶𝐷𝐸𝐹”〉 ++ 〈“𝐺”〉) | ||
Definition | df-s8 13450 | Define the length 8 word constructor. (Contributed by Mario Carneiro, 26-Feb-2016.) |
⊢ 〈“𝐴𝐵𝐶𝐷𝐸𝐹𝐺𝐻”〉 = (〈“𝐴𝐵𝐶𝐷𝐸𝐹𝐺”〉 ++ 〈“𝐻”〉) | ||
Theorem | cats1cld 13451 | Closure of concatenation with a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016.) |
⊢ 𝑇 = (𝑆 ++ 〈“𝑋”〉) & ⊢ (𝜑 → 𝑆 ∈ Word 𝐴) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) ⇒ ⊢ (𝜑 → 𝑇 ∈ Word 𝐴) | ||
Theorem | cats1co 13452 | Closure of concatenation with a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016.) |
⊢ 𝑇 = (𝑆 ++ 〈“𝑋”〉) & ⊢ (𝜑 → 𝑆 ∈ Word 𝐴) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) & ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → (𝐹 ∘ 𝑆) = 𝑈) & ⊢ 𝑉 = (𝑈 ++ 〈“(𝐹‘𝑋)”〉) ⇒ ⊢ (𝜑 → (𝐹 ∘ 𝑇) = 𝑉) | ||
Theorem | cats1cli 13453 | Closure of concatenation with a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016.) |
⊢ 𝑇 = (𝑆 ++ 〈“𝑋”〉) & ⊢ 𝑆 ∈ Word V ⇒ ⊢ 𝑇 ∈ Word V | ||
Theorem | cats1fvn 13454 | The last symbol of a concatenation with a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016.) |
⊢ 𝑇 = (𝑆 ++ 〈“𝑋”〉) & ⊢ 𝑆 ∈ Word V & ⊢ (#‘𝑆) = 𝑀 ⇒ ⊢ (𝑋 ∈ 𝑉 → (𝑇‘𝑀) = 𝑋) | ||
Theorem | cats1fv 13455 | A symbol other than the last in a concatenation with a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016.) |
⊢ 𝑇 = (𝑆 ++ 〈“𝑋”〉) & ⊢ 𝑆 ∈ Word V & ⊢ (#‘𝑆) = 𝑀 & ⊢ (𝑌 ∈ 𝑉 → (𝑆‘𝑁) = 𝑌) & ⊢ 𝑁 ∈ ℕ0 & ⊢ 𝑁 < 𝑀 ⇒ ⊢ (𝑌 ∈ 𝑉 → (𝑇‘𝑁) = 𝑌) | ||
Theorem | cats1len 13456 | The length of concatenation with a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016.) |
⊢ 𝑇 = (𝑆 ++ 〈“𝑋”〉) & ⊢ 𝑆 ∈ Word V & ⊢ (#‘𝑆) = 𝑀 & ⊢ (𝑀 + 1) = 𝑁 ⇒ ⊢ (#‘𝑇) = 𝑁 | ||
Theorem | cats1cat 13457 | Closure of concatenation with a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016.) |
⊢ 𝑇 = (𝑆 ++ 〈“𝑋”〉) & ⊢ 𝐴 ∈ Word V & ⊢ 𝑆 ∈ Word V & ⊢ 𝐶 = (𝐵 ++ 〈“𝑋”〉) & ⊢ 𝐵 = (𝐴 ++ 𝑆) ⇒ ⊢ 𝐶 = (𝐴 ++ 𝑇) | ||
Theorem | cats2cat 13458 | Closure of concatenation of concatenations with singleton words. (Contributed by AV, 1-Mar-2021.) |
⊢ 𝐵 ∈ Word V & ⊢ 𝐷 ∈ Word V & ⊢ 𝐴 = (𝐵 ++ 〈“𝑋”〉) & ⊢ 𝐶 = (〈“𝑌”〉 ++ 𝐷) ⇒ ⊢ (𝐴 ++ 𝐶) = ((𝐵 ++ 〈“𝑋𝑌”〉) ++ 𝐷) | ||
Theorem | s2eqd 13459 | Equality theorem for a doubleton word. (Contributed by Mario Carneiro, 27-Feb-2016.) |
⊢ (𝜑 → 𝐴 = 𝑁) & ⊢ (𝜑 → 𝐵 = 𝑂) ⇒ ⊢ (𝜑 → 〈“𝐴𝐵”〉 = 〈“𝑁𝑂”〉) | ||
Theorem | s3eqd 13460 | Equality theorem for a length 3 word. (Contributed by Mario Carneiro, 27-Feb-2016.) |
⊢ (𝜑 → 𝐴 = 𝑁) & ⊢ (𝜑 → 𝐵 = 𝑂) & ⊢ (𝜑 → 𝐶 = 𝑃) ⇒ ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉 = 〈“𝑁𝑂𝑃”〉) | ||
Theorem | s4eqd 13461 | Equality theorem for a length 4 word. (Contributed by Mario Carneiro, 27-Feb-2016.) |
⊢ (𝜑 → 𝐴 = 𝑁) & ⊢ (𝜑 → 𝐵 = 𝑂) & ⊢ (𝜑 → 𝐶 = 𝑃) & ⊢ (𝜑 → 𝐷 = 𝑄) ⇒ ⊢ (𝜑 → 〈“𝐴𝐵𝐶𝐷”〉 = 〈“𝑁𝑂𝑃𝑄”〉) | ||
Theorem | s5eqd 13462 | Equality theorem for a length 5 word. (Contributed by Mario Carneiro, 27-Feb-2016.) |
⊢ (𝜑 → 𝐴 = 𝑁) & ⊢ (𝜑 → 𝐵 = 𝑂) & ⊢ (𝜑 → 𝐶 = 𝑃) & ⊢ (𝜑 → 𝐷 = 𝑄) & ⊢ (𝜑 → 𝐸 = 𝑅) ⇒ ⊢ (𝜑 → 〈“𝐴𝐵𝐶𝐷𝐸”〉 = 〈“𝑁𝑂𝑃𝑄𝑅”〉) | ||
Theorem | s6eqd 13463 | Equality theorem for a length 6 word. (Contributed by Mario Carneiro, 27-Feb-2016.) |
⊢ (𝜑 → 𝐴 = 𝑁) & ⊢ (𝜑 → 𝐵 = 𝑂) & ⊢ (𝜑 → 𝐶 = 𝑃) & ⊢ (𝜑 → 𝐷 = 𝑄) & ⊢ (𝜑 → 𝐸 = 𝑅) & ⊢ (𝜑 → 𝐹 = 𝑆) ⇒ ⊢ (𝜑 → 〈“𝐴𝐵𝐶𝐷𝐸𝐹”〉 = 〈“𝑁𝑂𝑃𝑄𝑅𝑆”〉) | ||
Theorem | s7eqd 13464 | Equality theorem for a length 7 word. (Contributed by Mario Carneiro, 27-Feb-2016.) |
⊢ (𝜑 → 𝐴 = 𝑁) & ⊢ (𝜑 → 𝐵 = 𝑂) & ⊢ (𝜑 → 𝐶 = 𝑃) & ⊢ (𝜑 → 𝐷 = 𝑄) & ⊢ (𝜑 → 𝐸 = 𝑅) & ⊢ (𝜑 → 𝐹 = 𝑆) & ⊢ (𝜑 → 𝐺 = 𝑇) ⇒ ⊢ (𝜑 → 〈“𝐴𝐵𝐶𝐷𝐸𝐹𝐺”〉 = 〈“𝑁𝑂𝑃𝑄𝑅𝑆𝑇”〉) | ||
Theorem | s8eqd 13465 | Equality theorem for a length 8 word. (Contributed by Mario Carneiro, 27-Feb-2016.) |
⊢ (𝜑 → 𝐴 = 𝑁) & ⊢ (𝜑 → 𝐵 = 𝑂) & ⊢ (𝜑 → 𝐶 = 𝑃) & ⊢ (𝜑 → 𝐷 = 𝑄) & ⊢ (𝜑 → 𝐸 = 𝑅) & ⊢ (𝜑 → 𝐹 = 𝑆) & ⊢ (𝜑 → 𝐺 = 𝑇) & ⊢ (𝜑 → 𝐻 = 𝑈) ⇒ ⊢ (𝜑 → 〈“𝐴𝐵𝐶𝐷𝐸𝐹𝐺𝐻”〉 = 〈“𝑁𝑂𝑃𝑄𝑅𝑆𝑇𝑈”〉) | ||
Theorem | s2cld 13466 | A doubleton word is a word. (Contributed by Mario Carneiro, 27-Feb-2016.) |
⊢ (𝜑 → 𝐴 ∈ 𝑋) & ⊢ (𝜑 → 𝐵 ∈ 𝑋) ⇒ ⊢ (𝜑 → 〈“𝐴𝐵”〉 ∈ Word 𝑋) | ||
Theorem | s3cld 13467 | A length 3 string is a word. (Contributed by Mario Carneiro, 27-Feb-2016.) |
⊢ (𝜑 → 𝐴 ∈ 𝑋) & ⊢ (𝜑 → 𝐵 ∈ 𝑋) & ⊢ (𝜑 → 𝐶 ∈ 𝑋) ⇒ ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉 ∈ Word 𝑋) | ||
Theorem | s4cld 13468 | A length 4 string is a word. (Contributed by Mario Carneiro, 27-Feb-2016.) |
⊢ (𝜑 → 𝐴 ∈ 𝑋) & ⊢ (𝜑 → 𝐵 ∈ 𝑋) & ⊢ (𝜑 → 𝐶 ∈ 𝑋) & ⊢ (𝜑 → 𝐷 ∈ 𝑋) ⇒ ⊢ (𝜑 → 〈“𝐴𝐵𝐶𝐷”〉 ∈ Word 𝑋) | ||
Theorem | s5cld 13469 | A length 5 string is a word. (Contributed by Mario Carneiro, 27-Feb-2016.) |
⊢ (𝜑 → 𝐴 ∈ 𝑋) & ⊢ (𝜑 → 𝐵 ∈ 𝑋) & ⊢ (𝜑 → 𝐶 ∈ 𝑋) & ⊢ (𝜑 → 𝐷 ∈ 𝑋) & ⊢ (𝜑 → 𝐸 ∈ 𝑋) ⇒ ⊢ (𝜑 → 〈“𝐴𝐵𝐶𝐷𝐸”〉 ∈ Word 𝑋) | ||
Theorem | s6cld 13470 | A length 6 string is a word. (Contributed by Mario Carneiro, 27-Feb-2016.) |
⊢ (𝜑 → 𝐴 ∈ 𝑋) & ⊢ (𝜑 → 𝐵 ∈ 𝑋) & ⊢ (𝜑 → 𝐶 ∈ 𝑋) & ⊢ (𝜑 → 𝐷 ∈ 𝑋) & ⊢ (𝜑 → 𝐸 ∈ 𝑋) & ⊢ (𝜑 → 𝐹 ∈ 𝑋) ⇒ ⊢ (𝜑 → 〈“𝐴𝐵𝐶𝐷𝐸𝐹”〉 ∈ Word 𝑋) | ||
Theorem | s7cld 13471 | A length 7 string is a word. (Contributed by Mario Carneiro, 27-Feb-2016.) |
⊢ (𝜑 → 𝐴 ∈ 𝑋) & ⊢ (𝜑 → 𝐵 ∈ 𝑋) & ⊢ (𝜑 → 𝐶 ∈ 𝑋) & ⊢ (𝜑 → 𝐷 ∈ 𝑋) & ⊢ (𝜑 → 𝐸 ∈ 𝑋) & ⊢ (𝜑 → 𝐹 ∈ 𝑋) & ⊢ (𝜑 → 𝐺 ∈ 𝑋) ⇒ ⊢ (𝜑 → 〈“𝐴𝐵𝐶𝐷𝐸𝐹𝐺”〉 ∈ Word 𝑋) | ||
Theorem | s8cld 13472 | A length 7 string is a word. (Contributed by Mario Carneiro, 27-Feb-2016.) |
⊢ (𝜑 → 𝐴 ∈ 𝑋) & ⊢ (𝜑 → 𝐵 ∈ 𝑋) & ⊢ (𝜑 → 𝐶 ∈ 𝑋) & ⊢ (𝜑 → 𝐷 ∈ 𝑋) & ⊢ (𝜑 → 𝐸 ∈ 𝑋) & ⊢ (𝜑 → 𝐹 ∈ 𝑋) & ⊢ (𝜑 → 𝐺 ∈ 𝑋) & ⊢ (𝜑 → 𝐻 ∈ 𝑋) ⇒ ⊢ (𝜑 → 〈“𝐴𝐵𝐶𝐷𝐸𝐹𝐺𝐻”〉 ∈ Word 𝑋) | ||
Theorem | s2cl 13473 | A doubleton word is a word. (Contributed by Stefan O'Rear, 23-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.) |
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → 〈“𝐴𝐵”〉 ∈ Word 𝑋) | ||
Theorem | s3cl 13474 | A length 3 string is a word. (Contributed by Mario Carneiro, 26-Feb-2016.) |
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋) → 〈“𝐴𝐵𝐶”〉 ∈ Word 𝑋) | ||
Theorem | s2cli 13475 | A doubleton word is a word. (Contributed by Mario Carneiro, 26-Feb-2016.) |
⊢ 〈“𝐴𝐵”〉 ∈ Word V | ||
Theorem | s3cli 13476 | A length 3 string is a word. (Contributed by Mario Carneiro, 26-Feb-2016.) |
⊢ 〈“𝐴𝐵𝐶”〉 ∈ Word V | ||
Theorem | s4cli 13477 | A length 4 string is a word. (Contributed by Mario Carneiro, 26-Feb-2016.) |
⊢ 〈“𝐴𝐵𝐶𝐷”〉 ∈ Word V | ||
Theorem | s5cli 13478 | A length 5 string is a word. (Contributed by Mario Carneiro, 26-Feb-2016.) |
⊢ 〈“𝐴𝐵𝐶𝐷𝐸”〉 ∈ Word V | ||
Theorem | s6cli 13479 | A length 6 string is a word. (Contributed by Mario Carneiro, 26-Feb-2016.) |
⊢ 〈“𝐴𝐵𝐶𝐷𝐸𝐹”〉 ∈ Word V | ||
Theorem | s7cli 13480 | A length 7 string is a word. (Contributed by Mario Carneiro, 26-Feb-2016.) |
⊢ 〈“𝐴𝐵𝐶𝐷𝐸𝐹𝐺”〉 ∈ Word V | ||
Theorem | s8cli 13481 | A length 8 string is a word. (Contributed by Mario Carneiro, 26-Feb-2016.) |
⊢ 〈“𝐴𝐵𝐶𝐷𝐸𝐹𝐺𝐻”〉 ∈ Word V | ||
Theorem | s2fv0 13482 | Extract the first symbol from a doubleton word. (Contributed by Stefan O'Rear, 23-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.) |
⊢ (𝐴 ∈ 𝑉 → (〈“𝐴𝐵”〉‘0) = 𝐴) | ||
Theorem | s2fv1 13483 | Extract the second symbol from a doubleton word. (Contributed by Stefan O'Rear, 23-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.) |
⊢ (𝐵 ∈ 𝑉 → (〈“𝐴𝐵”〉‘1) = 𝐵) | ||
Theorem | s2len 13484 | The length of a doubleton word. (Contributed by Stefan O'Rear, 23-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.) |
⊢ (#‘〈“𝐴𝐵”〉) = 2 | ||
Theorem | s2dm 13485 | The domain of a doubleton word is an unordered pair. (Contributed by AV, 9-Jan-2020.) |
⊢ dom 〈“𝐴𝐵”〉 = {0, 1} | ||
Theorem | s3fv0 13486 | Extract the first symbol from a length 3 string. (Contributed by Mario Carneiro, 13-Jan-2017.) |
⊢ (𝐴 ∈ 𝑉 → (〈“𝐴𝐵𝐶”〉‘0) = 𝐴) | ||
Theorem | s3fv1 13487 | Extract the second symbol from a length 3 string. (Contributed by Mario Carneiro, 13-Jan-2017.) |
⊢ (𝐵 ∈ 𝑉 → (〈“𝐴𝐵𝐶”〉‘1) = 𝐵) | ||
Theorem | s3fv2 13488 | Extract the third symbol from a length 3 string. (Contributed by Mario Carneiro, 13-Jan-2017.) |
⊢ (𝐶 ∈ 𝑉 → (〈“𝐴𝐵𝐶”〉‘2) = 𝐶) | ||
Theorem | s3len 13489 | The length of a length 3 string. (Contributed by Mario Carneiro, 26-Feb-2016.) |
⊢ (#‘〈“𝐴𝐵𝐶”〉) = 3 | ||
Theorem | s4fv0 13490 | Extract the first symbol from a length 4 string. (Contributed by Thierry Arnoux, 8-Oct-2020.) |
⊢ (𝐴 ∈ 𝑉 → (〈“𝐴𝐵𝐶𝐷”〉‘0) = 𝐴) | ||
Theorem | s4fv1 13491 | Extract the second symbol from a length 4 string. (Contributed by Thierry Arnoux, 8-Oct-2020.) |
⊢ (𝐵 ∈ 𝑉 → (〈“𝐴𝐵𝐶𝐷”〉‘1) = 𝐵) | ||
Theorem | s4fv2 13492 | Extract the third symbol from a length 4 string. (Contributed by Thierry Arnoux, 8-Oct-2020.) |
⊢ (𝐶 ∈ 𝑉 → (〈“𝐴𝐵𝐶𝐷”〉‘2) = 𝐶) | ||
Theorem | s4fv3 13493 | Extract the fourth symbol from a length 4 string. (Contributed by Thierry Arnoux, 8-Oct-2020.) |
⊢ (𝐷 ∈ 𝑉 → (〈“𝐴𝐵𝐶𝐷”〉‘3) = 𝐷) | ||
Theorem | s4len 13494 | The length of a length 4 string. (Contributed by Mario Carneiro, 26-Feb-2016.) |
⊢ (#‘〈“𝐴𝐵𝐶𝐷”〉) = 4 | ||
Theorem | s5len 13495 | The length of a length 5 string. (Contributed by Mario Carneiro, 26-Feb-2016.) |
⊢ (#‘〈“𝐴𝐵𝐶𝐷𝐸”〉) = 5 | ||
Theorem | s6len 13496 | The length of a length 6 string. (Contributed by Mario Carneiro, 26-Feb-2016.) |
⊢ (#‘〈“𝐴𝐵𝐶𝐷𝐸𝐹”〉) = 6 | ||
Theorem | s7len 13497 | The length of a length 7 string. (Contributed by Mario Carneiro, 26-Feb-2016.) |
⊢ (#‘〈“𝐴𝐵𝐶𝐷𝐸𝐹𝐺”〉) = 7 | ||
Theorem | s8len 13498 | The length of a length 8 string. (Contributed by Mario Carneiro, 26-Feb-2016.) |
⊢ (#‘〈“𝐴𝐵𝐶𝐷𝐸𝐹𝐺𝐻”〉) = 8 | ||
Theorem | lsws2 13499 | The last symbol of a doubleton word is its second symbol. (Contributed by AV, 8-Feb-2021.) |
⊢ (𝐵 ∈ 𝑉 → ( lastS ‘〈“𝐴𝐵”〉) = 𝐵) | ||
Theorem | lsws3 13500 | The last symbol of a 3 letter word is its third symbol. (Contributed by AV, 8-Feb-2021.) |
⊢ (𝐶 ∈ 𝑉 → ( lastS ‘〈“𝐴𝐵𝐶”〉) = 𝐶) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |