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 ) ) ) )