Theorem lpadlem3

Description: Lemma for lpadlen1 . (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	lpadlem3	|- ( ph -> ( ( 0 ..^ ( L - ( # ` W ) ) ) X. { 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		lpadlen1.1	|- ( ph -> L <_ ( # ` W ) )
5		lencl	|- ( W e. Word S -> ( # ` W ) e. NN0 )
6	2 5	syl	|- ( ph -> ( # ` W ) e. NN0 )
7	6	nn0zd	|- ( ph -> ( # ` W ) e. ZZ )
8	1	nn0zd	|- ( ph -> L e. ZZ )
9		fzo0n	|- ( ( ( # ` W ) e. ZZ /\ L e. ZZ ) -> ( L <_ ( # ` W ) <-> ( 0 ..^ ( L - ( # ` W ) ) ) = (/) ) )
10	9	biimpa	|- ( ( ( ( # ` W ) e. ZZ /\ L e. ZZ ) /\ L <_ ( # ` W ) ) -> ( 0 ..^ ( L - ( # ` W ) ) ) = (/) )
11	7 8 4 10	syl21anc	|- ( ph -> ( 0 ..^ ( L - ( # ` W ) ) ) = (/) )
12	11	xpeq1d	|- ( ph -> ( ( 0 ..^ ( L - ( # ` W ) ) ) X. { C } ) = ( (/) X. { C } ) )
13		0xp	|- ( (/) X. { C } ) = (/)
14	12 13	eqtrdi	|- ( ph -> ( ( 0 ..^ ( L - ( # ` W ) ) ) X. { C } ) = (/) )