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∈WordS
lpadval.3 ⊢φ→C∈S
Assertion lpadval ⊢φ→CleftpadW⁡L=0..^L−W×C++W

Proof

Step Hyp Ref Expression
1 lpadval.1 ⊢φ→L∈ℕ0
2 lpadval.2 ⊢φ→W∈WordS
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 ⊢φ→CleftpadW=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 ⊢φ→CleftpadW⁡L=0..^L−W×C++W