Metamath Proof Explorer

Theorem lpadlen2

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

		Ref	Expression
	Hypotheses	lpadlen.1	$⊢ φ \to L \in ℕ_{0}$
		lpadlen.2	$⊢ φ \to W \in Word S$
		lpadlen.3	$⊢ φ \to C \in S$
		lpadlen2.1	$⊢ φ \to \|W\| \leq L$
	Assertion	lpadlen2	$⊢ φ \to \|(C leftpad W) (L)\| = L$

Proof

Step	Hyp	Ref	Expression
1		lpadlen.1	$⊢ φ \to L \in ℕ_{0}$
2		lpadlen.2	$⊢ φ \to W \in Word S$
3		lpadlen.3	$⊢ φ \to C \in S$
4		lpadlen2.1	$⊢ φ \to \|W\| \leq L$
5	1 2 3	lpadval	$⊢ φ \to (C leftpad W) (L) = ((0 ..^L - \|W\|) \times \{C\}) ++ W$
6	5	fveq2d	$⊢ φ \to \|(C leftpad W) (L)\| = \|((0 ..^L - \|W\|) \times \{C\}) ++ W\|$
7	3	lpadlem1	$⊢ φ \to (0 ..^L - \|W\|) \times \{C\} \in Word S$
8		ccatlen	$⊢ ((0 ..^L - \|W\|) \times \{C\} \in Word S \land W \in Word S) \to \|((0 ..^L - \|W\|) \times \{C\}) ++ W\| = \|(0 ..^L - \|W\|) \times \{C\}\| + \|W\|$
9	7 2 8	syl2anc	$⊢ φ \to \|((0 ..^L - \|W\|) \times \{C\}) ++ W\| = \|(0 ..^L - \|W\|) \times \{C\}\| + \|W\|$
10	1 2 3 4	lpadlem2	$⊢ φ \to \|(0 ..^L - \|W\|) \times \{C\}\| = L - \|W\|$
11	10	oveq1d	$⊢ φ \to \|(0 ..^L - \|W\|) \times \{C\}\| + \|W\| = L - \|W\| + \|W\|$
12	1	nn0cnd	$⊢ φ \to L \in ℂ$
13		lencl	$⊢ W \in Word S \to \|W\| \in ℕ_{0}$
14	2 13	syl	$⊢ φ \to \|W\| \in ℕ_{0}$
15	14	nn0cnd	$⊢ φ \to \|W\| \in ℂ$
16	12 15	npcand	$⊢ φ \to L - \|W\| + \|W\| = L$
17	9 11 16	3eqtrd	$⊢ φ \to \|((0 ..^L - \|W\|) \times \{C\}) ++ W\| = L$
18	6 17	eqtrd	$⊢ φ \to \|(C leftpad W) (L)\| = L$