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 ⊢ ( 𝜑 → 𝐿 ∈ ℕ0 )
lpadlen.2 ⊢ ( 𝜑 → 𝑊 ∈ Word 𝑆 )
lpadlen.3 ⊢ ( 𝜑 → 𝐶 ∈ 𝑆 )
lpadright.1 ⊢ ( 𝜑 → 𝑀 = if ( 𝐿 ≤ ( ♯ ‘ 𝑊 ) , 0 , ( 𝐿 − ( ♯ ‘ 𝑊 ) ) ) )
lpadright.2 ⊢ ( 𝜑 → 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
Assertion lpadright ( 𝜑 → ( ( ( 𝐶 leftpad 𝑊 ) ‘ 𝐿 ) ‘ ( 𝑁 + 𝑀 ) ) = ( 𝑊 ‘ 𝑁 ) )

Proof

Step Hyp Ref Expression
1 lpadlen.1 ⊢ ( 𝜑 → 𝐿 ∈ ℕ0 )
2 lpadlen.2 ⊢ ( 𝜑 → 𝑊 ∈ Word 𝑆 )
3 lpadlen.3 ⊢ ( 𝜑 → 𝐶 ∈ 𝑆 )
4 lpadright.1 ⊢ ( 𝜑 → 𝑀 = if ( 𝐿 ≤ ( ♯ ‘ 𝑊 ) , 0 , ( 𝐿 − ( ♯ ‘ 𝑊 ) ) ) )
5 lpadright.2 ⊢ ( 𝜑 → 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) )
6 1 2 3 lpadval ⊢ ( 𝜑 → ( ( 𝐶 leftpad 𝑊 ) ‘ 𝐿 ) = ( ( ( 0 ..^ ( 𝐿 − ( ♯ ‘ 𝑊 ) ) ) × { 𝐶 } ) ++ 𝑊 ) )
7 6 fveq1d ⊢ ( 𝜑 → ( ( ( 𝐶 leftpad 𝑊 ) ‘ 𝐿 ) ‘ ( 𝑁 + 𝑀 ) ) = ( ( ( ( 0 ..^ ( 𝐿 − ( ♯ ‘ 𝑊 ) ) ) × { 𝐶 } ) ++ 𝑊 ) ‘ ( 𝑁 + 𝑀 ) ) )
8 eqeq2 ⊢ ( 0 = if ( 𝐿 ≤ ( ♯ ‘ 𝑊 ) , 0 , ( 𝐿 − ( ♯ ‘ 𝑊 ) ) ) → ( ( ♯ ‘ ( ( 0 ..^ ( 𝐿 − ( ♯ ‘ 𝑊 ) ) ) × { 𝐶 } ) ) = 0 ↔ ( ♯ ‘ ( ( 0 ..^ ( 𝐿 − ( ♯ ‘ 𝑊 ) ) ) × { 𝐶 } ) ) = if ( 𝐿 ≤ ( ♯ ‘ 𝑊 ) , 0 , ( 𝐿 − ( ♯ ‘ 𝑊 ) ) ) ) )
9 eqeq2 ⊢ ( ( 𝐿 − ( ♯ ‘ 𝑊 ) ) = if ( 𝐿 ≤ ( ♯ ‘ 𝑊 ) , 0 , ( 𝐿 − ( ♯ ‘ 𝑊 ) ) ) → ( ( ♯ ‘ ( ( 0 ..^ ( 𝐿 − ( ♯ ‘ 𝑊 ) ) ) × { 𝐶 } ) ) = ( 𝐿 − ( ♯ ‘ 𝑊 ) ) ↔ ( ♯ ‘ ( ( 0 ..^ ( 𝐿 − ( ♯ ‘ 𝑊 ) ) ) × { 𝐶 } ) ) = if ( 𝐿 ≤ ( ♯ ‘ 𝑊 ) , 0 , ( 𝐿 − ( ♯ ‘ 𝑊 ) ) ) ) )
10 1 adantr ⊢ ( ( 𝜑 ∧ 𝐿 ≤ ( ♯ ‘ 𝑊 ) ) → 𝐿 ∈ ℕ0 )
11 2 adantr ⊢ ( ( 𝜑 ∧ 𝐿 ≤ ( ♯ ‘ 𝑊 ) ) → 𝑊 ∈ Word 𝑆 )
12 3 adantr ⊢ ( ( 𝜑 ∧ 𝐿 ≤ ( ♯ ‘ 𝑊 ) ) → 𝐶 ∈ 𝑆 )
13 simpr ⊢ ( ( 𝜑 ∧ 𝐿 ≤ ( ♯ ‘ 𝑊 ) ) → 𝐿 ≤ ( ♯ ‘ 𝑊 ) )
14 10 11 12 13 lpadlem3 ⊢ ( ( 𝜑 ∧ 𝐿 ≤ ( ♯ ‘ 𝑊 ) ) → ( ( 0 ..^ ( 𝐿 − ( ♯ ‘ 𝑊 ) ) ) × { 𝐶 } ) = ∅ )
15 14 fveq2d ⊢ ( ( 𝜑 ∧ 𝐿 ≤ ( ♯ ‘ 𝑊 ) ) → ( ♯ ‘ ( ( 0 ..^ ( 𝐿 − ( ♯ ‘ 𝑊 ) ) ) × { 𝐶 } ) ) = ( ♯ ‘ ∅ ) )
16 hash0 ⊢ ( ♯ ‘ ∅ ) = 0
17 15 16 eqtrdi ⊢ ( ( 𝜑 ∧ 𝐿 ≤ ( ♯ ‘ 𝑊 ) ) → ( ♯ ‘ ( ( 0 ..^ ( 𝐿 − ( ♯ ‘ 𝑊 ) ) ) × { 𝐶 } ) ) = 0 )
18 1 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐿 ≤ ( ♯ ‘ 𝑊 ) ) → 𝐿 ∈ ℕ0 )
19 2 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐿 ≤ ( ♯ ‘ 𝑊 ) ) → 𝑊 ∈ Word 𝑆 )
20 3 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐿 ≤ ( ♯ ‘ 𝑊 ) ) → 𝐶 ∈ 𝑆 )
21 lencl ⊢ ( 𝑊 ∈ Word 𝑆 → ( ♯ ‘ 𝑊 ) ∈ ℕ0 )
22 2 21 syl ⊢ ( 𝜑 → ( ♯ ‘ 𝑊 ) ∈ ℕ0 )
23 22 nn0red ⊢ ( 𝜑 → ( ♯ ‘ 𝑊 ) ∈ ℝ )
24 23 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐿 ≤ ( ♯ ‘ 𝑊 ) ) → ( ♯ ‘ 𝑊 ) ∈ ℝ )
25 1 nn0red ⊢ ( 𝜑 → 𝐿 ∈ ℝ )
26 25 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐿 ≤ ( ♯ ‘ 𝑊 ) ) → 𝐿 ∈ ℝ )
27 23 25 ltnled ⊢ ( 𝜑 → ( ( ♯ ‘ 𝑊 ) < 𝐿 ↔ ¬ 𝐿 ≤ ( ♯ ‘ 𝑊 ) ) )
28 27 biimpar ⊢ ( ( 𝜑 ∧ ¬ 𝐿 ≤ ( ♯ ‘ 𝑊 ) ) → ( ♯ ‘ 𝑊 ) < 𝐿 )
29 24 26 28 ltled ⊢ ( ( 𝜑 ∧ ¬ 𝐿 ≤ ( ♯ ‘ 𝑊 ) ) → ( ♯ ‘ 𝑊 ) ≤ 𝐿 )
30 18 19 20 29 lpadlem2 ⊢ ( ( 𝜑 ∧ ¬ 𝐿 ≤ ( ♯ ‘ 𝑊 ) ) → ( ♯ ‘ ( ( 0 ..^ ( 𝐿 − ( ♯ ‘ 𝑊 ) ) ) × { 𝐶 } ) ) = ( 𝐿 − ( ♯ ‘ 𝑊 ) ) )
31 8 9 17 30 ifbothda ⊢ ( 𝜑 → ( ♯ ‘ ( ( 0 ..^ ( 𝐿 − ( ♯ ‘ 𝑊 ) ) ) × { 𝐶 } ) ) = if ( 𝐿 ≤ ( ♯ ‘ 𝑊 ) , 0 , ( 𝐿 − ( ♯ ‘ 𝑊 ) ) ) )
32 31 4 eqtr4d ⊢ ( 𝜑 → ( ♯ ‘ ( ( 0 ..^ ( 𝐿 − ( ♯ ‘ 𝑊 ) ) ) × { 𝐶 } ) ) = 𝑀 )
33 32 oveq2d ⊢ ( 𝜑 → ( 𝑁 + ( ♯ ‘ ( ( 0 ..^ ( 𝐿 − ( ♯ ‘ 𝑊 ) ) ) × { 𝐶 } ) ) ) = ( 𝑁 + 𝑀 ) )
34 33 fveq2d ⊢ ( 𝜑 → ( ( ( ( 0 ..^ ( 𝐿 − ( ♯ ‘ 𝑊 ) ) ) × { 𝐶 } ) ++ 𝑊 ) ‘ ( 𝑁 + ( ♯ ‘ ( ( 0 ..^ ( 𝐿 − ( ♯ ‘ 𝑊 ) ) ) × { 𝐶 } ) ) ) ) = ( ( ( ( 0 ..^ ( 𝐿 − ( ♯ ‘ 𝑊 ) ) ) × { 𝐶 } ) ++ 𝑊 ) ‘ ( 𝑁 + 𝑀 ) ) )
35 3 lpadlem1 ⊢ ( 𝜑 → ( ( 0 ..^ ( 𝐿 − ( ♯ ‘ 𝑊 ) ) ) × { 𝐶 } ) ∈ Word 𝑆 )
36 ccatval3 ⊢ ( ( ( ( 0 ..^ ( 𝐿 − ( ♯ ‘ 𝑊 ) ) ) × { 𝐶 } ) ∈ Word 𝑆 ∧ 𝑊 ∈ Word 𝑆 ∧ 𝑁 ∈ ( 0 ..^ ( ♯ ‘ 𝑊 ) ) ) → ( ( ( ( 0 ..^ ( 𝐿 − ( ♯ ‘ 𝑊 ) ) ) × { 𝐶 } ) ++ 𝑊 ) ‘ ( 𝑁 + ( ♯ ‘ ( ( 0 ..^ ( 𝐿 − ( ♯ ‘ 𝑊 ) ) ) × { 𝐶 } ) ) ) ) = ( 𝑊 ‘ 𝑁 ) )
37 35 2 5 36 syl3anc ⊢ ( 𝜑 → ( ( ( ( 0 ..^ ( 𝐿 − ( ♯ ‘ 𝑊 ) ) ) × { 𝐶 } ) ++ 𝑊 ) ‘ ( 𝑁 + ( ♯ ‘ ( ( 0 ..^ ( 𝐿 − ( ♯ ‘ 𝑊 ) ) ) × { 𝐶 } ) ) ) ) = ( 𝑊 ‘ 𝑁 ) )
38 7 34 37 3eqtr2d ⊢ ( 𝜑 → ( ( ( 𝐶 leftpad 𝑊 ) ‘ 𝐿 ) ‘ ( 𝑁 + 𝑀 ) ) = ( 𝑊 ‘ 𝑁 ) )