Definition df-lpad 31965

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 31964	. 2 class leftpad
2		vc	. . 3 setvar 𝑐
3		vw	. . 3 setvar 𝑤
4		cvv 3491	. . 3 class V
5		vl	. . . 4 setvar 𝑙
6		cn0 11891	. . . 4 class ℕ0
7		cc0 10530	. . . . . . 7 class 0
8	5	cv 1535	. . . . . . . 8 class 𝑙
9	3	cv 1535	. . . . . . . . 9 class 𝑤
10		chash 13687	. . . . . . . . 9 class ♯
11	9, 10	cfv 6348	. . . . . . . 8 class (♯‘𝑤)
12		cmin 10863	. . . . . . . 8 class −
13	8, 11, 12	co 7149	. . . . . . 7 class (𝑙 − (♯‘𝑤))
14		cfzo 13030	. . . . . . 7 class ..^
15	7, 13, 14	co 7149	. . . . . 6 class (0..^(𝑙 − (♯‘𝑤)))
16	2	cv 1535	. . . . . . 7 class 𝑐
17	16	csn 4560	. . . . . 6 class {𝑐}
18	15, 17	cxp 5546	. . . . 5 class ((0..^(𝑙 − (♯‘𝑤))) × {𝑐})
19		cconcat 13915	. . . . 5 class ++
20	18, 9, 19	co 7149	. . . 4 class (((0..^(𝑙 − (♯‘𝑤))) × {𝑐}) ++ 𝑤)
21	5, 6, 20	cmpt 5139	. . 3 class (𝑙 ∈ ℕ0 ↦ (((0..^(𝑙 − (♯‘𝑤))) × {𝑐}) ++ 𝑤))
22	2, 3, 4, 4, 21	cmpo 7151	. 2 class (𝑐 ∈ V, 𝑤 ∈ V ↦ (𝑙 ∈ ℕ0 ↦ (((0..^(𝑙 − (♯‘𝑤))) × {𝑐}) ++ 𝑤)))
23	1, 22	wceq 1536	1 wff leftpad = (𝑐 ∈ V, 𝑤 ∈ V ↦ (𝑙 ∈ ℕ0 ↦ (((0..^(𝑙 − (♯‘𝑤))) × {𝑐}) ++ 𝑤)))

This definition is referenced by:  lpadval  31966