Metamath Proof Explorer

Theorem ccatval3

Description: Value of a symbol in the right half of a concatenated word, using an index relative to the subword. (Contributed by Stefan O'Rear, 16-Aug-2015) (Proof shortened by AV, 30-Apr-2020)

Ref Expression
Assertion ccatval3 
|- ( ( S e. Word B /\ T e. Word B /\ I e. ( 0 ..^ ( # ` T ) ) ) -> ( ( S ++ T ) ` ( I + ( # ` S ) ) ) = ( T ` I ) )

Proof

Step Hyp Ref Expression
1 lencl 
 |-  ( S e. Word B -> ( # ` S ) e. NN0 )
2 1 nn0zd 
 |-  ( S e. Word B -> ( # ` S ) e. ZZ )
3 2 anim1ci 
 |-  ( ( S e. Word B /\ I e. ( 0 ..^ ( # ` T ) ) ) -> ( I e. ( 0 ..^ ( # ` T ) ) /\ ( # ` S ) e. ZZ ) )
4 3 3adant2 
 |-  ( ( S e. Word B /\ T e. Word B /\ I e. ( 0 ..^ ( # ` T ) ) ) -> ( I e. ( 0 ..^ ( # ` T ) ) /\ ( # ` S ) e. ZZ ) )
5 fzo0addelr 
 |-  ( ( I e. ( 0 ..^ ( # ` T ) ) /\ ( # ` S ) e. ZZ ) -> ( I + ( # ` S ) ) e. ( ( # ` S ) ..^ ( ( # ` S ) + ( # ` T ) ) ) )
6 4 5 syl 
 |-  ( ( S e. Word B /\ T e. Word B /\ I e. ( 0 ..^ ( # ` T ) ) ) -> ( I + ( # ` S ) ) e. ( ( # ` S ) ..^ ( ( # ` S ) + ( # ` T ) ) ) )
7 ccatval2 
 |-  ( ( S e. Word B /\ T e. Word B /\ ( I + ( # ` S ) ) e. ( ( # ` S ) ..^ ( ( # ` S ) + ( # ` T ) ) ) ) -> ( ( S ++ T ) ` ( I + ( # ` S ) ) ) = ( T ` ( ( I + ( # ` S ) ) - ( # ` S ) ) ) )
8 6 7 syld3an3 
 |-  ( ( S e. Word B /\ T e. Word B /\ I e. ( 0 ..^ ( # ` T ) ) ) -> ( ( S ++ T ) ` ( I + ( # ` S ) ) ) = ( T ` ( ( I + ( # ` S ) ) - ( # ` S ) ) ) )
9 elfzoelz 
 |-  ( I e. ( 0 ..^ ( # ` T ) ) -> I e. ZZ )
10 9 3ad2ant3 
 |-  ( ( S e. Word B /\ T e. Word B /\ I e. ( 0 ..^ ( # ` T ) ) ) -> I e. ZZ )
11 10 zcnd 
 |-  ( ( S e. Word B /\ T e. Word B /\ I e. ( 0 ..^ ( # ` T ) ) ) -> I e. CC )
12 1 3ad2ant1 
 |-  ( ( S e. Word B /\ T e. Word B /\ I e. ( 0 ..^ ( # ` T ) ) ) -> ( # ` S ) e. NN0 )
13 12 nn0cnd 
 |-  ( ( S e. Word B /\ T e. Word B /\ I e. ( 0 ..^ ( # ` T ) ) ) -> ( # ` S ) e. CC )
14 11 13 pncand 
 |-  ( ( S e. Word B /\ T e. Word B /\ I e. ( 0 ..^ ( # ` T ) ) ) -> ( ( I + ( # ` S ) ) - ( # ` S ) ) = I )
15 14 fveq2d 
 |-  ( ( S e. Word B /\ T e. Word B /\ I e. ( 0 ..^ ( # ` T ) ) ) -> ( T ` ( ( I + ( # ` S ) ) - ( # ` S ) ) ) = ( T ` I ) )
16 8 15 eqtrd 
 |-  ( ( S e. Word B /\ T e. Word B /\ I e. ( 0 ..^ ( # ` T ) ) ) -> ( ( S ++ T ) ` ( I + ( # ` S ) ) ) = ( T ` I ) )