Metamath Proof Explorer

Theorem ccatlen

Description: The length of a concatenated word. (Contributed by Stefan O'Rear, 15-Aug-2015) (Revised by JJ, 1-Jan-2024)

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

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 fveq2d 
 |-  ( ( 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 ) ) ) ) ) ) )
3 fvex 
 |-  ( S ` x ) e. _V
4 fvex 
 |-  ( T ` ( x - ( # ` S ) ) ) e. _V
5 3 4 ifex 
 |-  if ( x e. ( 0 ..^ ( # ` S ) ) , ( S ` x ) , ( T ` ( x - ( # ` S ) ) ) ) e. _V
6 eqid 
 |-  ( x e. ( 0 ..^ ( ( # ` S ) + ( # ` T ) ) ) |-> if ( x e. ( 0 ..^ ( # ` S ) ) , ( S ` x ) , ( T ` ( x - ( # ` S ) ) ) ) ) = ( x e. ( 0 ..^ ( ( # ` S ) + ( # ` T ) ) ) |-> if ( x e. ( 0 ..^ ( # ` S ) ) , ( S ` x ) , ( T ` ( x - ( # ` S ) ) ) ) )
7 5 6 fnmpti 
 |-  ( x e. ( 0 ..^ ( ( # ` S ) + ( # ` T ) ) ) |-> if ( x e. ( 0 ..^ ( # ` S ) ) , ( S ` x ) , ( T ` ( x - ( # ` S ) ) ) ) ) Fn ( 0 ..^ ( ( # ` S ) + ( # ` T ) ) )
8 hashfn 
 |-  ( ( x e. ( 0 ..^ ( ( # ` S ) + ( # ` T ) ) ) |-> if ( x e. ( 0 ..^ ( # ` S ) ) , ( S ` x ) , ( T ` ( x - ( # ` S ) ) ) ) ) Fn ( 0 ..^ ( ( # ` S ) + ( # ` T ) ) ) -> ( # ` ( x e. ( 0 ..^ ( ( # ` S ) + ( # ` T ) ) ) |-> if ( x e. ( 0 ..^ ( # ` S ) ) , ( S ` x ) , ( T ` ( x - ( # ` S ) ) ) ) ) ) = ( # ` ( 0 ..^ ( ( # ` S ) + ( # ` T ) ) ) ) )
9 7 8 mp1i 
 |-  ( ( S e. Word A /\ T e. Word B ) -> ( # ` ( x e. ( 0 ..^ ( ( # ` S ) + ( # ` T ) ) ) |-> if ( x e. ( 0 ..^ ( # ` S ) ) , ( S ` x ) , ( T ` ( x - ( # ` S ) ) ) ) ) ) = ( # ` ( 0 ..^ ( ( # ` S ) + ( # ` T ) ) ) ) )
10 lencl 
 |-  ( S e. Word A -> ( # ` S ) e. NN0 )
11 lencl 
 |-  ( T e. Word B -> ( # ` T ) e. NN0 )
12 nn0addcl 
 |-  ( ( ( # ` S ) e. NN0 /\ ( # ` T ) e. NN0 ) -> ( ( # ` S ) + ( # ` T ) ) e. NN0 )
13 10 11 12 syl2an 
 |-  ( ( S e. Word A /\ T e. Word B ) -> ( ( # ` S ) + ( # ` T ) ) e. NN0 )
14 hashfzo0 
 |-  ( ( ( # ` S ) + ( # ` T ) ) e. NN0 -> ( # ` ( 0 ..^ ( ( # ` S ) + ( # ` T ) ) ) ) = ( ( # ` S ) + ( # ` T ) ) )
15 13 14 syl 
 |-  ( ( S e. Word A /\ T e. Word B ) -> ( # ` ( 0 ..^ ( ( # ` S ) + ( # ` T ) ) ) ) = ( ( # ` S ) + ( # ` T ) ) )
16 2 9 15 3eqtrd 
 |-  ( ( S e. Word A /\ T e. Word B ) -> ( # ` ( S ++ T ) ) = ( ( # ` S ) + ( # ` T ) ) )