Definition df-lpad

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

	Ref	Expression
Assertion	df-lpad	⊢ leftpad = ( 𝑐 ∈ V , 𝑤 ∈ V ↦ ( 𝑙 ∈ ℕ0 ↦ ( ( ( 0 ..^ ( 𝑙 − ( ♯ ‘ 𝑤 ) ) ) × { 𝑐 } ) ++ 𝑤 ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		clpad	⊢ leftpad
1		vc	⊢ 𝑐
2		cvv	⊢ V
3		vw	⊢ 𝑤
4		vl	⊢ 𝑙
5		cn0	⊢ ℕ0
6		cc0	⊢ 0
7		cfzo	⊢ ..^
8	4	cv	⊢ 𝑙
9		cmin	⊢ −
10		chash	⊢ ♯
11	3	cv	⊢ 𝑤
12	11 10	cfv	⊢ ( ♯ ‘ 𝑤 )
13	8 12 9	co	⊢ ( 𝑙 − ( ♯ ‘ 𝑤 ) )
14	6 13 7	co	⊢ ( 0 ..^ ( 𝑙 − ( ♯ ‘ 𝑤 ) ) )
15	1	cv	⊢ 𝑐
16	15	csn	⊢ { 𝑐 }
17	14 16	cxp	⊢ ( ( 0 ..^ ( 𝑙 − ( ♯ ‘ 𝑤 ) ) ) × { 𝑐 } )
18		cconcat	⊢ ++
19	17 11 18	co	⊢ ( ( ( 0 ..^ ( 𝑙 − ( ♯ ‘ 𝑤 ) ) ) × { 𝑐 } ) ++ 𝑤 )
20	4 5 19	cmpt	⊢ ( 𝑙 ∈ ℕ0 ↦ ( ( ( 0 ..^ ( 𝑙 − ( ♯ ‘ 𝑤 ) ) ) × { 𝑐 } ) ++ 𝑤 ) )
21	1 3 2 2 20	cmpo	⊢ ( 𝑐 ∈ V , 𝑤 ∈ V ↦ ( 𝑙 ∈ ℕ0 ↦ ( ( ( 0 ..^ ( 𝑙 − ( ♯ ‘ 𝑤 ) ) ) × { 𝑐 } ) ++ 𝑤 ) ) )
22	0 21	wceq	⊢ leftpad = ( 𝑐 ∈ V , 𝑤 ∈ V ↦ ( 𝑙 ∈ ℕ0 ↦ ( ( ( 0 ..^ ( 𝑙 − ( ♯ ‘ 𝑤 ) ) ) × { 𝑐 } ) ++ 𝑤 ) ) )