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

Metamath Proof Explorer

Theorem addlenpfx

Description: The sum of the lengths of two parts of a word is the length of the word. (Contributed by AV, 21-Oct-2018) (Revised by AV, 3-May-2020)

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

Proof

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 ⟨ 𝑀 , ( ♯ ‘ 𝑊 ) ⟩ ) ) ) = ( ♯ ‘ 𝑊 ) )