Theorem wrdlenccats1lenm1

Description: The length of a word is the length of the word concatenated with a singleton word minus 1. (Contributed by AV, 28-Jun-2018) (Revised by AV, 5-Mar-2022)

	Ref	Expression
Assertion	wrdlenccats1lenm1	|- ( W e. Word V -> ( ( # ` ( W ++ <" S "> ) ) - 1 ) = ( # ` W ) )

Proof

Step	Hyp	Ref	Expression
1		ccatws1len	|- ( W e. Word V -> ( # ` ( W ++ <" S "> ) ) = ( ( # ` W ) + 1 ) )
2	1	oveq1d	|- ( W e. Word V -> ( ( # ` ( W ++ <" S "> ) ) - 1 ) = ( ( ( # ` W ) + 1 ) - 1 ) )
3		lencl	|- ( W e. Word V -> ( # ` W ) e. NN0 )
4	3	nn0cnd	|- ( W e. Word V -> ( # ` W ) e. CC )
5		pncan1	|- ( ( # ` W ) e. CC -> ( ( ( # ` W ) + 1 ) - 1 ) = ( # ` W ) )
6	4 5	syl	|- ( W e. Word V -> ( ( ( # ` W ) + 1 ) - 1 ) = ( # ` W ) )
7	2 6	eqtrd	|- ( W e. Word V -> ( ( # ` ( W ++ <" S "> ) ) - 1 ) = ( # ` W ) )