Theorem lpadval

Description: Value of the leftpad function. (Contributed by Thierry Arnoux, 7-Aug-2023)

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

Proof

Step	Hyp	Ref	Expression
1		lpadval.1	⊢ ( 𝜑 → 𝐿 ∈ ℕ0 )
2		lpadval.2	⊢ ( 𝜑 → 𝑊 ∈ Word 𝑆 )
3		lpadval.3	⊢ ( 𝜑 → 𝐶 ∈ 𝑆 )
4		df-lpad	⊢ leftpad = ( 𝑐 ∈ V , 𝑤 ∈ V ↦ ( 𝑙 ∈ ℕ0 ↦ ( ( ( 0 ..^ ( 𝑙 − ( ♯ ‘ 𝑤 ) ) ) × { 𝑐 } ) ++ 𝑤 ) ) )
5	4	a1i	⊢ ( 𝜑 → leftpad = ( 𝑐 ∈ V , 𝑤 ∈ V ↦ ( 𝑙 ∈ ℕ0 ↦ ( ( ( 0 ..^ ( 𝑙 − ( ♯ ‘ 𝑤 ) ) ) × { 𝑐 } ) ++ 𝑤 ) ) ) )
6		simprr	⊢ ( ( 𝜑 ∧ ( 𝑐 = 𝐶 ∧ 𝑤 = 𝑊 ) ) → 𝑤 = 𝑊 )
7	6	fveq2d	⊢ ( ( 𝜑 ∧ ( 𝑐 = 𝐶 ∧ 𝑤 = 𝑊 ) ) → ( ♯ ‘ 𝑤 ) = ( ♯ ‘ 𝑊 ) )
8	7	oveq2d	⊢ ( ( 𝜑 ∧ ( 𝑐 = 𝐶 ∧ 𝑤 = 𝑊 ) ) → ( 𝑙 − ( ♯ ‘ 𝑤 ) ) = ( 𝑙 − ( ♯ ‘ 𝑊 ) ) )
9	8	oveq2d	⊢ ( ( 𝜑 ∧ ( 𝑐 = 𝐶 ∧ 𝑤 = 𝑊 ) ) → ( 0 ..^ ( 𝑙 − ( ♯ ‘ 𝑤 ) ) ) = ( 0 ..^ ( 𝑙 − ( ♯ ‘ 𝑊 ) ) ) )
10		simprl	⊢ ( ( 𝜑 ∧ ( 𝑐 = 𝐶 ∧ 𝑤 = 𝑊 ) ) → 𝑐 = 𝐶 )
11	10	sneqd	⊢ ( ( 𝜑 ∧ ( 𝑐 = 𝐶 ∧ 𝑤 = 𝑊 ) ) → { 𝑐 } = { 𝐶 } )
12	9 11	xpeq12d	⊢ ( ( 𝜑 ∧ ( 𝑐 = 𝐶 ∧ 𝑤 = 𝑊 ) ) → ( ( 0 ..^ ( 𝑙 − ( ♯ ‘ 𝑤 ) ) ) × { 𝑐 } ) = ( ( 0 ..^ ( 𝑙 − ( ♯ ‘ 𝑊 ) ) ) × { 𝐶 } ) )
13	12 6	oveq12d	⊢ ( ( 𝜑 ∧ ( 𝑐 = 𝐶 ∧ 𝑤 = 𝑊 ) ) → ( ( ( 0 ..^ ( 𝑙 − ( ♯ ‘ 𝑤 ) ) ) × { 𝑐 } ) ++ 𝑤 ) = ( ( ( 0 ..^ ( 𝑙 − ( ♯ ‘ 𝑊 ) ) ) × { 𝐶 } ) ++ 𝑊 ) )
14	13	mpteq2dv	⊢ ( ( 𝜑 ∧ ( 𝑐 = 𝐶 ∧ 𝑤 = 𝑊 ) ) → ( 𝑙 ∈ ℕ0 ↦ ( ( ( 0 ..^ ( 𝑙 − ( ♯ ‘ 𝑤 ) ) ) × { 𝑐 } ) ++ 𝑤 ) ) = ( 𝑙 ∈ ℕ0 ↦ ( ( ( 0 ..^ ( 𝑙 − ( ♯ ‘ 𝑊 ) ) ) × { 𝐶 } ) ++ 𝑊 ) ) )
15	3	elexd	⊢ ( 𝜑 → 𝐶 ∈ V )
16	2	elexd	⊢ ( 𝜑 → 𝑊 ∈ V )
17		nn0ex	⊢ ℕ0 ∈ V
18	17	a1i	⊢ ( 𝜑 → ℕ0 ∈ V )
19	18	mptexd	⊢ ( 𝜑 → ( 𝑙 ∈ ℕ0 ↦ ( ( ( 0 ..^ ( 𝑙 − ( ♯ ‘ 𝑊 ) ) ) × { 𝐶 } ) ++ 𝑊 ) ) ∈ V )
20	5 14 15 16 19	ovmpod	⊢ ( 𝜑 → ( 𝐶 leftpad 𝑊 ) = ( 𝑙 ∈ ℕ0 ↦ ( ( ( 0 ..^ ( 𝑙 − ( ♯ ‘ 𝑊 ) ) ) × { 𝐶 } ) ++ 𝑊 ) ) )
21		simpr	⊢ ( ( 𝜑 ∧ 𝑙 = 𝐿 ) → 𝑙 = 𝐿 )
22	21	oveq1d	⊢ ( ( 𝜑 ∧ 𝑙 = 𝐿 ) → ( 𝑙 − ( ♯ ‘ 𝑊 ) ) = ( 𝐿 − ( ♯ ‘ 𝑊 ) ) )
23	22	oveq2d	⊢ ( ( 𝜑 ∧ 𝑙 = 𝐿 ) → ( 0 ..^ ( 𝑙 − ( ♯ ‘ 𝑊 ) ) ) = ( 0 ..^ ( 𝐿 − ( ♯ ‘ 𝑊 ) ) ) )
24	23	xpeq1d	⊢ ( ( 𝜑 ∧ 𝑙 = 𝐿 ) → ( ( 0 ..^ ( 𝑙 − ( ♯ ‘ 𝑊 ) ) ) × { 𝐶 } ) = ( ( 0 ..^ ( 𝐿 − ( ♯ ‘ 𝑊 ) ) ) × { 𝐶 } ) )
25	24	oveq1d	⊢ ( ( 𝜑 ∧ 𝑙 = 𝐿 ) → ( ( ( 0 ..^ ( 𝑙 − ( ♯ ‘ 𝑊 ) ) ) × { 𝐶 } ) ++ 𝑊 ) = ( ( ( 0 ..^ ( 𝐿 − ( ♯ ‘ 𝑊 ) ) ) × { 𝐶 } ) ++ 𝑊 ) )
26		ovexd	⊢ ( 𝜑 → ( ( ( 0 ..^ ( 𝐿 − ( ♯ ‘ 𝑊 ) ) ) × { 𝐶 } ) ++ 𝑊 ) ∈ V )
27	20 25 1 26	fvmptd	⊢ ( 𝜑 → ( ( 𝐶 leftpad 𝑊 ) ‘ 𝐿 ) = ( ( ( 0 ..^ ( 𝐿 − ( ♯ ‘ 𝑊 ) ) ) × { 𝐶 } ) ++ 𝑊 ) )