Metamath Proof Explorer


Theorem lpadlen2

Description: Length of a left-padded word, in the case the given word W is shorter than the desired length. (Contributed by Thierry Arnoux, 7-Aug-2023)

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

Proof

Step Hyp Ref Expression
1 lpadlen.1 ( 𝜑𝐿 ∈ ℕ0 )
2 lpadlen.2 ( 𝜑𝑊 ∈ Word 𝑆 )
3 lpadlen.3 ( 𝜑𝐶𝑆 )
4 lpadlen2.1 ( 𝜑 → ( ♯ ‘ 𝑊 ) ≤ 𝐿 )
5 1 2 3 lpadval ( 𝜑 → ( ( 𝐶 leftpad 𝑊 ) ‘ 𝐿 ) = ( ( ( 0 ..^ ( 𝐿 − ( ♯ ‘ 𝑊 ) ) ) × { 𝐶 } ) ++ 𝑊 ) )
6 5 fveq2d ( 𝜑 → ( ♯ ‘ ( ( 𝐶 leftpad 𝑊 ) ‘ 𝐿 ) ) = ( ♯ ‘ ( ( ( 0 ..^ ( 𝐿 − ( ♯ ‘ 𝑊 ) ) ) × { 𝐶 } ) ++ 𝑊 ) ) )
7 3 lpadlem1 ( 𝜑 → ( ( 0 ..^ ( 𝐿 − ( ♯ ‘ 𝑊 ) ) ) × { 𝐶 } ) ∈ Word 𝑆 )
8 ccatlen ( ( ( ( 0 ..^ ( 𝐿 − ( ♯ ‘ 𝑊 ) ) ) × { 𝐶 } ) ∈ Word 𝑆𝑊 ∈ Word 𝑆 ) → ( ♯ ‘ ( ( ( 0 ..^ ( 𝐿 − ( ♯ ‘ 𝑊 ) ) ) × { 𝐶 } ) ++ 𝑊 ) ) = ( ( ♯ ‘ ( ( 0 ..^ ( 𝐿 − ( ♯ ‘ 𝑊 ) ) ) × { 𝐶 } ) ) + ( ♯ ‘ 𝑊 ) ) )
9 7 2 8 syl2anc ( 𝜑 → ( ♯ ‘ ( ( ( 0 ..^ ( 𝐿 − ( ♯ ‘ 𝑊 ) ) ) × { 𝐶 } ) ++ 𝑊 ) ) = ( ( ♯ ‘ ( ( 0 ..^ ( 𝐿 − ( ♯ ‘ 𝑊 ) ) ) × { 𝐶 } ) ) + ( ♯ ‘ 𝑊 ) ) )
10 1 2 3 4 lpadlem2 ( 𝜑 → ( ♯ ‘ ( ( 0 ..^ ( 𝐿 − ( ♯ ‘ 𝑊 ) ) ) × { 𝐶 } ) ) = ( 𝐿 − ( ♯ ‘ 𝑊 ) ) )
11 10 oveq1d ( 𝜑 → ( ( ♯ ‘ ( ( 0 ..^ ( 𝐿 − ( ♯ ‘ 𝑊 ) ) ) × { 𝐶 } ) ) + ( ♯ ‘ 𝑊 ) ) = ( ( 𝐿 − ( ♯ ‘ 𝑊 ) ) + ( ♯ ‘ 𝑊 ) ) )
12 1 nn0cnd ( 𝜑𝐿 ∈ ℂ )
13 lencl ( 𝑊 ∈ Word 𝑆 → ( ♯ ‘ 𝑊 ) ∈ ℕ0 )
14 2 13 syl ( 𝜑 → ( ♯ ‘ 𝑊 ) ∈ ℕ0 )
15 14 nn0cnd ( 𝜑 → ( ♯ ‘ 𝑊 ) ∈ ℂ )
16 12 15 npcand ( 𝜑 → ( ( 𝐿 − ( ♯ ‘ 𝑊 ) ) + ( ♯ ‘ 𝑊 ) ) = 𝐿 )
17 9 11 16 3eqtrd ( 𝜑 → ( ♯ ‘ ( ( ( 0 ..^ ( 𝐿 − ( ♯ ‘ 𝑊 ) ) ) × { 𝐶 } ) ++ 𝑊 ) ) = 𝐿 )
18 6 17 eqtrd ( 𝜑 → ( ♯ ‘ ( ( 𝐶 leftpad 𝑊 ) ‘ 𝐿 ) ) = 𝐿 )