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

Definition df-substr 13993
Description: Define an operation which extracts portions (called subwords or substrings) of words. Definition in Section 9.1 of [AhoHopUll] p. 318. (Contributed by Stefan O'Rear, 15-Aug-2015.)
Assertion
Ref Expression
df-substr substr = (𝑠 ∈ V, 𝑏 ∈ (ℤ × ℤ) ↦ if(((1st𝑏)..^(2nd𝑏)) ⊆ dom 𝑠, (𝑥 ∈ (0..^((2nd𝑏) − (1st𝑏))) ↦ (𝑠‘(𝑥 + (1st𝑏)))), ∅))
Distinct variable group:   𝑠,𝑏,𝑥

Detailed syntax breakdown of Definition df-substr
StepHypRef Expression
1 csubstr 13992 . 2 class substr
2 vs . . 3 setvar 𝑠
3 vb . . 3 setvar 𝑏
4 cvv 3495 . . 3 class V
5 cz 11970 . . . 4 class
65, 5cxp 5547 . . 3 class (ℤ × ℤ)
73cv 1527 . . . . . . 7 class 𝑏
8 c1st 7678 . . . . . . 7 class 1st
97, 8cfv 6349 . . . . . 6 class (1st𝑏)
10 c2nd 7679 . . . . . . 7 class 2nd
117, 10cfv 6349 . . . . . 6 class (2nd𝑏)
12 cfzo 13023 . . . . . 6 class ..^
139, 11, 12co 7145 . . . . 5 class ((1st𝑏)..^(2nd𝑏))
142cv 1527 . . . . . 6 class 𝑠
1514cdm 5549 . . . . 5 class dom 𝑠
1613, 15wss 3935 . . . 4 wff ((1st𝑏)..^(2nd𝑏)) ⊆ dom 𝑠
17 vx . . . . 5 setvar 𝑥
18 cc0 10526 . . . . . 6 class 0
19 cmin 10859 . . . . . . 7 class
2011, 9, 19co 7145 . . . . . 6 class ((2nd𝑏) − (1st𝑏))
2118, 20, 12co 7145 . . . . 5 class (0..^((2nd𝑏) − (1st𝑏)))
2217cv 1527 . . . . . . 7 class 𝑥
23 caddc 10529 . . . . . . 7 class +
2422, 9, 23co 7145 . . . . . 6 class (𝑥 + (1st𝑏))
2524, 14cfv 6349 . . . . 5 class (𝑠‘(𝑥 + (1st𝑏)))
2617, 21, 25cmpt 5138 . . . 4 class (𝑥 ∈ (0..^((2nd𝑏) − (1st𝑏))) ↦ (𝑠‘(𝑥 + (1st𝑏))))
27 c0 4290 . . . 4 class
2816, 26, 27cif 4465 . . 3 class if(((1st𝑏)..^(2nd𝑏)) ⊆ dom 𝑠, (𝑥 ∈ (0..^((2nd𝑏) − (1st𝑏))) ↦ (𝑠‘(𝑥 + (1st𝑏)))), ∅)
292, 3, 4, 6, 28cmpo 7147 . 2 class (𝑠 ∈ V, 𝑏 ∈ (ℤ × ℤ) ↦ if(((1st𝑏)..^(2nd𝑏)) ⊆ dom 𝑠, (𝑥 ∈ (0..^((2nd𝑏) − (1st𝑏))) ↦ (𝑠‘(𝑥 + (1st𝑏)))), ∅))
301, 29wceq 1528 1 wff substr = (𝑠 ∈ V, 𝑏 ∈ (ℤ × ℤ) ↦ if(((1st𝑏)..^(2nd𝑏)) ⊆ dom 𝑠, (𝑥 ∈ (0..^((2nd𝑏) − (1st𝑏))) ↦ (𝑠‘(𝑥 + (1st𝑏)))), ∅))
Colors of variables: wff setvar class
This definition is referenced by:  swrdnznd  13994  swrdval  13995  swrd00  13996  swrdcl  13997  swrd0  14010
  Copyright terms: Public domain W3C validator