Definition df-irng 33497

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 33489	. 2 class IntgRing
2		vr	. . 3 setvar 𝑟
3		vs	. . 3 setvar 𝑠
4		cvv 3422	. . 3 class V
5		vf	. . . 4 setvar 𝑓
6	2	cv 1538	. . . . . 6 class 𝑟
7	3	cv 1538	. . . . . 6 class 𝑠
8		cress 16867	. . . . . 6 class ↾s
9	6, 7, 8	co 7255	. . . . 5 class (𝑟 ↾s 𝑠)
10		cmn1 25195	. . . . 5 class Monic1p
11	9, 10	cfv 6418	. . . 4 class (Monic1p‘(𝑟 ↾s 𝑠))
12	5	cv 1538	. . . . . 6 class 𝑓
13	12	ccnv 5579	. . . . 5 class ◡𝑓
14		c0g 17067	. . . . . . 7 class 0g
15	6, 14	cfv 6418	. . . . . 6 class (0g‘𝑟)
16	15	csn 4558	. . . . 5 class {(0g‘𝑟)}
17	13, 16	cima 5583	. . . 4 class (◡𝑓 “ {(0g‘𝑟)})
18	5, 11, 17	ciun 4921	. . 3 class ∪ 𝑓 ∈ (Monic1p‘(𝑟 ↾s 𝑠))(◡𝑓 “ {(0g‘𝑟)})
19	2, 3, 4, 4, 18	cmpo 7257	. 2 class (𝑟 ∈ V, 𝑠 ∈ V ↦ ∪ 𝑓 ∈ (Monic1p‘(𝑟 ↾s 𝑠))(◡𝑓 “ {(0g‘𝑟)}))
20	1, 19	wceq 1539	1 wff IntgRing = (𝑟 ∈ V, 𝑠 ∈ V ↦ ∪ 𝑓 ∈ (Monic1p‘(𝑟 ↾s 𝑠))(◡𝑓 “ {(0g‘𝑟)}))

This definition is referenced by: (None)