This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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