Metamath Proof Explorer

Theorem lpadlem2

Description: Lemma for the leftpad theorems. (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 lpadlem2 ⊢ φ → 0 ..^ L − W × C = L − W

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 fzofi ⊢ 0 ..^ L − W ∈ Fin
6 snfi ⊢ C ∈ Fin
7 hashxp ⊢ 0 ..^ L − W ∈ Fin ∧ C ∈ Fin → 0 ..^ L − W × C = 0 ..^ L − W ⁢ C
8 5 6 7 mp2an ⊢ 0 ..^ L − W × C = 0 ..^ L − W ⁢ C
9 8 a1i ⊢ φ → 0 ..^ L − W × C = 0 ..^ L − W ⁢ C
10 lencl ⊢ W ∈ Word S → W ∈ ℕ 0
11 2 10 syl ⊢ φ → W ∈ ℕ 0
12 nn0sub2 ⊢ W ∈ ℕ 0 ∧ L ∈ ℕ 0 ∧ W ≤ L → L − W ∈ ℕ 0
13 11 1 4 12 syl3anc ⊢ φ → L − W ∈ ℕ 0
14 hashfzo0 ⊢ L − W ∈ ℕ 0 → 0 ..^ L − W = L − W
15 13 14 syl ⊢ φ → 0 ..^ L − W = L − W
16 hashsng ⊢ C ∈ S → C = 1
17 3 16 syl ⊢ φ → C = 1
18 15 17 oveq12d ⊢ φ → 0 ..^ L − W ⁢ C = L − W ⋅ 1
19 13 nn0cnd ⊢ φ → L − W ∈ ℂ
20 19 mulridd ⊢ φ → L − W ⋅ 1 = L − W
21 9 18 20 3eqtrd ⊢ φ → 0 ..^ L − W × C = L − W