Metamath Proof Explorer

Theorem ccatcl

Description: The concatenation of two words is a word. (Contributed by FL, 2-Feb-2014) (Proof shortened by Stefan O'Rear, 15-Aug-2015) (Proof shortened by AV, 29-Apr-2020)

Ref Expression
Assertion ccatcl 
|- ( ( S e. Word B /\ T e. Word B ) -> ( S ++ T ) e. Word B )

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 wrdf 
 |-  ( S e. Word B -> S : ( 0 ..^ ( # ` S ) ) --> B )
3 2 ad2antrr 
 |-  ( ( ( S e. Word B /\ T e. Word B ) /\ x e. ( 0 ..^ ( ( # ` S ) + ( # ` T ) ) ) ) -> S : ( 0 ..^ ( # ` S ) ) --> B )
4 3 ffvelrnda 
 |-  ( ( ( ( S e. Word B /\ T e. Word B ) /\ x e. ( 0 ..^ ( ( # ` S ) + ( # ` T ) ) ) ) /\ x e. ( 0 ..^ ( # ` S ) ) ) -> ( S ` x ) e. B )
5 wrdf 
 |-  ( T e. Word B -> T : ( 0 ..^ ( # ` T ) ) --> B )
6 5 ad3antlr 
 |-  ( ( ( ( S e. Word B /\ T e. Word B ) /\ x e. ( 0 ..^ ( ( # ` S ) + ( # ` T ) ) ) ) /\ -. x e. ( 0 ..^ ( # ` S ) ) ) -> T : ( 0 ..^ ( # ` T ) ) --> B )
7 simpr 
 |-  ( ( ( S e. Word B /\ T e. Word B ) /\ x e. ( 0 ..^ ( ( # ` S ) + ( # ` T ) ) ) ) -> x e. ( 0 ..^ ( ( # ` S ) + ( # ` T ) ) ) )
8 7 anim1i 
 |-  ( ( ( ( S e. Word B /\ T e. Word B ) /\ x e. ( 0 ..^ ( ( # ` S ) + ( # ` T ) ) ) ) /\ -. x e. ( 0 ..^ ( # ` S ) ) ) -> ( x e. ( 0 ..^ ( ( # ` S ) + ( # ` T ) ) ) /\ -. x e. ( 0 ..^ ( # ` S ) ) ) )
9 lencl 
 |-  ( S e. Word B -> ( # ` S ) e. NN0 )
10 9 nn0zd 
 |-  ( S e. Word B -> ( # ` S ) e. ZZ )
11 lencl 
 |-  ( T e. Word B -> ( # ` T ) e. NN0 )
12 11 nn0zd 
 |-  ( T e. Word B -> ( # ` T ) e. ZZ )
13 10 12 anim12i 
 |-  ( ( S e. Word B /\ T e. Word B ) -> ( ( # ` S ) e. ZZ /\ ( # ` T ) e. ZZ ) )
14 13 ad2antrr 
 |-  ( ( ( ( S e. Word B /\ T e. Word B ) /\ x e. ( 0 ..^ ( ( # ` S ) + ( # ` T ) ) ) ) /\ -. x e. ( 0 ..^ ( # ` S ) ) ) -> ( ( # ` S ) e. ZZ /\ ( # ` T ) e. ZZ ) )
15 fzocatel 
 |-  ( ( ( x e. ( 0 ..^ ( ( # ` S ) + ( # ` T ) ) ) /\ -. x e. ( 0 ..^ ( # ` S ) ) ) /\ ( ( # ` S ) e. ZZ /\ ( # ` T ) e. ZZ ) ) -> ( x - ( # ` S ) ) e. ( 0 ..^ ( # ` T ) ) )
16 8 14 15 syl2anc 
 |-  ( ( ( ( S e. Word B /\ T e. Word B ) /\ x e. ( 0 ..^ ( ( # ` S ) + ( # ` T ) ) ) ) /\ -. x e. ( 0 ..^ ( # ` S ) ) ) -> ( x - ( # ` S ) ) e. ( 0 ..^ ( # ` T ) ) )
17 6 16 ffvelrnd 
 |-  ( ( ( ( S e. Word B /\ T e. Word B ) /\ x e. ( 0 ..^ ( ( # ` S ) + ( # ` T ) ) ) ) /\ -. x e. ( 0 ..^ ( # ` S ) ) ) -> ( T ` ( x - ( # ` S ) ) ) e. B )
18 4 17 ifclda 
 |-  ( ( ( S e. Word B /\ T e. Word B ) /\ x e. ( 0 ..^ ( ( # ` S ) + ( # ` T ) ) ) ) -> if ( x e. ( 0 ..^ ( # ` S ) ) , ( S ` x ) , ( T ` ( x - ( # ` S ) ) ) ) e. B )
19 18 fmpttd 
 |-  ( ( S e. Word B /\ T e. Word B ) -> ( x e. ( 0 ..^ ( ( # ` S ) + ( # ` T ) ) ) |-> if ( x e. ( 0 ..^ ( # ` S ) ) , ( S ` x ) , ( T ` ( x - ( # ` S ) ) ) ) ) : ( 0 ..^ ( ( # ` S ) + ( # ` T ) ) ) --> B )
20 iswrdi 
 |-  ( ( x e. ( 0 ..^ ( ( # ` S ) + ( # ` T ) ) ) |-> if ( x e. ( 0 ..^ ( # ` S ) ) , ( S ` x ) , ( T ` ( x - ( # ` S ) ) ) ) ) : ( 0 ..^ ( ( # ` S ) + ( # ` T ) ) ) --> B -> ( x e. ( 0 ..^ ( ( # ` S ) + ( # ` T ) ) ) |-> if ( x e. ( 0 ..^ ( # ` S ) ) , ( S ` x ) , ( T ` ( x - ( # ` S ) ) ) ) ) e. Word B )
21 19 20 syl 
 |-  ( ( S e. Word B /\ T e. Word B ) -> ( x e. ( 0 ..^ ( ( # ` S ) + ( # ` T ) ) ) |-> if ( x e. ( 0 ..^ ( # ` S ) ) , ( S ` x ) , ( T ` ( x - ( # ` S ) ) ) ) ) e. Word B )
22 1 21 eqeltrd 
 |-  ( ( S e. Word B /\ T e. Word B ) -> ( S ++ T ) e. Word B )