Definition df-lpad 34712

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

Assertion

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

Distinct variable group:   𝑐,𝑙,𝑤

Detailed syntax breakdown of Definition df-lpad

Step	Hyp	Ref	Expression
1		clpad 34711	. 2 class leftpad
2		vc	. . 3 setvar 𝑐
3		vw	. . 3 setvar 𝑤
4		cvv 3464	. . 3 class V
5		vl	. . . 4 setvar 𝑙
6		cn0 12506	. . . 4 class ℕ0
7		cc0 11134	. . . . . . 7 class 0
8	5	cv 1539	. . . . . . . 8 class 𝑙
9	3	cv 1539	. . . . . . . . 9 class 𝑤
10		chash 14353	. . . . . . . . 9 class ♯
11	9, 10	cfv 6536	. . . . . . . 8 class (♯‘𝑤)
12		cmin 11471	. . . . . . . 8 class −
13	8, 11, 12	co 7410	. . . . . . 7 class (𝑙 − (♯‘𝑤))
14		cfzo 13676	. . . . . . 7 class ..^
15	7, 13, 14	co 7410	. . . . . 6 class (0..^(𝑙 − (♯‘𝑤)))
16	2	cv 1539	. . . . . . 7 class 𝑐
17	16	csn 4606	. . . . . 6 class {𝑐}
18	15, 17	cxp 5657	. . . . 5 class ((0..^(𝑙 − (♯‘𝑤))) × {𝑐})
19		cconcat 14593	. . . . 5 class ++
20	18, 9, 19	co 7410	. . . 4 class (((0..^(𝑙 − (♯‘𝑤))) × {𝑐}) ++ 𝑤)
21	5, 6, 20	cmpt 5206	. . 3 class (𝑙 ∈ ℕ0 ↦ (((0..^(𝑙 − (♯‘𝑤))) × {𝑐}) ++ 𝑤))
22	2, 3, 4, 4, 21	cmpo 7412	. 2 class (𝑐 ∈ V, 𝑤 ∈ V ↦ (𝑙 ∈ ℕ0 ↦ (((0..^(𝑙 − (♯‘𝑤))) × {𝑐}) ++ 𝑤)))
23	1, 22	wceq 1540	1 wff leftpad = (𝑐 ∈ V, 𝑤 ∈ V ↦ (𝑙 ∈ ℕ0 ↦ (((0..^(𝑙 − (♯‘𝑤))) × {𝑐}) ++ 𝑤)))

This definition is referenced by:  lpadval  34713