Metamath Proof Explorer

Theorem ccatval2

Description: Value of a symbol in the right half of a concatenated word. (Contributed by Stefan O'Rear, 15-Aug-2015) (Revised by Mario Carneiro, 22-Sep-2015)

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

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. ( ( # ` S ) ..^ ( ( # ` S ) + ( # ` T ) ) ) ) -> ( 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 fzodisj 
 |-  ( ( 0 ..^ ( # ` S ) ) i^i ( ( # ` S ) ..^ ( ( # ` S ) + ( # ` T ) ) ) ) = (/)
8 minel 
 |-  ( ( I e. ( ( # ` S ) ..^ ( ( # ` S ) + ( # ` T ) ) ) /\ ( ( 0 ..^ ( # ` S ) ) i^i ( ( # ` S ) ..^ ( ( # ` S ) + ( # ` T ) ) ) ) = (/) ) -> -. I e. ( 0 ..^ ( # ` S ) ) )
9 7 8 mpan2 
 |-  ( I e. ( ( # ` S ) ..^ ( ( # ` S ) + ( # ` T ) ) ) -> -. I e. ( 0 ..^ ( # ` S ) ) )
10 9 3ad2ant3 
 |-  ( ( S e. Word B /\ T e. Word B /\ I e. ( ( # ` S ) ..^ ( ( # ` S ) + ( # ` T ) ) ) ) -> -. I e. ( 0 ..^ ( # ` S ) ) )
11 10 iffalsed 
 |-  ( ( S e. Word B /\ T e. Word B /\ I e. ( ( # ` S ) ..^ ( ( # ` S ) + ( # ` T ) ) ) ) -> if ( I e. ( 0 ..^ ( # ` S ) ) , ( S ` I ) , ( T ` ( I - ( # ` S ) ) ) ) = ( T ` ( I - ( # ` S ) ) ) )
12 6 11 sylan9eqr 
 |-  ( ( ( S e. Word B /\ T e. Word B /\ I e. ( ( # ` S ) ..^ ( ( # ` S ) + ( # ` T ) ) ) ) /\ x = I ) -> if ( x e. ( 0 ..^ ( # ` S ) ) , ( S ` x ) , ( T ` ( x - ( # ` S ) ) ) ) = ( T ` ( I - ( # ` S ) ) ) )
13 wrdfin 
 |-  ( S e. Word B -> S e. Fin )
14 13 adantr 
 |-  ( ( S e. Word B /\ T e. Word B ) -> S e. Fin )
15 hashcl 
 |-  ( S e. Fin -> ( # ` S ) e. NN0 )
16 fzoss1 
 |-  ( ( # ` S ) e. ( ZZ>= ` 0 ) -> ( ( # ` S ) ..^ ( ( # ` S ) + ( # ` T ) ) ) C_ ( 0 ..^ ( ( # ` S ) + ( # ` T ) ) ) )
17 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
18 16 17 eleq2s 
 |-  ( ( # ` S ) e. NN0 -> ( ( # ` S ) ..^ ( ( # ` S ) + ( # ` T ) ) ) C_ ( 0 ..^ ( ( # ` S ) + ( # ` T ) ) ) )
19 14 15 18 3syl 
 |-  ( ( S e. Word B /\ T e. Word B ) -> ( ( # ` S ) ..^ ( ( # ` S ) + ( # ` T ) ) ) C_ ( 0 ..^ ( ( # ` S ) + ( # ` T ) ) ) )
20 19 sseld 
 |-  ( ( S e. Word B /\ T e. Word B ) -> ( I e. ( ( # ` S ) ..^ ( ( # ` S ) + ( # ` T ) ) ) -> I e. ( 0 ..^ ( ( # ` S ) + ( # ` T ) ) ) ) )
21 20 3impia 
 |-  ( ( S e. Word B /\ T e. Word B /\ I e. ( ( # ` S ) ..^ ( ( # ` S ) + ( # ` T ) ) ) ) -> I e. ( 0 ..^ ( ( # ` S ) + ( # ` T ) ) ) )
22 fvexd 
 |-  ( ( S e. Word B /\ T e. Word B /\ I e. ( ( # ` S ) ..^ ( ( # ` S ) + ( # ` T ) ) ) ) -> ( T ` ( I - ( # ` S ) ) ) e. _V )
23 2 12 21 22 fvmptd 
 |-  ( ( S e. Word B /\ T e. Word B /\ I e. ( ( # ` S ) ..^ ( ( # ` S ) + ( # ` T ) ) ) ) -> ( ( S ++ T ) ` I ) = ( T ` ( I - ( # ` S ) ) ) )