Theorem swrdlsw

Description: Extract the last single symbol from a word. (Contributed by Alexander van der Vekens, 23-Sep-2018)

	Ref	Expression
Assertion	swrdlsw	|- ( ( W e. Word V /\ W =/= (/) ) -> ( W substr <. ( ( # ` W ) - 1 ) , ( # ` W ) >. ) = <" ( lastS ` W ) "> )

Proof

Step	Hyp	Ref	Expression
1		hashneq0	|- ( W e. Word V -> ( 0 < ( # ` W ) <-> W =/= (/) ) )
2		lencl	|- ( W e. Word V -> ( # ` W ) e. NN0 )
3		nn0z	|- ( ( # ` W ) e. NN0 -> ( # ` W ) e. ZZ )
4		elnnz	|- ( ( # ` W ) e. NN <-> ( ( # ` W ) e. ZZ /\ 0 < ( # ` W ) ) )
5		fzo0end	|- ( ( # ` W ) e. NN -> ( ( # ` W ) - 1 ) e. ( 0 ..^ ( # ` W ) ) )
6	4 5	sylbir	|- ( ( ( # ` W ) e. ZZ /\ 0 < ( # ` W ) ) -> ( ( # ` W ) - 1 ) e. ( 0 ..^ ( # ` W ) ) )
7	6	ex	|- ( ( # ` W ) e. ZZ -> ( 0 < ( # ` W ) -> ( ( # ` W ) - 1 ) e. ( 0 ..^ ( # ` W ) ) ) )
8	2 3 7	3syl	|- ( W e. Word V -> ( 0 < ( # ` W ) -> ( ( # ` W ) - 1 ) e. ( 0 ..^ ( # ` W ) ) ) )
9	1 8	sylbird	|- ( W e. Word V -> ( W =/= (/) -> ( ( # ` W ) - 1 ) e. ( 0 ..^ ( # ` W ) ) ) )
10	9	imp	|- ( ( W e. Word V /\ W =/= (/) ) -> ( ( # ` W ) - 1 ) e. ( 0 ..^ ( # ` W ) ) )
11		swrds1	|- ( ( W e. Word V /\ ( ( # ` W ) - 1 ) e. ( 0 ..^ ( # ` W ) ) ) -> ( W substr <. ( ( # ` W ) - 1 ) , ( ( ( # ` W ) - 1 ) + 1 ) >. ) = <" ( W ` ( ( # ` W ) - 1 ) ) "> )
12	10 11	syldan	|- ( ( W e. Word V /\ W =/= (/) ) -> ( W substr <. ( ( # ` W ) - 1 ) , ( ( ( # ` W ) - 1 ) + 1 ) >. ) = <" ( W ` ( ( # ` W ) - 1 ) ) "> )
13		nn0cn	|- ( ( # ` W ) e. NN0 -> ( # ` W ) e. CC )
14		ax-1cn	|- 1 e. CC
15	13 14	jctir	|- ( ( # ` W ) e. NN0 -> ( ( # ` W ) e. CC /\ 1 e. CC ) )
16		npcan	|- ( ( ( # ` W ) e. CC /\ 1 e. CC ) -> ( ( ( # ` W ) - 1 ) + 1 ) = ( # ` W ) )
17	16	eqcomd	|- ( ( ( # ` W ) e. CC /\ 1 e. CC ) -> ( # ` W ) = ( ( ( # ` W ) - 1 ) + 1 ) )
18	2 15 17	3syl	|- ( W e. Word V -> ( # ` W ) = ( ( ( # ` W ) - 1 ) + 1 ) )
19	18	adantr	|- ( ( W e. Word V /\ W =/= (/) ) -> ( # ` W ) = ( ( ( # ` W ) - 1 ) + 1 ) )
20	19	opeq2d	|- ( ( W e. Word V /\ W =/= (/) ) -> <. ( ( # ` W ) - 1 ) , ( # ` W ) >. = <. ( ( # ` W ) - 1 ) , ( ( ( # ` W ) - 1 ) + 1 ) >. )
21	20	oveq2d	|- ( ( W e. Word V /\ W =/= (/) ) -> ( W substr <. ( ( # ` W ) - 1 ) , ( # ` W ) >. ) = ( W substr <. ( ( # ` W ) - 1 ) , ( ( ( # ` W ) - 1 ) + 1 ) >. ) )
22		lsw	|- ( W e. Word V -> ( lastS ` W ) = ( W ` ( ( # ` W ) - 1 ) ) )
23	22	adantr	|- ( ( W e. Word V /\ W =/= (/) ) -> ( lastS ` W ) = ( W ` ( ( # ` W ) - 1 ) ) )
24	23	s1eqd	|- ( ( W e. Word V /\ W =/= (/) ) -> <" ( lastS ` W ) "> = <" ( W ` ( ( # ` W ) - 1 ) ) "> )
25	12 21 24	3eqtr4d	|- ( ( W e. Word V /\ W =/= (/) ) -> ( W substr <. ( ( # ` W ) - 1 ) , ( # ` W ) >. ) = <" ( lastS ` W ) "> )