P. 116 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 11501-11600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	swrdccatin2 11501	The subword of a concatenation of two words within the second of the concatenated words. (Contributed by Alexander van der Vekens, 28-Mar-2018.) (Revised by Alexander van der Vekens, 27-May-2018.)
|- L = (♯ ` A )   =>    |- ( ( A e. Word V /\ B e. Word V ) -> ( ( M e. ( L ... N ) /\ N e. ( L ... ( L + (♯ ` B ) ) ) ) -> ( ( A ++ B ) substr <. M , N >. ) = ( B substr <. ( M - L ) , ( N - L ) >. ) ) )
Theorem	pfxccatin12lem2c 11502	Lemma for pfxccatin12lem2 11503 and pfxccatin12lem3 11504. (Contributed by AV, 30-Mar-2018.) (Revised by AV, 27-May-2018.)
|- L = (♯ ` A )   =>    |- ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + (♯ ` B ) ) ) ) ) -> ( ( A ++ B ) e. Word V /\ M e. ( 0 ... N ) /\ N e. ( 0 ... (♯ ` ( A ++ B ) ) ) ) )
Theorem	pfxccatin12lem2 11503	Lemma 2 for pfxccatin12 11505. (Contributed by AV, 30-Mar-2018.) (Revised by AV, 9-May-2020.)
|- L = (♯ ` A )   =>    |- ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + (♯ ` B ) ) ) ) ) -> ( ( K e. ( 0..^ ( N - M ) ) /\ -. K e. ( 0..^ ( L - M ) ) ) -> ( ( ( A ++ B ) substr <. M , N >. ) ` K ) = ( ( B prefix ( N - L ) ) ` ( K - (♯ ` ( A substr <. M , L >. ) ) ) ) ) )
Theorem	pfxccatin12lem3 11504	Lemma 3 for pfxccatin12 11505. (Contributed by AV, 30-Mar-2018.) (Revised by AV, 27-May-2018.)
|- L = (♯ ` A )   =>    |- ( ( ( A e. Word V /\ B e. Word V ) /\ ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + (♯ ` B ) ) ) ) ) -> ( ( K e. ( 0..^ ( N - M ) ) /\ K e. ( 0..^ ( L - M ) ) ) -> ( ( ( A ++ B ) substr <. M , N >. ) ` K ) = ( ( A substr <. M , L >. ) ` K ) ) )
Theorem	pfxccatin12 11505	The subword of a concatenation of two words within both of the concatenated words. (Contributed by Alexander van der Vekens, 5-Apr-2018.) (Revised by AV, 9-May-2020.)
|- L = (♯ ` A )   =>    |- ( ( A e. Word V /\ B e. Word V ) -> ( ( M e. ( 0 ... L ) /\ N e. ( L ... ( L + (♯ ` B ) ) ) ) -> ( ( A ++ B ) substr <. M , N >. ) = ( ( A substr <. M , L >. ) ++ ( B prefix ( N - L ) ) ) ) )
Theorem	pfxccat3 11506	The subword of a concatenation is either a subword of the first concatenated word or a subword of the second concatenated word or a concatenation of a suffix of the first word with a prefix of the second word. (Contributed by Alexander van der Vekens, 30-Mar-2018.) (Revised by AV, 10-May-2020.)
|- L = (♯ ` A )   =>    |- ( ( A e. Word V /\ B e. Word V ) -> ( ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( L + (♯ ` B ) ) ) ) -> ( ( A ++ B ) substr <. M , N >. ) = if ( N <_ L , ( A substr <. M , N >. ) , if ( L <_ M , ( B substr <. ( M - L ) , ( N - L ) >. ) , ( ( A substr <. M , L >. ) ++ ( B prefix ( N - L ) ) ) ) ) ) )
Theorem	swrdccat 11507	The subword of a concatenation of two words as concatenation of subwords of the two concatenated words. (Contributed by Alexander van der Vekens, 29-May-2018.)
|- L = (♯ ` A )   =>    |- ( ( A e. Word V /\ B e. Word V ) -> ( ( M e. ( 0 ... N ) /\ N e. ( 0 ... ( L + (♯ ` B ) ) ) ) -> ( ( A ++ B ) substr <. M , N >. ) = ( ( A substr <. M , if ( N <_ L , N , L ) >. ) ++ ( B substr <. if ( 0 <_ ( M - L ) , ( M - L ) , 0 ) , ( N - L ) >. ) ) ) )
Theorem	pfxccatpfx1 11508	A prefix of a concatenation being a prefix of the first concatenated word. (Contributed by AV, 10-May-2020.)
|- L = (♯ ` A )   =>    |- ( ( A e. Word V /\ B e. Word V /\ N e. ( 0 ... L ) ) -> ( ( A ++ B ) prefix N ) = ( A prefix N ) )
Theorem	pfxccatpfx2 11509	A prefix of a concatenation of two words being the first word concatenated with a prefix of the second word. (Contributed by AV, 10-May-2020.)
|- L = (♯ ` A )   &    |- M = (♯ ` B )   =>    |- ( ( A e. Word V /\ B e. Word V /\ N e. ( ( L + 1 ) ... ( L + M ) ) ) -> ( ( A ++ B ) prefix N ) = ( A ++ ( B prefix ( N - L ) ) ) )
Theorem	pfxccat3a 11510	A prefix of a concatenation is either a prefix of the first concatenated word or a concatenation of the first word with a prefix of the second word. (Contributed by Alexander van der Vekens, 31-Mar-2018.) (Revised by AV, 10-May-2020.)
|- L = (♯ ` A )   &    |- M = (♯ ` B )   =>    |- ( ( A e. Word V /\ B e. Word V ) -> ( N e. ( 0 ... ( L + M ) ) -> ( ( A ++ B ) prefix N ) = if ( N <_ L , ( A prefix N ) , ( A ++ ( B prefix ( N - L ) ) ) ) ) )
Theorem	swrdccat3blem 11511	Lemma for swrdccat3b 11512. (Contributed by AV, 30-May-2018.)
|- L = (♯ ` A )   =>    |- ( ( ( ( A e. Word V /\ B e. Word V ) /\ M e. ( 0 ... ( L + (♯ ` B ) ) ) ) /\ ( L + (♯ ` B ) ) <_ L ) -> if ( L <_ M , ( B substr <. ( M - L ) , (♯ ` B ) >. ) , ( ( A substr <. M , L >. ) ++ B ) ) = ( A substr <. M , ( L + (♯ ` B ) ) >. ) )
Theorem	swrdccat3b 11512	A suffix of a concatenation is either a suffix of the second concatenated word or a concatenation of a suffix of the first word with the second word. (Contributed by Alexander van der Vekens, 31-Mar-2018.) (Revised by Alexander van der Vekens, 30-May-2018.) (Proof shortened by AV, 14-Oct-2022.)
|- L = (♯ ` A )   =>    |- ( ( A e. Word V /\ B e. Word V ) -> ( M e. ( 0 ... ( L + (♯ ` B ) ) ) -> ( ( A ++ B ) substr <. M , ( L + (♯ ` B ) ) >. ) = if ( L <_ M , ( B substr <. ( M - L ) , (♯ ` B ) >. ) , ( ( A substr <. M , L >. ) ++ B ) ) ) )
Theorem	pfxccatid 11513	A prefix of a concatenation of length of the first concatenated word is the first word itself. (Contributed by Alexander van der Vekens, 20-Sep-2018.) (Revised by AV, 10-May-2020.)
|- ( ( A e. Word V /\ B e. Word V /\ N = (♯ ` A ) ) -> ( ( A ++ B ) prefix N ) = A )
Theorem	ccats1pfxeqbi 11514	A word is a prefix of a word with length greater by 1 than the first word iff the second word is the first word concatenated with the last symbol of the second word. (Contributed by AV, 24-Oct-2018.) (Revised by AV, 10-May-2020.)
|- ( ( W e. Word V /\ U e. Word V /\ (♯ ` U ) = ( (♯ ` W ) + 1 ) ) -> ( W = ( U prefix (♯ ` W ) ) <-> U = ( W ++ <" (lastS ` U ) "> ) ) )
Theorem	swrdccatin1d 11515	The subword of a concatenation of two words within the first of the concatenated words. (Contributed by AV, 31-May-2018.) (Revised by Mario Carneiro/AV, 21-Oct-2018.)
|- ( ph -> (♯ ` A ) = L )   &    |- ( ph -> ( A e. Word V /\ B e. Word V ) )   &    |- ( ph -> M e. ( 0 ... N ) )   &    |- ( ph -> N e. ( 0 ... L ) )   =>    |- ( ph -> ( ( A ++ B ) substr <. M , N >. ) = ( A substr <. M , N >. ) )
Theorem	swrdccatin2d 11516	The subword of a concatenation of two words within the second of the concatenated words. (Contributed by AV, 31-May-2018.) (Revised by Mario Carneiro/AV, 21-Oct-2018.)
|- ( ph -> (♯ ` A ) = L )   &    |- ( ph -> ( A e. Word V /\ B e. Word V ) )   &    |- ( ph -> M e. ( L ... N ) )   &    |- ( ph -> N e. ( L ... ( L + (♯ ` B ) ) ) )   =>    |- ( ph -> ( ( A ++ B ) substr <. M , N >. ) = ( B substr <. ( M - L ) , ( N - L ) >. ) )
Theorem	pfxccatin12d 11517	The subword of a concatenation of two words within both of the concatenated words. (Contributed by AV, 31-May-2018.) (Revised by AV, 10-May-2020.)
|- ( ph -> (♯ ` A ) = L )   &    |- ( ph -> ( A e. Word V /\ B e. Word V ) )   &    |- ( ph -> M e. ( 0 ... L ) )   &    |- ( ph -> N e. ( L ... ( L + (♯ ` B ) ) ) )   =>    |- ( ph -> ( ( A ++ B ) substr <. M , N >. ) = ( ( A substr <. M , L >. ) ++ ( B prefix ( N - L ) ) ) )
Theorem	reuccatpfxs1lem 11518*	Lemma for reuccatpfxs1 11519. (Contributed by Alexander van der Vekens, 5-Oct-2018.) (Revised by AV, 9-May-2020.)
|- ( ( ( W e. Word V /\ U e. X ) /\ A. s e. V ( ( W ++ <" s "> ) e. X -> S = s ) /\ A. x e. X ( x e. Word V /\ (♯ ` x ) = ( (♯ ` W ) + 1 ) ) ) -> ( W = ( U prefix (♯ ` W ) ) -> U = ( W ++ <" S "> ) ) )
Theorem	reuccatpfxs1 11519*	There is a unique word having the length of a given word increased by 1 with the given word as prefix if there is a unique symbol which extends the given word. (Contributed by Alexander van der Vekens, 6-Oct-2018.) (Revised by AV, 21-Jan-2022.) (Revised by AV, 13-Oct-2022.)
|- F/_ v X   =>    |- ( ( W e. Word V /\ A. x e. X ( x e. Word V /\ (♯ ` x ) = ( (♯ ` W ) + 1 ) ) ) -> ( E! v e. V ( W ++ <" v "> ) e. X -> E! x e. X W = ( x prefix (♯ ` W ) ) ) )
Theorem	reuccatpfxs1v 11520*	There is a unique word having the length of a given word increased by 1 with the given word as prefix if there is a unique symbol which extends the given word. (Contributed by Alexander van der Vekens, 6-Oct-2018.) (Revised by AV, 21-Jan-2022.) (Revised by AV, 10-May-2022.) (Proof shortened by AV, 13-Oct-2022.)
|- ( ( W e. Word V /\ A. x e. X ( x e. Word V /\ (♯ ` x ) = ( (♯ ` W ) + 1 ) ) ) -> ( E! v e. V ( W ++ <" v "> ) e. X -> E! x e. X W = ( x prefix (♯ ` W ) ) ) )
4.7.11  Longer string literals
Syntax	cs2 11521	Syntax for the length 2 word constructor.
class <" A B ">
Syntax	cs3 11522	Syntax for the length 3 word constructor.
class <" A B C ">
Syntax	cs4 11523	Syntax for the length 4 word constructor.
class <" A B C D ">
Syntax	cs5 11524	Syntax for the length 5 word constructor.
class <" A B C D E ">
Syntax	cs6 11525	Syntax for the length 6 word constructor.
class <" A B C D E F ">
Syntax	cs7 11526	Syntax for the length 7 word constructor.
class <" A B C D E F G ">
Syntax	cs8 11527	Syntax for the length 8 word constructor.
class <" A B C D E F G H ">
Definition	df-s2 11528	Define the length 2 word constructor. (Contributed by Mario Carneiro, 26-Feb-2016.)
|- <" A B "> = ( <" A "> ++ <" B "> )
Definition	df-s3 11529	Define the length 3 word constructor. (Contributed by Mario Carneiro, 26-Feb-2016.)
|- <" A B C "> = ( <" A B "> ++ <" C "> )
Definition	df-s4 11530	Define the length 4 word constructor. (Contributed by Mario Carneiro, 26-Feb-2016.)
|- <" A B C D "> = ( <" A B C "> ++ <" D "> )
Definition	df-s5 11531	Define the length 5 word constructor. (Contributed by Mario Carneiro, 26-Feb-2016.)
|- <" A B C D E "> = ( <" A B C D "> ++ <" E "> )
Definition	df-s6 11532	Define the length 6 word constructor. (Contributed by Mario Carneiro, 26-Feb-2016.)
|- <" A B C D E F "> = ( <" A B C D E "> ++ <" F "> )
Definition	df-s7 11533	Define the length 7 word constructor. (Contributed by Mario Carneiro, 26-Feb-2016.)
|- <" A B C D E F G "> = ( <" A B C D E F "> ++ <" G "> )
Definition	df-s8 11534	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 "> ++ <" H "> )
Theorem	cats1cld 11535	Closure of concatenation with a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016.)
|- T = ( S ++ <" X "> )   &    |- ( ph -> S e. Word A )   &    |- ( ph -> X e. A )   =>    |- ( ph -> T e. Word A )
Theorem	cats1fvn 11536	The last symbol of a concatenation with a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016.)
|- T = ( S ++ <" X "> )   &    |- S e. Word _V   &    |- (♯ ` S ) = M   =>    |- ( X e. V -> ( T ` M ) = X )
Theorem	cats1fvnd 11537	The last symbol of a concatenation with a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016.) (Revised by Jim Kingdon, 20-Jan-2026.)
|- T = ( S ++ <" X "> )   &    |- ( ph -> S e. Word _V )   &    |- ( ph -> X e. V )   &    |- ( ph -> (♯ ` S ) = M )   =>    |- ( ph -> ( T ` M ) = X )
Theorem	cats1fvd 11538	A symbol other than the last in a concatenation with a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016.) (Revised by Jim Kingdon, 20-Jan-2026.)
|- T = ( S ++ <" X "> )   &    |- ( ph -> S e. Word _V )   &    |- ( ph -> (♯ ` S ) = M )   &    |- ( ph -> Y e. V )   &    |- ( ph -> X e. W )   &    |- ( ph -> ( S ` N ) = Y )   &    |- ( ph -> N e. NN0 )   &    |- ( ph -> N < M )   =>    |- ( ph -> ( T ` N ) = Y )
Theorem	cats1lend 11539	The length of concatenation with a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016.) (Revised by Jim Kingdon, 19-Jan-2026.)
|- T = ( S ++ <" X "> )   &    |- ( ph -> S e. Word _V )   &    |- ( ph -> X e. W )   &    |- (♯ ` S ) = M   &    |- ( M + 1 ) = N   =>    |- ( ph -> (♯ ` T ) = N )
Theorem	cats1catd 11540	Closure of concatenation with a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016.) (Revised by Jim Kingdon, 19-Jan-2026.)
|- T = ( S ++ <" X "> )   &    |- ( ph -> A e. Word _V )   &    |- ( ph -> S e. Word _V )   &    |- ( ph -> X e. W )   &    |- ( ph -> C = ( B ++ <" X "> ) )   &    |- ( ph -> B = ( A ++ S ) )   =>    |- ( ph -> C = ( A ++ T ) )
Theorem	cats2catd 11541	Closure of concatenation of concatenations with singleton words. (Contributed by AV, 1-Mar-2021.) (Revised by Jim Kingdon, 19-Jan-2026.)
|- ( ph -> B e. Word _V )   &    |- ( ph -> D e. Word _V )   &    |- ( ph -> X e. V )   &    |- ( ph -> Y e. W )   &    |- ( ph -> A = ( B ++ <" X "> ) )   &    |- ( ph -> C = ( <" Y "> ++ D ) )   =>    |- ( ph -> ( A ++ C ) = ( ( B ++ <" X Y "> ) ++ D ) )
Theorem	s2eqd 11542	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 11543	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 11544	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 11545	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 11546	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 11547	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 11548	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	s3eq2 11549	Equality theorem for a length 3 word for the second symbol. (Contributed by AV, 4-Jan-2022.)
|- ( B = D -> <" A B C "> = <" A D C "> )
Theorem	s2cld 11550	A doubleton word 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 11551	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 11552	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 11553	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 11554	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 11555	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 11556	A length 8 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 11557	A doubleton word 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 11558	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	s2fv0g 11559	Extract the first symbol from a doubleton word. (Contributed by Stefan O'Rear, 23-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.)
|- ( ( A e. V /\ B e. W ) -> ( <" A B "> ` 0 ) = A )
Theorem	s2fv1g 11560	Extract the second symbol from a doubleton word. (Contributed by Stefan O'Rear, 23-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.)
|- ( ( A e. V /\ B e. W ) -> ( <" A B "> ` 1 ) = B )
Theorem	s2leng 11561	The length of a doubleton word. (Contributed by Stefan O'Rear, 23-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.)
|- ( ( A e. V /\ B e. W ) -> (♯ ` <" A B "> ) = 2 )
Theorem	s2dmg 11562	The domain of a doubleton word is an unordered pair. (Contributed by AV, 9-Jan-2020.)
|- ( ( A e. V /\ B e. W ) -> dom <" A B "> = { 0 , 1 } )
Theorem	s3fv0g 11563	Extract the first symbol from a length 3 string. (Contributed by Mario Carneiro, 13-Jan-2017.)
|- ( ( A e. V /\ B e. W /\ C e. X ) -> ( <" A B C "> ` 0 ) = A )
Theorem	s3fv1g 11564	Extract the second symbol from a length 3 string. (Contributed by Mario Carneiro, 13-Jan-2017.)
|- ( ( A e. V /\ B e. W /\ C e. X ) -> ( <" A B C "> ` 1 ) = B )
Theorem	s3fv2g 11565	Extract the third symbol from a length 3 string. (Contributed by Mario Carneiro, 13-Jan-2017.)
|- ( ( A e. V /\ B e. W /\ C e. X ) -> ( <" A B C "> ` 2 ) = C )
Theorem	s1s2d 11566	Concatenation of fixed length strings. (Contributed by Mario Carneiro, 26-Feb-2016.)
|- ( ph -> A e. V )   &    |- ( ph -> B e. W )   &    |- ( ph -> C e. X )   =>    |- ( ph -> <" A B C "> = ( <" A "> ++ <" B C "> ) )
Theorem	s1s3d 11567	Concatenation of fixed length strings. (Contributed by Mario Carneiro, 26-Feb-2016.)
|- ( ph -> A e. V )   &    |- ( ph -> B e. W )   &    |- ( ph -> C e. X )   &    |- ( ph -> D e. Y )   =>    |- ( ph -> <" A B C D "> = ( <" A "> ++ <" B C D "> ) )
Theorem	s1s4d 11568	Concatenation of fixed length strings. (Contributed by Mario Carneiro, 26-Feb-2016.)
|- ( ph -> A e. V )   &    |- ( ph -> B e. W )   &    |- ( ph -> C e. X )   &    |- ( ph -> D e. Y )   &    |- ( ph -> E e. Z )   =>    |- ( ph -> <" A B C D E "> = ( <" A "> ++ <" B C D E "> ) )
Theorem	s1s5d 11569	Concatenation of fixed length strings. (Contributed by Mario Carneiro, 26-Feb-2016.)
|- ( ph -> A e. V )   &    |- ( ph -> B e. W )   &    |- ( ph -> C e. X )   &    |- ( ph -> D e. Y )   &    |- ( ph -> E e. Z )   &    |- ( ph -> F e. P )   =>    |- ( ph -> <" A B C D E F "> = ( <" A "> ++ <" B C D E F "> ) )
Theorem	s1s6d 11570	Concatenation of fixed length strings. (Contributed by Mario Carneiro, 26-Feb-2016.)
|- ( ph -> A e. V )   &    |- ( ph -> B e. W )   &    |- ( ph -> C e. X )   &    |- ( ph -> D e. Y )   &    |- ( ph -> E e. Z )   &    |- ( ph -> F e. P )   &    |- ( ph -> G e. Q )   =>    |- ( ph -> <" A B C D E F G "> = ( <" A "> ++ <" B C D E F G "> ) )
Theorem	s1s7d 11571	Concatenation of fixed length strings. (Contributed by Mario Carneiro, 26-Feb-2016.)
|- ( ph -> A e. V )   &    |- ( ph -> B e. W )   &    |- ( ph -> C e. X )   &    |- ( ph -> D e. Y )   &    |- ( ph -> E e. Z )   &    |- ( ph -> F e. P )   &    |- ( ph -> G e. Q )   &    |- ( ph -> H e. R )   =>    |- ( ph -> <" A B C D E F G H "> = ( <" A "> ++ <" B C D E F G H "> ) )
Theorem	s2s2d 11572	Concatenation of fixed length strings. (Contributed by Mario Carneiro, 26-Feb-2016.)
|- ( ph -> A e. V )   &    |- ( ph -> B e. W )   &    |- ( ph -> C e. X )   &    |- ( ph -> D e. Y )   =>    |- ( ph -> <" A B C D "> = ( <" A B "> ++ <" C D "> ) )
Theorem	s4s2d 11573	Concatenation of fixed length strings. (Contributed by Mario Carneiro, 26-Feb-2016.)
|- ( ph -> A e. V )   &    |- ( ph -> B e. W )   &    |- ( ph -> C e. X )   &    |- ( ph -> D e. Y )   &    |- ( ph -> E e. Z )   &    |- ( ph -> F e. P )   =>    |- ( ph -> <" A B C D E F "> = ( <" A B C D "> ++ <" E F "> ) )
Theorem	s4s3d 11574	Concatenation of fixed length strings. (Contributed by Mario Carneiro, 26-Feb-2016.)
|- ( ph -> A e. V )   &    |- ( ph -> B e. W )   &    |- ( ph -> C e. X )   &    |- ( ph -> D e. Y )   &    |- ( ph -> E e. Z )   &    |- ( ph -> F e. P )   &    |- ( ph -> G e. Q )   =>    |- ( ph -> <" A B C D E F G "> = ( <" A B C D "> ++ <" E F G "> ) )
Theorem	s3s4d 11575	Concatenation of fixed length strings. (Contributed by AV, 1-Mar-2021.)
|- ( ph -> A e. V )   &    |- ( ph -> B e. W )   &    |- ( ph -> C e. X )   &    |- ( ph -> D e. Y )   &    |- ( ph -> E e. Z )   &    |- ( ph -> F e. P )   &    |- ( ph -> G e. Q )   =>    |- ( ph -> <" A B C D E F G "> = ( <" A B C "> ++ <" D E F G "> ) )
Theorem	s2s5d 11576	Concatenation of fixed length strings. (Contributed by AV, 1-Mar-2021.)
|- ( ph -> A e. V )   &    |- ( ph -> B e. W )   &    |- ( ph -> C e. X )   &    |- ( ph -> D e. Y )   &    |- ( ph -> E e. Z )   &    |- ( ph -> F e. P )   &    |- ( ph -> G e. Q )   =>    |- ( ph -> <" A B C D E F G "> = ( <" A B "> ++ <" C D E F G "> ) )
Theorem	s5s2d 11577	Concatenation of fixed length strings. (Contributed by AV, 1-Mar-2021.)
|- ( ph -> A e. V )   &    |- ( ph -> B e. W )   &    |- ( ph -> C e. X )   &    |- ( ph -> D e. Y )   &    |- ( ph -> E e. Z )   &    |- ( ph -> F e. P )   &    |- ( ph -> G e. Q )   =>    |- ( ph -> <" A B C D E F G "> = ( <" A B C D E "> ++ <" F G "> ) )
Theorem	s4s4d 11578	Concatenation of fixed length strings. (Contributed by Mario Carneiro, 26-Feb-2016.)
|- ( ph -> A e. V )   &    |- ( ph -> B e. W )   &    |- ( ph -> C e. X )   &    |- ( ph -> D e. Y )   &    |- ( ph -> E e. Z )   &    |- ( ph -> F e. P )   &    |- ( ph -> G e. Q )   &    |- ( ph -> H e. R )   =>    |- ( ph -> <" A B C D E F G H "> = ( <" A B C D "> ++ <" E F G H "> ) )
4.8  Elementary real and complex functions
4.8.1  The "shift" operation
Syntax	cshi 11579	Extend class notation with function shifter.
class shift
Definition	df-shft 11580*	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 11590 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 11581*	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 11582*	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	shftfvalg 11583*	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.)
|- ( ( A e. CC /\ F e. V ) -> ( F shift A ) = { <. x , y >. | ( x e. CC /\ ( x - A ) F y ) } )
Theorem	ovshftex 11584	Existence of the result of applying shift. (Contributed by Jim Kingdon, 15-Aug-2021.)
|- ( ( F e. V /\ A e. CC ) -> ( F shift A ) e. _V )
Theorem	shftfibg 11585	Value of a fiber of the relation F. (Contributed by Jim Kingdon, 15-Aug-2021.)
|- ( ( F e. V /\ A e. CC /\ B e. CC ) -> ( ( F shift A ) " { B } ) = ( F " { ( B - A ) } ) )
Theorem	shftfval 11586*	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 11587*	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 11588	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 11589*	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 11590	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 11591	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 11592	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 11593	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 11594	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 11595*	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 11596	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 11597	Identity law for the shift operation. (Contributed by Mario Carneiro, 5-Nov-2013.)
|- F e. _V   =>    |- ( F shift 0 ) = ( F |` CC )
Theorem	shftidt 11598	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 11599	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 11600	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 ) )