Definition df-concat 11022

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

Assertion

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

Distinct variable group:   t, s, x

Detailed syntax breakdown of Definition df-concat

Step	Hyp	Ref	Expression
1		cconcat 11021	. 2 class ++
2		vs	. . 3 setvar s
3		vt	. . 3 setvar t
4		cvv 2771	. . 3 class _V
5		vx	. . . 4 setvar x
6		cc0 7907	. . . . 5 class 0
7	2	cv 1371	. . . . . . 7 class s
8		chash 10901	. . . . . . 7 class ♯
9	7, 8	cfv 5268	. . . . . 6 class (♯ ` s )
10	3	cv 1371	. . . . . . 7 class t
11	10, 8	cfv 5268	. . . . . 6 class (♯ ` t )
12		caddc 7910	. . . . . 6 class +
13	9, 11, 12	co 5934	. . . . 5 class ( (♯ ` s ) + (♯ ` t ) )
14		cfzo 10246	. . . . 5 class ..^
15	6, 13, 14	co 5934	. . . 4 class ( 0..^ ( (♯ ` s ) + (♯ ` t ) ) )
16	5	cv 1371	. . . . . 6 class x
17	6, 9, 14	co 5934	. . . . . 6 class ( 0..^ (♯ ` s ) )
18	16, 17	wcel 2175	. . . . 5 wff x e. ( 0..^ (♯ ` s ) )
19	16, 7	cfv 5268	. . . . 5 class ( s ` x )
20		cmin 8225	. . . . . . 7 class -
21	16, 9, 20	co 5934	. . . . . 6 class ( x - (♯ ` s ) )
22	21, 10	cfv 5268	. . . . 5 class ( t ` ( x - (♯ ` s ) ) )
23	18, 19, 22	cif 3570	. . . 4 class if ( x e. ( 0..^ (♯ ` s ) ) , ( s ` x ) , ( t ` ( x - (♯ ` s ) ) ) )
24	5, 15, 23	cmpt 4104	. . 3 class ( x e. ( 0..^ ( (♯ ` s ) + (♯ ` t ) ) ) |-> if ( x e. ( 0..^ (♯ ` s ) ) , ( s ` x ) , ( t ` ( x - (♯ ` s ) ) ) ) )
25	2, 3, 4, 4, 24	cmpo 5936	. 2 class ( s e. _V , t e. _V |-> ( x e. ( 0..^ ( (♯ ` s ) + (♯ ` t ) ) ) |-> if ( x e. ( 0..^ (♯ ` s ) ) , ( s ` x ) , ( t ` ( x - (♯ ` s ) ) ) ) ) )
26	1, 25	wceq 1372	1 wff ++ = ( s e. _V , t e. _V |-> ( x e. ( 0..^ ( (♯ ` s ) + (♯ ` t ) ) ) |-> if ( x e. ( 0..^ (♯ ` s ) ) , ( s ` x ) , ( t ` ( x - (♯ ` s ) ) ) ) ) )

This definition is referenced by:  ccatfvalfi  11023