![]() |
Metamath
Proof Explorer Theorem List (p. 146 of 482) | < 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: | ![]() (1-30715) |
![]() (30716-32238) |
![]() (32239-48161) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | wrdsymbcl 14501 | 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 14502 | 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 14503 | A word over an alphabet is a word over the universal class. (Contributed by AV, 8-Feb-2021.) (Proof shortened by JJ, 18-Nov-2022.) |
β’ (π β Word π β π β Word V) | ||
Theorem | wrdlndm 14504 | The length of a word is not in the domain of the word (regarded as a function). (Contributed by AV, 3-Mar-2021.) (Proof shortened by JJ, 18-Nov-2022.) |
β’ (π β Word π β (β―βπ) β dom π) | ||
Theorem | iswrdsymb 14505* | 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 14506 | 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 14507 | 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 14508 | The length of a nonempty word is a positive integer. (Contributed by Mario Carneiro, 1-Oct-2015.) |
β’ ((π β Word π β§ π β β ) β (β―βπ) β β) | ||
Theorem | wrdffz 14509 | A word is a function from a finite interval of integers. (Contributed by AV, 10-Feb-2021.) |
β’ (π β Word π β π:(0...((β―βπ) β 1))βΆπ) | ||
Theorem | wrdeq 14510 | Equality theorem for the set of words. (Contributed by Mario Carneiro, 26-Feb-2016.) |
β’ (π = π β Word π = Word π) | ||
Theorem | wrdeqi 14511 | Equality theorem for the set of words, inference form. (Contributed by AV, 23-May-2021.) |
β’ π = π β β’ Word π = Word π | ||
Theorem | iswrddm0 14512 | A function with empty domain is a word. (Contributed by AV, 13-Oct-2018.) |
β’ (π:β βΆπ β π β Word π) | ||
Theorem | wrd0 14513 | 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 14514 | The empty word is the only word over an empty alphabet. (Contributed by AV, 25-Oct-2018.) |
β’ (π β Word β β π = β ) | ||
Theorem | ffz0iswrd 14515 | A sequence with zero-based indices is a word. (Contributed by AV, 31-Jan-2018.) (Proof shortened by AV, 13-Oct-2018.) (Proof shortened by JJ, 18-Nov-2022.) |
β’ (π:(0...πΏ)βΆπ β π β Word π) | ||
Theorem | wrdsymb 14516 | A word is a word over the symbols it consists of. (Contributed by AV, 1-Dec-2022.) |
β’ (π β Word π΄ β π β Word (π β (0..^(β―βπ)))) | ||
Theorem | nfwrd 14517 | Hypothesis builder for Word π. (Contributed by Mario Carneiro, 26-Feb-2016.) |
β’ β²π₯π β β’ β²π₯Word π | ||
Theorem | csbwrdg 14518* | Class substitution for the symbols of a word. (Contributed by Alexander van der Vekens, 15-Jul-2018.) |
β’ (π β π β β¦π / π₯β¦Word π₯ = Word π) | ||
Theorem | wrdnval 14519* | 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 π β£ (β―βπ€) = π} = (π βm (0..^π))) | ||
Theorem | wrdmap 14520 | Words as a mapping. (Contributed by Thierry Arnoux, 4-Mar-2020.) |
β’ ((π β π β§ π β β0) β ((π β Word π β§ (β―βπ) = π) β π β (π βm (0..^π)))) | ||
Theorem | hashwrdn 14521* | 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 14522* | 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 | wrdsymb0 14523 | 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 14524 | A word with length at least 1 is not empty. (Contributed by AV, 14-Oct-2018.) |
β’ (π β Word π β (π β β β 1 β€ (β―βπ))) | ||
Theorem | len0nnbi 14525 | The length of a word is a positive integer iff the word is not empty. (Contributed by AV, 22-Mar-2022.) |
β’ (π β Word π β (π β β β (β―βπ) β β)) | ||
Theorem | wrdlenge2n0 14526 | 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 14527 | 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 14528* | 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 14529 | 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 14530 | 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 14531* | 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 14532* | 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 14533* | 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 14534 | A word truncated by a symbol is a word. (Contributed by AV, 29-Jan-2021.) |
β’ (πΉ β Word π β (πΉ βΎ (0..^((β―βπΉ) β 1))) β Word π) | ||
Theorem | wrdred1hash 14535 | 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 14536 | Extend class notation with the Last Symbol of a word. |
class lastS | ||
Definition | df-lsw 14537 | 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 14538 | 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 14539 | 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 14540 | The last symbol of an empty word does not exist. (Contributed by Alexander van der Vekens, 11-Nov-2018.) |
β’ (lastSββ ) = β | ||
Theorem | lsw1 14541 | 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 14542 | 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 14543 | 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 14544 | Syntax for the concatenation operator. |
class ++ | ||
Definition | df-concat 14545* | 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 14546 | 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 14547* | Value of the concatenation operator. (Contributed by Stefan O'Rear, 15-Aug-2015.) |
β’ ((π β π β§ π β π) β (π ++ π) = (π₯ β (0..^((β―βπ) + (β―βπ))) β¦ if(π₯ β (0..^(β―βπ)), (πβπ₯), (πβ(π₯ β (β―βπ)))))) | ||
Theorem | ccatcl 14548 | 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 14549 | The length of a concatenated word. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by JJ, 1-Jan-2024.) |
β’ ((π β Word π΄ β§ π β Word π΅) β (β―β(π ++ π)) = ((β―βπ) + (β―βπ))) | ||
Theorem | ccat0 14550 | 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 14551 | 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 | ccatval2 14552 | 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 14553 | 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 14554 | 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 14555 | 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 14556 | 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 14557 | 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 14558 | 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 14559 | The first symbol of the right (nonempty) half of a concatenated word. (Contributed by AV, 23-Apr-2022.) |
β’ ((π΄ β Word π β§ π΅ β Word π β§ π΅ β β ) β ((π΄ ++ π΅)β(β―βπ΄)) = (π΅β0)) | ||
Theorem | ccatlid 14560 | 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 14561 | 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 14562 | Associative law for concatenation of words. (Contributed by Stefan O'Rear, 15-Aug-2015.) |
β’ ((π β Word π΅ β§ π β Word π΅ β§ π β Word π΅) β ((π ++ π) ++ π) = (π ++ (π ++ π))) | ||
Theorem | ccatrn 14563 | The range of a concatenated word. (Contributed by Stefan O'Rear, 15-Aug-2015.) |
β’ ((π β Word π΅ β§ π β Word π΅) β ran (π ++ π) = (ran π βͺ ran π)) | ||
Theorem | ccatidid 14564 | Concatenation of the empty word by the empty word. (Contributed by AV, 26-Mar-2022.) |
β’ (β ++ β ) = β | ||
Theorem | lswccatn0lsw 14565 | 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 14566 | 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 14567 | 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 14568 | 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 14569 | Syntax for the singleton word constructor. |
class β¨βπ΄ββ© | ||
Definition | df-s1 14570 | 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 14578, and not, as maybe expected, the empty word, see also s1nz 14581. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.) |
β’ β¨βπ΄ββ© = {β¨0, ( I βπ΄)β©} | ||
Theorem | ids1 14571 | Identity function protection for a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016.) |
β’ β¨βπ΄ββ© = β¨β( I βπ΄)ββ© | ||
Theorem | s1val 14572 | Value of a singleton word. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.) |
β’ (π΄ β π β β¨βπ΄ββ© = {β¨0, π΄β©}) | ||
Theorem | s1rn 14573 | The range of a singleton word. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ (π΄ β π β ran β¨βπ΄ββ© = {π΄}) | ||
Theorem | s1eq 14574 | Equality theorem for a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016.) |
β’ (π΄ = π΅ β β¨βπ΄ββ© = β¨βπ΅ββ©) | ||
Theorem | s1eqd 14575 | Equality theorem for a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016.) |
β’ (π β π΄ = π΅) β β’ (π β β¨βπ΄ββ© = β¨βπ΅ββ©) | ||
Theorem | s1cl 14576 | 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 14577 | A singleton word is a word. (Contributed by Mario Carneiro, 26-Feb-2016.) |
β’ (π β π΄ β π΅) β β’ (π β β¨βπ΄ββ© β Word π΅) | ||
Theorem | s1prc 14578 | Value of a singleton word if the symbol is a proper class. (Contributed by AV, 26-Mar-2022.) |
β’ (Β¬ π΄ β V β β¨βπ΄ββ© = β¨ββ ββ©) | ||
Theorem | s1cli 14579 | A singleton word is a word. (Contributed by Mario Carneiro, 26-Feb-2016.) |
β’ β¨βπ΄ββ© β Word V | ||
Theorem | s1len 14580 | Length of a singleton word. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.) |
β’ (β―ββ¨βπ΄ββ©) = 1 | ||
Theorem | s1nz 14581 | 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 14582 | The domain of a singleton word is a singleton. (Contributed by AV, 9-Jan-2020.) |
β’ dom β¨βπ΄ββ© = {0} | ||
Theorem | s1dmALT 14583 | Alternate version of s1dm 14582, 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 14584 | Sole symbol of a singleton word. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.) |
β’ (π΄ β π΅ β (β¨βπ΄ββ©β0) = π΄) | ||
Theorem | lsws1 14585 | The last symbol of a singleton word is its symbol. (Contributed by AV, 22-Oct-2018.) |
β’ (π΄ β π β (lastSββ¨βπ΄ββ©) = π΄) | ||
Theorem | eqs1 14586 | 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 14587* | A word of length 1 is a singleton word. (Contributed by AV, 24-Jan-2021.) |
β’ ((π β Word π β§ (β―βπ) = 1) β βπ β π π = β¨βπ ββ©) | ||
Theorem | wrdl1s1 14588 | 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 14589 | The singleton word function is injective. (Contributed by Mario Carneiro, 1-Oct-2015.) (Revised by Mario Carneiro, 26-Feb-2016.) |
β’ ((π β π΄ β§ π β π΄) β (β¨βπββ© = β¨βπββ© β π = π)) | ||
Theorem | ccatws1cl 14590 | 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 14591 | 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 14592 | The concatenation of two singleton words is a word. (Contributed by Alexander van der Vekens, 22-Sep-2018.) |
β’ ((π β π β§ π β π) β (β¨βπββ© ++ β¨βπββ©) β Word π) | ||
Theorem | ccats1alpha 14593 | 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 14594 | 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 14595 | 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 14596 | 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 14597 | 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 | ccatw2s1cl 14598 | 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 14599 | 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 14600 | 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..^(β―βπ))) β ((π ++ β¨βπββ©)βπΌ) = (πβπΌ)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |