Theorem lpadlen2

Description: Length of a left-padded word, in the case the given word W is shorter than the desired length. (Contributed by Thierry Arnoux, 7-Aug-2023)

	Ref	Expression
Hypotheses	lpadlen.1	|- ( ph -> L e. NN0 )
	lpadlen.2	|- ( ph -> W e. Word S )
	lpadlen.3	|- ( ph -> C e. S )
	lpadlen2.1	|- ( ph -> ( # ` W ) <_ L )
Assertion	lpadlen2	|- ( ph -> ( # ` ( ( C leftpad W ) ` L ) ) = L )

Proof

Step	Hyp	Ref	Expression
1		lpadlen.1	|- ( ph -> L e. NN0 )
2		lpadlen.2	|- ( ph -> W e. Word S )
3		lpadlen.3	|- ( ph -> C e. S )
4		lpadlen2.1	|- ( ph -> ( # ` W ) <_ L )
5	1 2 3	lpadval	|- ( ph -> ( ( C leftpad W ) ` L ) = ( ( ( 0 ..^ ( L - ( # ` W ) ) ) X. { C } ) ++ W ) )
6	5	fveq2d	|- ( ph -> ( # ` ( ( C leftpad W ) ` L ) ) = ( # ` ( ( ( 0 ..^ ( L - ( # ` W ) ) ) X. { C } ) ++ W ) ) )
7	3	lpadlem1	|- ( ph -> ( ( 0 ..^ ( L - ( # ` W ) ) ) X. { C } ) e. Word S )
8		ccatlen	|- ( ( ( ( 0 ..^ ( L - ( # ` W ) ) ) X. { C } ) e. Word S /\ W e. Word S ) -> ( # ` ( ( ( 0 ..^ ( L - ( # ` W ) ) ) X. { C } ) ++ W ) ) = ( ( # ` ( ( 0 ..^ ( L - ( # ` W ) ) ) X. { C } ) ) + ( # ` W ) ) )
9	7 2 8	syl2anc	|- ( ph -> ( # ` ( ( ( 0 ..^ ( L - ( # ` W ) ) ) X. { C } ) ++ W ) ) = ( ( # ` ( ( 0 ..^ ( L - ( # ` W ) ) ) X. { C } ) ) + ( # ` W ) ) )
10	1 2 3 4	lpadlem2	|- ( ph -> ( # ` ( ( 0 ..^ ( L - ( # ` W ) ) ) X. { C } ) ) = ( L - ( # ` W ) ) )
11	10	oveq1d	|- ( ph -> ( ( # ` ( ( 0 ..^ ( L - ( # ` W ) ) ) X. { C } ) ) + ( # ` W ) ) = ( ( L - ( # ` W ) ) + ( # ` W ) ) )
12	1	nn0cnd	|- ( ph -> L e. CC )
13		lencl	|- ( W e. Word S -> ( # ` W ) e. NN0 )
14	2 13	syl	|- ( ph -> ( # ` W ) e. NN0 )
15	14	nn0cnd	|- ( ph -> ( # ` W ) e. CC )
16	12 15	npcand	|- ( ph -> ( ( L - ( # ` W ) ) + ( # ` W ) ) = L )
17	9 11 16	3eqtrd	|- ( ph -> ( # ` ( ( ( 0 ..^ ( L - ( # ` W ) ) ) X. { C } ) ++ W ) ) = L )
18	6 17	eqtrd	|- ( ph -> ( # ` ( ( C leftpad W ) ` L ) ) = L )