Definition df-irng

Description: Define the subring of elements of r integral over s in a ring. (Contributed by Mario Carneiro, 2-Dec-2014)

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		citr	⊢ 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	4	cv	⊢ 𝑓
12	11	ccnv	⊢ ◡ 𝑓
13		c0g	⊢ 0g
14	6 13	cfv	⊢ ( 0g ‘ 𝑟 )
15	14	csn	⊢ { ( 0g ‘ 𝑟 ) }
16	12 15	cima	⊢ ( ◡ 𝑓 “ { ( 0g ‘ 𝑟 ) } )
17	4 10 16	ciun	⊢ ∪ 𝑓 ∈ ( Monic1p ‘ ( 𝑟 ↾s 𝑠 ) ) ( ◡ 𝑓 “ { ( 0g ‘ 𝑟 ) } )
18	1 3 2 2 17	cmpo	⊢ ( 𝑟 ∈ V , 𝑠 ∈ V ↦ ∪ 𝑓 ∈ ( Monic1p ‘ ( 𝑟 ↾s 𝑠 ) ) ( ◡ 𝑓 “ { ( 0g ‘ 𝑟 ) } ) )
19	0 18	wceq	⊢ IntgRing = ( 𝑟 ∈ V , 𝑠 ∈ V ↦ ∪ 𝑓 ∈ ( Monic1p ‘ ( 𝑟 ↾s 𝑠 ) ) ( ◡ 𝑓 “ { ( 0g ‘ 𝑟 ) } ) )