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

Proof

Step Hyp Ref Expression
1 swrdcl ⊢ W ∈ Word V → W substr M W ∈ Word V
2 pfxcl ⊢ W ∈ Word V → W prefix M ∈ Word V
3 ccatlen ⊢ W substr M W ∈ Word V ∧ W prefix M ∈ Word V → W substr M W ++ W prefix M = W substr M W + W prefix M
4 1 2 3 syl2anc ⊢ W ∈ Word V → W substr M W ++ W prefix M = W substr M W + W prefix M
5 4 adantr ⊢ W ∈ Word V ∧ M ∈ 0 … W → W substr M W ++ W prefix M = W substr M W + W prefix M
6 swrdrlen ⊢ W ∈ Word V ∧ M ∈ 0 … W → W substr M W = W − M
7 fznn0sub ⊢ M ∈ 0 … W → W − M ∈ ℕ 0
8 7 adantl ⊢ W ∈ Word V ∧ M ∈ 0 … W → W − M ∈ ℕ 0
9 6 8 eqeltrd ⊢ W ∈ Word V ∧ M ∈ 0 … W → W substr M W ∈ ℕ 0
10 9 nn0cnd ⊢ W ∈ Word V ∧ M ∈ 0 … W → W substr M W ∈ ℂ
11 pfxlen ⊢ W ∈ Word V ∧ M ∈ 0 … W → W prefix M = M
12 elfznn0 ⊢ M ∈ 0 … W → M ∈ ℕ 0
13 12 adantl ⊢ W ∈ Word V ∧ M ∈ 0 … W → M ∈ ℕ 0
14 11 13 eqeltrd ⊢ W ∈ Word V ∧ M ∈ 0 … W → W prefix M ∈ ℕ 0
15 14 nn0cnd ⊢ W ∈ Word V ∧ M ∈ 0 … W → W prefix M ∈ ℂ
16 10 15 addcomd ⊢ W ∈ Word V ∧ M ∈ 0 … W → W substr M W + W prefix M = W prefix M + W substr M W
17 addlenpfx ⊢ W ∈ Word V ∧ M ∈ 0 … W → W prefix M + W substr M W = W
18 5 16 17 3eqtrd ⊢ W ∈ Word V ∧ M ∈ 0 … W → W substr M W ++ W prefix M = W