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 = (r \in V, s \in V ⟼ ⋃_{f \in {Monic}_{1p} (r ↾_{𝑠} s)} {(r {evalSub}_{1} s) (f)}^{-1} [\{0_{r}\}])$

Detailed syntax breakdown

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

Metamath Proof Explorer

Definition df-irng

Detailed syntax breakdown