df-lpad

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

		Ref	Expression
	Assertion	df-lpad	$⊢ leftpad = (c \in V, w \in V ⟼ (l \in ℕ_{0} ⟼ ((0 ..^l - \|w\|) \times \{c\}) ++ w))$

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\|) \times \{c\})$
18		cconcat	$class ++$
19	17 11 18	co	$class (((0 ..^l - \|w\|) \times \{c\}) ++ w)$
20	4 5 19	cmpt	$class (l \in ℕ_{0} ⟼ ((0 ..^l - \|w\|) \times \{c\}) ++ w)$
21	1 3 2 2 20	cmpo	$class (c \in V, w \in V ⟼ (l \in ℕ_{0} ⟼ ((0 ..^l - \|w\|) \times \{c\}) ++ w))$
22	0 21	wceq	$wff leftpad = (c \in V, w \in V ⟼ (l \in ℕ_{0} ⟼ ((0 ..^l - \|w\|) \times \{c\}) ++ w))$

Metamath Proof Explorer