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 ⊢ W ∈ Word V ∧ M ∈ 0 … W → W prefix M + W substr M W = W

Proof

Step Hyp Ref Expression
1 pfxlen ⊢ W ∈ Word V ∧ M ∈ 0 … W → W prefix M = M
2 swrdrlen ⊢ W ∈ Word V ∧ M ∈ 0 … W → W substr M W = W − M
3 1 2 oveq12d ⊢ W ∈ Word V ∧ M ∈ 0 … W → W prefix M + W substr M W = M + W - M
4 elfznn0 ⊢ M ∈ 0 … W → M ∈ ℕ 0
5 4 nn0cnd ⊢ M ∈ 0 … W → M ∈ ℂ
6 lencl ⊢ W ∈ Word V → W ∈ ℕ 0
7 6 nn0cnd ⊢ W ∈ Word V → W ∈ ℂ
8 pncan3 ⊢ M ∈ ℂ ∧ W ∈ ℂ → M + W - M = W
9 5 7 8 syl2anr ⊢ W ∈ Word V ∧ M ∈ 0 … W → M + W - M = W
10 3 9 eqtrd ⊢ W ∈ Word V ∧ M ∈ 0 … W → W prefix M + W substr M W = W