Theorem pfxtrcfv0

Description: The first symbol in a word truncated by one symbol. (Contributed by Alexander van der Vekens, 16-Jun-2018) (Revised by AV, 3-May-2020)

	Ref	Expression
Assertion	pfxtrcfv0	|- ( ( W e. Word V /\ 2 <_ ( # ` W ) ) -> ( ( W prefix ( ( # ` W ) - 1 ) ) ` 0 ) = ( W ` 0 ) )

Proof

Step	Hyp	Ref	Expression
1		simpl	|- ( ( W e. Word V /\ 2 <_ ( # ` W ) ) -> W e. Word V )
2		wrdlenge2n0	|- ( ( W e. Word V /\ 2 <_ ( # ` W ) ) -> W =/= (/) )
3		2z	|- 2 e. ZZ
4	3	a1i	|- ( ( W e. Word V /\ 2 <_ ( # ` W ) ) -> 2 e. ZZ )
5		lencl	|- ( W e. Word V -> ( # ` W ) e. NN0 )
6	5	nn0zd	|- ( W e. Word V -> ( # ` W ) e. ZZ )
7	6	adantr	|- ( ( W e. Word V /\ 2 <_ ( # ` W ) ) -> ( # ` W ) e. ZZ )
8		simpr	|- ( ( W e. Word V /\ 2 <_ ( # ` W ) ) -> 2 <_ ( # ` W ) )
9		eluz2	|- ( ( # ` W ) e. ( ZZ>= ` 2 ) <-> ( 2 e. ZZ /\ ( # ` W ) e. ZZ /\ 2 <_ ( # ` W ) ) )
10	4 7 8 9	syl3anbrc	|- ( ( W e. Word V /\ 2 <_ ( # ` W ) ) -> ( # ` W ) e. ( ZZ>= ` 2 ) )
11		uz2m1nn	|- ( ( # ` W ) e. ( ZZ>= ` 2 ) -> ( ( # ` W ) - 1 ) e. NN )
12	10 11	syl	|- ( ( W e. Word V /\ 2 <_ ( # ` W ) ) -> ( ( # ` W ) - 1 ) e. NN )
13		lbfzo0	|- ( 0 e. ( 0 ..^ ( ( # ` W ) - 1 ) ) <-> ( ( # ` W ) - 1 ) e. NN )
14	12 13	sylibr	|- ( ( W e. Word V /\ 2 <_ ( # ` W ) ) -> 0 e. ( 0 ..^ ( ( # ` W ) - 1 ) ) )
15		pfxtrcfv	|- ( ( W e. Word V /\ W =/= (/) /\ 0 e. ( 0 ..^ ( ( # ` W ) - 1 ) ) ) -> ( ( W prefix ( ( # ` W ) - 1 ) ) ` 0 ) = ( W ` 0 ) )
16	1 2 14 15	syl3anc	|- ( ( W e. Word V /\ 2 <_ ( # ` W ) ) -> ( ( W prefix ( ( # ` W ) - 1 ) ) ` 0 ) = ( W ` 0 ) )