Metamath Proof Explorer


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 eqtrid
 |-  ( X e. V -> ( T ` M ) = X )