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 ‘ 𝑏 ) ) ) ) , ∅ ) )