Theorem lpadlem2

Description: Lemma for the leftpad theorems. (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	lpadlem2	|- ( ph -> ( # ` ( ( 0 ..^ ( L - ( # ` W ) ) ) X. { C } ) ) = ( 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		lpadlen2.1	|- ( ph -> ( # ` W ) <_ L )
5		fzofi	|- ( 0 ..^ ( L - ( # ` W ) ) ) e. Fin
6		snfi	|- { C } e. Fin
7		hashxp	|- ( ( ( 0 ..^ ( L - ( # ` W ) ) ) e. Fin /\ { C } e. Fin ) -> ( # ` ( ( 0 ..^ ( L - ( # ` W ) ) ) X. { C } ) ) = ( ( # ` ( 0 ..^ ( L - ( # ` W ) ) ) ) x. ( # ` { C } ) ) )
8	5 6 7	mp2an	|- ( # ` ( ( 0 ..^ ( L - ( # ` W ) ) ) X. { C } ) ) = ( ( # ` ( 0 ..^ ( L - ( # ` W ) ) ) ) x. ( # ` { C } ) )
9	8	a1i	|- ( ph -> ( # ` ( ( 0 ..^ ( L - ( # ` W ) ) ) X. { C } ) ) = ( ( # ` ( 0 ..^ ( L - ( # ` W ) ) ) ) x. ( # ` { C } ) ) )
10		lencl	|- ( W e. Word S -> ( # ` W ) e. NN0 )
11	2 10	syl	|- ( ph -> ( # ` W ) e. NN0 )
12		nn0sub2	|- ( ( ( # ` W ) e. NN0 /\ L e. NN0 /\ ( # ` W ) <_ L ) -> ( L - ( # ` W ) ) e. NN0 )
13	11 1 4 12	syl3anc	|- ( ph -> ( L - ( # ` W ) ) e. NN0 )
14		hashfzo0	|- ( ( L - ( # ` W ) ) e. NN0 -> ( # ` ( 0 ..^ ( L - ( # ` W ) ) ) ) = ( L - ( # ` W ) ) )
15	13 14	syl	|- ( ph -> ( # ` ( 0 ..^ ( L - ( # ` W ) ) ) ) = ( L - ( # ` W ) ) )
16		hashsng	|- ( C e. S -> ( # ` { C } ) = 1 )
17	3 16	syl	|- ( ph -> ( # ` { C } ) = 1 )
18	15 17	oveq12d	|- ( ph -> ( ( # ` ( 0 ..^ ( L - ( # ` W ) ) ) ) x. ( # ` { C } ) ) = ( ( L - ( # ` W ) ) x. 1 ) )
19	13	nn0cnd	|- ( ph -> ( L - ( # ` W ) ) e. CC )
20	19	mulridd	|- ( ph -> ( ( L - ( # ` W ) ) x. 1 ) = ( L - ( # ` W ) ) )
21	9 18 20	3eqtrd	|- ( ph -> ( # ` ( ( 0 ..^ ( L - ( # ` W ) ) ) X. { C } ) ) = ( L - ( # ` W ) ) )