Definition df-irng

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

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		citr	|- IntgRing
1		vr	|- r
2		cvv	|- _V
3		vs	|- s
4		vf	|- f
5		cmn1	|- Monic1p
6	1	cv	|- r
7		cress	|- |`s
8	3	cv	|- s
9	6 8 7	co	|- ( r |`s s )
10	9 5	cfv	|- ( Monic1p ` ( r |`s s ) )
11	4	cv	|- f
12	11	ccnv	|- `' f
13		c0g	|- 0g
14	6 13	cfv	|- ( 0g ` r )
15	14	csn	|- { ( 0g ` r ) }
16	12 15	cima	|- ( `' f " { ( 0g ` r ) } )
17	4 10 16	ciun	|- U_ f e. ( Monic1p ` ( r |`s s ) ) ( `' f " { ( 0g ` r ) } )
18	1 3 2 2 17	cmpo	|- ( r e. _V , s e. _V |-> U_ f e. ( Monic1p ` ( r |`s s ) ) ( `' f " { ( 0g ` r ) } ) )
19	0 18	wceq	|- IntgRing = ( r e. _V , s e. _V |-> U_ f e. ( Monic1p ` ( r |`s s ) ) ( `' f " { ( 0g ` r ) } ) )