Metamath Proof Explorer

Theorem ccatws1lenp1b

Description: The length of a word is N iff the length of the concatenation of the word with a singleton word is N + 1 . (Contributed by AV, 4-Mar-2022)

Ref Expression
Assertion ccatws1lenp1b 
|- ( ( W e. Word V /\ N e. NN0 ) -> ( ( # ` ( W ++ <" X "> ) ) = ( N + 1 ) <-> ( # ` W ) = N ) )

Proof

Step Hyp Ref Expression
1 ccatws1len 
 |-  ( W e. Word V -> ( # ` ( W ++ <" X "> ) ) = ( ( # ` W ) + 1 ) )
2 1 adantr 
 |-  ( ( W e. Word V /\ N e. NN0 ) -> ( # ` ( W ++ <" X "> ) ) = ( ( # ` W ) + 1 ) )
3 2 eqeq1d 
 |-  ( ( W e. Word V /\ N e. NN0 ) -> ( ( # ` ( W ++ <" X "> ) ) = ( N + 1 ) <-> ( ( # ` W ) + 1 ) = ( N + 1 ) ) )
4 lencl 
 |-  ( W e. Word V -> ( # ` W ) e. NN0 )
5 4 nn0cnd 
 |-  ( W e. Word V -> ( # ` W ) e. CC )
6 5 adantr 
 |-  ( ( W e. Word V /\ N e. NN0 ) -> ( # ` W ) e. CC )
7 nn0cn 
 |-  ( N e. NN0 -> N e. CC )
8 7 adantl 
 |-  ( ( W e. Word V /\ N e. NN0 ) -> N e. CC )
9 1cnd 
 |-  ( ( W e. Word V /\ N e. NN0 ) -> 1 e. CC )
10 6 8 9 addcan2d 
 |-  ( ( W e. Word V /\ N e. NN0 ) -> ( ( ( # ` W ) + 1 ) = ( N + 1 ) <-> ( # ` W ) = N ) )
11 3 10 bitrd 
 |-  ( ( W e. Word V /\ N e. NN0 ) -> ( ( # ` ( W ++ <" X "> ) ) = ( N + 1 ) <-> ( # ` W ) = N ) )