Theorem lpadleft

Description: The contents of prefix of a left-padded word is always the letter C . (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 )
	lpadleft.1	|- ( ph -> N e. ( 0 ..^ ( L - ( # ` W ) ) ) )
Assertion	lpadleft	|- ( ph -> ( ( ( C leftpad W ) ` L ) ` N ) = C )

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		lpadleft.1	|- ( ph -> N e. ( 0 ..^ ( L - ( # ` W ) ) ) )
5	1 2 3	lpadval	|- ( ph -> ( ( C leftpad W ) ` L ) = ( ( ( 0 ..^ ( L - ( # ` W ) ) ) X. { C } ) ++ W ) )
6	5	fveq1d	|- ( ph -> ( ( ( C leftpad W ) ` L ) ` N ) = ( ( ( ( 0 ..^ ( L - ( # ` W ) ) ) X. { C } ) ++ W ) ` N ) )
7	3	lpadlem1	|- ( ph -> ( ( 0 ..^ ( L - ( # ` W ) ) ) X. { C } ) e. Word S )
8		lencl	|- ( W e. Word S -> ( # ` W ) e. NN0 )
9	2 8	syl	|- ( ph -> ( # ` W ) e. NN0 )
10		elfzo0	|- ( N e. ( 0 ..^ ( L - ( # ` W ) ) ) <-> ( N e. NN0 /\ ( L - ( # ` W ) ) e. NN /\ N < ( L - ( # ` W ) ) ) )
11	4 10	sylib	|- ( ph -> ( N e. NN0 /\ ( L - ( # ` W ) ) e. NN /\ N < ( L - ( # ` W ) ) ) )
12	11	simp2d	|- ( ph -> ( L - ( # ` W ) ) e. NN )
13	12	nnnn0d	|- ( ph -> ( L - ( # ` W ) ) e. NN0 )
14		nn0sub	|- ( ( ( # ` W ) e. NN0 /\ L e. NN0 ) -> ( ( # ` W ) <_ L <-> ( L - ( # ` W ) ) e. NN0 ) )
15	14	biimpar	|- ( ( ( ( # ` W ) e. NN0 /\ L e. NN0 ) /\ ( L - ( # ` W ) ) e. NN0 ) -> ( # ` W ) <_ L )
16	9 1 13 15	syl21anc	|- ( ph -> ( # ` W ) <_ L )
17	1 2 3 16	lpadlem2	|- ( ph -> ( # ` ( ( 0 ..^ ( L - ( # ` W ) ) ) X. { C } ) ) = ( L - ( # ` W ) ) )
18	17	oveq2d	|- ( ph -> ( 0 ..^ ( # ` ( ( 0 ..^ ( L - ( # ` W ) ) ) X. { C } ) ) ) = ( 0 ..^ ( L - ( # ` W ) ) ) )
19	4 18	eleqtrrd	|- ( ph -> N e. ( 0 ..^ ( # ` ( ( 0 ..^ ( L - ( # ` W ) ) ) X. { C } ) ) ) )
20		ccatval1	|- ( ( ( ( 0 ..^ ( L - ( # ` W ) ) ) X. { C } ) e. Word S /\ W e. Word S /\ N e. ( 0 ..^ ( # ` ( ( 0 ..^ ( L - ( # ` W ) ) ) X. { C } ) ) ) ) -> ( ( ( ( 0 ..^ ( L - ( # ` W ) ) ) X. { C } ) ++ W ) ` N ) = ( ( ( 0 ..^ ( L - ( # ` W ) ) ) X. { C } ) ` N ) )
21	7 2 19 20	syl3anc	|- ( ph -> ( ( ( ( 0 ..^ ( L - ( # ` W ) ) ) X. { C } ) ++ W ) ` N ) = ( ( ( 0 ..^ ( L - ( # ` W ) ) ) X. { C } ) ` N ) )
22		fvconst2g	|- ( ( C e. S /\ N e. ( 0 ..^ ( L - ( # ` W ) ) ) ) -> ( ( ( 0 ..^ ( L - ( # ` W ) ) ) X. { C } ) ` N ) = C )
23	3 4 22	syl2anc	|- ( ph -> ( ( ( 0 ..^ ( L - ( # ` W ) ) ) X. { C } ) ` N ) = C )
24	6 21 23	3eqtrd	|- ( ph -> ( ( ( C leftpad W ) ` L ) ` N ) = C )