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	⊢ ++ = ( 𝑠 ∈ V , 𝑡 ∈ V ↦ ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑠 ) + ( ♯ ‘ 𝑡 ) ) ) ↦ if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑠 ) ) , ( 𝑠 ‘ 𝑥 ) , ( 𝑡 ‘ ( 𝑥 − ( ♯ ‘ 𝑠 ) ) ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cconcat	⊢ ++
1		vs	⊢ 𝑠
2		cvv	⊢ V
3		vt	⊢ 𝑡
4		vx	⊢ 𝑥
5		cc0	⊢ 0
6		cfzo	⊢ ..^
7		chash	⊢ ♯
8	1	cv	⊢ 𝑠
9	8 7	cfv	⊢ ( ♯ ‘ 𝑠 )
10		caddc	⊢ +
11	3	cv	⊢ 𝑡
12	11 7	cfv	⊢ ( ♯ ‘ 𝑡 )
13	9 12 10	co	⊢ ( ( ♯ ‘ 𝑠 ) + ( ♯ ‘ 𝑡 ) )
14	5 13 6	co	⊢ ( 0 ..^ ( ( ♯ ‘ 𝑠 ) + ( ♯ ‘ 𝑡 ) ) )
15	4	cv	⊢ 𝑥
16	5 9 6	co	⊢ ( 0 ..^ ( ♯ ‘ 𝑠 ) )
17	15 16	wcel	⊢ 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑠 ) )
18	15 8	cfv	⊢ ( 𝑠 ‘ 𝑥 )
19		cmin	⊢ −
20	15 9 19	co	⊢ ( 𝑥 − ( ♯ ‘ 𝑠 ) )
21	20 11	cfv	⊢ ( 𝑡 ‘ ( 𝑥 − ( ♯ ‘ 𝑠 ) ) )
22	17 18 21	cif	⊢ if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑠 ) ) , ( 𝑠 ‘ 𝑥 ) , ( 𝑡 ‘ ( 𝑥 − ( ♯ ‘ 𝑠 ) ) ) )
23	4 14 22	cmpt	⊢ ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑠 ) + ( ♯ ‘ 𝑡 ) ) ) ↦ if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑠 ) ) , ( 𝑠 ‘ 𝑥 ) , ( 𝑡 ‘ ( 𝑥 − ( ♯ ‘ 𝑠 ) ) ) ) )
24	1 3 2 2 23	cmpo	⊢ ( 𝑠 ∈ V , 𝑡 ∈ V ↦ ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑠 ) + ( ♯ ‘ 𝑡 ) ) ) ↦ if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑠 ) ) , ( 𝑠 ‘ 𝑥 ) , ( 𝑡 ‘ ( 𝑥 − ( ♯ ‘ 𝑠 ) ) ) ) ) )
25	0 24	wceq	⊢ ++ = ( 𝑠 ∈ V , 𝑡 ∈ V ↦ ( 𝑥 ∈ ( 0 ..^ ( ( ♯ ‘ 𝑠 ) + ( ♯ ‘ 𝑡 ) ) ) ↦ if ( 𝑥 ∈ ( 0 ..^ ( ♯ ‘ 𝑠 ) ) , ( 𝑠 ‘ 𝑥 ) , ( 𝑡 ‘ ( 𝑥 − ( ♯ ‘ 𝑠 ) ) ) ) ) )