This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )