MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-concat Structured version   Visualization version   GIF version

Definition df-concat 13458
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 ++ = (𝑠 ∈ V, 𝑡 ∈ V ↦ (𝑥 ∈ (0..^((♯‘𝑠) + (♯‘𝑡))) ↦ if(𝑥 ∈ (0..^(♯‘𝑠)), (𝑠𝑥), (𝑡‘(𝑥 − (♯‘𝑠))))))
Distinct variable group:   𝑡,𝑠,𝑥

Detailed syntax breakdown of Definition df-concat
StepHypRef Expression
1 cconcat 13450 . 2 class ++
2 vs . . 3 setvar 𝑠
3 vt . . 3 setvar 𝑡
4 cvv 3328 . . 3 class V
5 vx . . . 4 setvar 𝑥
6 cc0 10099 . . . . 5 class 0
72cv 1619 . . . . . . 7 class 𝑠
8 chash 13282 . . . . . . 7 class
97, 8cfv 6037 . . . . . 6 class (♯‘𝑠)
103cv 1619 . . . . . . 7 class 𝑡
1110, 8cfv 6037 . . . . . 6 class (♯‘𝑡)
12 caddc 10102 . . . . . 6 class +
139, 11, 12co 6801 . . . . 5 class ((♯‘𝑠) + (♯‘𝑡))
14 cfzo 12630 . . . . 5 class ..^
156, 13, 14co 6801 . . . 4 class (0..^((♯‘𝑠) + (♯‘𝑡)))
165cv 1619 . . . . . 6 class 𝑥
176, 9, 14co 6801 . . . . . 6 class (0..^(♯‘𝑠))
1816, 17wcel 2127 . . . . 5 wff 𝑥 ∈ (0..^(♯‘𝑠))
1916, 7cfv 6037 . . . . 5 class (𝑠𝑥)
20 cmin 10429 . . . . . . 7 class
2116, 9, 20co 6801 . . . . . 6 class (𝑥 − (♯‘𝑠))
2221, 10cfv 6037 . . . . 5 class (𝑡‘(𝑥 − (♯‘𝑠)))
2318, 19, 22cif 4218 . . . 4 class if(𝑥 ∈ (0..^(♯‘𝑠)), (𝑠𝑥), (𝑡‘(𝑥 − (♯‘𝑠))))
245, 15, 23cmpt 4869 . . 3 class (𝑥 ∈ (0..^((♯‘𝑠) + (♯‘𝑡))) ↦ if(𝑥 ∈ (0..^(♯‘𝑠)), (𝑠𝑥), (𝑡‘(𝑥 − (♯‘𝑠)))))
252, 3, 4, 4, 24cmpt2 6803 . 2 class (𝑠 ∈ V, 𝑡 ∈ V ↦ (𝑥 ∈ (0..^((♯‘𝑠) + (♯‘𝑡))) ↦ if(𝑥 ∈ (0..^(♯‘𝑠)), (𝑠𝑥), (𝑡‘(𝑥 − (♯‘𝑠))))))
261, 25wceq 1620 1 wff ++ = (𝑠 ∈ V, 𝑡 ∈ V ↦ (𝑥 ∈ (0..^((♯‘𝑠) + (♯‘𝑡))) ↦ if(𝑥 ∈ (0..^(♯‘𝑠)), (𝑠𝑥), (𝑡‘(𝑥 − (♯‘𝑠))))))
Colors of variables: wff setvar class
This definition is referenced by:  ccatfn  13515  ccatfval  13516
  Copyright terms: Public domain W3C validator