Metamath Proof Explorer

Theorem lpadleft

Description: The contents of prefix of a left-padded word is always the letter C . (Contributed by Thierry Arnoux, 7-Aug-2023)

Ref Expression
Hypotheses lpadlen.1 ⊢ φ → L ∈ ℕ 0
lpadlen.2 ⊢ φ → W ∈ Word S
lpadlen.3 ⊢ φ → C ∈ S
lpadleft.1 ⊢ φ → N ∈ 0 ..^ L − W
Assertion lpadleft ⊢ φ → C leftpad W ⁡ L ⁡ N = C

Proof

Step Hyp Ref Expression
1 lpadlen.1 ⊢ φ → L ∈ ℕ 0
2 lpadlen.2 ⊢ φ → W ∈ Word S
3 lpadlen.3 ⊢ φ → C ∈ S
4 lpadleft.1 ⊢ φ → N ∈ 0 ..^ L − W
5 1 2 3 lpadval ⊢ φ → C leftpad W ⁡ L = 0 ..^ L − W × C ++ W
6 5 fveq1d ⊢ φ → C leftpad W ⁡ L ⁡ N = 0 ..^ L − W × C ++ W ⁡ N
7 3 lpadlem1 ⊢ φ → 0 ..^ L − W × C ∈ Word S
8 lencl ⊢ W ∈ Word S → W ∈ ℕ 0
9 2 8 syl ⊢ φ → W ∈ ℕ 0
10 elfzo0 ⊢ N ∈ 0 ..^ L − W ↔ N ∈ ℕ 0 ∧ L − W ∈ ℕ ∧ N < L − W
11 4 10 sylib ⊢ φ → N ∈ ℕ 0 ∧ L − W ∈ ℕ ∧ N < L − W
12 11 simp2d ⊢ φ → L − W ∈ ℕ
13 12 nnnn0d ⊢ φ → L − W ∈ ℕ 0
14 nn0sub ⊢ W ∈ ℕ 0 ∧ L ∈ ℕ 0 → W ≤ L ↔ L − W ∈ ℕ 0
15 14 biimpar ⊢ W ∈ ℕ 0 ∧ L ∈ ℕ 0 ∧ L − W ∈ ℕ 0 → W ≤ L
16 9 1 13 15 syl21anc ⊢ φ → W ≤ L
17 1 2 3 16 lpadlem2 ⊢ φ → 0 ..^ L − W × C = L − W
18 17 oveq2d ⊢ φ → 0 ..^ 0 ..^ L − W × C = 0 ..^ L − W
19 4 18 eleqtrrd ⊢ φ → N ∈ 0 ..^ 0 ..^ L − W × C
20 ccatval1 ⊢ 0 ..^ L − W × C ∈ Word S ∧ W ∈ Word S ∧ N ∈ 0 ..^ 0 ..^ L − W × C → 0 ..^ L − W × C ++ W ⁡ N = 0 ..^ L − W × C ⁡ N
21 7 2 19 20 syl3anc ⊢ φ → 0 ..^ L − W × C ++ W ⁡ N = 0 ..^ L − W × C ⁡ N
22 fvconst2g ⊢ C ∈ S ∧ N ∈ 0 ..^ L − W → 0 ..^ L − W × C ⁡ N = C
23 3 4 22 syl2anc ⊢ φ → 0 ..^ L − W × C ⁡ N = C
24 6 21 23 3eqtrd ⊢ φ → C leftpad W ⁡ L ⁡ N = C