Metamath Proof Explorer

Definition df-concat

Description: Define the concatenation operator which combines two words. Definition in Section 9.1 of AhoHopUll p. 318. (Contributed by FL, 14-Jan-2014) (Revised by Stefan O'Rear, 15-Aug-2015)

Ref Expression
Assertion df-concat 
|- ++ = ( s e. _V , t e. _V |-> ( x e. ( 0 ..^ ( ( # ` s ) + ( # ` t ) ) ) |-> if ( x e. ( 0 ..^ ( # ` s ) ) , ( s ` x ) , ( t ` ( x - ( # ` s ) ) ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cconcat 
 |-  ++
1 vs 
 |-  s
2 cvv 
 |-  _V
3 vt 
 |-  t
4 vx 
 |-  x
5 cc0 
 |-  0
6 cfzo 
 |-  ..^
7 chash 
 |-  #
8 1 cv 
 |-  s
9 8 7 cfv 
 |-  ( # ` s )
10 caddc 
 |-  +
11 3 cv 
 |-  t
12 11 7 cfv 
 |-  ( # ` t )
13 9 12 10 co 
 |-  ( ( # ` s ) + ( # ` t ) )
14 5 13 6 co 
 |-  ( 0 ..^ ( ( # ` s ) + ( # ` t ) ) )
15 4 cv 
 |-  x
16 5 9 6 co 
 |-  ( 0 ..^ ( # ` s ) )
17 15 16 wcel 
 |-  x e. ( 0 ..^ ( # ` s ) )
18 15 8 cfv 
 |-  ( s ` x )
19 cmin 
 |-  -
20 15 9 19 co 
 |-  ( x - ( # ` s ) )
21 20 11 cfv 
 |-  ( t ` ( x - ( # ` s ) ) )
22 17 18 21 cif 
 |-  if ( x e. ( 0 ..^ ( # ` s ) ) , ( s ` x ) , ( t ` ( x - ( # ` s ) ) ) )
23 4 14 22 cmpt 
 |-  ( x e. ( 0 ..^ ( ( # ` s ) + ( # ` t ) ) ) |-> if ( x e. ( 0 ..^ ( # ` s ) ) , ( s ` x ) , ( t ` ( x - ( # ` s ) ) ) ) )
24 1 3 2 2 23 cmpo 
 |-  ( s e. _V , t e. _V |-> ( x e. ( 0 ..^ ( ( # ` s ) + ( # ` t ) ) ) |-> if ( x e. ( 0 ..^ ( # ` s ) ) , ( s ` x ) , ( t ` ( x - ( # ` s ) ) ) ) ) )
25 0 24 wceq 
 |-  ++ = ( s e. _V , t e. _V |-> ( x e. ( 0 ..^ ( ( # ` s ) + ( # ` t ) ) ) |-> if ( x e. ( 0 ..^ ( # ` s ) ) , ( s ` x ) , ( t ` ( x - ( # ` s ) ) ) ) ) )