Definition df-irng

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

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cirng	⊢ IntgRing
1		vr	⊢ 𝑟
2		cvv	⊢ V
3		vs	⊢ 𝑠
4		vf	⊢ 𝑓
5		cmn1	⊢ Monic1p
6	1	cv	⊢ 𝑟
7		cress	⊢ ↾s
8	3	cv	⊢ 𝑠
9	6 8 7	co	⊢ ( 𝑟 ↾s 𝑠 )
10	9 5	cfv	⊢ ( Monic1p ‘ ( 𝑟 ↾s 𝑠 ) )
11		ces1	⊢ evalSub1
12	6 8 11	co	⊢ ( 𝑟 evalSub1 𝑠 )
13	4	cv	⊢ 𝑓
14	13 12	cfv	⊢ ( ( 𝑟 evalSub1 𝑠 ) ‘ 𝑓 )
15	14	ccnv	⊢ ◡ ( ( 𝑟 evalSub1 𝑠 ) ‘ 𝑓 )
16		c0g	⊢ 0g
17	6 16	cfv	⊢ ( 0g ‘ 𝑟 )
18	17	csn	⊢ { ( 0g ‘ 𝑟 ) }
19	15 18	cima	⊢ ( ◡ ( ( 𝑟 evalSub1 𝑠 ) ‘ 𝑓 ) “ { ( 0g ‘ 𝑟 ) } )
20	4 10 19	ciun	⊢ ∪ 𝑓 ∈ ( Monic1p ‘ ( 𝑟 ↾s 𝑠 ) ) ( ◡ ( ( 𝑟 evalSub1 𝑠 ) ‘ 𝑓 ) “ { ( 0g ‘ 𝑟 ) } )
21	1 3 2 2 20	cmpo	⊢ ( 𝑟 ∈ V , 𝑠 ∈ V ↦ ∪ 𝑓 ∈ ( Monic1p ‘ ( 𝑟 ↾s 𝑠 ) ) ( ◡ ( ( 𝑟 evalSub1 𝑠 ) ‘ 𝑓 ) “ { ( 0g ‘ 𝑟 ) } ) )
22	0 21	wceq	⊢ IntgRing = ( 𝑟 ∈ V , 𝑠 ∈ V ↦ ∪ 𝑓 ∈ ( Monic1p ‘ ( 𝑟 ↾s 𝑠 ) ) ( ◡ ( ( 𝑟 evalSub1 𝑠 ) ‘ 𝑓 ) “ { ( 0g ‘ 𝑟 ) } ) )