Home | Metamath
Proof Explorer Theorem List (p. 140 of 450) | < 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-28697) |
Hilbert Space Explorer
(28698-30220) |
Users' Mathboxes
(30221-44913) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | wrdnfi 13901* | 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 13902* | Obsolete version of wrdnfi 13901 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 13903 | 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 13904 | A word with length at least 1 is not empty. (Contributed by AV, 14-Oct-2018.) |
⊢ (𝑊 ∈ Word 𝑉 → (𝑊 ≠ ∅ ↔ 1 ≤ (♯‘𝑊))) | ||
Theorem | len0nnbi 13905 | The length of a word is a positive integer iff the word is not empty. (Contributed by AV, 22-Mar-2022.) |
⊢ (𝑊 ∈ Word 𝑆 → (𝑊 ≠ ∅ ↔ (♯‘𝑊) ∈ ℕ)) | ||
Theorem | wrdlenge2n0 13906 | 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 13907 | 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 13908* | 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 13909 | 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 13910 | 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 13911* | Two words are equal iff they have the same length and the same symbol at each position. (Contributed by AV, 13-Apr-2018.) (Revised by JJ, 30-Dec-2023.) |
⊢ ((𝑈 ∈ Word 𝑆 ∧ 𝑊 ∈ Word 𝑇) → (𝑈 = 𝑊 ↔ ((♯‘𝑈) = (♯‘𝑊) ∧ ∀𝑖 ∈ (0..^(♯‘𝑈))(𝑈‘𝑖) = (𝑊‘𝑖)))) | ||
Theorem | elovmpowrd 13912* | Implications for the value of an operation defined by the maps-to notation with a class abstraction 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 13913* | 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 13914 | A word truncated by a symbol is a word. (Contributed by AV, 29-Jan-2021.) |
⊢ (𝐹 ∈ Word 𝑆 → (𝐹 ↾ (0..^((♯‘𝐹) − 1))) ∈ Word 𝑆) | ||
Theorem | wrdred1hash 13915 | 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 13916 | Extend class notation with the Last Symbol of a word. |
class lastS | ||
Definition | df-lsw 13917 | 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 13918 | 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 13919 | 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 13920 | The last symbol of an empty word does not exist. (Contributed by Alexander van der Vekens, 11-Nov-2018.) |
⊢ (lastS‘∅) = ∅ | ||
Theorem | lsw1 13921 | 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 13922 | 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 13923 | 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 13924 | Syntax for the concatenation operator. |
class ++ | ||
Definition | df-concat 13925* | 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 13926 | 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 13927* | Value of the concatenation operator. (Contributed by Stefan O'Rear, 15-Aug-2015.) |
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑊) → (𝑆 ++ 𝑇) = (𝑥 ∈ (0..^((♯‘𝑆) + (♯‘𝑇))) ↦ if(𝑥 ∈ (0..^(♯‘𝑆)), (𝑆‘𝑥), (𝑇‘(𝑥 − (♯‘𝑆)))))) | ||
Theorem | ccatcl 13928 | 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 13929 | The length of a concatenated word. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by JJ, 1-Jan-2024.) |
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝑇 ∈ Word 𝐵) → (♯‘(𝑆 ++ 𝑇)) = ((♯‘𝑆) + (♯‘𝑇))) | ||
Theorem | ccatlenOLD 13930 | Obsolete version of ccatlen 13929 as of 1-Jan-2024. The length of a concatenated word. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → (♯‘(𝑆 ++ 𝑇)) = ((♯‘𝑆) + (♯‘𝑇))) | ||
Theorem | ccat0 13931 | 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 13932 | 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 | ccatval1OLD 13933 | Obsolete version of ccatval1 13932 as of 18-Jan-2024. 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.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝐼 ∈ (0..^(♯‘𝑆))) → ((𝑆 ++ 𝑇)‘𝐼) = (𝑆‘𝐼)) | ||
Theorem | ccatval2 13934 | 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 13935 | 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 13936 | 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 13937 | 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 13938 | 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 13939 | 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 13940 | 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 13941 | The first symbol of the right (nonempty) half of a concatenated word. (Contributed by AV, 23-Apr-2022.) |
⊢ ((𝐴 ∈ Word 𝑉 ∧ 𝐵 ∈ Word 𝑉 ∧ 𝐵 ≠ ∅) → ((𝐴 ++ 𝐵)‘(♯‘𝐴)) = (𝐵‘0)) | ||
Theorem | ccatlid 13942 | 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 13943 | 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 13944 | Associative law for concatenation of words. (Contributed by Stefan O'Rear, 15-Aug-2015.) |
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵) → ((𝑆 ++ 𝑇) ++ 𝑈) = (𝑆 ++ (𝑇 ++ 𝑈))) | ||
Theorem | ccatrn 13945 | The range of a concatenated word. (Contributed by Stefan O'Rear, 15-Aug-2015.) |
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → ran (𝑆 ++ 𝑇) = (ran 𝑆 ∪ ran 𝑇)) | ||
Theorem | ccatidid 13946 | Concatenation of the empty word by the empty word. (Contributed by AV, 26-Mar-2022.) |
⊢ (∅ ++ ∅) = ∅ | ||
Theorem | lswccatn0lsw 13947 | 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 13948 | 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 13949 | 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 13950 | 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 13951 | Syntax for the singleton word constructor. |
class 〈“𝐴”〉 | ||
Definition | df-s1 13952 | 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 13960, and not, as maybe expected, the empty word, see also s1nz 13963. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.) |
⊢ 〈“𝐴”〉 = {〈0, ( I ‘𝐴)〉} | ||
Theorem | ids1 13953 | Identity function protection for a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016.) |
⊢ 〈“𝐴”〉 = 〈“( I ‘𝐴)”〉 | ||
Theorem | s1val 13954 | Value of a singleton word. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.) |
⊢ (𝐴 ∈ 𝑉 → 〈“𝐴”〉 = {〈0, 𝐴〉}) | ||
Theorem | s1rn 13955 | The range of a singleton word. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ (𝐴 ∈ 𝑉 → ran 〈“𝐴”〉 = {𝐴}) | ||
Theorem | s1eq 13956 | Equality theorem for a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016.) |
⊢ (𝐴 = 𝐵 → 〈“𝐴”〉 = 〈“𝐵”〉) | ||
Theorem | s1eqd 13957 | Equality theorem for a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → 〈“𝐴”〉 = 〈“𝐵”〉) | ||
Theorem | s1cl 13958 | 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 13959 | A singleton word is a word. (Contributed by Mario Carneiro, 26-Feb-2016.) |
⊢ (𝜑 → 𝐴 ∈ 𝐵) ⇒ ⊢ (𝜑 → 〈“𝐴”〉 ∈ Word 𝐵) | ||
Theorem | s1prc 13960 | Value of a singleton word if the symbol is a proper class. (Contributed by AV, 26-Mar-2022.) |
⊢ (¬ 𝐴 ∈ V → 〈“𝐴”〉 = 〈“∅”〉) | ||
Theorem | s1cli 13961 | A singleton word is a word. (Contributed by Mario Carneiro, 26-Feb-2016.) |
⊢ 〈“𝐴”〉 ∈ Word V | ||
Theorem | s1len 13962 | Length of a singleton word. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.) |
⊢ (♯‘〈“𝐴”〉) = 1 | ||
Theorem | s1nz 13963 | 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 13964 | The domain of a singleton word is a singleton. (Contributed by AV, 9-Jan-2020.) |
⊢ dom 〈“𝐴”〉 = {0} | ||
Theorem | s1dmALT 13965 | Alternate version of s1dm 13964, 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 13966 | Sole symbol of a singleton word. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.) |
⊢ (𝐴 ∈ 𝐵 → (〈“𝐴”〉‘0) = 𝐴) | ||
Theorem | lsws1 13967 | The last symbol of a singleton word is its symbol. (Contributed by AV, 22-Oct-2018.) |
⊢ (𝐴 ∈ 𝑉 → (lastS‘〈“𝐴”〉) = 𝐴) | ||
Theorem | eqs1 13968 | 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 13969* | A word of length 1 is a singleton word. (Contributed by AV, 24-Jan-2021.) |
⊢ ((𝑊 ∈ Word 𝑆 ∧ (♯‘𝑊) = 1) → ∃𝑠 ∈ 𝑆 𝑊 = 〈“𝑠”〉) | ||
Theorem | wrdl1s1 13970 | 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 13971 | The singleton word function is injective. (Contributed by Mario Carneiro, 1-Oct-2015.) (Revised by Mario Carneiro, 26-Feb-2016.) |
⊢ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) → (〈“𝑆”〉 = 〈“𝑇”〉 ↔ 𝑆 = 𝑇)) | ||
Theorem | ccatws1cl 13972 | 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 13973 | 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 13974 | The concatenation of two singleton words is a word. (Contributed by Alexander van der Vekens, 22-Sep-2018.) |
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (〈“𝑋”〉 ++ 〈“𝑌”〉) ∈ Word 𝑉) | ||
Theorem | ccats1alpha 13975 | 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 13976 | 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 13977 | 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 13978 | 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 13979 | 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 | ccat2s1lenOLD 13980 | Obsolete version of ccat2s1len 13979 as of 14-Jan-2024. The length of the concatenation of two singleton words. (Contributed by Alexander van der Vekens, 22-Sep-2018.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (♯‘(〈“𝑋”〉 ++ 〈“𝑌”〉)) = 2) | ||
Theorem | ccatw2s1cl 13981 | 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 13982 | 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 13983 | 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 | ccats1val1OLD 13984 | Obsolete version of ccats1val1 13983 as of 20-Jan-2024. 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.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑆 ∈ 𝑉 ∧ 𝐼 ∈ (0..^(♯‘𝑊))) → ((𝑊 ++ 〈“𝑆”〉)‘𝐼) = (𝑊‘𝐼)) | ||
Theorem | ccats1val2 13985 | 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 13986 | 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 13987 | 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 13988 | 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 | ccat2s1p1OLD 13989 | Obsolete version of ccat2s1p1 13987 as of 20-Jan-2024. Extract the first of two concatenated singleton words. (Contributed by Alexander van der Vekens, 22-Sep-2018.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → ((〈“𝑋”〉 ++ 〈“𝑌”〉)‘0) = 𝑋) | ||
Theorem | ccat2s1p2OLD 13990 | Obsolete version of ccat2s1p2 13988 as of 20-Jan-2024. Extract the second of two concatenated singleton words. (Contributed by Alexander van der Vekens, 22-Sep-2018.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → ((〈“𝑋”〉 ++ 〈“𝑌”〉)‘1) = 𝑌) | ||
Theorem | ccatw2s1ass 13991 | Associative law for a concatenation of a word with two singleton words. (Contributed by Alexander van der Vekens, 22-Sep-2018.) |
⊢ (𝑊 ∈ Word 𝑉 → ((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉) = (𝑊 ++ (〈“𝑋”〉 ++ 〈“𝑌”〉))) | ||
Theorem | ccatw2s1assOLD 13992 | Obsolete version of ccatw2s1ass 13991 as of 29-Jan-2024. Associative law for a concatenation of a word with two singleton words. (Contributed by Alexander van der Vekens, 22-Sep-2018.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → ((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉) = (𝑊 ++ (〈“𝑋”〉 ++ 〈“𝑌”〉))) | ||
Theorem | ccatws1n0 13993 | 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 13994 | 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 13995 | 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 13996 | 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 13997 | 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 | ccatw2s1p1OLD 13998 | Obsolete version of ccatw2s1p1 13997 as of 29-Jan-2024. 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.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = 𝑁) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘𝑁) = 𝑋) | ||
Theorem | ccatw2s1p2 13999 | 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 14000 | 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 ∧ 𝐼 < (♯‘𝑊)) → (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘𝐼) = (𝑊‘𝐼)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |