Step |
Hyp |
Ref |
Expression |
1 |
|
pfxlen |
⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( ♯ ‘ ( 𝑊 prefix 𝑀 ) ) = 𝑀 ) |
2 |
|
swrdrlen |
⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( ♯ ‘ ( 𝑊 substr 〈 𝑀 , ( ♯ ‘ 𝑊 ) 〉 ) ) = ( ( ♯ ‘ 𝑊 ) − 𝑀 ) ) |
3 |
1 2
|
oveq12d |
⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( ( ♯ ‘ ( 𝑊 prefix 𝑀 ) ) + ( ♯ ‘ ( 𝑊 substr 〈 𝑀 , ( ♯ ‘ 𝑊 ) 〉 ) ) ) = ( 𝑀 + ( ( ♯ ‘ 𝑊 ) − 𝑀 ) ) ) |
4 |
|
elfznn0 |
⊢ ( 𝑀 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) → 𝑀 ∈ ℕ0 ) |
5 |
4
|
nn0cnd |
⊢ ( 𝑀 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) → 𝑀 ∈ ℂ ) |
6 |
|
lencl |
⊢ ( 𝑊 ∈ Word 𝑉 → ( ♯ ‘ 𝑊 ) ∈ ℕ0 ) |
7 |
6
|
nn0cnd |
⊢ ( 𝑊 ∈ Word 𝑉 → ( ♯ ‘ 𝑊 ) ∈ ℂ ) |
8 |
|
pncan3 |
⊢ ( ( 𝑀 ∈ ℂ ∧ ( ♯ ‘ 𝑊 ) ∈ ℂ ) → ( 𝑀 + ( ( ♯ ‘ 𝑊 ) − 𝑀 ) ) = ( ♯ ‘ 𝑊 ) ) |
9 |
5 7 8
|
syl2anr |
⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( 𝑀 + ( ( ♯ ‘ 𝑊 ) − 𝑀 ) ) = ( ♯ ‘ 𝑊 ) ) |
10 |
3 9
|
eqtrd |
⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( ( ♯ ‘ ( 𝑊 prefix 𝑀 ) ) + ( ♯ ‘ ( 𝑊 substr 〈 𝑀 , ( ♯ ‘ 𝑊 ) 〉 ) ) ) = ( ♯ ‘ 𝑊 ) ) |