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

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