Theorem lpadlen1

Description: Length of a left-padded word, in the case the length of the given word W is at least the desired length. (Contributed by Thierry Arnoux, 7-Aug-2023)

	Ref	Expression
Hypotheses	lpadlen.1	$$⊢\phi \to L\in {\mathbb{N}}_0$$
	lpadlen.2	$$⊢\phi \to W\in \mathrm{Word}S$$
	lpadlen.3	$$⊢\phi \to C\in S$$
	lpadlen1.1	$$⊢\phi \to L\le \left|W\right|$$
Assertion	lpadlen1	$$⊢\phi \to \left|\left(C\mathrm{leftpad}W\right)\left(L\right)\right|=\left|W\right|$$

Proof

Step	Hyp	Ref	Expression
1		lpadlen.1	$$⊢\phi \to L\in {\mathbb{N}}_0$$
2		lpadlen.2	$$⊢\phi \to W\in \mathrm{Word}S$$
3		lpadlen.3	$$⊢\phi \to C\in S$$
4		lpadlen1.1	$$⊢\phi \to L\le \left|W\right|$$
5	1 2 3	lpadval	$$⊢\phi \to \left(C\mathrm{leftpad}W\right)\left(L\right)=\left(\left(0..^L-\left|W\right|\right)\times \left\{C\right\}\right)\mathrm{++}W$$
6	1 2 3 4	lpadlem3	$$⊢\phi \to \left(0..^L-\left|W\right|\right)\times \left\{C\right\}=\varnothing$$
7	6	oveq1d	$$⊢\phi \to \left(\left(0..^L-\left|W\right|\right)\times \left\{C\right\}\right)\mathrm{++}W=\varnothing \mathrm{++}W$$
8		ccatlid	$$⊢W\in \mathrm{Word}S\to \varnothing \mathrm{++}W=W$$
9	2 8	syl	$$⊢\phi \to \varnothing \mathrm{++}W=W$$
10	5 7 9	3eqtrd	$$⊢\phi \to \left(C\mathrm{leftpad}W\right)\left(L\right)=W$$
11	10	fveq2d	$$⊢\phi \to \left|\left(C\mathrm{leftpad}W\right)\left(L\right)\right|=\left|W\right|$$