Metamath Proof Explorer


Theorem ccat1st1st

Description: The first symbol of a word concatenated with its first symbol is the first symbol of the word. This theorem holds even if W is the empty word. (Contributed by AV, 26-Mar-2022)

Ref Expression
Assertion ccat1st1st
|- ( W e. Word V -> ( ( W ++ <" ( W ` 0 ) "> ) ` 0 ) = ( W ` 0 ) )

Proof

Step Hyp Ref Expression
1 hasheq0
 |-  ( W e. Word V -> ( ( # ` W ) = 0 <-> W = (/) ) )
2 1 biimpa
 |-  ( ( W e. Word V /\ ( # ` W ) = 0 ) -> W = (/) )
3 s1cli
 |-  <" (/) "> e. Word _V
4 ccatlid
 |-  ( <" (/) "> e. Word _V -> ( (/) ++ <" (/) "> ) = <" (/) "> )
5 3 4 ax-mp
 |-  ( (/) ++ <" (/) "> ) = <" (/) ">
6 5 fveq1i
 |-  ( ( (/) ++ <" (/) "> ) ` 0 ) = ( <" (/) "> ` 0 )
7 0ex
 |-  (/) e. _V
8 s1fv
 |-  ( (/) e. _V -> ( <" (/) "> ` 0 ) = (/) )
9 7 8 ax-mp
 |-  ( <" (/) "> ` 0 ) = (/)
10 6 9 eqtri
 |-  ( ( (/) ++ <" (/) "> ) ` 0 ) = (/)
11 id
 |-  ( W = (/) -> W = (/) )
12 fveq1
 |-  ( W = (/) -> ( W ` 0 ) = ( (/) ` 0 ) )
13 0fv
 |-  ( (/) ` 0 ) = (/)
14 12 13 eqtrdi
 |-  ( W = (/) -> ( W ` 0 ) = (/) )
15 14 s1eqd
 |-  ( W = (/) -> <" ( W ` 0 ) "> = <" (/) "> )
16 11 15 oveq12d
 |-  ( W = (/) -> ( W ++ <" ( W ` 0 ) "> ) = ( (/) ++ <" (/) "> ) )
17 16 fveq1d
 |-  ( W = (/) -> ( ( W ++ <" ( W ` 0 ) "> ) ` 0 ) = ( ( (/) ++ <" (/) "> ) ` 0 ) )
18 10 17 14 3eqtr4a
 |-  ( W = (/) -> ( ( W ++ <" ( W ` 0 ) "> ) ` 0 ) = ( W ` 0 ) )
19 2 18 syl
 |-  ( ( W e. Word V /\ ( # ` W ) = 0 ) -> ( ( W ++ <" ( W ` 0 ) "> ) ` 0 ) = ( W ` 0 ) )
20 1 necon3bid
 |-  ( W e. Word V -> ( ( # ` W ) =/= 0 <-> W =/= (/) ) )
21 20 biimpa
 |-  ( ( W e. Word V /\ ( # ` W ) =/= 0 ) -> W =/= (/) )
22 lennncl
 |-  ( ( W e. Word V /\ W =/= (/) ) -> ( # ` W ) e. NN )
23 21 22 syldan
 |-  ( ( W e. Word V /\ ( # ` W ) =/= 0 ) -> ( # ` W ) e. NN )
24 lbfzo0
 |-  ( 0 e. ( 0 ..^ ( # ` W ) ) <-> ( # ` W ) e. NN )
25 23 24 sylibr
 |-  ( ( W e. Word V /\ ( # ` W ) =/= 0 ) -> 0 e. ( 0 ..^ ( # ` W ) ) )
26 ccats1val1
 |-  ( ( W e. Word V /\ 0 e. ( 0 ..^ ( # ` W ) ) ) -> ( ( W ++ <" ( W ` 0 ) "> ) ` 0 ) = ( W ` 0 ) )
27 25 26 syldan
 |-  ( ( W e. Word V /\ ( # ` W ) =/= 0 ) -> ( ( W ++ <" ( W ` 0 ) "> ) ` 0 ) = ( W ` 0 ) )
28 19 27 pm2.61dane
 |-  ( W e. Word V -> ( ( W ++ <" ( W ` 0 ) "> ) ` 0 ) = ( W ` 0 ) )