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 ∈ Word S
lpadlen.3 ⊢ φ → C ∈ S
lpadright.1 ⊢ φ → M = if L ≤ W 0 L − W
lpadright.2 ⊢ φ → N ∈ 0 ..^ W
Assertion lpadright ⊢ φ → C leftpad W ⁡ L ⁡ N + M = W ⁡ N

Proof

Step Hyp Ref Expression
1 lpadlen.1 ⊢ φ → L ∈ ℕ 0
2 lpadlen.2 ⊢ φ → W ∈ Word S
3 lpadlen.3 ⊢ φ → C ∈ S
4 lpadright.1 ⊢ φ → M = if L ≤ W 0 L − W
5 lpadright.2 ⊢ φ → N ∈ 0 ..^ W
6 1 2 3 lpadval ⊢ φ → C leftpad W ⁡ L = 0 ..^ L − W × C ++ W
7 6 fveq1d ⊢ φ → C leftpad W ⁡ L ⁡ N + M = 0 ..^ L − W × C ++ W ⁡ N + M
8 eqeq2 ⊢ 0 = if L ≤ W 0 L − W → 0 ..^ L − W × C = 0 ↔ 0 ..^ L − W × C = if L ≤ W 0 L − W
9 eqeq2 ⊢ L − W = if L ≤ W 0 L − W → 0 ..^ L − W × C = L − W ↔ 0 ..^ L − W × C = if L ≤ W 0 L − W
10 1 adantr ⊢ φ ∧ L ≤ W → L ∈ ℕ 0
11 2 adantr ⊢ φ ∧ L ≤ W → W ∈ Word S
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 syl6eq ⊢ φ ∧ L ≤ W → 0 ..^ L − W × C = 0
18 1 adantr ⊢ φ ∧ ¬ L ≤ W → L ∈ ℕ 0
19 2 adantr ⊢ φ ∧ ¬ L ≤ W → W ∈ Word S
20 3 adantr ⊢ φ ∧ ¬ L ≤ W → C ∈ S
21 lencl ⊢ W ∈ Word S → 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 = if L ≤ W 0 L − 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 ∈ Word S
36 ccatval3 ⊢ 0 ..^ L − W × C ∈ Word S ∧ W ∈ Word S ∧ 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 ⊢ φ → C leftpad W ⁡ L ⁡ N + M = W ⁡ N