Definition df-irng 33597

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 33589	. 2 class IntgRing
2		vr	. . 3 setvar 𝑟
3		vs	. . 3 setvar 𝑠
4		cvv 3432	. . 3 class V
5		vf	. . . 4 setvar 𝑓
6	2	cv 1538	. . . . . 6 class 𝑟
7	3	cv 1538	. . . . . 6 class 𝑠
8		cress 16941	. . . . . 6 class ↾s
9	6, 7, 8	co 7275	. . . . 5 class (𝑟 ↾s 𝑠)
10		cmn1 25290	. . . . 5 class Monic1p
11	9, 10	cfv 6433	. . . 4 class (Monic1p‘(𝑟 ↾s 𝑠))
12	5	cv 1538	. . . . . 6 class 𝑓
13	12	ccnv 5588	. . . . 5 class ◡𝑓
14		c0g 17150	. . . . . . 7 class 0g
15	6, 14	cfv 6433	. . . . . 6 class (0g‘𝑟)
16	15	csn 4561	. . . . 5 class {(0g‘𝑟)}
17	13, 16	cima 5592	. . . 4 class (◡𝑓 “ {(0g‘𝑟)})
18	5, 11, 17	ciun 4924	. . 3 class ∪ 𝑓 ∈ (Monic1p‘(𝑟 ↾s 𝑠))(◡𝑓 “ {(0g‘𝑟)})
19	2, 3, 4, 4, 18	cmpo 7277	. 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)