Metamath Proof Explorer

Theorem ccatval1

Description: Value of a symbol in the left half of a concatenated word. (Contributed by Stefan O'Rear, 15-Aug-2015) (Revised by Mario Carneiro, 22-Sep-2015) (Proof shortened by AV, 30-Apr-2020) (Revised by JJ, 18-Jan-2024)

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

Proof

Step Hyp Ref Expression
1 ccatfval 
 |-  ( ( S e. Word A /\ T e. Word B ) -> ( S ++ T ) = ( x e. ( 0 ..^ ( ( # ` S ) + ( # ` T ) ) ) |-> if ( x e. ( 0 ..^ ( # ` S ) ) , ( S ` x ) , ( T ` ( x - ( # ` S ) ) ) ) ) )
2 1 3adant3 
 |-  ( ( S e. Word A /\ T e. Word B /\ I e. ( 0 ..^ ( # ` S ) ) ) -> ( S ++ T ) = ( x e. ( 0 ..^ ( ( # ` S ) + ( # ` T ) ) ) |-> if ( x e. ( 0 ..^ ( # ` S ) ) , ( S ` x ) , ( T ` ( x - ( # ` S ) ) ) ) ) )
3 eleq1 
 |-  ( x = I -> ( x e. ( 0 ..^ ( # ` S ) ) <-> I e. ( 0 ..^ ( # ` S ) ) ) )
4 fveq2 
 |-  ( x = I -> ( S ` x ) = ( S ` I ) )
5 fvoveq1 
 |-  ( x = I -> ( T ` ( x - ( # ` S ) ) ) = ( T ` ( I - ( # ` S ) ) ) )
6 3 4 5 ifbieq12d 
 |-  ( x = I -> if ( x e. ( 0 ..^ ( # ` S ) ) , ( S ` x ) , ( T ` ( x - ( # ` S ) ) ) ) = if ( I e. ( 0 ..^ ( # ` S ) ) , ( S ` I ) , ( T ` ( I - ( # ` S ) ) ) ) )
7 iftrue 
 |-  ( I e. ( 0 ..^ ( # ` S ) ) -> if ( I e. ( 0 ..^ ( # ` S ) ) , ( S ` I ) , ( T ` ( I - ( # ` S ) ) ) ) = ( S ` I ) )
8 7 3ad2ant3 
 |-  ( ( S e. Word A /\ T e. Word B /\ I e. ( 0 ..^ ( # ` S ) ) ) -> if ( I e. ( 0 ..^ ( # ` S ) ) , ( S ` I ) , ( T ` ( I - ( # ` S ) ) ) ) = ( S ` I ) )
9 6 8 sylan9eqr 
 |-  ( ( ( S e. Word A /\ T e. Word B /\ I e. ( 0 ..^ ( # ` S ) ) ) /\ x = I ) -> if ( x e. ( 0 ..^ ( # ` S ) ) , ( S ` x ) , ( T ` ( x - ( # ` S ) ) ) ) = ( S ` I ) )
10 id 
 |-  ( I e. ( 0 ..^ ( # ` S ) ) -> I e. ( 0 ..^ ( # ` S ) ) )
11 lencl 
 |-  ( T e. Word B -> ( # ` T ) e. NN0 )
12 elfzoext 
 |-  ( ( I e. ( 0 ..^ ( # ` S ) ) /\ ( # ` T ) e. NN0 ) -> I e. ( 0 ..^ ( ( # ` S ) + ( # ` T ) ) ) )
13 10 11 12 syl2anr 
 |-  ( ( T e. Word B /\ I e. ( 0 ..^ ( # ` S ) ) ) -> I e. ( 0 ..^ ( ( # ` S ) + ( # ` T ) ) ) )
14 13 3adant1 
 |-  ( ( S e. Word A /\ T e. Word B /\ I e. ( 0 ..^ ( # ` S ) ) ) -> I e. ( 0 ..^ ( ( # ` S ) + ( # ` T ) ) ) )
15 fvexd 
 |-  ( ( S e. Word A /\ T e. Word B /\ I e. ( 0 ..^ ( # ` S ) ) ) -> ( S ` I ) e. _V )
16 2 9 14 15 fvmptd 
 |-  ( ( S e. Word A /\ T e. Word B /\ I e. ( 0 ..^ ( # ` S ) ) ) -> ( ( S ++ T ) ` I ) = ( S ` I ) )