Metamath Proof Explorer

Theorem lpadright

Description: The suffix of a left-padded word the original word W . (Contributed by Thierry Arnoux, 7-Aug-2023)

Ref Expression
Hypotheses lpadlen.1 ⊢φ→L∈ℕ0
lpadlen.2 ⊢φ→W∈WordS
lpadlen.3 ⊢φ→C∈S
lpadright.1 ⊢φ→M=ifL≤W0L−W
lpadright.2 ⊢φ→N∈0..^W
Assertion lpadright ⊢φ→CleftpadW⁡L⁡N+M=W⁡N

Proof

Step Hyp Ref Expression
1 lpadlen.1 ⊢φ→L∈ℕ0
2 lpadlen.2 ⊢φ→W∈WordS
3 lpadlen.3 ⊢φ→C∈S
4 lpadright.1 ⊢φ→M=ifL≤W0L−W
5 lpadright.2 ⊢φ→N∈0..^W
6 1 2 3 lpadval ⊢φ→CleftpadW⁡L=0..^L−W×C++W
7 6 fveq1d ⊢φ→CleftpadW⁡L⁡N+M=0..^L−W×C++W⁡N+M
8 eqeq2 ⊢0=ifL≤W0L−W→0..^L−W×C=0↔0..^L−W×C=ifL≤W0L−W
9 eqeq2 ⊢L−W=ifL≤W0L−W→0..^L−W×C=L−W↔0..^L−W×C=ifL≤W0L−W
10 1 adantr ⊢φ∧L≤W→L∈ℕ0
11 2 adantr ⊢φ∧L≤W→W∈WordS
12 3 adantr ⊢φ∧L≤W→C∈S
13 simpr ⊢φ∧L≤W→L≤W
14 10 11 12 13 lpadlem3 ⊢φ∧L≤W→0..^L−W×C=∅
15 14 fveq2d ⊢φ∧L≤W→0..^L−W×C=∅
16 hash0 ⊢∅=0
17 15 16 eqtrdi ⊢φ∧L≤W→0..^L−W×C=0
18 1 adantr ⊢φ∧¬L≤W→L∈ℕ0
19 2 adantr ⊢φ∧¬L≤W→W∈WordS
20 3 adantr ⊢φ∧¬L≤W→C∈S
21 lencl ⊢W∈WordS→W∈ℕ0
22 2 21 syl ⊢φ→W∈ℕ0
23 22 nn0red ⊢φ→W∈ℝ
24 23 adantr ⊢φ∧¬L≤W→W∈ℝ
25 1 nn0red ⊢φ→L∈ℝ
26 25 adantr ⊢φ∧¬L≤W→L∈ℝ
27 23 25 ltnled ⊢φ→W<L↔¬L≤W
28 27 biimpar ⊢φ∧¬L≤W→W<L
29 24 26 28 ltled ⊢φ∧¬L≤W→W≤L
30 18 19 20 29 lpadlem2 ⊢φ∧¬L≤W→0..^L−W×C=L−W
31 8 9 17 30 ifbothda ⊢φ→0..^L−W×C=ifL≤W0L−W
32 31 4 eqtr4d ⊢φ→0..^L−W×C=M
33 32 oveq2d ⊢φ→N+0..^L−W×C=N+M
34 33 fveq2d ⊢φ→0..^L−W×C++W⁡N+0..^L−W×C=0..^L−W×C++W⁡N+M
35 3 lpadlem1 ⊢φ→0..^L−W×C∈WordS
36 ccatval3 ⊢0..^L−W×C∈WordS∧W∈WordS∧N∈0..^W→0..^L−W×C++W⁡N+0..^L−W×C=W⁡N
37 35 2 5 36 syl3anc ⊢φ→0..^L−W×C++W⁡N+0..^L−W×C=W⁡N
38 7 34 37 3eqtr2d ⊢φ→CleftpadW⁡L⁡N+M=W⁡N