Metamath Proof Explorer

Theorem cats1fv

Description: A symbol other than the last in 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
cats1fv.4 
|- ( Y e. V -> ( S ` N ) = Y )
cats1fv.5 
|- N e. NN0
cats1fv.6 
|- N < M
Assertion cats1fv 
|- ( Y e. V -> ( T ` N ) = Y )

Proof

Step Hyp Ref Expression
1 cats1cld.1 
 |-  T = ( S ++ <" X "> )
2 cats1cli.2 
 |-  S e. Word _V
3 cats1fvn.3 
 |-  ( # ` S ) = M
4 cats1fv.4 
 |-  ( Y e. V -> ( S ` N ) = Y )
5 cats1fv.5 
 |-  N e. NN0
6 cats1fv.6 
 |-  N < M
7 1 fveq1i 
 |-  ( T ` N ) = ( ( S ++ <" X "> ) ` N )
8 s1cli 
 |-  <" X "> e. Word _V
9 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
10 5 9 eleqtri 
 |-  N e. ( ZZ>= ` 0 )
11 lencl 
 |-  ( S e. Word _V -> ( # ` S ) e. NN0 )
12 nn0z 
 |-  ( ( # ` S ) e. NN0 -> ( # ` S ) e. ZZ )
13 2 11 12 mp2b 
 |-  ( # ` S ) e. ZZ
14 6 3 breqtrri 
 |-  N < ( # ` S )
15 elfzo2 
 |-  ( N e. ( 0 ..^ ( # ` S ) ) <-> ( N e. ( ZZ>= ` 0 ) /\ ( # ` S ) e. ZZ /\ N < ( # ` S ) ) )
16 10 13 14 15 mpbir3an 
 |-  N e. ( 0 ..^ ( # ` S ) )
17 ccatval1 
 |-  ( ( S e. Word _V /\ <" X "> e. Word _V /\ N e. ( 0 ..^ ( # ` S ) ) ) -> ( ( S ++ <" X "> ) ` N ) = ( S ` N ) )
18 2 8 16 17 mp3an 
 |-  ( ( S ++ <" X "> ) ` N ) = ( S ` N )
19 7 18 eqtri 
 |-  ( T ` N ) = ( S ` N )
20 19 4 eqtrid 
 |-  ( Y e. V -> ( T ` N ) = Y )