Metamath Proof Explorer

Definition df-lpad

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

Ref Expression
Assertion df-lpad ⊢ leftpad = c ∈ V , w ∈ V ⟼ l ∈ ℕ 0 ⟼ 0 ..^ l − w × c ++ w

Detailed syntax breakdown

Step Hyp Ref Expression
0 clpad class leftpad
1 vc setvar c
2 cvv class V
3 vw setvar w
4 vl setvar l
5 cn0 class ℕ 0
6 cc0 class 0
7 cfzo class ..^
8 4 cv setvar l
9 cmin class −
10 chash class .
11 3 cv setvar w
12 11 10 cfv class w
13 8 12 9 co class l − w
14 6 13 7 co class 0 ..^ l − w
15 1 cv setvar c
16 15 csn class c
17 14 16 cxp class 0 ..^ l − w × c
18 cconcat class ++
19 17 11 18 co class 0 ..^ l − w × c ++ w
20 4 5 19 cmpt class l ∈ ℕ 0 ⟼ 0 ..^ l − w × c ++ w
21 1 3 2 2 20 cmpo class c ∈ V , w ∈ V ⟼ l ∈ ℕ 0 ⟼ 0 ..^ l − w × c ++ w
22 0 21 wceq wff leftpad = c ∈ V , w ∈ V ⟼ l ∈ ℕ 0 ⟼ 0 ..^ l − w × c ++ w