Definition df-irng 32572

Description: Define the subring of elements of a ring 𝑟 integral over a subset 𝑠. (Contributed by Mario Carneiro, 2-Dec-2014.) (Revised by Thierry Arnoux, 28-Jan-2025.)

Assertion

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

Distinct variable group:   𝑓,𝑟,𝑠

Detailed syntax breakdown of Definition df-irng

Step	Hyp	Ref	Expression
1		cirng 32571	. 2 class IntgRing
2		vr	. . 3 setvar 𝑟
3		vs	. . 3 setvar 𝑠
4		cvv 3472	. . 3 class V
5		vf	. . . 4 setvar 𝑓
6	2	cv 1540	. . . . . 6 class 𝑟
7	3	cv 1540	. . . . . 6 class 𝑠
8		cress 17154	. . . . . 6 class ↾s
9	6, 7, 8	co 7392	. . . . 5 class (𝑟 ↾s 𝑠)
10		cmn1 25569	. . . . 5 class Monic1p
11	9, 10	cfv 6531	. . . 4 class (Monic1p‘(𝑟 ↾s 𝑠))
12	5	cv 1540	. . . . . . 7 class 𝑓
13		ces1 21758	. . . . . . . 8 class evalSub1
14	6, 7, 13	co 7392	. . . . . . 7 class (𝑟 evalSub1 𝑠)
15	12, 14	cfv 6531	. . . . . 6 class ((𝑟 evalSub1 𝑠)‘𝑓)
16	15	ccnv 5667	. . . . 5 class ◡((𝑟 evalSub1 𝑠)‘𝑓)
17		c0g 17366	. . . . . . 7 class 0g
18	6, 17	cfv 6531	. . . . . 6 class (0g‘𝑟)
19	18	csn 4621	. . . . 5 class {(0g‘𝑟)}
20	16, 19	cima 5671	. . . 4 class (◡((𝑟 evalSub1 𝑠)‘𝑓) “ {(0g‘𝑟)})
21	5, 11, 20	ciun 4989	. . 3 class ∪ 𝑓 ∈ (Monic1p‘(𝑟 ↾s 𝑠))(◡((𝑟 evalSub1 𝑠)‘𝑓) “ {(0g‘𝑟)})
22	2, 3, 4, 4, 21	cmpo 7394	. 2 class (𝑟 ∈ V, 𝑠 ∈ V ↦ ∪ 𝑓 ∈ (Monic1p‘(𝑟 ↾s 𝑠))(◡((𝑟 evalSub1 𝑠)‘𝑓) “ {(0g‘𝑟)}))
23	1, 22	wceq 1541	1 wff IntgRing = (𝑟 ∈ V, 𝑠 ∈ V ↦ ∪ 𝑓 ∈ (Monic1p‘(𝑟 ↾s 𝑠))(◡((𝑟 evalSub1 𝑠)‘𝑓) “ {(0g‘𝑟)}))

This definition is referenced by:  irngval  32573