This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem lenrevpfxcctswrd

Description: The length of the concatenation of the rest of a word and the prefix of the word is the length of the word. (Contributed by Alexander van der Vekens, 1-Apr-2018) (Revised by AV, 9-May-2020)

Ref Expression
Assertion lenrevpfxcctswrd ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( ♯ ‘ ( ( 𝑊 substr ⟨ 𝑀 , ( ♯ ‘ 𝑊 ) ⟩ ) ++ ( 𝑊 prefix 𝑀 ) ) ) = ( ♯ ‘ 𝑊 ) )

Proof

Step Hyp Ref Expression
1 swrdcl ⊢ ( 𝑊 ∈ Word 𝑉 → ( 𝑊 substr ⟨ 𝑀 , ( ♯ ‘ 𝑊 ) ⟩ ) ∈ Word 𝑉 )
2 pfxcl ⊢ ( 𝑊 ∈ Word 𝑉 → ( 𝑊 prefix 𝑀 ) ∈ Word 𝑉 )
3 ccatlen ⊢ ( ( ( 𝑊 substr ⟨ 𝑀 , ( ♯ ‘ 𝑊 ) ⟩ ) ∈ Word 𝑉 ∧ ( 𝑊 prefix 𝑀 ) ∈ Word 𝑉 ) → ( ♯ ‘ ( ( 𝑊 substr ⟨ 𝑀 , ( ♯ ‘ 𝑊 ) ⟩ ) ++ ( 𝑊 prefix 𝑀 ) ) ) = ( ( ♯ ‘ ( 𝑊 substr ⟨ 𝑀 , ( ♯ ‘ 𝑊 ) ⟩ ) ) + ( ♯ ‘ ( 𝑊 prefix 𝑀 ) ) ) )
4 1 2 3 syl2anc ⊢ ( 𝑊 ∈ Word 𝑉 → ( ♯ ‘ ( ( 𝑊 substr ⟨ 𝑀 , ( ♯ ‘ 𝑊 ) ⟩ ) ++ ( 𝑊 prefix 𝑀 ) ) ) = ( ( ♯ ‘ ( 𝑊 substr ⟨ 𝑀 , ( ♯ ‘ 𝑊 ) ⟩ ) ) + ( ♯ ‘ ( 𝑊 prefix 𝑀 ) ) ) )
5 4 adantr ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( ♯ ‘ ( ( 𝑊 substr ⟨ 𝑀 , ( ♯ ‘ 𝑊 ) ⟩ ) ++ ( 𝑊 prefix 𝑀 ) ) ) = ( ( ♯ ‘ ( 𝑊 substr ⟨ 𝑀 , ( ♯ ‘ 𝑊 ) ⟩ ) ) + ( ♯ ‘ ( 𝑊 prefix 𝑀 ) ) ) )
6 swrdrlen ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( ♯ ‘ ( 𝑊 substr ⟨ 𝑀 , ( ♯ ‘ 𝑊 ) ⟩ ) ) = ( ( ♯ ‘ 𝑊 ) − 𝑀 ) )
7 fznn0sub ⊢ ( 𝑀 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) → ( ( ♯ ‘ 𝑊 ) − 𝑀 ) ∈ ℕ0 )
8 7 adantl ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( ( ♯ ‘ 𝑊 ) − 𝑀 ) ∈ ℕ0 )
9 6 8 eqeltrd ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( ♯ ‘ ( 𝑊 substr ⟨ 𝑀 , ( ♯ ‘ 𝑊 ) ⟩ ) ) ∈ ℕ0 )
10 9 nn0cnd ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( ♯ ‘ ( 𝑊 substr ⟨ 𝑀 , ( ♯ ‘ 𝑊 ) ⟩ ) ) ∈ ℂ )
11 pfxlen ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( ♯ ‘ ( 𝑊 prefix 𝑀 ) ) = 𝑀 )
12 elfznn0 ⊢ ( 𝑀 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) → 𝑀 ∈ ℕ0 )
13 12 adantl ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → 𝑀 ∈ ℕ0 )
14 11 13 eqeltrd ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( ♯ ‘ ( 𝑊 prefix 𝑀 ) ) ∈ ℕ0 )
15 14 nn0cnd ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( ♯ ‘ ( 𝑊 prefix 𝑀 ) ) ∈ ℂ )
16 10 15 addcomd ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( ( ♯ ‘ ( 𝑊 substr ⟨ 𝑀 , ( ♯ ‘ 𝑊 ) ⟩ ) ) + ( ♯ ‘ ( 𝑊 prefix 𝑀 ) ) ) = ( ( ♯ ‘ ( 𝑊 prefix 𝑀 ) ) + ( ♯ ‘ ( 𝑊 substr ⟨ 𝑀 , ( ♯ ‘ 𝑊 ) ⟩ ) ) ) )
17 addlenpfx ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( ( ♯ ‘ ( 𝑊 prefix 𝑀 ) ) + ( ♯ ‘ ( 𝑊 substr ⟨ 𝑀 , ( ♯ ‘ 𝑊 ) ⟩ ) ) ) = ( ♯ ‘ 𝑊 ) )
18 5 16 17 3eqtrd ⊢ ( ( 𝑊 ∈ Word 𝑉 ∧ 𝑀 ∈ ( 0 ... ( ♯ ‘ 𝑊 ) ) ) → ( ♯ ‘ ( ( 𝑊 substr ⟨ 𝑀 , ( ♯ ‘ 𝑊 ) ⟩ ) ++ ( 𝑊 prefix 𝑀 ) ) ) = ( ♯ ‘ 𝑊 ) )