Metamath Proof Explorer

Theorem pfxcctswrd

Description: The concatenation of the prefix of a word and the rest of the word yields the word itself. (Contributed by AV, 21-Oct-2018) (Revised by AV, 9-May-2020)

Ref Expression
Assertion pfxcctswrd ⊢ W ∈ Word V ∧ M ∈ 0 … W → W prefix M ++ W substr M W = W

Proof

Step Hyp Ref Expression
1 lencl ⊢ W ∈ Word V → W ∈ ℕ 0
2 nn0fz0 ⊢ W ∈ ℕ 0 ↔ W ∈ 0 … W
3 1 2 sylib ⊢ W ∈ Word V → W ∈ 0 … W
4 3 adantr ⊢ W ∈ Word V ∧ M ∈ 0 … W → W ∈ 0 … W
5 ccatpfx ⊢ W ∈ Word V ∧ M ∈ 0 … W ∧ W ∈ 0 … W → W prefix M ++ W substr M W = W prefix W
6 4 5 mpd3an3 ⊢ W ∈ Word V ∧ M ∈ 0 … W → W prefix M ++ W substr M W = W prefix W
7 pfxid ⊢ W ∈ Word V → W prefix W = W
8 7 adantr ⊢ W ∈ Word V ∧ M ∈ 0 … W → W prefix W = W
9 6 8 eqtrd ⊢ W ∈ Word V ∧ M ∈ 0 … W → W prefix M ++ W substr M W = W