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∈V,t∈V⟼x∈0..^s+t⟼ifx∈0..^ss⁡xt⁡x−s

Detailed syntax breakdown

Step Hyp Ref Expression
0 cconcat class++
1 vs setvars
2 cvv classV
3 vt setvart
4 vx setvarx
5 cc0 class0
6 cfzo class..^
7 chash class.
8 1 cv setvars
9 8 7 cfv classs
10 caddc class+
11 3 cv setvart
12 11 7 cfv classt
13 9 12 10 co classs+t
14 5 13 6 co class0..^s+t
15 4 cv setvarx
16 5 9 6 co class0..^s
17 15 16 wcel wffx∈0..^s
18 15 8 cfv classs⁡x
19 cmin class−
20 15 9 19 co classx−s
21 20 11 cfv classt⁡x−s
22 17 18 21 cif classifx∈0..^ss⁡xt⁡x−s
23 4 14 22 cmpt classx∈0..^s+t⟼ifx∈0..^ss⁡xt⁡x−s
24 1 3 2 2 23 cmpo classs∈V,t∈V⟼x∈0..^s+t⟼ifx∈0..^ss⁡xt⁡x−s
25 0 24 wceq wff++=s∈V,t∈V⟼x∈0..^s+t⟼ifx∈0..^ss⁡xt⁡x−s