Definition df-irng 31530

Description: Define the subring of elements of r integral over s in a ring. (Contributed by Mario Carneiro, 2-Dec-2014.)

Assertion

Ref	Expression
df-irng	|- IntgRing = ( r e. _V , s e. _V |-> U_ f e. (Monic1p ` ( r ↾s s ) ) ( `' f " { ( 0g ` r ) } ) )

Distinct variable group:   f, r, s

Detailed syntax breakdown of Definition df-irng

Step	Hyp	Ref	Expression
1		citr 31522	. 2 class IntgRing
2		vr	. . 3 setvar r
3		vs	. . 3 setvar s
4		cvv 3200	. . 3 class _V
5		vf	. . . 4 setvar f
6	2	cv 1482	. . . . . 6 class r
7	3	cv 1482	. . . . . 6 class s
8		cress 15858	. . . . . 6 class ↾s
9	6, 7, 8	co 6650	. . . . 5 class ( r ↾s s )
10		cmn1 23885	. . . . 5 class Monic1p
11	9, 10	cfv 5888	. . . 4 class (Monic1p ` ( r ↾s s ) )
12	5	cv 1482	. . . . . 6 class f
13	12	ccnv 5113	. . . . 5 class `' f
14		c0g 16100	. . . . . . 7 class 0g
15	6, 14	cfv 5888	. . . . . 6 class ( 0g ` r )
16	15	csn 4177	. . . . 5 class { ( 0g ` r ) }
17	13, 16	cima 5117	. . . 4 class ( `' f " { ( 0g ` r ) } )
18	5, 11, 17	ciun 4520	. . 3 class U_ f e. (Monic1p ` ( r ↾s s ) ) ( `' f " { ( 0g ` r ) } )
19	2, 3, 4, 4, 18	cmpt2 6652	. 2 class ( r e. _V , s e. _V |-> U_ f e. (Monic1p ` ( r ↾s s ) ) ( `' f " { ( 0g ` r ) } ) )
20	1, 19	wceq 1483	1 wff IntgRing = ( r e. _V , s e. _V |-> U_ f e. (Monic1p ` ( r ↾s s ) ) ( `' f " { ( 0g ` r ) } ) )

This definition is referenced by: (None)