Metamath Proof Explorer

Theorem lpadval

Description: Value of the leftpad function. (Contributed by Thierry Arnoux, 7-Aug-2023)

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

Proof

Step Hyp Ref Expression
1 lpadval.1 ⊢ φ → L ∈ ℕ 0
2 lpadval.2 ⊢ φ → W ∈ Word S
3 lpadval.3 ⊢ φ → C ∈ S
4 df-lpad ⊢ leftpad = c ∈ V , w ∈ V ⟼ l ∈ ℕ 0 ⟼ 0 ..^ l − w × c ++ w
5 4 a1i ⊢ φ → leftpad = c ∈ V , w ∈ V ⟼ l ∈ ℕ 0 ⟼ 0 ..^ l − w × c ++ w
6 simprr ⊢ φ ∧ c = C ∧ w = W → w = W
7 6 fveq2d ⊢ φ ∧ c = C ∧ w = W → w = W
8 7 oveq2d ⊢ φ ∧ c = C ∧ w = W → l − w = l − W
9 8 oveq2d ⊢ φ ∧ c = C ∧ w = W → 0 ..^ l − w = 0 ..^ l − W
10 simprl ⊢ φ ∧ c = C ∧ w = W → c = C
11 10 sneqd ⊢ φ ∧ c = C ∧ w = W → c = C
12 9 11 xpeq12d ⊢ φ ∧ c = C ∧ w = W → 0 ..^ l − w × c = 0 ..^ l − W × C
13 12 6 oveq12d ⊢ φ ∧ c = C ∧ w = W → 0 ..^ l − w × c ++ w = 0 ..^ l − W × C ++ W
14 13 mpteq2dv ⊢ φ ∧ c = C ∧ w = W → l ∈ ℕ 0 ⟼ 0 ..^ l − w × c ++ w = l ∈ ℕ 0 ⟼ 0 ..^ l − W × C ++ W
15 3 elexd ⊢ φ → C ∈ V
16 2 elexd ⊢ φ → W ∈ V
17 nn0ex ⊢ ℕ 0 ∈ V
18 17 a1i ⊢ φ → ℕ 0 ∈ V
19 18 mptexd ⊢ φ → l ∈ ℕ 0 ⟼ 0 ..^ l − W × C ++ W ∈ V
20 5 14 15 16 19 ovmpod ⊢ φ → C leftpad W = l ∈ ℕ 0 ⟼ 0 ..^ l − W × C ++ W
21 simpr ⊢ φ ∧ l = L → l = L
22 21 oveq1d ⊢ φ ∧ l = L → l − W = L − W
23 22 oveq2d ⊢ φ ∧ l = L → 0 ..^ l − W = 0 ..^ L − W
24 23 xpeq1d ⊢ φ ∧ l = L → 0 ..^ l − W × C = 0 ..^ L − W × C
25 24 oveq1d ⊢ φ ∧ l = L → 0 ..^ l − W × C ++ W = 0 ..^ L − W × C ++ W
26 ovexd ⊢ φ → 0 ..^ L − W × C ++ W ∈ V
27 20 25 1 26 fvmptd ⊢ φ → C leftpad W ⁡ L = 0 ..^ L − W × C ++ W