Metamath Proof Explorer


Theorem lpadleft

Description: The contents of prefix of a left-padded word is always the letter C . (Contributed by Thierry Arnoux, 7-Aug-2023)

Ref Expression
Hypotheses lpadlen.1 ( 𝜑𝐿 ∈ ℕ0 )
lpadlen.2 ( 𝜑𝑊 ∈ Word 𝑆 )
lpadlen.3 ( 𝜑𝐶𝑆 )
lpadleft.1 ( 𝜑𝑁 ∈ ( 0 ..^ ( 𝐿 − ( ♯ ‘ 𝑊 ) ) ) )
Assertion lpadleft ( 𝜑 → ( ( ( 𝐶 leftpad 𝑊 ) ‘ 𝐿 ) ‘ 𝑁 ) = 𝐶 )

Proof

Step Hyp Ref Expression
1 lpadlen.1 ( 𝜑𝐿 ∈ ℕ0 )
2 lpadlen.2 ( 𝜑𝑊 ∈ Word 𝑆 )
3 lpadlen.3 ( 𝜑𝐶𝑆 )
4 lpadleft.1 ( 𝜑𝑁 ∈ ( 0 ..^ ( 𝐿 − ( ♯ ‘ 𝑊 ) ) ) )
5 1 2 3 lpadval ( 𝜑 → ( ( 𝐶 leftpad 𝑊 ) ‘ 𝐿 ) = ( ( ( 0 ..^ ( 𝐿 − ( ♯ ‘ 𝑊 ) ) ) × { 𝐶 } ) ++ 𝑊 ) )
6 5 fveq1d ( 𝜑 → ( ( ( 𝐶 leftpad 𝑊 ) ‘ 𝐿 ) ‘ 𝑁 ) = ( ( ( ( 0 ..^ ( 𝐿 − ( ♯ ‘ 𝑊 ) ) ) × { 𝐶 } ) ++ 𝑊 ) ‘ 𝑁 ) )
7 3 lpadlem1 ( 𝜑 → ( ( 0 ..^ ( 𝐿 − ( ♯ ‘ 𝑊 ) ) ) × { 𝐶 } ) ∈ Word 𝑆 )
8 lencl ( 𝑊 ∈ Word 𝑆 → ( ♯ ‘ 𝑊 ) ∈ ℕ0 )
9 2 8 syl ( 𝜑 → ( ♯ ‘ 𝑊 ) ∈ ℕ0 )
10 elfzo0 ( 𝑁 ∈ ( 0 ..^ ( 𝐿 − ( ♯ ‘ 𝑊 ) ) ) ↔ ( 𝑁 ∈ ℕ0 ∧ ( 𝐿 − ( ♯ ‘ 𝑊 ) ) ∈ ℕ ∧ 𝑁 < ( 𝐿 − ( ♯ ‘ 𝑊 ) ) ) )
11 4 10 sylib ( 𝜑 → ( 𝑁 ∈ ℕ0 ∧ ( 𝐿 − ( ♯ ‘ 𝑊 ) ) ∈ ℕ ∧ 𝑁 < ( 𝐿 − ( ♯ ‘ 𝑊 ) ) ) )
12 11 simp2d ( 𝜑 → ( 𝐿 − ( ♯ ‘ 𝑊 ) ) ∈ ℕ )
13 12 nnnn0d ( 𝜑 → ( 𝐿 − ( ♯ ‘ 𝑊 ) ) ∈ ℕ0 )
14 nn0sub ( ( ( ♯ ‘ 𝑊 ) ∈ ℕ0𝐿 ∈ ℕ0 ) → ( ( ♯ ‘ 𝑊 ) ≤ 𝐿 ↔ ( 𝐿 − ( ♯ ‘ 𝑊 ) ) ∈ ℕ0 ) )
15 14 biimpar ( ( ( ( ♯ ‘ 𝑊 ) ∈ ℕ0𝐿 ∈ ℕ0 ) ∧ ( 𝐿 − ( ♯ ‘ 𝑊 ) ) ∈ ℕ0 ) → ( ♯ ‘ 𝑊 ) ≤ 𝐿 )
16 9 1 13 15 syl21anc ( 𝜑 → ( ♯ ‘ 𝑊 ) ≤ 𝐿 )
17 1 2 3 16 lpadlem2 ( 𝜑 → ( ♯ ‘ ( ( 0 ..^ ( 𝐿 − ( ♯ ‘ 𝑊 ) ) ) × { 𝐶 } ) ) = ( 𝐿 − ( ♯ ‘ 𝑊 ) ) )
18 17 oveq2d ( 𝜑 → ( 0 ..^ ( ♯ ‘ ( ( 0 ..^ ( 𝐿 − ( ♯ ‘ 𝑊 ) ) ) × { 𝐶 } ) ) ) = ( 0 ..^ ( 𝐿 − ( ♯ ‘ 𝑊 ) ) ) )
19 4 18 eleqtrrd ( 𝜑𝑁 ∈ ( 0 ..^ ( ♯ ‘ ( ( 0 ..^ ( 𝐿 − ( ♯ ‘ 𝑊 ) ) ) × { 𝐶 } ) ) ) )
20 ccatval1 ( ( ( ( 0 ..^ ( 𝐿 − ( ♯ ‘ 𝑊 ) ) ) × { 𝐶 } ) ∈ Word 𝑆𝑊 ∈ Word 𝑆𝑁 ∈ ( 0 ..^ ( ♯ ‘ ( ( 0 ..^ ( 𝐿 − ( ♯ ‘ 𝑊 ) ) ) × { 𝐶 } ) ) ) ) → ( ( ( ( 0 ..^ ( 𝐿 − ( ♯ ‘ 𝑊 ) ) ) × { 𝐶 } ) ++ 𝑊 ) ‘ 𝑁 ) = ( ( ( 0 ..^ ( 𝐿 − ( ♯ ‘ 𝑊 ) ) ) × { 𝐶 } ) ‘ 𝑁 ) )
21 7 2 19 20 syl3anc ( 𝜑 → ( ( ( ( 0 ..^ ( 𝐿 − ( ♯ ‘ 𝑊 ) ) ) × { 𝐶 } ) ++ 𝑊 ) ‘ 𝑁 ) = ( ( ( 0 ..^ ( 𝐿 − ( ♯ ‘ 𝑊 ) ) ) × { 𝐶 } ) ‘ 𝑁 ) )
22 fvconst2g ( ( 𝐶𝑆𝑁 ∈ ( 0 ..^ ( 𝐿 − ( ♯ ‘ 𝑊 ) ) ) ) → ( ( ( 0 ..^ ( 𝐿 − ( ♯ ‘ 𝑊 ) ) ) × { 𝐶 } ) ‘ 𝑁 ) = 𝐶 )
23 3 4 22 syl2anc ( 𝜑 → ( ( ( 0 ..^ ( 𝐿 − ( ♯ ‘ 𝑊 ) ) ) × { 𝐶 } ) ‘ 𝑁 ) = 𝐶 )
24 6 21 23 3eqtrd ( 𝜑 → ( ( ( 𝐶 leftpad 𝑊 ) ‘ 𝐿 ) ‘ 𝑁 ) = 𝐶 )