Metamath Proof Explorer

Theorem lswccats1fst

Description: The last symbol of a nonempty word concatenated with its first symbol is the first symbol. (Contributed by AV, 28-Jun-2018) (Proof shortened by AV, 1-May-2020)

Ref Expression
Assertion lswccats1fst 
|- ( ( P e. Word V /\ 1 <_ ( # ` P ) ) -> ( lastS ` ( P ++ <" ( P ` 0 ) "> ) ) = ( ( P ++ <" ( P ` 0 ) "> ) ` 0 ) )

Proof

Step Hyp Ref Expression
1 wrdsymb1 
 |-  ( ( P e. Word V /\ 1 <_ ( # ` P ) ) -> ( P ` 0 ) e. V )
2 lswccats1 
 |-  ( ( P e. Word V /\ ( P ` 0 ) e. V ) -> ( lastS ` ( P ++ <" ( P ` 0 ) "> ) ) = ( P ` 0 ) )
3 1 2 syldan 
 |-  ( ( P e. Word V /\ 1 <_ ( # ` P ) ) -> ( lastS ` ( P ++ <" ( P ` 0 ) "> ) ) = ( P ` 0 ) )
4 simpl 
 |-  ( ( P e. Word V /\ 1 <_ ( # ` P ) ) -> P e. Word V )
5 1 s1cld 
 |-  ( ( P e. Word V /\ 1 <_ ( # ` P ) ) -> <" ( P ` 0 ) "> e. Word V )
6 lencl 
 |-  ( P e. Word V -> ( # ` P ) e. NN0 )
7 elnnnn0c 
 |-  ( ( # ` P ) e. NN <-> ( ( # ` P ) e. NN0 /\ 1 <_ ( # ` P ) ) )
8 7 biimpri 
 |-  ( ( ( # ` P ) e. NN0 /\ 1 <_ ( # ` P ) ) -> ( # ` P ) e. NN )
9 6 8 sylan 
 |-  ( ( P e. Word V /\ 1 <_ ( # ` P ) ) -> ( # ` P ) e. NN )
10 lbfzo0 
 |-  ( 0 e. ( 0 ..^ ( # ` P ) ) <-> ( # ` P ) e. NN )
11 9 10 sylibr 
 |-  ( ( P e. Word V /\ 1 <_ ( # ` P ) ) -> 0 e. ( 0 ..^ ( # ` P ) ) )
12 ccatval1 
 |-  ( ( P e. Word V /\ <" ( P ` 0 ) "> e. Word V /\ 0 e. ( 0 ..^ ( # ` P ) ) ) -> ( ( P ++ <" ( P ` 0 ) "> ) ` 0 ) = ( P ` 0 ) )
13 4 5 11 12 syl3anc 
 |-  ( ( P e. Word V /\ 1 <_ ( # ` P ) ) -> ( ( P ++ <" ( P ` 0 ) "> ) ` 0 ) = ( P ` 0 ) )
14 3 13 eqtr4d 
 |-  ( ( P e. Word V /\ 1 <_ ( # ` P ) ) -> ( lastS ` ( P ++ <" ( P ` 0 ) "> ) ) = ( ( P ++ <" ( P ` 0 ) "> ) ` 0 ) )