Metamath Proof Explorer

Theorem ccatw2s1len

Description: The length of the concatenation of a word with two singleton words. (Contributed by Alexander van der Vekens, 22-Sep-2018) (Revised by AV, 5-Mar-2022)

Ref Expression
Assertion ccatw2s1len 
|- ( W e. Word V -> ( # ` ( ( W ++ <" X "> ) ++ <" Y "> ) ) = ( ( # ` W ) + 2 ) )

Proof

Step Hyp Ref Expression
1 ccatws1clv 
 |-  ( W e. Word V -> ( W ++ <" X "> ) e. Word _V )
2 ccatws1len 
 |-  ( ( W ++ <" X "> ) e. Word _V -> ( # ` ( ( W ++ <" X "> ) ++ <" Y "> ) ) = ( ( # ` ( W ++ <" X "> ) ) + 1 ) )
3 1 2 syl 
 |-  ( W e. Word V -> ( # ` ( ( W ++ <" X "> ) ++ <" Y "> ) ) = ( ( # ` ( W ++ <" X "> ) ) + 1 ) )
4 ccatws1len 
 |-  ( W e. Word V -> ( # ` ( W ++ <" X "> ) ) = ( ( # ` W ) + 1 ) )
5 4 oveq1d 
 |-  ( W e. Word V -> ( ( # ` ( W ++ <" X "> ) ) + 1 ) = ( ( ( # ` W ) + 1 ) + 1 ) )
6 lencl 
 |-  ( W e. Word V -> ( # ` W ) e. NN0 )
7 nn0cn 
 |-  ( ( # ` W ) e. NN0 -> ( # ` W ) e. CC )
8 add1p1 
 |-  ( ( # ` W ) e. CC -> ( ( ( # ` W ) + 1 ) + 1 ) = ( ( # ` W ) + 2 ) )
9 6 7 8 3syl 
 |-  ( W e. Word V -> ( ( ( # ` W ) + 1 ) + 1 ) = ( ( # ` W ) + 2 ) )
10 3 5 9 3eqtrd 
 |-  ( W e. Word V -> ( # ` ( ( W ++ <" X "> ) ++ <" Y "> ) ) = ( ( # ` W ) + 2 ) )