Home | Metamath
Proof Explorer Theorem List (p. 143 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 | swrdco 14201 | Mapping of words commutes with the substring operation. (Contributed by AV, 11-Nov-2018.) |
⊢ ((𝑊 ∈ Word 𝐴 ∧ (𝑀 ∈ (0...𝑁) ∧ 𝑁 ∈ (0...(♯‘𝑊))) ∧ 𝐹:𝐴⟶𝐵) → (𝐹 ∘ (𝑊 substr 〈𝑀, 𝑁〉)) = ((𝐹 ∘ 𝑊) substr 〈𝑀, 𝑁〉)) | ||
Theorem | pfxco 14202 | Mapping of words commutes with the prefix operation. (Contributed by AV, 15-May-2020.) |
⊢ ((𝑊 ∈ Word 𝐴 ∧ 𝑁 ∈ (0...(♯‘𝑊)) ∧ 𝐹:𝐴⟶𝐵) → (𝐹 ∘ (𝑊 prefix 𝑁)) = ((𝐹 ∘ 𝑊) prefix 𝑁)) | ||
Theorem | lswco 14203 | 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 14204 | Mapping of words commutes with the "repeated symbol" operation. (Contributed by AV, 11-Nov-2018.) |
⊢ ((𝑆 ∈ 𝐴 ∧ 𝑁 ∈ ℕ0 ∧ 𝐹:𝐴⟶𝐵) → (𝐹 ∘ (𝑆 repeatS 𝑁)) = ((𝐹‘𝑆) repeatS 𝑁)) | ||
Syntax | cs2 14205 | Syntax for the length 2 word constructor. |
class 〈“𝐴𝐵”〉 | ||
Syntax | cs3 14206 | Syntax for the length 3 word constructor. |
class 〈“𝐴𝐵𝐶”〉 | ||
Syntax | cs4 14207 | Syntax for the length 4 word constructor. |
class 〈“𝐴𝐵𝐶𝐷”〉 | ||
Syntax | cs5 14208 | Syntax for the length 5 word constructor. |
class 〈“𝐴𝐵𝐶𝐷𝐸”〉 | ||
Syntax | cs6 14209 | Syntax for the length 6 word constructor. |
class 〈“𝐴𝐵𝐶𝐷𝐸𝐹”〉 | ||
Syntax | cs7 14210 | Syntax for the length 7 word constructor. |
class 〈“𝐴𝐵𝐶𝐷𝐸𝐹𝐺”〉 | ||
Syntax | cs8 14211 | Syntax for the length 8 word constructor. |
class 〈“𝐴𝐵𝐶𝐷𝐸𝐹𝐺𝐻”〉 | ||
Definition | df-s2 14212 | Define the length 2 word constructor. (Contributed by Mario Carneiro, 26-Feb-2016.) |
⊢ 〈“𝐴𝐵”〉 = (〈“𝐴”〉 ++ 〈“𝐵”〉) | ||
Definition | df-s3 14213 | Define the length 3 word constructor. (Contributed by Mario Carneiro, 26-Feb-2016.) |
⊢ 〈“𝐴𝐵𝐶”〉 = (〈“𝐴𝐵”〉 ++ 〈“𝐶”〉) | ||
Definition | df-s4 14214 | Define the length 4 word constructor. (Contributed by Mario Carneiro, 26-Feb-2016.) |
⊢ 〈“𝐴𝐵𝐶𝐷”〉 = (〈“𝐴𝐵𝐶”〉 ++ 〈“𝐷”〉) | ||
Definition | df-s5 14215 | Define the length 5 word constructor. (Contributed by Mario Carneiro, 26-Feb-2016.) |
⊢ 〈“𝐴𝐵𝐶𝐷𝐸”〉 = (〈“𝐴𝐵𝐶𝐷”〉 ++ 〈“𝐸”〉) | ||
Definition | df-s6 14216 | Define the length 6 word constructor. (Contributed by Mario Carneiro, 26-Feb-2016.) |
⊢ 〈“𝐴𝐵𝐶𝐷𝐸𝐹”〉 = (〈“𝐴𝐵𝐶𝐷𝐸”〉 ++ 〈“𝐹”〉) | ||
Definition | df-s7 14217 | Define the length 7 word constructor. (Contributed by Mario Carneiro, 26-Feb-2016.) |
⊢ 〈“𝐴𝐵𝐶𝐷𝐸𝐹𝐺”〉 = (〈“𝐴𝐵𝐶𝐷𝐸𝐹”〉 ++ 〈“𝐺”〉) | ||
Definition | df-s8 14218 | Define the length 8 word constructor. (Contributed by Mario Carneiro, 26-Feb-2016.) |
⊢ 〈“𝐴𝐵𝐶𝐷𝐸𝐹𝐺𝐻”〉 = (〈“𝐴𝐵𝐶𝐷𝐸𝐹𝐺”〉 ++ 〈“𝐻”〉) | ||
Theorem | cats1cld 14219 | Closure of concatenation with a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016.) |
⊢ 𝑇 = (𝑆 ++ 〈“𝑋”〉) & ⊢ (𝜑 → 𝑆 ∈ Word 𝐴) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) ⇒ ⊢ (𝜑 → 𝑇 ∈ Word 𝐴) | ||
Theorem | cats1co 14220 | Closure of concatenation with a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016.) |
⊢ 𝑇 = (𝑆 ++ 〈“𝑋”〉) & ⊢ (𝜑 → 𝑆 ∈ Word 𝐴) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) & ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → (𝐹 ∘ 𝑆) = 𝑈) & ⊢ 𝑉 = (𝑈 ++ 〈“(𝐹‘𝑋)”〉) ⇒ ⊢ (𝜑 → (𝐹 ∘ 𝑇) = 𝑉) | ||
Theorem | cats1cli 14221 | Closure of concatenation with a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016.) |
⊢ 𝑇 = (𝑆 ++ 〈“𝑋”〉) & ⊢ 𝑆 ∈ Word V ⇒ ⊢ 𝑇 ∈ Word V | ||
Theorem | cats1fvn 14222 | The last symbol of a concatenation with a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016.) |
⊢ 𝑇 = (𝑆 ++ 〈“𝑋”〉) & ⊢ 𝑆 ∈ Word V & ⊢ (♯‘𝑆) = 𝑀 ⇒ ⊢ (𝑋 ∈ 𝑉 → (𝑇‘𝑀) = 𝑋) | ||
Theorem | cats1fv 14223 | 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 14224 | The length of concatenation with a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016.) |
⊢ 𝑇 = (𝑆 ++ 〈“𝑋”〉) & ⊢ 𝑆 ∈ Word V & ⊢ (♯‘𝑆) = 𝑀 & ⊢ (𝑀 + 1) = 𝑁 ⇒ ⊢ (♯‘𝑇) = 𝑁 | ||
Theorem | cats1cat 14225 | Closure of concatenation with a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016.) |
⊢ 𝑇 = (𝑆 ++ 〈“𝑋”〉) & ⊢ 𝐴 ∈ Word V & ⊢ 𝑆 ∈ Word V & ⊢ 𝐶 = (𝐵 ++ 〈“𝑋”〉) & ⊢ 𝐵 = (𝐴 ++ 𝑆) ⇒ ⊢ 𝐶 = (𝐴 ++ 𝑇) | ||
Theorem | cats2cat 14226 | Closure of concatenation of concatenations with singleton words. (Contributed by AV, 1-Mar-2021.) |
⊢ 𝐵 ∈ Word V & ⊢ 𝐷 ∈ Word V & ⊢ 𝐴 = (𝐵 ++ 〈“𝑋”〉) & ⊢ 𝐶 = (〈“𝑌”〉 ++ 𝐷) ⇒ ⊢ (𝐴 ++ 𝐶) = ((𝐵 ++ 〈“𝑋𝑌”〉) ++ 𝐷) | ||
Theorem | s2eqd 14227 | Equality theorem for a doubleton word. (Contributed by Mario Carneiro, 27-Feb-2016.) |
⊢ (𝜑 → 𝐴 = 𝑁) & ⊢ (𝜑 → 𝐵 = 𝑂) ⇒ ⊢ (𝜑 → 〈“𝐴𝐵”〉 = 〈“𝑁𝑂”〉) | ||
Theorem | s3eqd 14228 | Equality theorem for a length 3 word. (Contributed by Mario Carneiro, 27-Feb-2016.) |
⊢ (𝜑 → 𝐴 = 𝑁) & ⊢ (𝜑 → 𝐵 = 𝑂) & ⊢ (𝜑 → 𝐶 = 𝑃) ⇒ ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉 = 〈“𝑁𝑂𝑃”〉) | ||
Theorem | s4eqd 14229 | Equality theorem for a length 4 word. (Contributed by Mario Carneiro, 27-Feb-2016.) |
⊢ (𝜑 → 𝐴 = 𝑁) & ⊢ (𝜑 → 𝐵 = 𝑂) & ⊢ (𝜑 → 𝐶 = 𝑃) & ⊢ (𝜑 → 𝐷 = 𝑄) ⇒ ⊢ (𝜑 → 〈“𝐴𝐵𝐶𝐷”〉 = 〈“𝑁𝑂𝑃𝑄”〉) | ||
Theorem | s5eqd 14230 | Equality theorem for a length 5 word. (Contributed by Mario Carneiro, 27-Feb-2016.) |
⊢ (𝜑 → 𝐴 = 𝑁) & ⊢ (𝜑 → 𝐵 = 𝑂) & ⊢ (𝜑 → 𝐶 = 𝑃) & ⊢ (𝜑 → 𝐷 = 𝑄) & ⊢ (𝜑 → 𝐸 = 𝑅) ⇒ ⊢ (𝜑 → 〈“𝐴𝐵𝐶𝐷𝐸”〉 = 〈“𝑁𝑂𝑃𝑄𝑅”〉) | ||
Theorem | s6eqd 14231 | Equality theorem for a length 6 word. (Contributed by Mario Carneiro, 27-Feb-2016.) |
⊢ (𝜑 → 𝐴 = 𝑁) & ⊢ (𝜑 → 𝐵 = 𝑂) & ⊢ (𝜑 → 𝐶 = 𝑃) & ⊢ (𝜑 → 𝐷 = 𝑄) & ⊢ (𝜑 → 𝐸 = 𝑅) & ⊢ (𝜑 → 𝐹 = 𝑆) ⇒ ⊢ (𝜑 → 〈“𝐴𝐵𝐶𝐷𝐸𝐹”〉 = 〈“𝑁𝑂𝑃𝑄𝑅𝑆”〉) | ||
Theorem | s7eqd 14232 | Equality theorem for a length 7 word. (Contributed by Mario Carneiro, 27-Feb-2016.) |
⊢ (𝜑 → 𝐴 = 𝑁) & ⊢ (𝜑 → 𝐵 = 𝑂) & ⊢ (𝜑 → 𝐶 = 𝑃) & ⊢ (𝜑 → 𝐷 = 𝑄) & ⊢ (𝜑 → 𝐸 = 𝑅) & ⊢ (𝜑 → 𝐹 = 𝑆) & ⊢ (𝜑 → 𝐺 = 𝑇) ⇒ ⊢ (𝜑 → 〈“𝐴𝐵𝐶𝐷𝐸𝐹𝐺”〉 = 〈“𝑁𝑂𝑃𝑄𝑅𝑆𝑇”〉) | ||
Theorem | s8eqd 14233 | Equality theorem for a length 8 word. (Contributed by Mario Carneiro, 27-Feb-2016.) |
⊢ (𝜑 → 𝐴 = 𝑁) & ⊢ (𝜑 → 𝐵 = 𝑂) & ⊢ (𝜑 → 𝐶 = 𝑃) & ⊢ (𝜑 → 𝐷 = 𝑄) & ⊢ (𝜑 → 𝐸 = 𝑅) & ⊢ (𝜑 → 𝐹 = 𝑆) & ⊢ (𝜑 → 𝐺 = 𝑇) & ⊢ (𝜑 → 𝐻 = 𝑈) ⇒ ⊢ (𝜑 → 〈“𝐴𝐵𝐶𝐷𝐸𝐹𝐺𝐻”〉 = 〈“𝑁𝑂𝑃𝑄𝑅𝑆𝑇𝑈”〉) | ||
Theorem | s3eq2 14234 | Equality theorem for a length 3 word for the second symbol. (Contributed by AV, 4-Jan-2022.) |
⊢ (𝐵 = 𝐷 → 〈“𝐴𝐵𝐶”〉 = 〈“𝐴𝐷𝐶”〉) | ||
Theorem | s2cld 14235 | A doubleton word is a word. (Contributed by Mario Carneiro, 27-Feb-2016.) |
⊢ (𝜑 → 𝐴 ∈ 𝑋) & ⊢ (𝜑 → 𝐵 ∈ 𝑋) ⇒ ⊢ (𝜑 → 〈“𝐴𝐵”〉 ∈ Word 𝑋) | ||
Theorem | s3cld 14236 | A length 3 string is a word. (Contributed by Mario Carneiro, 27-Feb-2016.) |
⊢ (𝜑 → 𝐴 ∈ 𝑋) & ⊢ (𝜑 → 𝐵 ∈ 𝑋) & ⊢ (𝜑 → 𝐶 ∈ 𝑋) ⇒ ⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉 ∈ Word 𝑋) | ||
Theorem | s4cld 14237 | A length 4 string is a word. (Contributed by Mario Carneiro, 27-Feb-2016.) |
⊢ (𝜑 → 𝐴 ∈ 𝑋) & ⊢ (𝜑 → 𝐵 ∈ 𝑋) & ⊢ (𝜑 → 𝐶 ∈ 𝑋) & ⊢ (𝜑 → 𝐷 ∈ 𝑋) ⇒ ⊢ (𝜑 → 〈“𝐴𝐵𝐶𝐷”〉 ∈ Word 𝑋) | ||
Theorem | s5cld 14238 | A length 5 string is a word. (Contributed by Mario Carneiro, 27-Feb-2016.) |
⊢ (𝜑 → 𝐴 ∈ 𝑋) & ⊢ (𝜑 → 𝐵 ∈ 𝑋) & ⊢ (𝜑 → 𝐶 ∈ 𝑋) & ⊢ (𝜑 → 𝐷 ∈ 𝑋) & ⊢ (𝜑 → 𝐸 ∈ 𝑋) ⇒ ⊢ (𝜑 → 〈“𝐴𝐵𝐶𝐷𝐸”〉 ∈ Word 𝑋) | ||
Theorem | s6cld 14239 | A length 6 string is a word. (Contributed by Mario Carneiro, 27-Feb-2016.) |
⊢ (𝜑 → 𝐴 ∈ 𝑋) & ⊢ (𝜑 → 𝐵 ∈ 𝑋) & ⊢ (𝜑 → 𝐶 ∈ 𝑋) & ⊢ (𝜑 → 𝐷 ∈ 𝑋) & ⊢ (𝜑 → 𝐸 ∈ 𝑋) & ⊢ (𝜑 → 𝐹 ∈ 𝑋) ⇒ ⊢ (𝜑 → 〈“𝐴𝐵𝐶𝐷𝐸𝐹”〉 ∈ Word 𝑋) | ||
Theorem | s7cld 14240 | A length 7 string is a word. (Contributed by Mario Carneiro, 27-Feb-2016.) |
⊢ (𝜑 → 𝐴 ∈ 𝑋) & ⊢ (𝜑 → 𝐵 ∈ 𝑋) & ⊢ (𝜑 → 𝐶 ∈ 𝑋) & ⊢ (𝜑 → 𝐷 ∈ 𝑋) & ⊢ (𝜑 → 𝐸 ∈ 𝑋) & ⊢ (𝜑 → 𝐹 ∈ 𝑋) & ⊢ (𝜑 → 𝐺 ∈ 𝑋) ⇒ ⊢ (𝜑 → 〈“𝐴𝐵𝐶𝐷𝐸𝐹𝐺”〉 ∈ Word 𝑋) | ||
Theorem | s8cld 14241 | A length 7 string is a word. (Contributed by Mario Carneiro, 27-Feb-2016.) |
⊢ (𝜑 → 𝐴 ∈ 𝑋) & ⊢ (𝜑 → 𝐵 ∈ 𝑋) & ⊢ (𝜑 → 𝐶 ∈ 𝑋) & ⊢ (𝜑 → 𝐷 ∈ 𝑋) & ⊢ (𝜑 → 𝐸 ∈ 𝑋) & ⊢ (𝜑 → 𝐹 ∈ 𝑋) & ⊢ (𝜑 → 𝐺 ∈ 𝑋) & ⊢ (𝜑 → 𝐻 ∈ 𝑋) ⇒ ⊢ (𝜑 → 〈“𝐴𝐵𝐶𝐷𝐸𝐹𝐺𝐻”〉 ∈ Word 𝑋) | ||
Theorem | s2cl 14242 | A doubleton word is a word. (Contributed by Stefan O'Rear, 23-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.) |
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → 〈“𝐴𝐵”〉 ∈ Word 𝑋) | ||
Theorem | s3cl 14243 | A length 3 string is a word. (Contributed by Mario Carneiro, 26-Feb-2016.) |
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋) → 〈“𝐴𝐵𝐶”〉 ∈ Word 𝑋) | ||
Theorem | s2cli 14244 | A doubleton word is a word. (Contributed by Mario Carneiro, 26-Feb-2016.) |
⊢ 〈“𝐴𝐵”〉 ∈ Word V | ||
Theorem | s3cli 14245 | A length 3 string is a word. (Contributed by Mario Carneiro, 26-Feb-2016.) |
⊢ 〈“𝐴𝐵𝐶”〉 ∈ Word V | ||
Theorem | s4cli 14246 | A length 4 string is a word. (Contributed by Mario Carneiro, 26-Feb-2016.) |
⊢ 〈“𝐴𝐵𝐶𝐷”〉 ∈ Word V | ||
Theorem | s5cli 14247 | A length 5 string is a word. (Contributed by Mario Carneiro, 26-Feb-2016.) |
⊢ 〈“𝐴𝐵𝐶𝐷𝐸”〉 ∈ Word V | ||
Theorem | s6cli 14248 | A length 6 string is a word. (Contributed by Mario Carneiro, 26-Feb-2016.) |
⊢ 〈“𝐴𝐵𝐶𝐷𝐸𝐹”〉 ∈ Word V | ||
Theorem | s7cli 14249 | A length 7 string is a word. (Contributed by Mario Carneiro, 26-Feb-2016.) |
⊢ 〈“𝐴𝐵𝐶𝐷𝐸𝐹𝐺”〉 ∈ Word V | ||
Theorem | s8cli 14250 | A length 8 string is a word. (Contributed by Mario Carneiro, 26-Feb-2016.) |
⊢ 〈“𝐴𝐵𝐶𝐷𝐸𝐹𝐺𝐻”〉 ∈ Word V | ||
Theorem | s2fv0 14251 | 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 14252 | 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 14253 | The length of a doubleton word. (Contributed by Stefan O'Rear, 23-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.) |
⊢ (♯‘〈“𝐴𝐵”〉) = 2 | ||
Theorem | s2dm 14254 | The domain of a doubleton word is an unordered pair. (Contributed by AV, 9-Jan-2020.) |
⊢ dom 〈“𝐴𝐵”〉 = {0, 1} | ||
Theorem | s3fv0 14255 | Extract the first symbol from a length 3 string. (Contributed by Mario Carneiro, 13-Jan-2017.) |
⊢ (𝐴 ∈ 𝑉 → (〈“𝐴𝐵𝐶”〉‘0) = 𝐴) | ||
Theorem | s3fv1 14256 | Extract the second symbol from a length 3 string. (Contributed by Mario Carneiro, 13-Jan-2017.) |
⊢ (𝐵 ∈ 𝑉 → (〈“𝐴𝐵𝐶”〉‘1) = 𝐵) | ||
Theorem | s3fv2 14257 | Extract the third symbol from a length 3 string. (Contributed by Mario Carneiro, 13-Jan-2017.) |
⊢ (𝐶 ∈ 𝑉 → (〈“𝐴𝐵𝐶”〉‘2) = 𝐶) | ||
Theorem | s3len 14258 | The length of a length 3 string. (Contributed by Mario Carneiro, 26-Feb-2016.) |
⊢ (♯‘〈“𝐴𝐵𝐶”〉) = 3 | ||
Theorem | s4fv0 14259 | Extract the first symbol from a length 4 string. (Contributed by Thierry Arnoux, 8-Oct-2020.) |
⊢ (𝐴 ∈ 𝑉 → (〈“𝐴𝐵𝐶𝐷”〉‘0) = 𝐴) | ||
Theorem | s4fv1 14260 | Extract the second symbol from a length 4 string. (Contributed by Thierry Arnoux, 8-Oct-2020.) |
⊢ (𝐵 ∈ 𝑉 → (〈“𝐴𝐵𝐶𝐷”〉‘1) = 𝐵) | ||
Theorem | s4fv2 14261 | Extract the third symbol from a length 4 string. (Contributed by Thierry Arnoux, 8-Oct-2020.) |
⊢ (𝐶 ∈ 𝑉 → (〈“𝐴𝐵𝐶𝐷”〉‘2) = 𝐶) | ||
Theorem | s4fv3 14262 | Extract the fourth symbol from a length 4 string. (Contributed by Thierry Arnoux, 8-Oct-2020.) |
⊢ (𝐷 ∈ 𝑉 → (〈“𝐴𝐵𝐶𝐷”〉‘3) = 𝐷) | ||
Theorem | s4len 14263 | The length of a length 4 string. (Contributed by Mario Carneiro, 26-Feb-2016.) |
⊢ (♯‘〈“𝐴𝐵𝐶𝐷”〉) = 4 | ||
Theorem | s5len 14264 | The length of a length 5 string. (Contributed by Mario Carneiro, 26-Feb-2016.) |
⊢ (♯‘〈“𝐴𝐵𝐶𝐷𝐸”〉) = 5 | ||
Theorem | s6len 14265 | The length of a length 6 string. (Contributed by Mario Carneiro, 26-Feb-2016.) |
⊢ (♯‘〈“𝐴𝐵𝐶𝐷𝐸𝐹”〉) = 6 | ||
Theorem | s7len 14266 | The length of a length 7 string. (Contributed by Mario Carneiro, 26-Feb-2016.) |
⊢ (♯‘〈“𝐴𝐵𝐶𝐷𝐸𝐹𝐺”〉) = 7 | ||
Theorem | s8len 14267 | The length of a length 8 string. (Contributed by Mario Carneiro, 26-Feb-2016.) |
⊢ (♯‘〈“𝐴𝐵𝐶𝐷𝐸𝐹𝐺𝐻”〉) = 8 | ||
Theorem | lsws2 14268 | The last symbol of a doubleton word is its second symbol. (Contributed by AV, 8-Feb-2021.) |
⊢ (𝐵 ∈ 𝑉 → (lastS‘〈“𝐴𝐵”〉) = 𝐵) | ||
Theorem | lsws3 14269 | The last symbol of a 3 letter word is its third symbol. (Contributed by AV, 8-Feb-2021.) |
⊢ (𝐶 ∈ 𝑉 → (lastS‘〈“𝐴𝐵𝐶”〉) = 𝐶) | ||
Theorem | lsws4 14270 | The last symbol of a 4 letter word is its fourth symbol. (Contributed by AV, 8-Feb-2021.) |
⊢ (𝐷 ∈ 𝑉 → (lastS‘〈“𝐴𝐵𝐶𝐷”〉) = 𝐷) | ||
Theorem | s2prop 14271 | A length 2 word is an unordered pair of ordered pairs. (Contributed by Alexander van der Vekens, 14-Aug-2017.) |
⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → 〈“𝐴𝐵”〉 = {〈0, 𝐴〉, 〈1, 𝐵〉}) | ||
Theorem | s2dmALT 14272 | Alternate version of s2dm 14254, having a shorter proof, but requiring that 𝐴 and 𝐵 are sets. (Contributed by AV, 9-Jan-2020.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → dom 〈“𝐴𝐵”〉 = {0, 1}) | ||
Theorem | s3tpop 14273 | A length 3 word is an unordered triple of ordered pairs. (Contributed by AV, 23-Jan-2021.) |
⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) → 〈“𝐴𝐵𝐶”〉 = {〈0, 𝐴〉, 〈1, 𝐵〉, 〈2, 𝐶〉}) | ||
Theorem | s4prop 14274 | A length 4 word is a union of two unordered pairs of ordered pairs. (Contributed by Alexander van der Vekens, 14-Aug-2017.) |
⊢ (((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) → 〈“𝐴𝐵𝐶𝐷”〉 = ({〈0, 𝐴〉, 〈1, 𝐵〉} ∪ {〈2, 𝐶〉, 〈3, 𝐷〉})) | ||
Theorem | s3fn 14275 | A length 3 word is a function with a triple as domain. (Contributed by Alexander van der Vekens, 5-Dec-2017.) (Revised by AV, 23-Jan-2021.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → 〈“𝐴𝐵𝐶”〉 Fn {0, 1, 2}) | ||
Theorem | funcnvs1 14276 | The converse of a singleton word is a function. (Contributed by AV, 22-Jan-2021.) |
⊢ Fun ◡〈“𝐴”〉 | ||
Theorem | funcnvs2 14277 | The converse of a length 2 word is a function if its symbols are different sets. (Contributed by AV, 23-Jan-2021.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐴 ≠ 𝐵) → Fun ◡〈“𝐴𝐵”〉) | ||
Theorem | funcnvs3 14278 | The converse of a length 3 word is a function if its symbols are different sets. (Contributed by Alexander van der Vekens, 31-Jan-2018.) (Revised by AV, 23-Jan-2021.) |
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ (𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶)) → Fun ◡〈“𝐴𝐵𝐶”〉) | ||
Theorem | funcnvs4 14279 | The converse of a length 4 word is a function if its symbols are different sets. (Contributed by AV, 10-Feb-2021.) |
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉)) ∧ ((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷) ∧ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷) ∧ 𝐶 ≠ 𝐷)) → Fun ◡〈“𝐴𝐵𝐶𝐷”〉) | ||
Theorem | s2f1o 14280 | A length 2 word with mutually different symbols is a one-to-one function onto the set of the symbols. (Contributed by Alexander van der Vekens, 14-Aug-2017.) |
⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐴 ≠ 𝐵) → (𝐸 = 〈“𝐴𝐵”〉 → 𝐸:{0, 1}–1-1-onto→{𝐴, 𝐵})) | ||
Theorem | f1oun2prg 14281 | A union of unordered pairs of ordered pairs with different elements is a one-to-one onto function. (Contributed by Alexander van der Vekens, 14-Aug-2017.) |
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌)) → (((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷) ∧ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷)) → ({〈0, 𝐴〉, 〈1, 𝐵〉} ∪ {〈2, 𝐶〉, 〈3, 𝐷〉}):({0, 1} ∪ {2, 3})–1-1-onto→({𝐴, 𝐵} ∪ {𝐶, 𝐷}))) | ||
Theorem | s4f1o 14282 | A length 4 word with mutually different symbols is a one-to-one function onto the set of the symbols. (Contributed by Alexander van der Vekens, 14-Aug-2017.) |
⊢ (((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) → (((𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐴 ≠ 𝐷) ∧ (𝐵 ≠ 𝐶 ∧ 𝐵 ≠ 𝐷 ∧ 𝐶 ≠ 𝐷)) → (𝐸 = 〈“𝐴𝐵𝐶𝐷”〉 → 𝐸:dom 𝐸–1-1-onto→({𝐴, 𝐵} ∪ {𝐶, 𝐷})))) | ||
Theorem | s4dom 14283 | The domain of a length 4 word is the union of two (disjunct) pairs. (Contributed by Alexander van der Vekens, 15-Aug-2017.) |
⊢ (((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑆 ∧ 𝐷 ∈ 𝑆)) → (𝐸 = 〈“𝐴𝐵𝐶𝐷”〉 → dom 𝐸 = ({0, 1} ∪ {2, 3}))) | ||
Theorem | s2co 14284 | Mapping a doubleton word by a function. (Contributed by Mario Carneiro, 27-Feb-2016.) |
⊢ (𝜑 → 𝐹:𝑋⟶𝑌) & ⊢ (𝜑 → 𝐴 ∈ 𝑋) & ⊢ (𝜑 → 𝐵 ∈ 𝑋) ⇒ ⊢ (𝜑 → (𝐹 ∘ 〈“𝐴𝐵”〉) = 〈“(𝐹‘𝐴)(𝐹‘𝐵)”〉) | ||
Theorem | s3co 14285 | Mapping a length 3 string by a function. (Contributed by Mario Carneiro, 27-Feb-2016.) |
⊢ (𝜑 → 𝐹:𝑋⟶𝑌) & ⊢ (𝜑 → 𝐴 ∈ 𝑋) & ⊢ (𝜑 → 𝐵 ∈ 𝑋) & ⊢ (𝜑 → 𝐶 ∈ 𝑋) ⇒ ⊢ (𝜑 → (𝐹 ∘ 〈“𝐴𝐵𝐶”〉) = 〈“(𝐹‘𝐴)(𝐹‘𝐵)(𝐹‘𝐶)”〉) | ||
Theorem | s0s1 14286 | Concatenation of fixed length strings. (This special case of ccatlid 13942 is provided to complete the pattern s0s1 14286, df-s2 14212, df-s3 14213, ...) (Contributed by Mario Carneiro, 28-Feb-2016.) |
⊢ 〈“𝐴”〉 = (∅ ++ 〈“𝐴”〉) | ||
Theorem | s1s2 14287 | Concatenation of fixed length strings. (Contributed by Mario Carneiro, 26-Feb-2016.) |
⊢ 〈“𝐴𝐵𝐶”〉 = (〈“𝐴”〉 ++ 〈“𝐵𝐶”〉) | ||
Theorem | s1s3 14288 | Concatenation of fixed length strings. (Contributed by Mario Carneiro, 26-Feb-2016.) |
⊢ 〈“𝐴𝐵𝐶𝐷”〉 = (〈“𝐴”〉 ++ 〈“𝐵𝐶𝐷”〉) | ||
Theorem | s1s4 14289 | Concatenation of fixed length strings. (Contributed by Mario Carneiro, 26-Feb-2016.) |
⊢ 〈“𝐴𝐵𝐶𝐷𝐸”〉 = (〈“𝐴”〉 ++ 〈“𝐵𝐶𝐷𝐸”〉) | ||
Theorem | s1s5 14290 | Concatenation of fixed length strings. (Contributed by Mario Carneiro, 26-Feb-2016.) |
⊢ 〈“𝐴𝐵𝐶𝐷𝐸𝐹”〉 = (〈“𝐴”〉 ++ 〈“𝐵𝐶𝐷𝐸𝐹”〉) | ||
Theorem | s1s6 14291 | Concatenation of fixed length strings. (Contributed by Mario Carneiro, 26-Feb-2016.) |
⊢ 〈“𝐴𝐵𝐶𝐷𝐸𝐹𝐺”〉 = (〈“𝐴”〉 ++ 〈“𝐵𝐶𝐷𝐸𝐹𝐺”〉) | ||
Theorem | s1s7 14292 | Concatenation of fixed length strings. (Contributed by Mario Carneiro, 26-Feb-2016.) |
⊢ 〈“𝐴𝐵𝐶𝐷𝐸𝐹𝐺𝐻”〉 = (〈“𝐴”〉 ++ 〈“𝐵𝐶𝐷𝐸𝐹𝐺𝐻”〉) | ||
Theorem | s2s2 14293 | Concatenation of fixed length strings. (Contributed by Mario Carneiro, 26-Feb-2016.) |
⊢ 〈“𝐴𝐵𝐶𝐷”〉 = (〈“𝐴𝐵”〉 ++ 〈“𝐶𝐷”〉) | ||
Theorem | s4s2 14294 | Concatenation of fixed length strings. (Contributed by Mario Carneiro, 26-Feb-2016.) |
⊢ 〈“𝐴𝐵𝐶𝐷𝐸𝐹”〉 = (〈“𝐴𝐵𝐶𝐷”〉 ++ 〈“𝐸𝐹”〉) | ||
Theorem | s4s3 14295 | Concatenation of fixed length strings. (Contributed by Mario Carneiro, 26-Feb-2016.) |
⊢ 〈“𝐴𝐵𝐶𝐷𝐸𝐹𝐺”〉 = (〈“𝐴𝐵𝐶𝐷”〉 ++ 〈“𝐸𝐹𝐺”〉) | ||
Theorem | s4s4 14296 | Concatenation of fixed length strings. (Contributed by Mario Carneiro, 26-Feb-2016.) |
⊢ 〈“𝐴𝐵𝐶𝐷𝐸𝐹𝐺𝐻”〉 = (〈“𝐴𝐵𝐶𝐷”〉 ++ 〈“𝐸𝐹𝐺𝐻”〉) | ||
Theorem | s3s4 14297 | Concatenation of fixed length strings. (Contributed by AV, 1-Mar-2021.) |
⊢ 〈“𝐴𝐵𝐶𝐷𝐸𝐹𝐺”〉 = (〈“𝐴𝐵𝐶”〉 ++ 〈“𝐷𝐸𝐹𝐺”〉) | ||
Theorem | s2s5 14298 | Concatenation of fixed length strings. (Contributed by AV, 1-Mar-2021.) |
⊢ 〈“𝐴𝐵𝐶𝐷𝐸𝐹𝐺”〉 = (〈“𝐴𝐵”〉 ++ 〈“𝐶𝐷𝐸𝐹𝐺”〉) | ||
Theorem | s5s2 14299 | Concatenation of fixed length strings. (Contributed by AV, 1-Mar-2021.) |
⊢ 〈“𝐴𝐵𝐶𝐷𝐸𝐹𝐺”〉 = (〈“𝐴𝐵𝐶𝐷𝐸”〉 ++ 〈“𝐹𝐺”〉) | ||
Theorem | s2eq2s1eq 14300 | Two length 2 words are equal iff the corresponding singleton words consisting of their symbols are equal. (Contributed by Alexander van der Vekens, 24-Sep-2018.) |
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉)) → (〈“𝐴𝐵”〉 = 〈“𝐶𝐷”〉 ↔ (〈“𝐴”〉 = 〈“𝐶”〉 ∧ 〈“𝐵”〉 = 〈“𝐷”〉))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |