Theorem cats1fvn

Description: The last symbol of a concatenation with a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016)

	Ref	Expression
Hypotheses	cats1cld.1	|- T = ( S ++ <" X "> )
	cats1cli.2	|- S e. Word _V
	cats1fvn.3	|- ( # ` S ) = M
Assertion	cats1fvn	|- ( X e. V -> ( T ` M ) = X )

Proof

Step	Hyp	Ref	Expression
1		cats1cld.1	|- T = ( S ++ <" X "> )
2		cats1cli.2	|- S e. Word _V
3		cats1fvn.3	|- ( # ` S ) = M
4	3	oveq2i	|- ( 0 + ( # ` S ) ) = ( 0 + M )
5		lencl	|- ( S e. Word _V -> ( # ` S ) e. NN0 )
6	2 5	ax-mp	|- ( # ` S ) e. NN0
7	3 6	eqeltrri	|- M e. NN0
8	7	nn0cni	|- M e. CC
9	8	addid2i	|- ( 0 + M ) = M
10	4 9	eqtr2i	|- M = ( 0 + ( # ` S ) )
11	1 10	fveq12i	|- ( T ` M ) = ( ( S ++ <" X "> ) ` ( 0 + ( # ` S ) ) )
12		s1cli	|- <" X "> e. Word _V
13		s1len	|- ( # ` <" X "> ) = 1
14		1nn	|- 1 e. NN
15	13 14	eqeltri	|- ( # ` <" X "> ) e. NN
16		lbfzo0	|- ( 0 e. ( 0 ..^ ( # ` <" X "> ) ) <-> ( # ` <" X "> ) e. NN )
17	15 16	mpbir	|- 0 e. ( 0 ..^ ( # ` <" X "> ) )
18		ccatval3	|- ( ( S e. Word _V /\ <" X "> e. Word _V /\ 0 e. ( 0 ..^ ( # ` <" X "> ) ) ) -> ( ( S ++ <" X "> ) ` ( 0 + ( # ` S ) ) ) = ( <" X "> ` 0 ) )
19	2 12 17 18	mp3an	|- ( ( S ++ <" X "> ) ` ( 0 + ( # ` S ) ) ) = ( <" X "> ` 0 )
20	11 19	eqtri	|- ( T ` M ) = ( <" X "> ` 0 )
21		s1fv	|- ( X e. V -> ( <" X "> ` 0 ) = X )
22	20 21	syl5eq	|- ( X e. V -> ( T ` M ) = X )