Metamath Proof Explorer

Theorem pfx1

Description: The prefix of length one of a nonempty word expressed as a singleton word. (Contributed by AV, 15-May-2020)

Ref Expression
Assertion pfx1 
|- ( ( W e. Word V /\ W =/= (/) ) -> ( W prefix 1 ) = <" ( W ` 0 ) "> )

Proof

Step Hyp Ref Expression
1 1nn0 
 |-  1 e. NN0
2 1 a1i 
 |-  ( W =/= (/) -> 1 e. NN0 )
3 pfxval 
 |-  ( ( W e. Word V /\ 1 e. NN0 ) -> ( W prefix 1 ) = ( W substr <. 0 , 1 >. ) )
4 2 3 sylan2 
 |-  ( ( W e. Word V /\ W =/= (/) ) -> ( W prefix 1 ) = ( W substr <. 0 , 1 >. ) )
5 1e0p1 
 |-  1 = ( 0 + 1 )
6 5 opeq2i 
 |-  <. 0 , 1 >. = <. 0 , ( 0 + 1 ) >.
7 6 oveq2i 
 |-  ( W substr <. 0 , 1 >. ) = ( W substr <. 0 , ( 0 + 1 ) >. )
8 7 a1i 
 |-  ( ( W e. Word V /\ W =/= (/) ) -> ( W substr <. 0 , 1 >. ) = ( W substr <. 0 , ( 0 + 1 ) >. ) )
9 lennncl 
 |-  ( ( W e. Word V /\ W =/= (/) ) -> ( # ` W ) e. NN )
10 lbfzo0 
 |-  ( 0 e. ( 0 ..^ ( # ` W ) ) <-> ( # ` W ) e. NN )
11 9 10 sylibr 
 |-  ( ( W e. Word V /\ W =/= (/) ) -> 0 e. ( 0 ..^ ( # ` W ) ) )
12 swrds1 
 |-  ( ( W e. Word V /\ 0 e. ( 0 ..^ ( # ` W ) ) ) -> ( W substr <. 0 , ( 0 + 1 ) >. ) = <" ( W ` 0 ) "> )
13 11 12 syldan 
 |-  ( ( W e. Word V /\ W =/= (/) ) -> ( W substr <. 0 , ( 0 + 1 ) >. ) = <" ( W ` 0 ) "> )
14 4 8 13 3eqtrd 
 |-  ( ( W e. Word V /\ W =/= (/) ) -> ( W prefix 1 ) = <" ( W ` 0 ) "> )