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	$$⊢\mathrm{IntgRing}=\left(r\in \mathrm{V},s\in \mathrm{V}⟼\bigcup _{f\in {Monic}_{\mathrm{1p}}\left(r{\upharpoonright }_{𝑠}s\right)}{\left(r{\mathrm{evalSub}}_{1}s\right)\left(f\right)}^{-1}\left[\left\{0_r\right\}\right]\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cirng	$$class\mathrm{IntgRing}$$
1		vr	$$setvarr$$
2		cvv	$$class\mathrm{V}$$
3		vs	$$setvars$$
4		vf	$$setvarf$$
5		cmn1	$$class{Monic}_{\mathrm{1p}}$$
6	1	cv	$$setvarr$$
7		cress	$$class{\upharpoonright }_{𝑠}$$
8	3	cv	$$setvars$$
9	6 8 7	co	$$class\left(r{\upharpoonright }_{𝑠}s\right)$$
10	9 5	cfv	$$class{Monic}_{\mathrm{1p}}\left(r{\upharpoonright }_{𝑠}s\right)$$
11		ces1	$$class{\mathrm{evalSub}}_1$$
12	6 8 11	co	$$class\left(r{\mathrm{evalSub}}_{1}s\right)$$
13	4	cv	$$setvarf$$
14	13 12	cfv	$$class\left(r{\mathrm{evalSub}}_{1}s\right)\left(f\right)$$
15	14	ccnv	$$class{\left(r{\mathrm{evalSub}}_{1}s\right)\left(f\right)}^{-1}$$
16		c0g	$$class{0}_{𝑔}$$
17	6 16	cfv	$$class{0}_r$$
18	17	csn	$$class\left\{0_r\right\}$$
19	15 18	cima	$$class{\left(r{\mathrm{evalSub}}_{1}s\right)\left(f\right)}^{-1}\left[\left\{0_r\right\}\right]$$
20	4 10 19	ciun	$$class\bigcup _{f\in {Monic}_{\mathrm{1p}}\left(r{\upharpoonright }_{𝑠}s\right)}{\left(r{\mathrm{evalSub}}_{1}s\right)\left(f\right)}^{-1}\left[\left\{0_r\right\}\right]$$
21	1 3 2 2 20	cmpo	$$class\left(r\in \mathrm{V},s\in \mathrm{V}⟼\bigcup _{f\in {Monic}_{\mathrm{1p}}\left(r{\upharpoonright }_{𝑠}s\right)}{\left(r{\mathrm{evalSub}}_{1}s\right)\left(f\right)}^{-1}\left[\left\{0_r\right\}\right]\right)$$
22	0 21	wceq	$$wff\mathrm{IntgRing}=\left(r\in \mathrm{V},s\in \mathrm{V}⟼\bigcup _{f\in {Monic}_{\mathrm{1p}}\left(r{\upharpoonright }_{𝑠}s\right)}{\left(r{\mathrm{evalSub}}_{1}s\right)\left(f\right)}^{-1}\left[\left\{0_r\right\}\right]\right)$$