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

Metamath Proof Explorer

Definition df-substr

Description: Define an operation which extracts portions (calledsubwords or substrings) of words. Definition in Section 9.1 of AhoHopUll p. 318. (Contributed by Stefan O'Rear, 15-Aug-2015)

Ref Expression
Assertion df-substr substr = ( 𝑠 ∈ V , 𝑏 ∈ ( ℤ × ℤ ) ↦ if ( ( ( 1st ‘ 𝑏 ) ..^ ( 2nd ‘ 𝑏 ) ) ⊆ dom 𝑠 , ( 𝑥 ∈ ( 0 ..^ ( ( 2nd ‘ 𝑏 ) − ( 1st ‘ 𝑏 ) ) ) ↦ ( 𝑠 ‘ ( 𝑥 + ( 1st ‘ 𝑏 ) ) ) ) , ∅ ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 csubstr ⊢ substr
1 vs ⊢ 𝑠
2 cvv ⊢ V
3 vb ⊢ 𝑏
4 cz ⊢ ℤ
5 4 4 cxp ⊢ ( ℤ × ℤ )
6 c1st ⊢ 1st
7 3 cv ⊢ 𝑏
8 7 6 cfv ⊢ ( 1st ‘ 𝑏 )
9 cfzo ⊢ ..^
10 c2nd ⊢ 2nd
11 7 10 cfv ⊢ ( 2nd ‘ 𝑏 )
12 8 11 9 co ⊢ ( ( 1st ‘ 𝑏 ) ..^ ( 2nd ‘ 𝑏 ) )
13 1 cv ⊢ 𝑠
14 13 cdm ⊢ dom 𝑠
15 12 14 wss ⊢ ( ( 1st ‘ 𝑏 ) ..^ ( 2nd ‘ 𝑏 ) ) ⊆ dom 𝑠
16 vx ⊢ 𝑥
17 cc0 ⊢ 0
18 cmin ⊢ −
19 11 8 18 co ⊢ ( ( 2nd ‘ 𝑏 ) − ( 1st ‘ 𝑏 ) )
20 17 19 9 co ⊢ ( 0 ..^ ( ( 2nd ‘ 𝑏 ) − ( 1st ‘ 𝑏 ) ) )
21 16 cv ⊢ 𝑥
22 caddc ⊢ +
23 21 8 22 co ⊢ ( 𝑥 + ( 1st ‘ 𝑏 ) )
24 23 13 cfv ⊢ ( 𝑠 ‘ ( 𝑥 + ( 1st ‘ 𝑏 ) ) )
25 16 20 24 cmpt ⊢ ( 𝑥 ∈ ( 0 ..^ ( ( 2nd ‘ 𝑏 ) − ( 1st ‘ 𝑏 ) ) ) ↦ ( 𝑠 ‘ ( 𝑥 + ( 1st ‘ 𝑏 ) ) ) )
26 c0 ⊢ ∅
27 15 25 26 cif ⊢ if ( ( ( 1st ‘ 𝑏 ) ..^ ( 2nd ‘ 𝑏 ) ) ⊆ dom 𝑠 , ( 𝑥 ∈ ( 0 ..^ ( ( 2nd ‘ 𝑏 ) − ( 1st ‘ 𝑏 ) ) ) ↦ ( 𝑠 ‘ ( 𝑥 + ( 1st ‘ 𝑏 ) ) ) ) , ∅ )
28 1 3 2 5 27 cmpo ⊢ ( 𝑠 ∈ V , 𝑏 ∈ ( ℤ × ℤ ) ↦ if ( ( ( 1st ‘ 𝑏 ) ..^ ( 2nd ‘ 𝑏 ) ) ⊆ dom 𝑠 , ( 𝑥 ∈ ( 0 ..^ ( ( 2nd ‘ 𝑏 ) − ( 1st ‘ 𝑏 ) ) ) ↦ ( 𝑠 ‘ ( 𝑥 + ( 1st ‘ 𝑏 ) ) ) ) , ∅ ) )
29 0 28 wceq ⊢ substr = ( 𝑠 ∈ V , 𝑏 ∈ ( ℤ × ℤ ) ↦ if ( ( ( 1st ‘ 𝑏 ) ..^ ( 2nd ‘ 𝑏 ) ) ⊆ dom 𝑠 , ( 𝑥 ∈ ( 0 ..^ ( ( 2nd ‘ 𝑏 ) − ( 1st ‘ 𝑏 ) ) ) ↦ ( 𝑠 ‘ ( 𝑥 + ( 1st ‘ 𝑏 ) ) ) ) , ∅ ) )