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 eqtrdi φ 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