Home | Metamath
Proof Explorer Theorem List (p. 133 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 | eqwrd 13201* | 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 13202* | 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 13203* | 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 | lsw 13204 | 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 13205 | 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 13206 | The last symbol of an empty word does not exist. (Contributed by Alexander van der Vekens, 11-Nov-2018.) |
⊢ ( lastS ‘∅) = ∅ | ||
Theorem | lsw1 13207 | 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 13208 | 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 13209 | 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 13210 | 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 13211* | Value of the concatenation operator. (Contributed by Stefan O'Rear, 15-Aug-2015.) |
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑊) → (𝑆 ++ 𝑇) = (𝑥 ∈ (0..^((#‘𝑆) + (#‘𝑇))) ↦ if(𝑥 ∈ (0..^(#‘𝑆)), (𝑆‘𝑥), (𝑇‘(𝑥 − (#‘𝑆)))))) | ||
Theorem | ccatcl 13212 | 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 13213 | The length of a concatenated word. (Contributed by Stefan O'Rear, 15-Aug-2015.) |
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → (#‘(𝑆 ++ 𝑇)) = ((#‘𝑆) + (#‘𝑇))) | ||
Theorem | ccatval1 13214 | 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 13215 | 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 13216 | 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 13217 | 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 13218 | 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 13219 | 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 13220 | 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 13221 | 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 13222 | 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 13223 | 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 13224 | Associative law for concatenation of words. (Contributed by Stefan O'Rear, 15-Aug-2015.) |
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵 ∧ 𝑈 ∈ Word 𝐵) → ((𝑆 ++ 𝑇) ++ 𝑈) = (𝑆 ++ (𝑇 ++ 𝑈))) | ||
Theorem | ccatrn 13225 | The range of a concatenated word. (Contributed by Stefan O'Rear, 15-Aug-2015.) |
⊢ ((𝑆 ∈ Word 𝐵 ∧ 𝑇 ∈ Word 𝐵) → ran (𝑆 ++ 𝑇) = (ran 𝑆 ∪ ran 𝑇)) | ||
Theorem | lswccatn0lsw 13226 | 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 13227 | 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 13228 | 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 13229 | 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 13230 | Identity function protection for a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016.) |
⊢ 〈“𝐴”〉 = 〈“( I ‘𝐴)”〉 | ||
Theorem | s1val 13231 | Value of a single-symbol word. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.) |
⊢ (𝐴 ∈ 𝑉 → 〈“𝐴”〉 = {〈0, 𝐴〉}) | ||
Theorem | s1rn 13232 | The range of a single-symbol word. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ (𝐴 ∈ 𝑉 → ran 〈“𝐴”〉 = {𝐴}) | ||
Theorem | s1eq 13233 | Equality theorem for a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016.) |
⊢ (𝐴 = 𝐵 → 〈“𝐴”〉 = 〈“𝐵”〉) | ||
Theorem | s1eqd 13234 | Equality theorem for a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → 〈“𝐴”〉 = 〈“𝐵”〉) | ||
Theorem | s1cl 13235 | 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 13236 | A singleton word is a word. (Contributed by Mario Carneiro, 26-Feb-2016.) |
⊢ (𝜑 → 𝐴 ∈ 𝐵) ⇒ ⊢ (𝜑 → 〈“𝐴”〉 ∈ Word 𝐵) | ||
Theorem | s1cli 13237 | A singleton word is a word. (Contributed by Mario Carneiro, 26-Feb-2016.) |
⊢ 〈“𝐴”〉 ∈ Word V | ||
Theorem | s1len 13238 | Length of a singleton word. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.) |
⊢ (#‘〈“𝐴”〉) = 1 | ||
Theorem | s1nz 13239 | 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 13240 | Obsolete proof of s1nz 13239 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 13241 | The domain of a singleton word is a singleton. (Contributed by AV, 9-Jan-2020.) |
⊢ dom 〈“𝐴”〉 = {0} | ||
Theorem | s1dmALT 13242 | Alternate version of s1dm 13241, 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 13243 | Sole symbol of a singleton word. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.) |
⊢ (𝐴 ∈ 𝐵 → (〈“𝐴”〉‘0) = 𝐴) | ||
Theorem | lsws1 13244 | The last symbol of a singleton word is its symbol. (Contributed by AV, 22-Oct-2018.) |
⊢ (𝐴 ∈ 𝑉 → ( lastS ‘〈“𝐴”〉) = 𝐴) | ||
Theorem | eqs1 13245 | 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 13246* | A word of length 1 is a singleton word. (Contributed by AV, 24-Jan-2021.) |
⊢ ((𝑊 ∈ Word 𝑆 ∧ (#‘𝑊) = 1) → ∃𝑠 ∈ 𝑆 𝑊 = 〈“𝑠”〉) | ||
Theorem | wrdl1s1 13247 | 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 13248 | The singleton word function is injective. (Contributed by Mario Carneiro, 1-Oct-2015.) (Revised by Mario Carneiro, 26-Feb-2016.) |
⊢ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) → (〈“𝑆”〉 = 〈“𝑇”〉 ↔ 𝑆 = 𝑇)) | ||
Theorem | ccatws1cl 13249 | 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 13250 | The concatenation of two singleton words is a word. (Contributed by Alexander van der Vekens, 22-Sep-2018.) |
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (〈“𝑋”〉 ++ 〈“𝑌”〉) ∈ Word 𝑉) | ||
Theorem | ccatws1len 13251 | 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 13252 | 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 13253 | The length of the concatenation of two singleton words. (Contributed by Alexander van der Vekens, 22-Sep-2018.) |
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (#‘(〈“𝑋”〉 ++ 〈“𝑌”〉)) = 2) | ||
Theorem | ccatw2s1len 13254 | The length of the concatenation of a word with two singleton words. (Contributed by Alexander van der Vekens, 22-Sep-2018.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (#‘((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)) = ((#‘𝑊) + 2)) | ||
Theorem | ccats1val1 13255 | 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 13256 | 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 | ccat2s1p1 13257 | Extract the first of two concatenated singleton words. (Contributed by Alexander van der Vekens, 22-Sep-2018.) |
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → ((〈“𝑋”〉 ++ 〈“𝑌”〉)‘0) = 𝑋) | ||
Theorem | ccat2s1p2 13258 | Extract the second of two concatenated singleton words. (Contributed by Alexander van der Vekens, 22-Sep-2018.) |
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → ((〈“𝑋”〉 ++ 〈“𝑌”〉)‘1) = 𝑌) | ||
Theorem | ccatw2s1ass 13259 | Associative law for a concatenation of a word with two singleton words. (Contributed by Alexander van der Vekens, 22-Sep-2018.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → ((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉) = (𝑊 ++ (〈“𝑋”〉 ++ 〈“𝑌”〉))) | ||
Theorem | ccatws1lenrev 13260 | The length of a word concatenated with a singleton word. (Contributed by Alexander van der Vekens, 3-Oct-2018.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑋 ∈ 𝑉) → ((#‘(𝑊 ++ 〈“𝑋”〉)) = 𝑁 → (#‘𝑊) = (𝑁 − 1))) | ||
Theorem | ccatws1n0 13261 | The concatenation of a word with a singleton word is not the empty set. (Contributed by Alexander van der Vekens, 29-Sep-2018.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑋 ∈ 𝑉) → (𝑊 ++ 〈“𝑋”〉) ≠ ∅) | ||
Theorem | ccatws1ls 13262 | 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 13263 | 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 13264 | 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 13265 | 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 13266 | 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 13267 | 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.) |
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝐼 ∈ ℕ0 ∧ 𝐼 < (#‘𝑊)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘𝐼) = (𝑊‘𝐼)) | ||
Theorem | ccat2s1fst 13268 | The first symbol of the concatenation of a word with two single symbols. (Contributed by Alexander van der Vekens, 22-Sep-2018.) |
⊢ (((𝑊 ∈ Word 𝑉 ∧ 0 < (#‘𝑊)) ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → (((𝑊 ++ 〈“𝑋”〉) ++ 〈“𝑌”〉)‘0) = (𝑊‘0)) | ||
Theorem | swrdval 13269* | Value of a subword. (Contributed by Stefan O'Rear, 15-Aug-2015.) |
⊢ ((𝑆 ∈ 𝑉 ∧ 𝐹 ∈ ℤ ∧ 𝐿 ∈ ℤ) → (𝑆 substr 〈𝐹, 𝐿〉) = if((𝐹..^𝐿) ⊆ dom 𝑆, (𝑥 ∈ (0..^(𝐿 − 𝐹)) ↦ (𝑆‘(𝑥 + 𝐹))), ∅)) | ||
Theorem | swrd00 13270 | A zero length substring. (Contributed by Stefan O'Rear, 27-Aug-2015.) |
⊢ (𝑆 substr 〈𝑋, 𝑋〉) = ∅ | ||
Theorem | swrdcl 13271 | 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 13272* | 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 | swrd0val 13273 | Value of the subword extractor for left-anchored subwords. (Contributed by Stefan O'Rear, 24-Aug-2015.) |
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝐿 ∈ (0...(#‘𝑆))) → (𝑆 substr 〈0, 𝐿〉) = (𝑆 ↾ (0..^𝐿))) | ||
Theorem | swrd0len 13274 | Length of a left-anchored subword. (Contributed by Stefan O'Rear, 24-Aug-2015.) |
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝐿 ∈ (0...(#‘𝑆))) → (#‘(𝑆 substr 〈0, 𝐿〉)) = 𝐿) | ||
Theorem | swrdlen 13275 | Length of an extracted subword. (Contributed by Stefan O'Rear, 16-Aug-2015.) |
⊢ ((𝑆 ∈ Word 𝐴 ∧ 𝐹 ∈ (0...𝐿) ∧ 𝐿 ∈ (0...(#‘𝑆))) → (#‘(𝑆 substr 〈𝐹, 𝐿〉)) = (𝐿 − 𝐹)) | ||
Theorem | swrdfv 13276 | 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 | swrdf 13277 | 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 13278 | 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 | swrd0f 13279 | A left-anchored 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, 2-May-2020.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ (0...(#‘𝑊))) → (𝑊 substr 〈0, 𝑁〉):(0..^𝑁)⟶𝑉) | ||
Theorem | swrdid 13280 | A word is a subword of itself. (Contributed by Stefan O'Rear, 16-Aug-2015.) (Proof shortened by AV, 2-May-2020.) |
⊢ (𝑆 ∈ Word 𝐴 → (𝑆 substr 〈0, (#‘𝑆)〉) = 𝑆) | ||
Theorem | swrdrn 13281 | 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 | swrdn0 13282 | A prefixing subword consisting of at least one symbol is not empty. (Contributed by Alexander van der Vekens, 4-Aug-2018.) (Proof shortened by AV, 2-May-2020.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ ∧ 𝑁 ≤ (#‘𝑊)) → (𝑊 substr 〈0, 𝑁〉) ≠ ∅) | ||
Theorem | swrdlend 13283 | 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 13284 | 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 13285 | Value of the subword extractor outside its intended domain. (Contributed by Alexander van der Vekens, 24-May-2018.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝐵 ≤ 𝐴 ∨ (#‘𝑊) ≤ 𝐴 ∨ 𝐵 ≤ 0) → (𝑊 substr 〈𝐴, 𝐵〉) = ∅)) | ||
Theorem | swrd0 13286 | 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 13287 | Length of a right-anchored subword. (Contributed by Alexander van der Vekens, 5-Apr-2018.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐼 ∈ (0...(#‘𝑊))) → (#‘(𝑊 substr 〈𝐼, (#‘𝑊)〉)) = ((#‘𝑊) − 𝐼)) | ||
Theorem | swrd0len0 13288 | Length of a prefix of a word reduced by a single symbol, analogous to swrd0len 13274. (Contributed by AV, 4-Aug-2018.) (Proof shortened by AV, 14-Oct-2018.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑁 ∈ ℕ0 ∧ (#‘𝑊) = (𝑁 + 1)) → (#‘(𝑊 substr 〈0, 𝑁〉)) = 𝑁) | ||
Theorem | addlenrevswrd 13289 | The sum of the lengths of two reversed parts of a word is the length of the word. (Contributed by Alexander van der Vekens, 1-Apr-2018.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...(#‘𝑊))) → ((#‘(𝑊 substr 〈𝑀, (#‘𝑊)〉)) + (#‘(𝑊 substr 〈0, 𝑀〉))) = (#‘𝑊)) | ||
Theorem | addlenswrd 13290 | The sum of the lengths of two parts of a word is the length of the word. (Contributed by AV, 21-Oct-2018.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ (0...(#‘𝑊))) → ((#‘(𝑊 substr 〈0, 𝑀〉)) + (#‘(𝑊 substr 〈𝑀, (#‘𝑊)〉))) = (#‘𝑊)) | ||
Theorem | swrd0fv 13291 | A symbol in an left-anchored subword, indexed using the subword's indices. (Contributed by Alexander van der Vekens, 16-Jun-2018.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (0...(#‘𝑊)) ∧ 𝐼 ∈ (0..^𝐿)) → ((𝑊 substr 〈0, 𝐿〉)‘𝐼) = (𝑊‘𝐼)) | ||
Theorem | swrd0fv0 13292 | The first symbol in a left-anchored subword. (Contributed by Alexander van der Vekens, 16-Jun-2018.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐼 ∈ (1...(#‘𝑊))) → ((𝑊 substr 〈0, 𝐼〉)‘0) = (𝑊‘0)) | ||
Theorem | swrdtrcfv 13293 | A symbol in a word truncated by one symbol. (Contributed by Alexander van der Vekens, 16-Jun-2018.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝑊 ≠ ∅ ∧ 𝐼 ∈ (0..^((#‘𝑊) − 1))) → ((𝑊 substr 〈0, ((#‘𝑊) − 1)〉)‘𝐼) = (𝑊‘𝐼)) | ||
Theorem | swrdtrcfv0 13294 | The first symbol in a word truncated by one symbol. (Contributed by Alexander van der Vekens, 16-Jun-2018.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 2 ≤ (#‘𝑊)) → ((𝑊 substr 〈0, ((#‘𝑊) − 1)〉)‘0) = (𝑊‘0)) | ||
Theorem | swrd0fvlsw 13295 | The last symbol in a left-anchored subword. (Contributed by Alexander van der Vekens, 24-Jun-2018.) |
⊢ ((𝑊 ∈ Word 𝑉 ∧ 𝐿 ∈ (1...(#‘𝑊))) → ( lastS ‘(𝑊 substr 〈0, 𝐿〉)) = (𝑊‘(𝐿 − 1))) | ||
Theorem | swrdeq 13296* | Two subwords of words are equal iff they have the same length and the same symbols at each position. (Contributed by Alexander van der Vekens, 7-Aug-2018.) |
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ (𝑀 ≤ (#‘𝑊) ∧ 𝑁 ≤ (#‘𝑈))) → ((𝑊 substr 〈0, 𝑀〉) = (𝑈 substr 〈0, 𝑁〉) ↔ (𝑀 = 𝑁 ∧ ∀𝑖 ∈ (0..^𝑀)(𝑊‘𝑖) = (𝑈‘𝑖)))) | ||
Theorem | swrdlen2 13297 | Length of an extracted subword. (Contributed by AV, 5-May-2020.) |
⊢ ((𝑆 ∈ Word 𝑉 ∧ (𝐹 ∈ ℕ0 ∧ 𝐿 ∈ (ℤ≥‘𝐹)) ∧ 𝐿 ≤ (#‘𝑆)) → (#‘(𝑆 substr 〈𝐹, 𝐿〉)) = (𝐿 − 𝐹)) | ||
Theorem | swrdfv2 13298 | A symbol in an extracted subword, indexed using the word's indices. (Contributed by AV, 5-May-2020.) |
⊢ (((𝑆 ∈ Word 𝑉 ∧ (𝐹 ∈ ℕ0 ∧ 𝐿 ∈ (ℤ≥‘𝐹)) ∧ 𝐿 ≤ (#‘𝑆)) ∧ 𝑋 ∈ (𝐹..^𝐿)) → ((𝑆 substr 〈𝐹, 𝐿〉)‘(𝑋 − 𝐹)) = (𝑆‘𝑋)) | ||
Theorem | swrdsb0eq 13299 | 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 13300 | Two subwords with the same bounds have the same length. (Contributed by AV, 4-May-2020.) |
⊢ (((𝑊 ∈ Word 𝑉 ∧ 𝑈 ∈ Word 𝑉) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ (𝑁 ≤ (#‘𝑊) ∧ 𝑁 ≤ (#‘𝑈))) → (#‘(𝑊 substr 〈𝑀, 𝑁〉)) = (#‘(𝑈 substr 〈𝑀, 𝑁〉))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |