Metamath Proof Explorer

Theorem ccatval1OLD

Description: Obsolete version of ccatval1 as of 18-Jan-2024. 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) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 ccatfval 
 |-  ( ( S e. Word B /\ 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 B /\ 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 B /\ 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 B /\ T e. Word B /\ I e. ( 0 ..^ ( # ` S ) ) ) /\ x = I ) -> if ( x e. ( 0 ..^ ( # ` S ) ) , ( S ` x ) , ( T ` ( x - ( # ` S ) ) ) ) = ( S ` I ) )
10 simp3 
 |-  ( ( S e. Word B /\ T e. Word B /\ I e. ( 0 ..^ ( # ` S ) ) ) -> I e. ( 0 ..^ ( # ` S ) ) )
11 lencl 
 |-  ( T e. Word B -> ( # ` T ) e. NN0 )
12 11 3ad2ant2 
 |-  ( ( S e. Word B /\ T e. Word B /\ I e. ( 0 ..^ ( # ` S ) ) ) -> ( # ` T ) e. NN0 )
13 elfzoext 
 |-  ( ( I e. ( 0 ..^ ( # ` S ) ) /\ ( # ` T ) e. NN0 ) -> I e. ( 0 ..^ ( ( # ` S ) + ( # ` T ) ) ) )
14 10 12 13 syl2anc 
 |-  ( ( S e. Word B /\ T e. Word B /\ I e. ( 0 ..^ ( # ` S ) ) ) -> I e. ( 0 ..^ ( ( # ` S ) + ( # ` T ) ) ) )
15 fvexd 
 |-  ( ( S e. Word B /\ T e. Word B /\ I e. ( 0 ..^ ( # ` S ) ) ) -> ( S ` I ) e. _V )
16 2 9 14 15 fvmptd 
 |-  ( ( S e. Word B /\ T e. Word B /\ I e. ( 0 ..^ ( # ` S ) ) ) -> ( ( S ++ T ) ` I ) = ( S ` I ) )