Definition df-substr 13303

Description: Define an operation which extracts portions 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 = ( s e. _V , b e. ( ZZ X. ZZ ) |-> if ( ( ( 1st ` b )..^ ( 2nd ` b ) ) C_ dom s , ( x e. ( 0..^ ( ( 2nd ` b ) - ( 1st ` b ) ) ) |-> ( s ` ( x + ( 1st ` b ) ) ) ) , (/) ) )

Distinct variable group:   s, b, x

Detailed syntax breakdown of Definition df-substr

Step	Hyp	Ref	Expression
1		csubstr 13295	. 2 class substr
2		vs	. . 3 setvar s
3		vb	. . 3 setvar b
4		cvv 3200	. . 3 class _V
5		cz 11377	. . . 4 class ZZ
6	5, 5	cxp 5112	. . 3 class ( ZZ X. ZZ )
7	3	cv 1482	. . . . . . 7 class b
8		c1st 7166	. . . . . . 7 class 1st
9	7, 8	cfv 5888	. . . . . 6 class ( 1st ` b )
10		c2nd 7167	. . . . . . 7 class 2nd
11	7, 10	cfv 5888	. . . . . 6 class ( 2nd ` b )
12		cfzo 12465	. . . . . 6 class ..^
13	9, 11, 12	co 6650	. . . . 5 class ( ( 1st ` b )..^ ( 2nd ` b ) )
14	2	cv 1482	. . . . . 6 class s
15	14	cdm 5114	. . . . 5 class dom s
16	13, 15	wss 3574	. . . 4 wff ( ( 1st ` b )..^ ( 2nd ` b ) ) C_ dom s
17		vx	. . . . 5 setvar x
18		cc0 9936	. . . . . 6 class 0
19		cmin 10266	. . . . . . 7 class -
20	11, 9, 19	co 6650	. . . . . 6 class ( ( 2nd ` b ) - ( 1st ` b ) )
21	18, 20, 12	co 6650	. . . . 5 class ( 0..^ ( ( 2nd ` b ) - ( 1st ` b ) ) )
22	17	cv 1482	. . . . . . 7 class x
23		caddc 9939	. . . . . . 7 class +
24	22, 9, 23	co 6650	. . . . . 6 class ( x + ( 1st ` b ) )
25	24, 14	cfv 5888	. . . . 5 class ( s ` ( x + ( 1st ` b ) ) )
26	17, 21, 25	cmpt 4729	. . . 4 class ( x e. ( 0..^ ( ( 2nd ` b ) - ( 1st ` b ) ) ) |-> ( s ` ( x + ( 1st ` b ) ) ) )
27		c0 3915	. . . 4 class (/)
28	16, 26, 27	cif 4086	. . 3 class if ( ( ( 1st ` b )..^ ( 2nd ` b ) ) C_ dom s , ( x e. ( 0..^ ( ( 2nd ` b ) - ( 1st ` b ) ) ) |-> ( s ` ( x + ( 1st ` b ) ) ) ) , (/) )
29	2, 3, 4, 6, 28	cmpt2 6652	. 2 class ( s e. _V , b e. ( ZZ X. ZZ ) |-> if ( ( ( 1st ` b )..^ ( 2nd ` b ) ) C_ dom s , ( x e. ( 0..^ ( ( 2nd ` b ) - ( 1st ` b ) ) ) |-> ( s ` ( x + ( 1st ` b ) ) ) ) , (/) ) )
30	1, 29	wceq 1483	1 wff substr = ( s e. _V , b e. ( ZZ X. ZZ ) |-> if ( ( ( 1st ` b )..^ ( 2nd ` b ) ) C_ dom s , ( x e. ( 0..^ ( ( 2nd ` b ) - ( 1st ` b ) ) ) |-> ( s ` ( x + ( 1st ` b ) ) ) ) , (/) ) )

This definition is referenced by:  swrdval  13417  swrd00  13418  swrdcl  13419  swrd0  13434