Definition df-lpad 32634

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 32633	. 2 class leftpad
2		vc	. . 3 setvar 𝑐
3		vw	. . 3 setvar 𝑤
4		cvv 3430	. . 3 class V
5		vl	. . . 4 setvar 𝑙
6		cn0 12216	. . . 4 class ℕ0
7		cc0 10855	. . . . . . 7 class 0
8	5	cv 1540	. . . . . . . 8 class 𝑙
9	3	cv 1540	. . . . . . . . 9 class 𝑤
10		chash 14025	. . . . . . . . 9 class ♯
11	9, 10	cfv 6430	. . . . . . . 8 class (♯‘𝑤)
12		cmin 11188	. . . . . . . 8 class −
13	8, 11, 12	co 7268	. . . . . . 7 class (𝑙 − (♯‘𝑤))
14		cfzo 13364	. . . . . . 7 class ..^
15	7, 13, 14	co 7268	. . . . . 6 class (0..^(𝑙 − (♯‘𝑤)))
16	2	cv 1540	. . . . . . 7 class 𝑐
17	16	csn 4566	. . . . . 6 class {𝑐}
18	15, 17	cxp 5586	. . . . 5 class ((0..^(𝑙 − (♯‘𝑤))) × {𝑐})
19		cconcat 14254	. . . . 5 class ++
20	18, 9, 19	co 7268	. . . 4 class (((0..^(𝑙 − (♯‘𝑤))) × {𝑐}) ++ 𝑤)
21	5, 6, 20	cmpt 5161	. . 3 class (𝑙 ∈ ℕ0 ↦ (((0..^(𝑙 − (♯‘𝑤))) × {𝑐}) ++ 𝑤))
22	2, 3, 4, 4, 21	cmpo 7270	. 2 class (𝑐 ∈ V, 𝑤 ∈ V ↦ (𝑙 ∈ ℕ0 ↦ (((0..^(𝑙 − (♯‘𝑤))) × {𝑐}) ++ 𝑤)))
23	1, 22	wceq 1541	1 wff leftpad = (𝑐 ∈ V, 𝑤 ∈ V ↦ (𝑙 ∈ ℕ0 ↦ (((0..^(𝑙 − (♯‘𝑤))) × {𝑐}) ++ 𝑤)))

This definition is referenced by:  lpadval  32635