P. 134 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 13301-13400   *Has distinct variable group(s)

Type	Label	Description
Statement
Definition	df-concat 13301*	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.)
|- ++ = ( s e. _V , t e. _V |-> ( x e. ( 0..^ ( ( # ` s ) + ( # ` t ) ) ) |-> if ( x e. ( 0..^ ( # ` s ) ) , ( s ` x ) , ( t ` ( x - ( # ` s ) ) ) ) ) )
Definition	df-s1 13302	Define the canonical injection from symbols to words. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.)
|- <" A "> = { <. 0 , ( _I ` A ) >. }
Definition	df-substr 13303*	Define an operation which extracts portions of words. Definition in section 9.1 of [AhoHopUll] p. 318. (Contributed by Stefan O'Rear, 15-Aug-2015.)
|- substr = ( s e. _V , b e. ( ZZ X. ZZ ) |-> if ( ( ( 1st ` b )..^ ( 2nd ` b ) ) C_ dom s , ( x e. ( 0..^ ( ( 2nd ` b ) - ( 1st ` b ) ) ) |-> ( s ` ( x + ( 1st ` b ) ) ) ) , (/) ) )
Definition	df-splice 13304*	Define an operation which replaces portions of words. (Contributed by Stefan O'Rear, 15-Aug-2015.)
|- splice = ( s e. _V , b e. _V |-> ( ( ( s substr <. 0 , ( 1st ` ( 1st ` b ) ) >. ) ++ ( 2nd ` b ) ) ++ ( s substr <. ( 2nd ` ( 1st ` b ) ) , ( # ` s ) >. ) ) )
Definition	df-reverse 13305*	Define an operation which reverses the order of symbols in a word. (Contributed by Stefan O'Rear, 26-Aug-2015.)
|- reverse = ( s e. _V |-> ( x e. ( 0..^ ( # ` s ) ) |-> ( s ` ( ( ( # ` s ) - 1 ) - x ) ) ) )
Definition	df-reps 13306*	Definition to construct a word consisting of one repeated symbol, often called "repeated symbol word" for short in the following. (Contributed by Alexander van der Vekens, 4-Nov-2018.)
|- repeatS = ( s e. _V , n e. NN0 |-> ( x e. ( 0..^ n ) |-> s ) )
Theorem	iswrd 13307*	Property of being a word over a set with a quantifier over the length. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.) (Proof shortened by AV, 13-May-2020.)
|- ( W e. Word S <-> E. l e. NN0 W : ( 0..^ l ) --> S )
Theorem	wrdval 13308*	Value of the set of words over a set. (Contributed by Stefan O'Rear, 10-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.)
|- ( S e. V -> Word S = U_ l e. NN0 ( S ^m ( 0..^ l ) ) )
Theorem	iswrdi 13309	A zero-based sequence is a word. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.)
|- ( W : ( 0..^ L ) --> S -> W e. Word S )
Theorem	wrdf 13310	A word is a zero-based sequence with a recoverable upper limit. (Contributed by Stefan O'Rear, 15-Aug-2015.)
|- ( W e. Word S -> W : ( 0..^ ( # ` W ) ) --> S )
Theorem	iswrdb 13311	A word over an alphabet is a function of an open range of nonnegative integers (of length equal to the length of the word) into the alphabet. (Contributed by Alexander van der Vekens, 30-Jul-2018.)
|- ( W e. Word S <-> W : ( 0..^ ( # ` W ) ) --> S )
Theorem	wrddm 13312	The indices of a word (i.e. its domain regarded as function) are elements of an open range of nonnegative integers (of length equal to the length of the word). (Contributed by AV, 2-May-2020.)
|- ( W e. Word S -> dom W = ( 0..^ ( # ` W ) ) )
Theorem	sswrd 13313	The set of words respects ordering on the base set. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.) (Proof shortened by AV, 13-May-2020.)
|- ( S C_ T -> Word S C_ Word T )
Theorem	snopiswrd 13314	A singleton of an ordered pair (with 0 as first component) is a word. (Contributed by AV, 23-Nov-2018.) (Proof shortened by AV, 18-Apr-2021.)
|- ( S e. V -> { <. 0 , S >. } e. Word V )
Theorem	wrdexg 13315	The set of words over a set is a set. (Contributed by Mario Carneiro, 26-Feb-2016.)
|- ( S e. V -> Word S e. _V )
Theorem	wrdexb 13316	The set of words over a set is a set, bidirectional version. (Contributed by Mario Carneiro, 26-Feb-2016.) (Proof shortened by AV, 23-Nov-2018.)
|- ( S e. _V <-> Word S e. _V )
Theorem	wrdexi 13317	The set of words over a set is a set, inference form. (Contributed by AV, 23-May-2021.)
|- S e. _V   =>    |- Word S e. _V
Theorem	wrdsymbcl 13318	A symbol within a word over an alphabet belongs to the alphabet. (Contributed by Alexander van der Vekens, 28-Jun-2018.)
|- ( ( W e. Word V /\ I e. ( 0..^ ( # ` W ) ) ) -> ( W ` I ) e. V )
Theorem	wrdfn 13319	A word is a function with a zero-based sequence of integers as domain. (Contributed by Alexander van der Vekens, 13-Apr-2018.)
|- ( W e. Word S -> W Fn ( 0..^ ( # ` W ) ) )
Theorem	wrdv 13320	A word over an alphabet is a word over the universal class. (Contributed by AV, 8-Feb-2021.)
|- ( W e. Word V -> W e. Word _V )
Theorem	wrdlndm 13321	The length of a word is not in the domain of the word (regarded as function). (Contributed by AV, 3-Mar-2021.)
|- ( W e. Word V -> ( # ` W ) e/ dom W )
Theorem	iswrdsymb 13322*	An arbitrary word is a word over an alphabet if all of its symbols belong to the alphabet. (Contributed by AV, 23-Jan-2021.)
|- ( ( W e. Word _V /\ A. i e. ( 0..^ ( # ` W ) ) ( W ` i ) e. V ) -> W e. Word V )
Theorem	wrdfin 13323	A word is a finite set. (Contributed by Stefan O'Rear, 2-Nov-2015.) (Proof shortened by AV, 18-Nov-2018.)
|- ( W e. Word S -> W e. Fin )
Theorem	lencl 13324	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.)
|- ( W e. Word S -> ( # ` W ) e. NN0 )
Theorem	lennncl 13325	The length of a nonempty word is a positive integer. (Contributed by Mario Carneiro, 1-Oct-2015.)
|- ( ( W e. Word S /\ W =/= (/) ) -> ( # ` W ) e. NN )
Theorem	wrdffz 13326	A word is a function from a finite interval of integers. (Contributed by AV, 10-Feb-2021.)
|- ( W e. Word S -> W : ( 0 ... ( ( # ` W ) - 1 ) ) --> S )
Theorem	wrdeq 13327	Equality theorem for the set of words. (Contributed by Mario Carneiro, 26-Feb-2016.)
|- ( S = T -> Word S = Word T )
Theorem	wrdeqi 13328	Equality theorem for the set of words, inference form. (Contributed by AV, 23-May-2021.)
|- S = T   =>    |- Word S = Word T
Theorem	iswrddm0 13329	A function with empty domain is a word. (Contributed by AV, 13-Oct-2018.)
|- ( W : (/) --> S -> W e. Word S )
Theorem	wrd0 13330	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.)
|- (/) e. Word S
Theorem	0wrd0 13331	The empty word is the only word over an empty alphabet. (Contributed by AV, 25-Oct-2018.)
|- ( W e. Word (/) <-> W = (/) )
Theorem	ffz0iswrd 13332	A sequence with zero-based indices is a word. (Contributed by AV, 31-Jan-2018.) (Proof shortened by AV, 13-Oct-2018.)
|- ( W : ( 0 ... L ) --> S -> W e. Word S )
Theorem	nfwrd 13333	Hypothesis builder for Word S. (Contributed by Mario Carneiro, 26-Feb-2016.)
|- F/_ x S   =>    |- F/_ xWord S
Theorem	csbwrdg 13334*	Class substitution for the symbols of a word. (Contributed by Alexander van der Vekens, 15-Jul-2018.)
|- ( S e. V -> [_ S / x ]_Word x = Word S )
Theorem	wrdnval 13335*	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.)
|- ( ( V e. X /\ N e. NN0 ) -> { w e. Word V | ( # ` w ) = N } = ( V ^m ( 0..^ N ) ) )
Theorem	wrdmap 13336	Words as a mapping. (Contributed by Thierry Arnoux, 4-Mar-2020.)
|- ( ( V e. X /\ N e. NN0 ) -> ( ( W e. Word V /\ ( # ` W ) = N ) <-> W e. ( V ^m ( 0..^ N ) ) ) )
Theorem	hashwrdn 13337*	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.)
|- ( ( V e. Fin /\ N e. NN0 ) -> ( # ` { w e. Word V | ( # ` w ) = N } ) = ( ( # ` V ) ^ N ) )
Theorem	wrdnfi 13338*	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.)
|- ( ( V e. Fin /\ N e. NN0 ) -> { w e. Word V | ( # ` w ) = N } e. Fin )
Theorem	wrdsymb0 13339	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.)
|- ( ( W e. Word V /\ I e. ZZ ) -> ( ( I < 0 \/ ( # ` W ) <_ I ) -> ( W ` I ) = (/) ) )
Theorem	wrdlenge1n0 13340	A word with length at least 1 is not empty. (Contributed by AV, 14-Oct-2018.)
|- ( W e. Word V -> ( W =/= (/) <-> 1 <_ ( # ` W ) ) )
Theorem	wrdlenge2n0 13341	A word with length at least 2 is not empty. (Contributed by AV, 18-Jun-2018.) (Proof shortened by AV, 14-Oct-2018.)
|- ( ( W e. Word V /\ 2 <_ ( # ` W ) ) -> W =/= (/) )
Theorem	wrdsymb1 13342	The first symbol of a nonempty word over an alphabet belongs to the alphabet. (Contributed by Alexander van der Vekens, 28-Jun-2018.)
|- ( ( W e. Word V /\ 1 <_ ( # ` W ) ) -> ( W ` 0 ) e. V )
Theorem	wrdlen1 13343*	A word of length 1 starts with a symbol. (Contributed by AV, 20-Jul-2018.) (Proof shortened by AV, 19-Oct-2018.)
|- ( ( W e. Word V /\ ( # ` W ) = 1 ) -> E. v e. V ( W ` 0 ) = v )
Theorem	fstwrdne 13344	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.)
|- ( ( W e. Word V /\ W =/= (/) ) -> ( W ` 0 ) e. V )
Theorem	fstwrdne0 13345	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.)
|- ( ( N e. NN /\ ( W e. Word V /\ ( # ` W ) = N ) ) -> ( W ` 0 ) e. V )
Theorem	eqwrd 13346*	Two words are equal iff they have the same length and the same symbol at each position. (Contributed by AV, 13-Apr-2018.)
|- ( ( U e. Word V /\ W e. Word V ) -> ( U = W <-> ( ( # ` U ) = ( # ` W ) /\ A. i e. ( 0..^ ( # ` U ) ) ( U ` i ) = ( W ` i ) ) ) )
Theorem	elovmpt2wrd 13347*	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 ph may depend on z as well as on v and y. (Contributed by Alexander van der Vekens, 15-Jul-2018.)
|- O = ( v e. _V , y e. _V |-> { z e. Word v | ph } )   =>    |- ( Z e. ( V O Y ) -> ( V e. _V /\ Y e. _V /\ Z e. Word V ) )
Theorem	elovmptnn0wrd 13348*	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 ph may depend on z as well as on v and y and n. (Contributed by AV, 16-Jul-2018.) (Revised by AV, 16-May-2019.)
|- O = ( v e. _V , y e. _V |-> ( n e. NN0 |-> { z e. Word v | ph } ) )   =>    |- ( Z e. ( ( V O Y ) ` N ) -> ( ( V e. _V /\ Y e. _V ) /\ ( N e. NN0 /\ Z e. Word V ) ) )
Theorem	wrdred1 13349	A word truncated by a symbol is a word. (Contributed by AV, 29-Jan-2021.)
|- ( F e. Word S -> ( F |` ( 0..^ ( ( # ` F ) - 1 ) ) ) e. Word S )
Theorem	wrdred1hash 13350	The length of a word truncated by a symbol. (Contributed by Alexander van der Vekens, 1-Nov-2017.) (Revised by AV, 29-Jan-2021.)
|- ( ( F e. Word S /\ 1 <_ ( # ` F ) ) -> ( # ` ( F |` ( 0..^ ( ( # ` F ) - 1 ) ) ) ) = ( ( # ` F ) - 1 ) )
5.7.2  Last symbol of a word
Theorem	lsw 13351	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.)
|- ( W e. X -> ( lastS ` W ) = ( W ` ( ( # ` W ) - 1 ) ) )
Theorem	lsw0 13352	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.)
|- ( ( W e. Word V /\ ( # ` W ) = 0 ) -> ( lastS ` W ) = (/) )
Theorem	lsw0g 13353	The last symbol of an empty word does not exist. (Contributed by Alexander van der Vekens, 11-Nov-2018.)
|- ( lastS ` (/) ) = (/)
Theorem	lsw1 13354	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.)
|- ( ( W e. Word V /\ ( # ` W ) = 1 ) -> ( lastS ` W ) = ( W ` 0 ) )
Theorem	lswcl 13355	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.)
|- ( ( W e. Word V /\ W =/= (/) ) -> ( lastS ` W ) e. V )
Theorem	lswlgt0cl 13356	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.)
|- ( ( N e. NN /\ ( W e. Word V /\ ( # ` W ) = N ) ) -> ( lastS ` W ) e. V )
5.7.3  Concatenations of words
Theorem	ccatfn 13357	The concatenation operator is a two-argument function. (Contributed by Mario Carneiro, 27-Sep-2015.) (Proof shortened by AV, 29-Apr-2020.)
|- ++ Fn ( _V X. _V )
Theorem	ccatfval 13358*	Value of the concatenation operator. (Contributed by Stefan O'Rear, 15-Aug-2015.)
|- ( ( S e. V /\ T e. W ) -> ( S ++ T ) = ( x e. ( 0..^ ( ( # ` S ) + ( # ` T ) ) ) |-> if ( x e. ( 0..^ ( # ` S ) ) , ( S ` x ) , ( T ` ( x - ( # ` S ) ) ) ) ) )
Theorem	ccatcl 13359	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.)
|- ( ( S e. Word B /\ T e. Word B ) -> ( S ++ T ) e. Word B )
Theorem	ccatlen 13360	The length of a concatenated word. (Contributed by Stefan O'Rear, 15-Aug-2015.)
|- ( ( S e. Word B /\ T e. Word B ) -> ( # ` ( S ++ T ) ) = ( ( # ` S ) + ( # ` T ) ) )
Theorem	ccatval1 13361	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.)
|- ( ( S e. Word B /\ T e. Word B /\ I e. ( 0..^ ( # ` S ) ) ) -> ( ( S ++ T ) ` I ) = ( S ` I ) )
Theorem	ccatval2 13362	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.)
|- ( ( S e. Word B /\ T e. Word B /\ I e. ( ( # ` S )..^ ( ( # ` S ) + ( # ` T ) ) ) ) -> ( ( S ++ T ) ` I ) = ( T ` ( I - ( # ` S ) ) ) )
Theorem	ccatval3 13363	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.)
|- ( ( S e. Word B /\ T e. Word B /\ I e. ( 0..^ ( # ` T ) ) ) -> ( ( S ++ T ) ` ( I + ( # ` S ) ) ) = ( T ` I ) )
Theorem	elfzelfzccat 13364	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.)
|- ( ( A e. Word V /\ B e. Word V ) -> ( N e. ( 0 ... ( # ` A ) ) -> N e. ( 0 ... ( # ` ( A ++ B ) ) ) ) )
Theorem	ccatvalfn 13365	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.)
|- ( ( A e. Word V /\ B e. Word V ) -> ( A ++ B ) Fn ( 0..^ ( ( # ` A ) + ( # ` B ) ) ) )
Theorem	ccatsymb 13366	The symbol at a given position in a concatenated word. (Contributed by AV, 26-May-2018.) (Proof shortened by AV, 24-Nov-2018.)
|- ( ( A e. Word V /\ B e. Word V /\ I e. ZZ ) -> ( ( A ++ B ) ` I ) = if ( I < ( # ` A ) , ( A ` I ) , ( B ` ( I - ( # ` A ) ) ) ) )
Theorem	ccatfv0 13367	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.)
|- ( ( A e. Word V /\ B e. Word V /\ 0 < ( # ` A ) ) -> ( ( A ++ B ) ` 0 ) = ( A ` 0 ) )
Theorem	ccatval1lsw 13368	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.)
|- ( ( A e. Word V /\ B e. Word V /\ A =/= (/) ) -> ( ( A ++ B ) ` ( ( # ` A ) - 1 ) ) = ( lastS ` A ) )
Theorem	ccatlid 13369	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.)
|- ( S e. Word B -> ( (/) ++ S ) = S )
Theorem	ccatrid 13370	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.)
|- ( S e. Word B -> ( S ++ (/) ) = S )
Theorem	ccatass 13371	Associative law for concatenation of words. (Contributed by Stefan O'Rear, 15-Aug-2015.)
|- ( ( S e. Word B /\ T e. Word B /\ U e. Word B ) -> ( ( S ++ T ) ++ U ) = ( S ++ ( T ++ U ) ) )
Theorem	ccatrn 13372	The range of a concatenated word. (Contributed by Stefan O'Rear, 15-Aug-2015.)
|- ( ( S e. Word B /\ T e. Word B ) -> ran ( S ++ T ) = ( ran S u. ran T ) )
Theorem	lswccatn0lsw 13373	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.)
|- ( ( A e. Word V /\ B e. Word V /\ B =/= (/) ) -> ( lastS ` ( A ++ B ) ) = ( lastS ` B ) )
Theorem	lswccat0lsw 13374	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.)
|- ( W e. Word V -> ( lastS ` ( W ++ (/) ) ) = ( lastS ` W ) )
Theorem	ccatalpha 13375	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.)
|- ( ( A e. Word _V /\ B e. Word _V ) -> ( ( A ++ B ) e. Word S <-> ( A e. Word S /\ B e. Word S ) ) )
Theorem	ccatrcl1 13376	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.)
|- ( ( A e. Word X /\ B e. Word Y /\ ( W = ( A ++ B ) /\ W e. Word S ) ) -> A e. Word S )
5.7.4  Singleton words
Theorem	ids1 13377	Identity function protection for a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016.)
|- <" A "> = <" ( _I ` A ) ">
Theorem	s1val 13378	Value of a single-symbol word. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.)
|- ( A e. V -> <" A "> = { <. 0 , A >. } )
Theorem	s1rn 13379	The range of a single-symbol word. (Contributed by Mario Carneiro, 18-Jul-2016.)
|- ( A e. V -> ran <" A "> = { A } )
Theorem	s1eq 13380	Equality theorem for a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016.)
|- ( A = B -> <" A "> = <" B "> )
Theorem	s1eqd 13381	Equality theorem for a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016.)
|- ( ph -> A = B )   =>    |- ( ph -> <" A "> = <" B "> )
Theorem	s1cl 13382	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.)
|- ( A e. B -> <" A "> e. Word B )
Theorem	s1cld 13383	A singleton word is a word. (Contributed by Mario Carneiro, 26-Feb-2016.)
|- ( ph -> A e. B )   =>    |- ( ph -> <" A "> e. Word B )
Theorem	s1cli 13384	A singleton word is a word. (Contributed by Mario Carneiro, 26-Feb-2016.)
|- <" A "> e. Word _V
Theorem	s1len 13385	Length of a singleton word. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.)
|- ( # ` <" A "> ) = 1
Theorem	s1nz 13386	A singleton word is not the empty string. (Contributed by Mario Carneiro, 27-Feb-2016.) (Proof shortened by Kyle Wyonch, 18-Jul-2021.)
|- <" A "> =/= (/)
Theorem	s1nzOLD 13387	Obsolete proof of s1nz 13386 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.)
|- <" A "> =/= (/)
Theorem	s1dm 13388	The domain of a singleton word is a singleton. (Contributed by AV, 9-Jan-2020.)
|- dom <" A "> = { 0 }
Theorem	s1dmALT 13389	Alternate version of s1dm 13388, having a shorter proof, but requiring that A ia a set. (Contributed by AV, 9-Jan-2020.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( A e. S -> dom <" A "> = { 0 } )
Theorem	s1fv 13390	Sole symbol of a singleton word. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.)
|- ( A e. B -> ( <" A "> ` 0 ) = A )
Theorem	lsws1 13391	The last symbol of a singleton word is its symbol. (Contributed by AV, 22-Oct-2018.)
|- ( A e. V -> ( lastS ` <" A "> ) = A )
Theorem	eqs1 13392	A word of length 1 is a singleton word. (Contributed by Stefan O'Rear, 23-Aug-2015.) (Proof shortened by AV, 1-May-2020.)
|- ( ( W e. Word A /\ ( # ` W ) = 1 ) -> W = <" ( W ` 0 ) "> )
Theorem	wrdl1exs1 13393*	A word of length 1 is a singleton word. (Contributed by AV, 24-Jan-2021.)
|- ( ( W e. Word S /\ ( # ` W ) = 1 ) -> E. s e. S W = <" s "> )
Theorem	wrdl1s1 13394	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.)
|- ( S e. V -> ( W = <" S "> <-> ( W e. Word V /\ ( # ` W ) = 1 /\ ( W ` 0 ) = S ) ) )
Theorem	s111 13395	The singleton word function is injective. (Contributed by Mario Carneiro, 1-Oct-2015.) (Revised by Mario Carneiro, 26-Feb-2016.)
|- ( ( S e. A /\ T e. A ) -> ( <" S "> = <" T "> <-> S = T ) )
5.7.5  Concatenations with singleton words
Theorem	ccatws1cl 13396	The concatenation of a word with a singleton word is a word. (Contributed by Alexander van der Vekens, 22-Sep-2018.)
|- ( ( W e. Word V /\ X e. V ) -> ( W ++ <" X "> ) e. Word V )
Theorem	ccat2s1cl 13397	The concatenation of two singleton words is a word. (Contributed by Alexander van der Vekens, 22-Sep-2018.)
|- ( ( X e. V /\ Y e. V ) -> ( <" X "> ++ <" Y "> ) e. Word V )
Theorem	ccatws1len 13398	The length of the concatenation of a word with a singleton word. (Contributed by Alexander van der Vekens, 22-Sep-2018.)
|- ( ( W e. Word V /\ X e. V ) -> ( # ` ( W ++ <" X "> ) ) = ( ( # ` W ) + 1 ) )
Theorem	wrdlenccats1lenm1 13399	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.)
|- ( ( W e. Word V /\ S e. V ) -> ( # ` W ) = ( ( # ` ( W ++ <" S "> ) ) - 1 ) )
Theorem	ccat2s1len 13400	The length of the concatenation of two singleton words. (Contributed by Alexander van der Vekens, 22-Sep-2018.)
|- ( ( X e. V /\ Y e. V ) -> ( # ` ( <" X "> ++ <" Y "> ) ) = 2 )