Theorem lpadlen1

Description: Length of a left-padded word, in the case the length of the given word W is at least 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 )
	lpadlen1.1	|- ( ph -> L <_ ( # ` W ) )
Assertion	lpadlen1	|- ( ph -> ( # ` ( ( C leftpad W ) ` L ) ) = ( # ` W ) )

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		lpadlen1.1	|- ( ph -> L <_ ( # ` W ) )
5	1 2 3	lpadval	|- ( ph -> ( ( C leftpad W ) ` L ) = ( ( ( 0 ..^ ( L - ( # ` W ) ) ) X. { C } ) ++ W ) )
6	1 2 3 4	lpadlem3	|- ( ph -> ( ( 0 ..^ ( L - ( # ` W ) ) ) X. { C } ) = (/) )
7	6	oveq1d	|- ( ph -> ( ( ( 0 ..^ ( L - ( # ` W ) ) ) X. { C } ) ++ W ) = ( (/) ++ W ) )
8		ccatlid	|- ( W e. Word S -> ( (/) ++ W ) = W )
9	2 8	syl	|- ( ph -> ( (/) ++ W ) = W )
10	5 7 9	3eqtrd	|- ( ph -> ( ( C leftpad W ) ` L ) = W )
11	10	fveq2d	|- ( ph -> ( # ` ( ( C leftpad W ) ` L ) ) = ( # ` W ) )