Metamath Proof Explorer

Theorem wrdeqs1cat

Description: Decompose a nonempty word by separating off the first symbol. (Contributed by Stefan O'Rear, 25-Aug-2015) (Revised by Mario Carneiro, 1-Oct-2015) (Proof shortened by AV, 12-Oct-2022)

Ref Expression
Assertion wrdeqs1cat 
|- ( ( W e. Word A /\ W =/= (/) ) -> W = ( <" ( W ` 0 ) "> ++ ( W substr <. 1 , ( # ` W ) >. ) ) )

Proof

Step Hyp Ref Expression
1 simpl 
 |-  ( ( W e. Word A /\ W =/= (/) ) -> W e. Word A )
2 wrdfin 
 |-  ( W e. Word A -> W e. Fin )
3 1elfz0hash 
 |-  ( ( W e. Fin /\ W =/= (/) ) -> 1 e. ( 0 ... ( # ` W ) ) )
4 2 3 sylan 
 |-  ( ( W e. Word A /\ W =/= (/) ) -> 1 e. ( 0 ... ( # ` W ) ) )
5 lennncl 
 |-  ( ( W e. Word A /\ W =/= (/) ) -> ( # ` W ) e. NN )
6 5 nnnn0d 
 |-  ( ( W e. Word A /\ W =/= (/) ) -> ( # ` W ) e. NN0 )
7 eluzfz2 
 |-  ( ( # ` W ) e. ( ZZ>= ` 0 ) -> ( # ` W ) e. ( 0 ... ( # ` W ) ) )
8 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
9 7 8 eleq2s 
 |-  ( ( # ` W ) e. NN0 -> ( # ` W ) e. ( 0 ... ( # ` W ) ) )
10 6 9 syl 
 |-  ( ( W e. Word A /\ W =/= (/) ) -> ( # ` W ) e. ( 0 ... ( # ` W ) ) )
11 ccatpfx 
 |-  ( ( W e. Word A /\ 1 e. ( 0 ... ( # ` W ) ) /\ ( # ` W ) e. ( 0 ... ( # ` W ) ) ) -> ( ( W prefix 1 ) ++ ( W substr <. 1 , ( # ` W ) >. ) ) = ( W prefix ( # ` W ) ) )
12 1 4 10 11 syl3anc 
 |-  ( ( W e. Word A /\ W =/= (/) ) -> ( ( W prefix 1 ) ++ ( W substr <. 1 , ( # ` W ) >. ) ) = ( W prefix ( # ` W ) ) )
13 pfx1 
 |-  ( ( W e. Word A /\ W =/= (/) ) -> ( W prefix 1 ) = <" ( W ` 0 ) "> )
14 13 oveq1d 
 |-  ( ( W e. Word A /\ W =/= (/) ) -> ( ( W prefix 1 ) ++ ( W substr <. 1 , ( # ` W ) >. ) ) = ( <" ( W ` 0 ) "> ++ ( W substr <. 1 , ( # ` W ) >. ) ) )
15 pfxid 
 |-  ( W e. Word A -> ( W prefix ( # ` W ) ) = W )
16 15 adantr 
 |-  ( ( W e. Word A /\ W =/= (/) ) -> ( W prefix ( # ` W ) ) = W )
17 12 14 16 3eqtr3rd 
 |-  ( ( W e. Word A /\ W =/= (/) ) -> W = ( <" ( W ` 0 ) "> ++ ( W substr <. 1 , ( # ` W ) >. ) ) )