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 ⊢ φ → L ∈ ℕ 0
lpadlen.2 ⊢ φ → W ∈ Word S
lpadlen.3 ⊢ φ → C ∈ S
lpadlen2.1 ⊢ φ → W ≤ L
Assertion lpadlen2 ⊢ φ → C leftpad W ⁡ L = L

Proof

Step Hyp Ref Expression
1 lpadlen.1 ⊢ φ → L ∈ ℕ 0
2 lpadlen.2 ⊢ φ → W ∈ Word S
3 lpadlen.3 ⊢ φ → C ∈ S
4 lpadlen2.1 ⊢ φ → W ≤ L
5 1 2 3 lpadval ⊢ φ → C leftpad W ⁡ L = 0 ..^ L − W × C ++ W
6 5 fveq2d ⊢ φ → C leftpad W ⁡ L = 0 ..^ L − W × C ++ W
7 3 lpadlem1 ⊢ φ → 0 ..^ L − W × C ∈ Word S
8 ccatlen ⊢ 0 ..^ L − W × C ∈ Word S ∧ W ∈ Word S → 0 ..^ L − W × C ++ W = 0 ..^ L − W × C + W
9 7 2 8 syl2anc ⊢ φ → 0 ..^ L − W × C ++ W = 0 ..^ L − W × C + W
10 1 2 3 4 lpadlem2 ⊢ φ → 0 ..^ L − W × C = L − W
11 10 oveq1d ⊢ φ → 0 ..^ L − W × C + W = L - W + W
12 1 nn0cnd ⊢ φ → L ∈ ℂ
13 lencl ⊢ W ∈ Word S → W ∈ ℕ 0
14 2 13 syl ⊢ φ → W ∈ ℕ 0
15 14 nn0cnd ⊢ φ → W ∈ ℂ
16 12 15 npcand ⊢ φ → L - W + W = L
17 9 11 16 3eqtrd ⊢ φ → 0 ..^ L − W × C ++ W = L
18 6 17 eqtrd ⊢ φ → C leftpad W ⁡ L = L