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