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 ⟼ if x ∈ 0 ..^ s s ⁡ x t ⁡ x − s

Detailed syntax breakdown

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