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