P. 129 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 12801-12900   *Has distinct variable group(s)

Type	Label	Description
Statement
Definition	df-s8 12801	Define the length 8 word constructor. (Contributed by Mario Carneiro, 26-Feb-2016.)
|- <" A B C D E F G H "> = ( <" A B C D E F G "> concat <" H "> )
Theorem	cats1cld 12802	Closure of concatenation with a singleton. (Contributed by Mario Carneiro, 26-Feb-2016.)
|- T = ( S concat <" X "> )   &    |- ( ph -> S e. Word A )   &    |- ( ph -> X e. A )   =>    |- ( ph -> T e. Word A )
Theorem	cats1co 12803	Closure of concatenation with a singleton. (Contributed by Mario Carneiro, 26-Feb-2016.)
|- T = ( S concat <" X "> )   &    |- ( ph -> S e. Word A )   &    |- ( ph -> X e. A )   &    |- ( ph -> F : A --> B )   &    |- ( ph -> ( F o. S ) = U )   &    |- V = ( U concat <" ( F ` X ) "> )   =>    |- ( ph -> ( F o. T ) = V )
Theorem	cats1cli 12804	Closure of concatenation with a singleton. (Contributed by Mario Carneiro, 26-Feb-2016.)
|- T = ( S concat <" X "> )   &    |- S e. Word _V   =>    |- T e. Word _V
Theorem	cats1fvn 12805	The last symbol of a concatenation with a singleton. (Contributed by Mario Carneiro, 26-Feb-2016.)
|- T = ( S concat <" X "> )   &    |- S e. Word _V   &    |- ( # ` S ) = M   =>    |- ( X e. V -> ( T ` M ) = X )
Theorem	cats1fv 12806	A symbol other than the last in a concatenation with a singleton. (Contributed by Mario Carneiro, 26-Feb-2016.)
|- T = ( S concat <" X "> )   &    |- S e. Word _V   &    |- ( # ` S ) = M   &    |- ( Y e. V -> ( S ` N ) = Y )   &    |- N e. NN0   &    |- N < M   =>    |- ( Y e. V -> ( T ` N ) = Y )
Theorem	cats1len 12807	The length of concatenation with a singleton. (Contributed by Mario Carneiro, 26-Feb-2016.)
|- T = ( S concat <" X "> )   &    |- S e. Word _V   &    |- ( # ` S ) = M   &    |- ( M + 1 ) = N   =>    |- ( # ` T ) = N
Theorem	cats1cat 12808	Closure of concatenation with a singleton. (Contributed by Mario Carneiro, 26-Feb-2016.)
|- T = ( S concat <" X "> )   &    |- A e. Word _V   &    |- S e. Word _V   &    |- C = ( B concat <" X "> )   &    |- B = ( A concat S )   =>    |- C = ( A concat T )
Theorem	s2eqd 12809	Equality theorem for a doubleton word. (Contributed by Mario Carneiro, 27-Feb-2016.)
|- ( ph -> A = N )   &    |- ( ph -> B = O )   =>    |- ( ph -> <" A B "> = <" N O "> )
Theorem	s3eqd 12810	Equality theorem for a length 3 word. (Contributed by Mario Carneiro, 27-Feb-2016.)
|- ( ph -> A = N )   &    |- ( ph -> B = O )   &    |- ( ph -> C = P )   =>    |- ( ph -> <" A B C "> = <" N O P "> )
Theorem	s4eqd 12811	Equality theorem for a length 4 word. (Contributed by Mario Carneiro, 27-Feb-2016.)
|- ( ph -> A = N )   &    |- ( ph -> B = O )   &    |- ( ph -> C = P )   &    |- ( ph -> D = Q )   =>    |- ( ph -> <" A B C D "> = <" N O P Q "> )
Theorem	s5eqd 12812	Equality theorem for a length 5 word. (Contributed by Mario Carneiro, 27-Feb-2016.)
|- ( ph -> A = N )   &    |- ( ph -> B = O )   &    |- ( ph -> C = P )   &    |- ( ph -> D = Q )   &    |- ( ph -> E = R )   =>    |- ( ph -> <" A B C D E "> = <" N O P Q R "> )
Theorem	s6eqd 12813	Equality theorem for a length 6 word. (Contributed by Mario Carneiro, 27-Feb-2016.)
|- ( ph -> A = N )   &    |- ( ph -> B = O )   &    |- ( ph -> C = P )   &    |- ( ph -> D = Q )   &    |- ( ph -> E = R )   &    |- ( ph -> F = S )   =>    |- ( ph -> <" A B C D E F "> = <" N O P Q R S "> )
Theorem	s7eqd 12814	Equality theorem for a length 7 word. (Contributed by Mario Carneiro, 27-Feb-2016.)
|- ( ph -> A = N )   &    |- ( ph -> B = O )   &    |- ( ph -> C = P )   &    |- ( ph -> D = Q )   &    |- ( ph -> E = R )   &    |- ( ph -> F = S )   &    |- ( ph -> G = T )   =>    |- ( ph -> <" A B C D E F G "> = <" N O P Q R S T "> )
Theorem	s8eqd 12815	Equality theorem for a length 8 word. (Contributed by Mario Carneiro, 27-Feb-2016.)
|- ( ph -> A = N )   &    |- ( ph -> B = O )   &    |- ( ph -> C = P )   &    |- ( ph -> D = Q )   &    |- ( ph -> E = R )   &    |- ( ph -> F = S )   &    |- ( ph -> G = T )   &    |- ( ph -> H = U )   =>    |- ( ph -> <" A B C D E F G H "> = <" N O P Q R S T U "> )
Theorem	s2cld 12816	A doubleton is a word. (Contributed by Mario Carneiro, 27-Feb-2016.)
|- ( ph -> A e. X )   &    |- ( ph -> B e. X )   =>    |- ( ph -> <" A B "> e. Word X )
Theorem	s3cld 12817	A length 3 string is a word. (Contributed by Mario Carneiro, 27-Feb-2016.)
|- ( ph -> A e. X )   &    |- ( ph -> B e. X )   &    |- ( ph -> C e. X )   =>    |- ( ph -> <" A B C "> e. Word X )
Theorem	s4cld 12818	A length 4 string is a word. (Contributed by Mario Carneiro, 27-Feb-2016.)
|- ( ph -> A e. X )   &    |- ( ph -> B e. X )   &    |- ( ph -> C e. X )   &    |- ( ph -> D e. X )   =>    |- ( ph -> <" A B C D "> e. Word X )
Theorem	s5cld 12819	A length 5 string is a word. (Contributed by Mario Carneiro, 27-Feb-2016.)
|- ( ph -> A e. X )   &    |- ( ph -> B e. X )   &    |- ( ph -> C e. X )   &    |- ( ph -> D e. X )   &    |- ( ph -> E e. X )   =>    |- ( ph -> <" A B C D E "> e. Word X )
Theorem	s6cld 12820	A length 6 string is a word. (Contributed by Mario Carneiro, 27-Feb-2016.)
|- ( ph -> A e. X )   &    |- ( ph -> B e. X )   &    |- ( ph -> C e. X )   &    |- ( ph -> D e. X )   &    |- ( ph -> E e. X )   &    |- ( ph -> F e. X )   =>    |- ( ph -> <" A B C D E F "> e. Word X )
Theorem	s7cld 12821	A length 7 string is a word. (Contributed by Mario Carneiro, 27-Feb-2016.)
|- ( ph -> A e. X )   &    |- ( ph -> B e. X )   &    |- ( ph -> C e. X )   &    |- ( ph -> D e. X )   &    |- ( ph -> E e. X )   &    |- ( ph -> F e. X )   &    |- ( ph -> G e. X )   =>    |- ( ph -> <" A B C D E F G "> e. Word X )
Theorem	s8cld 12822	A length 7 string is a word. (Contributed by Mario Carneiro, 27-Feb-2016.)
|- ( ph -> A e. X )   &    |- ( ph -> B e. X )   &    |- ( ph -> C e. X )   &    |- ( ph -> D e. X )   &    |- ( ph -> E e. X )   &    |- ( ph -> F e. X )   &    |- ( ph -> G e. X )   &    |- ( ph -> H e. X )   =>    |- ( ph -> <" A B C D E F G H "> e. Word X )
Theorem	s2cl 12823	A doubleton is a word. (Contributed by Stefan O'Rear, 23-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.)
|- ( ( A e. X /\ B e. X ) -> <" A B "> e. Word X )
Theorem	s3cl 12824	A length 3 string is a word. (Contributed by Mario Carneiro, 26-Feb-2016.)
|- ( ( A e. X /\ B e. X /\ C e. X ) -> <" A B C "> e. Word X )
Theorem	s2cli 12825	A doubleton is a word. (Contributed by Mario Carneiro, 26-Feb-2016.)
|- <" A B "> e. Word _V
Theorem	s3cli 12826	A length 3 string is a word. (Contributed by Mario Carneiro, 26-Feb-2016.)
|- <" A B C "> e. Word _V
Theorem	s4cli 12827	A length 4 string is a word. (Contributed by Mario Carneiro, 26-Feb-2016.)
|- <" A B C D "> e. Word _V
Theorem	s5cli 12828	A length 5 string is a word. (Contributed by Mario Carneiro, 26-Feb-2016.)
|- <" A B C D E "> e. Word _V
Theorem	s6cli 12829	A length 6 string is a word. (Contributed by Mario Carneiro, 26-Feb-2016.)
|- <" A B C D E F "> e. Word _V
Theorem	s7cli 12830	A length 7 string is a word. (Contributed by Mario Carneiro, 26-Feb-2016.)
|- <" A B C D E F G "> e. Word _V
Theorem	s8cli 12831	A length 8 string is a word. (Contributed by Mario Carneiro, 26-Feb-2016.)
|- <" A B C D E F G H "> e. Word _V
Theorem	s2fv0 12832	Extract the first symbol from a doubleton. (Contributed by Stefan O'Rear, 23-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.)
|- ( A e. V -> ( <" A B "> ` 0 ) = A )
Theorem	s2fv1 12833	Extract the second symbol from a doubleton. (Contributed by Stefan O'Rear, 23-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.)
|- ( B e. V -> ( <" A B "> ` 1 ) = B )
Theorem	s2len 12834	The length of a doubleton. (Contributed by Stefan O'Rear, 23-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.)
|- ( # ` <" A B "> ) = 2
Theorem	s3fv0 12835	Extract the first symbol from a length 3 string. (Contributed by Mario Carneiro, 13-Jan-2017.)
|- ( A e. V -> ( <" A B C "> ` 0 ) = A )
Theorem	s3fv1 12836	Extract the second symbol from a length 3 string. (Contributed by Mario Carneiro, 13-Jan-2017.)
|- ( B e. V -> ( <" A B C "> ` 1 ) = B )
Theorem	s3fv2 12837	Extract the third symbol from a length 3 string. (Contributed by Mario Carneiro, 13-Jan-2017.)
|- ( C e. V -> ( <" A B C "> ` 2 ) = C )
Theorem	s3len 12838	The length of a length 3 string. (Contributed by Mario Carneiro, 26-Feb-2016.)
|- ( # ` <" A B C "> ) = 3
Theorem	s4len 12839	The length of a length 4 string. (Contributed by Mario Carneiro, 26-Feb-2016.)
|- ( # ` <" A B C D "> ) = 4
Theorem	s5len 12840	The length of a length 5 string. (Contributed by Mario Carneiro, 26-Feb-2016.)
|- ( # ` <" A B C D E "> ) = 5
Theorem	s6len 12841	The length of a length 6 string. (Contributed by Mario Carneiro, 26-Feb-2016.)
|- ( # ` <" A B C D E F "> ) = 6
Theorem	s7len 12842	The length of a length 7 string. (Contributed by Mario Carneiro, 26-Feb-2016.)
|- ( # ` <" A B C D E F G "> ) = 7
Theorem	s8len 12843	The length of a length 8 string. (Contributed by Mario Carneiro, 26-Feb-2016.)
|- ( # ` <" A B C D E F G H "> ) = 8
Theorem	s2prop 12844	A length 2 word is an unordered pair of ordered pairs. (Contributed by Alexander van der Vekens, 14-Aug-2017.)
|- ( ( A e. S /\ B e. S ) -> <" A B "> = { <. 0 , A >. , <. 1 , B >. } )
Theorem	s4prop 12845	A length 4 word is a union of two unordered pairs of ordered pairs. (Contributed by Alexander van der Vekens, 14-Aug-2017.)
|- ( ( ( A e. S /\ B e. S ) /\ ( C e. S /\ D e. S ) ) -> <" A B C D "> = ( { <. 0 , A >. , <. 1 , B >. } u. { <. 2 , C >. , <. 3 , D >. } ) )
Theorem	s2f1o 12846	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.)
|- ( ( A e. S /\ B e. S /\ A =/= B ) -> ( E = <" A B "> -> E : { 0 , 1 } -1-1-onto-> { A , B } ) )
Theorem	f1oun2prg 12847	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.)
|- ( ( ( A e. V /\ B e. W ) /\ ( C e. X /\ D e. Y ) ) -> ( ( ( A =/= B /\ A =/= C /\ A =/= D ) /\ ( B =/= C /\ B =/= D /\ C =/= D ) ) -> ( { <. 0 , A >. , <. 1 , B >. } u. { <. 2 , C >. , <. 3 , D >. } ) : ( { 0 , 1 } u. { 2 , 3 } ) -1-1-onto-> ( { A , B } u. { C , D } ) ) )
Theorem	s4f1o 12848	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.)
|- ( ( ( A e. S /\ B e. S ) /\ ( C e. S /\ D e. S ) ) -> ( ( ( A =/= B /\ A =/= C /\ A =/= D ) /\ ( B =/= C /\ B =/= D /\ C =/= D ) ) -> ( E = <" A B C D "> -> E : dom E -1-1-onto-> ( { A , B } u. { C , D } ) ) ) )
Theorem	s4dom 12849	The domain of a length 4 word is the union of two (disjunct) pairs. (Contributed by Alexander van der Vekens, 15-Aug-2017.)
|- ( ( ( A e. S /\ B e. S ) /\ ( C e. S /\ D e. S ) ) -> ( E = <" A B C D "> -> dom E = ( { 0 , 1 } u. { 2 , 3 } ) ) )
Theorem	s2co 12850	Mapping a doubleton by a function. (Contributed by Mario Carneiro, 27-Feb-2016.)
|- ( ph -> F : X --> Y )   &    |- ( ph -> A e. X )   &    |- ( ph -> B e. X )   =>    |- ( ph -> ( F o. <" A B "> ) = <" ( F ` A ) ( F ` B ) "> )
Theorem	s3co 12851	Mapping a length 3 string by a function. (Contributed by Mario Carneiro, 27-Feb-2016.)
|- ( ph -> F : X --> Y )   &    |- ( ph -> A e. X )   &    |- ( ph -> B e. X )   &    |- ( ph -> C e. X )   =>    |- ( ph -> ( F o. <" A B C "> ) = <" ( F ` A ) ( F ` B ) ( F ` C ) "> )
Theorem	s0s1 12852	Concatenation of fixed length strings. (This special case of ccatlid 12585 is provided to complete the pattern s0s1 12852, df-s2 12795, df-s3 12796, ...) (Contributed by Mario Carneiro, 28-Feb-2016.)
|- <" A "> = ( (/) concat <" A "> )
Theorem	s1s2 12853	Concatenation of fixed length strings. (Contributed by Mario Carneiro, 26-Feb-2016.)
|- <" A B C "> = ( <" A "> concat <" B C "> )
Theorem	s1s3 12854	Concatenation of fixed length strings. (Contributed by Mario Carneiro, 26-Feb-2016.)
|- <" A B C D "> = ( <" A "> concat <" B C D "> )
Theorem	s1s4 12855	Concatenation of fixed length strings. (Contributed by Mario Carneiro, 26-Feb-2016.)
|- <" A B C D E "> = ( <" A "> concat <" B C D E "> )
Theorem	s1s5 12856	Concatenation of fixed length strings. (Contributed by Mario Carneiro, 26-Feb-2016.)
|- <" A B C D E F "> = ( <" A "> concat <" B C D E F "> )
Theorem	s1s6 12857	Concatenation of fixed length strings. (Contributed by Mario Carneiro, 26-Feb-2016.)
|- <" A B C D E F G "> = ( <" A "> concat <" B C D E F G "> )
Theorem	s1s7 12858	Concatenation of fixed length strings. (Contributed by Mario Carneiro, 26-Feb-2016.)
|- <" A B C D E F G H "> = ( <" A "> concat <" B C D E F G H "> )
Theorem	s2s2 12859	Concatenation of fixed length strings. (Contributed by Mario Carneiro, 26-Feb-2016.)
|- <" A B C D "> = ( <" A B "> concat <" C D "> )
Theorem	s4s2 12860	Concatenation of fixed length strings. (Contributed by Mario Carneiro, 26-Feb-2016.)
|- <" A B C D E F "> = ( <" A B C D "> concat <" E F "> )
Theorem	s4s3 12861	Concatenation of fixed length strings. (Contributed by Mario Carneiro, 26-Feb-2016.)
|- <" A B C D E F G "> = ( <" A B C D "> concat <" E F G "> )
Theorem	s4s4 12862	Concatenation of fixed length strings. (Contributed by Mario Carneiro, 26-Feb-2016.)
|- <" A B C D E F G H "> = ( <" A B C D "> concat <" E F G H "> )
Theorem	s2eq2s1eq 12863	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.)
|- ( ( ( A e. V /\ B e. V ) /\ ( C e. V /\ D e. V ) ) -> ( <" A B "> = <" C D "> <-> ( <" A "> = <" C "> /\ <" B "> = <" D "> ) ) )
Theorem	s2eq2seq 12864	Two length 2 words are equal iff the corresponding symbols are equal. (Contributed by AV, 20-Oct-2018.)
|- ( ( ( A e. V /\ B e. V ) /\ ( C e. V /\ D e. V ) ) -> ( <" A B "> = <" C D "> <-> ( A = C /\ B = D ) ) )
Theorem	swrds2 12865	Extract two adjacent symbols from a word. (Contributed by Stefan O'Rear, 23-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.)
|- ( ( W e. Word A /\ I e. NN0 /\ ( I + 1 ) e. ( 0..^ ( # ` W ) ) ) -> ( W substr <. I , ( I + 2 ) >. ) = <" ( W ` I ) ( W ` ( I + 1 ) ) "> )
Theorem	wrdlen2i 12866	Implications of a word of length 2. (Contributed by AV, 27-Jul-2018.) (Proof shortened by AV, 14-Oct-2018.)
|- ( ( S e. V /\ T e. V ) -> ( W = { <. 0 , S >. , <. 1 , T >. } -> ( ( W e. Word V /\ ( # ` W ) = 2 ) /\ ( ( W ` 0 ) = S /\ ( W ` 1 ) = T ) ) ) )
Theorem	wrd2pr2op 12867	A word of length 2 represented as unordered pair of ordered pairs. (Contributed by AV, 20-Oct-2018.)
|- ( ( W e. Word V /\ ( # ` W ) = 2 ) -> W = { <. 0 , ( W ` 0 ) >. , <. 1 , ( W ` 1 ) >. } )
Theorem	wrdlen2 12868	A word of length 2. (Contributed by AV, 20-Oct-2018.)
|- ( ( S e. V /\ T e. V ) -> ( W = { <. 0 , S >. , <. 1 , T >. } <-> ( ( W e. Word V /\ ( # ` W ) = 2 ) /\ ( ( W ` 0 ) = S /\ ( W ` 1 ) = T ) ) ) )
Theorem	wrdlen2s2 12869	A word of length 2 as doubleton. (Contributed by AV, 20-Oct-2018.)
|- ( ( W e. Word V /\ ( # ` W ) = 2 ) -> W = <" ( W ` 0 ) ( W ` 1 ) "> )
Theorem	repsw2 12870	The "repeated symbol word" of length 2. (Contributed by AV, 6-Nov-2018.)
|- ( S e. V -> ( S repeatS 2 ) = <" S S "> )
Theorem	repsw3 12871	The "repeated symbol word" of length 3. (Contributed by AV, 6-Nov-2018.)
|- ( S e. V -> ( S repeatS 3 ) = <" S S S "> )
Theorem	swrd2lsw 12872	Extract the last two single symbol from a word. (Contributed by Alexander van der Vekens, 23-Sep-2018.)
|- ( ( W e. Word V /\ 1 < ( # ` W ) ) -> ( W substr <. ( ( # ` W ) - 2 ) , ( # ` W ) >. ) = <" ( W ` ( ( # ` W ) - 2 ) ) ( lastS ` W ) "> )
Theorem	2swrd2eqwrdeq 12873	Two words of length at least 2 are equal if and only if they have the same prefix and the same two single symbols suffix. (Contributed by AV, 24-Sep-2018.) (Revised by Mario Carneiro/AV, 23-Oct-2018.)
|- ( ( W e. Word V /\ U e. Word V /\ 1 < ( # ` W ) ) -> ( W = U <-> ( ( # ` W ) = ( # ` U ) /\ ( ( W substr <. 0 , ( ( # ` W ) - 2 ) >. ) = ( U substr <. 0 , ( ( # ` W ) - 2 ) >. ) /\ ( W ` ( ( # ` W ) - 2 ) ) = ( U ` ( ( # ` W ) - 2 ) ) /\ ( lastS ` W ) = ( lastS ` U ) ) ) ) )
Theorem	ccatw2s1ccatws2 12874	The concatenation of a word with two singleton words equals the concatenation of the word with the doubleton consisting of the symbols of the two singletons. (Contributed by Mario Carneiro/AV, 21-Oct-2018.)
|- ( ( W e. Word V /\ X e. V /\ Y e. V ) -> ( ( W concat <" X "> ) concat <" Y "> ) = ( W concat <" X Y "> ) )
Theorem	ccat2s1fvwALT 12875	Alternate proof of ccat2s1fvw 12624 using words of length 2, see df-s2 12795. A symbol of the concatenation of a word with two single symbols corresponding to the symbol of the word. (Contributed by AV, 22-Sep-2018.) (Proof shortened by Mario Carneiro/AV, 21-Oct-2018.) (New usage is discouraged.) (Proof modification is discouraged.)
|- ( ( ( W e. Word V /\ I e. NN0 /\ I < ( # ` W ) ) /\ ( X e. V /\ Y e. V ) ) -> ( ( ( W concat <" X "> ) concat <" Y "> ) ` I ) = ( W ` I ) )
Theorem	wwlktovf 12876*	Lemma 1 for wrd2f1tovbij 12880. (Contributed by Alexander van der Vekens, 27-Jul-2018.)
|- D = { w e. Word V | ( ( # ` w ) = 2 /\ ( w ` 0 ) = P /\ { ( w ` 0 ) , ( w ` 1 ) } e. X ) }   &    |- R = { n e. V | { P , n } e. X }   &    |- F = ( t e. D |-> ( t ` 1 ) )   =>    |- F : D --> R
Theorem	wwlktovf1 12877*	Lemma 2 for wrd2f1tovbij 12880. (Contributed by Alexander van der Vekens, 27-Jul-2018.)
|- D = { w e. Word V | ( ( # ` w ) = 2 /\ ( w ` 0 ) = P /\ { ( w ` 0 ) , ( w ` 1 ) } e. X ) }   &    |- R = { n e. V | { P , n } e. X }   &    |- F = ( t e. D |-> ( t ` 1 ) )   =>    |- F : D -1-1-> R
Theorem	wwlktovfo 12878*	Lemma 3 for wrd2f1tovbij 12880. (Contributed by Alexander van der Vekens, 27-Jul-2018.)
|- D = { w e. Word V | ( ( # ` w ) = 2 /\ ( w ` 0 ) = P /\ { ( w ` 0 ) , ( w ` 1 ) } e. X ) }   &    |- R = { n e. V | { P , n } e. X }   &    |- F = ( t e. D |-> ( t ` 1 ) )   =>    |- ( P e. V -> F : D -onto-> R )
Theorem	wwlktovf1o 12879*	Lemma 4 for wrd2f1tovbij 12880. (Contributed by Alexander van der Vekens, 28-Jul-2018.)
|- D = { w e. Word V | ( ( # ` w ) = 2 /\ ( w ` 0 ) = P /\ { ( w ` 0 ) , ( w ` 1 ) } e. X ) }   &    |- R = { n e. V | { P , n } e. X }   &    |- F = ( t e. D |-> ( t ` 1 ) )   =>    |- ( P e. V -> F : D -1-1-onto-> R )
Theorem	wrd2f1tovbij 12880*	There is a bijection between words of length two with a fixed first symbol contained in a pair and the symbols contained in a pair together with the fixed symbol. (Contributed by Alexander van der Vekens, 28-Jul-2018.)
|- ( ( V e. Y /\ P e. V ) -> E. f f : { w e. Word V | ( ( # ` w ) = 2 /\ ( w ` 0 ) = P /\ { ( w ` 0 ) , ( w ` 1 ) } e. X ) } -1-1-onto-> { n e. V | { P , n } e. X } )
5.8  Elementary real and complex functions
5.8.1  The "shift" operation
Syntax	cshi 12881	Extend class notation with function shifter.
class shift
Definition	df-shft 12882*	Define a function shifter. This operation offsets the value argument of a function (ordinarily on a subset of CC) and produces a new function on CC. See shftval 12889 for its value. (Contributed by NM, 20-Jul-2005.)
|- shift = ( f e. _V , x e. CC |-> { <. y , z >. | ( y e. CC /\ ( y - x ) f z ) } )
Theorem	shftlem 12883*	Two ways to write a shifted set ( B + A ). (Contributed by Mario Carneiro, 3-Nov-2013.)
|- ( ( A e. CC /\ B C_ CC ) -> { x e. CC | ( x - A ) e. B } = { x | E. y e. B x = ( y + A ) } )
Theorem	shftuz 12884*	A shift of the upper integers. (Contributed by Mario Carneiro, 5-Nov-2013.)
|- ( ( A e. ZZ /\ B e. ZZ ) -> { x e. CC | ( x - A ) e. ( ZZ>= ` B ) } = ( ZZ>= ` ( B + A ) ) )
Theorem	shftfval 12885*	The value of the sequence shifter operation is a function on CC. A is ordinarily an integer. (Contributed by NM, 20-Jul-2005.) (Revised by Mario Carneiro, 3-Nov-2013.)
|- F e. _V   =>    |- ( A e. CC -> ( F shift A ) = { <. x , y >. | ( x e. CC /\ ( x - A ) F y ) } )
Theorem	shftdm 12886*	Domain of a relation shifted by A. The set on the right is more commonly notated as ( dom F + A ) (meaning add A to every element of dom F). (Contributed by Mario Carneiro, 3-Nov-2013.)
|- F e. _V   =>    |- ( A e. CC -> dom ( F shift A ) = { x e. CC | ( x - A ) e. dom F } )
Theorem	shftfib 12887	Value of a fiber of the relation F. (Contributed by Mario Carneiro, 4-Nov-2013.)
|- F e. _V   =>    |- ( ( A e. CC /\ B e. CC ) -> ( ( F shift A ) " { B } ) = ( F " { ( B - A ) } ) )
Theorem	shftfn 12888*	Functionality and domain of a sequence shifted by A. (Contributed by NM, 20-Jul-2005.) (Revised by Mario Carneiro, 3-Nov-2013.)
|- F e. _V   =>    |- ( ( F Fn B /\ A e. CC ) -> ( F shift A ) Fn { x e. CC | ( x - A ) e. B } )
Theorem	shftval 12889	Value of a sequence shifted by A. (Contributed by NM, 20-Jul-2005.) (Revised by Mario Carneiro, 4-Nov-2013.)
|- F e. _V   =>    |- ( ( A e. CC /\ B e. CC ) -> ( ( F shift A ) ` B ) = ( F ` ( B - A ) ) )
Theorem	shftval2 12890	Value of a sequence shifted by A - B. (Contributed by NM, 20-Jul-2005.) (Revised by Mario Carneiro, 5-Nov-2013.)
|- F e. _V   =>    |- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( F shift ( A - B ) ) ` ( A + C ) ) = ( F ` ( B + C ) ) )
Theorem	shftval3 12891	Value of a sequence shifted by A - B. (Contributed by NM, 20-Jul-2005.)
|- F e. _V   =>    |- ( ( A e. CC /\ B e. CC ) -> ( ( F shift ( A - B ) ) ` A ) = ( F ` B ) )
Theorem	shftval4 12892	Value of a sequence shifted by -u A. (Contributed by NM, 18-Aug-2005.) (Revised by Mario Carneiro, 5-Nov-2013.)
|- F e. _V   =>    |- ( ( A e. CC /\ B e. CC ) -> ( ( F shift -u A ) ` B ) = ( F ` ( A + B ) ) )
Theorem	shftval5 12893	Value of a shifted sequence. (Contributed by NM, 19-Aug-2005.) (Revised by Mario Carneiro, 5-Nov-2013.)
|- F e. _V   =>    |- ( ( A e. CC /\ B e. CC ) -> ( ( F shift A ) ` ( B + A ) ) = ( F ` B ) )
Theorem	shftf 12894*	Functionality of a shifted sequence. (Contributed by NM, 19-Aug-2005.) (Revised by Mario Carneiro, 5-Nov-2013.)
|- F e. _V   =>    |- ( ( F : B --> C /\ A e. CC ) -> ( F shift A ) : { x e. CC | ( x - A ) e. B } --> C )
Theorem	2shfti 12895	Composite shift operations. (Contributed by NM, 19-Aug-2005.) (Revised by Mario Carneiro, 5-Nov-2013.)
|- F e. _V   =>    |- ( ( A e. CC /\ B e. CC ) -> ( ( F shift A ) shift B ) = ( F shift ( A + B ) ) )
Theorem	shftidt2 12896	Identity law for the shift operation. (Contributed by Mario Carneiro, 5-Nov-2013.)
|- F e. _V   =>    |- ( F shift 0 ) = ( F |` CC )
Theorem	shftidt 12897	Identity law for the shift operation. (Contributed by NM, 19-Aug-2005.) (Revised by Mario Carneiro, 5-Nov-2013.)
|- F e. _V   =>    |- ( A e. CC -> ( ( F shift 0 ) ` A ) = ( F ` A ) )
Theorem	shftcan1 12898	Cancellation law for the shift operation. (Contributed by NM, 4-Aug-2005.) (Revised by Mario Carneiro, 5-Nov-2013.)
|- F e. _V   =>    |- ( ( A e. CC /\ B e. CC ) -> ( ( ( F shift A ) shift -u A ) ` B ) = ( F ` B ) )
Theorem	shftcan2 12899	Cancellation law for the shift operation. (Contributed by NM, 4-Aug-2005.) (Revised by Mario Carneiro, 5-Nov-2013.)
|- F e. _V   =>    |- ( ( A e. CC /\ B e. CC ) -> ( ( ( F shift -u A ) shift A ) ` B ) = ( F ` B ) )
Theorem	seqshft 12900	Shifting the index set of a sequence. (Contributed by NM, 17-Mar-2005.) (Revised by Mario Carneiro, 27-Feb-2014.)
|- F e. _V   =>    |- ( ( M e. ZZ /\ N e. ZZ ) -> seq M ( .+ , ( F shift N ) ) = ( seq ( M - N ) ( .+ , F ) shift N ) )