Theorem lpadlem2

Description: Lemma for the leftpad theorems. (Contributed by Thierry Arnoux, 7-Aug-2023)

	Ref	Expression
Hypotheses	lpadlen.1	⊢ ( 𝜑 → 𝐿 ∈ ℕ0 )
	lpadlen.2	⊢ ( 𝜑 → 𝑊 ∈ Word 𝑆 )
	lpadlen.3	⊢ ( 𝜑 → 𝐶 ∈ 𝑆 )
	lpadlen2.1	⊢ ( 𝜑 → ( ♯ ‘ 𝑊 ) ≤ 𝐿 )
Assertion	lpadlem2	⊢ ( 𝜑 → ( ♯ ‘ ( ( 0 ..^ ( 𝐿 − ( ♯ ‘ 𝑊 ) ) ) × { 𝐶 } ) ) = ( 𝐿 − ( ♯ ‘ 𝑊 ) ) )

Proof

Step	Hyp	Ref	Expression
1		lpadlen.1	⊢ ( 𝜑 → 𝐿 ∈ ℕ0 )
2		lpadlen.2	⊢ ( 𝜑 → 𝑊 ∈ Word 𝑆 )
3		lpadlen.3	⊢ ( 𝜑 → 𝐶 ∈ 𝑆 )
4		lpadlen2.1	⊢ ( 𝜑 → ( ♯ ‘ 𝑊 ) ≤ 𝐿 )
5		fzofi	⊢ ( 0 ..^ ( 𝐿 − ( ♯ ‘ 𝑊 ) ) ) ∈ Fin
6		snfi	⊢ { 𝐶 } ∈ Fin
7		hashxp	⊢ ( ( ( 0 ..^ ( 𝐿 − ( ♯ ‘ 𝑊 ) ) ) ∈ Fin ∧ { 𝐶 } ∈ Fin ) → ( ♯ ‘ ( ( 0 ..^ ( 𝐿 − ( ♯ ‘ 𝑊 ) ) ) × { 𝐶 } ) ) = ( ( ♯ ‘ ( 0 ..^ ( 𝐿 − ( ♯ ‘ 𝑊 ) ) ) ) · ( ♯ ‘ { 𝐶 } ) ) )
8	5 6 7	mp2an	⊢ ( ♯ ‘ ( ( 0 ..^ ( 𝐿 − ( ♯ ‘ 𝑊 ) ) ) × { 𝐶 } ) ) = ( ( ♯ ‘ ( 0 ..^ ( 𝐿 − ( ♯ ‘ 𝑊 ) ) ) ) · ( ♯ ‘ { 𝐶 } ) )
9	8	a1i	⊢ ( 𝜑 → ( ♯ ‘ ( ( 0 ..^ ( 𝐿 − ( ♯ ‘ 𝑊 ) ) ) × { 𝐶 } ) ) = ( ( ♯ ‘ ( 0 ..^ ( 𝐿 − ( ♯ ‘ 𝑊 ) ) ) ) · ( ♯ ‘ { 𝐶 } ) ) )
10		lencl	⊢ ( 𝑊 ∈ Word 𝑆 → ( ♯ ‘ 𝑊 ) ∈ ℕ0 )
11	2 10	syl	⊢ ( 𝜑 → ( ♯ ‘ 𝑊 ) ∈ ℕ0 )
12		nn0sub2	⊢ ( ( ( ♯ ‘ 𝑊 ) ∈ ℕ0 ∧ 𝐿 ∈ ℕ0 ∧ ( ♯ ‘ 𝑊 ) ≤ 𝐿 ) → ( 𝐿 − ( ♯ ‘ 𝑊 ) ) ∈ ℕ0 )
13	11 1 4 12	syl3anc	⊢ ( 𝜑 → ( 𝐿 − ( ♯ ‘ 𝑊 ) ) ∈ ℕ0 )
14		hashfzo0	⊢ ( ( 𝐿 − ( ♯ ‘ 𝑊 ) ) ∈ ℕ0 → ( ♯ ‘ ( 0 ..^ ( 𝐿 − ( ♯ ‘ 𝑊 ) ) ) ) = ( 𝐿 − ( ♯ ‘ 𝑊 ) ) )
15	13 14	syl	⊢ ( 𝜑 → ( ♯ ‘ ( 0 ..^ ( 𝐿 − ( ♯ ‘ 𝑊 ) ) ) ) = ( 𝐿 − ( ♯ ‘ 𝑊 ) ) )
16		hashsng	⊢ ( 𝐶 ∈ 𝑆 → ( ♯ ‘ { 𝐶 } ) = 1 )
17	3 16	syl	⊢ ( 𝜑 → ( ♯ ‘ { 𝐶 } ) = 1 )
18	15 17	oveq12d	⊢ ( 𝜑 → ( ( ♯ ‘ ( 0 ..^ ( 𝐿 − ( ♯ ‘ 𝑊 ) ) ) ) · ( ♯ ‘ { 𝐶 } ) ) = ( ( 𝐿 − ( ♯ ‘ 𝑊 ) ) · 1 ) )
19	13	nn0cnd	⊢ ( 𝜑 → ( 𝐿 − ( ♯ ‘ 𝑊 ) ) ∈ ℂ )
20	19	mulid1d	⊢ ( 𝜑 → ( ( 𝐿 − ( ♯ ‘ 𝑊 ) ) · 1 ) = ( 𝐿 − ( ♯ ‘ 𝑊 ) ) )
21	9 18 20	3eqtrd	⊢ ( 𝜑 → ( ♯ ‘ ( ( 0 ..^ ( 𝐿 − ( ♯ ‘ 𝑊 ) ) ) × { 𝐶 } ) ) = ( 𝐿 − ( ♯ ‘ 𝑊 ) ) )