Definition df-irng 34363

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 34362	. 2 class IntgRing
2		vr	. . 3 setvar 𝑟
3		vs	. . 3 setvar 𝑠
4		cvv 3450	. . 3 class V
5		vf	. . . 4 setvar 𝑓
6	2	cv 1568	. . . . . 6 class 𝑟
7	3	cv 1568	. . . . . 6 class 𝑠
8		cress 17414	. . . . . 6 class ↾s
9	6, 7, 8	co 7421	. . . . 5 class (𝑟 ↾s 𝑠)
10		cmn1 26450	. . . . 5 class Monic1p
11	9, 10	cfv 6539	. . . 4 class (Monic1p‘(𝑟 ↾s 𝑠))
12	5	cv 1568	. . . . . . 7 class 𝑓
13		ces1 22637	. . . . . . . 8 class evalSub1
14	6, 7, 13	co 7421	. . . . . . 7 class (𝑟 evalSub1 𝑠)
15	12, 14	cfv 6539	. . . . . 6 class ((𝑟 evalSub1 𝑠)‘𝑓)
16	15	ccnv 5649	. . . . 5 class ◡((𝑟 evalSub1 𝑠)‘𝑓)
17		c0g 17616	. . . . . . 7 class 0g
18	6, 17	cfv 6539	. . . . . 6 class (0g‘𝑟)
19	18	csn 4584	. . . . 5 class {(0g‘𝑟)}
20	16, 19	cima 5653	. . . 4 class (◡((𝑟 evalSub1 𝑠)‘𝑓) “ {(0g‘𝑟)})
21	5, 11, 20	ciun 4950	. . 3 class ∪ 𝑓 ∈ (Monic1p‘(𝑟 ↾s 𝑠))(◡((𝑟 evalSub1 𝑠)‘𝑓) “ {(0g‘𝑟)})
22	2, 3, 4, 4, 21	cmpo 7423	. 2 class (𝑟 ∈ V, 𝑠 ∈ V ↦ ∪ 𝑓 ∈ (Monic1p‘(𝑟 ↾s 𝑠))(◡((𝑟 evalSub1 𝑠)‘𝑓) “ {(0g‘𝑟)}))
23	1, 22	wceq 1569	1 wff IntgRing = (𝑟 ∈ V, 𝑠 ∈ V ↦ ∪ 𝑓 ∈ (Monic1p‘(𝑟 ↾s 𝑠))(◡((𝑟 evalSub1 𝑠)‘𝑓) “ {(0g‘𝑟)}))

This definition is used by:  irngval  34364