Definition df-irng 32901

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

Assertion

Ref	Expression
df-irng	⊢ IntgRing = (𝑟 ∈ V, 𝑠 ∈ V ↦ ∪ 𝑓 ∈ (Monic1p‘(𝑟 ↾s 𝑠))(◡𝑓 “ {(0g‘𝑟)}))

Distinct variable group:   𝑓,𝑟,𝑠

Detailed syntax breakdown of Definition df-irng

Step	Hyp	Ref	Expression
1		citr 32893	. 2 class IntgRing
2		vr	. . 3 setvar 𝑟
3		vs	. . 3 setvar 𝑠
4		cvv 3491	. . 3 class V
5		vf	. . . 4 setvar 𝑓
6	2	cv 1535	. . . . . 6 class 𝑟
7	3	cv 1535	. . . . . 6 class 𝑠
8		cress 16477	. . . . . 6 class ↾s
9	6, 7, 8	co 7149	. . . . 5 class (𝑟 ↾s 𝑠)
10		cmn1 24715	. . . . 5 class Monic1p
11	9, 10	cfv 6348	. . . 4 class (Monic1p‘(𝑟 ↾s 𝑠))
12	5	cv 1535	. . . . . 6 class 𝑓
13	12	ccnv 5547	. . . . 5 class ◡𝑓
14		c0g 16706	. . . . . . 7 class 0g
15	6, 14	cfv 6348	. . . . . 6 class (0g‘𝑟)
16	15	csn 4560	. . . . 5 class {(0g‘𝑟)}
17	13, 16	cima 5551	. . . 4 class (◡𝑓 “ {(0g‘𝑟)})
18	5, 11, 17	ciun 4912	. . 3 class ∪ 𝑓 ∈ (Monic1p‘(𝑟 ↾s 𝑠))(◡𝑓 “ {(0g‘𝑟)})
19	2, 3, 4, 4, 18	cmpo 7151	. 2 class (𝑟 ∈ V, 𝑠 ∈ V ↦ ∪ 𝑓 ∈ (Monic1p‘(𝑟 ↾s 𝑠))(◡𝑓 “ {(0g‘𝑟)}))
20	1, 19	wceq 1536	1 wff IntgRing = (𝑟 ∈ V, 𝑠 ∈ V ↦ ∪ 𝑓 ∈ (Monic1p‘(𝑟 ↾s 𝑠))(◡𝑓 “ {(0g‘𝑟)}))

This definition is referenced by: (None)