Theorem irngval

Description: The elements of a field R integral over a subset S . In the case of a subfield, those are the algebraic numbers over the field S within the field R . That is, the numbers X which are roots of monic polynomials P ( X ) with coefficients in S . (Contributed by Thierry Arnoux, 28-Jan-2025)

	Ref	Expression
Hypotheses	irngval.o	$$⊢O=R{\mathrm{evalSub}}_{1}S$$
	irngval.u	$$⊢U=R{\upharpoonright }_{𝑠}S$$
	irngval.b	$$⊢B={\mathrm{Base}}_R$$
	irngval.0	$$⊢\underset{\dot{}}{0}=0_R$$
	irngval.r	$$⊢\phi \to R\in \mathrm{Ring}$$
	irngval.s	$$⊢\phi \to S\subseteq B$$
Assertion	irngval	$$⊢\phi \to R\mathrm{IntgRing}S=\bigcup _{f\in {Monic}_{\mathrm{1p}}\left(U\right)}{O\left(f\right)}^{-1}\left[\left\{\underset{\dot{}}{0}\right\}\right]$$

Proof

Step	Hyp	Ref	Expression
1		irngval.o	$$⊢O=R{\mathrm{evalSub}}_{1}S$$
2		irngval.u	$$⊢U=R{\upharpoonright }_{𝑠}S$$
3		irngval.b	$$⊢B={\mathrm{Base}}_R$$
4		irngval.0	$$⊢\underset{\dot{}}{0}=0_R$$
5		irngval.r	$$⊢\phi \to R\in \mathrm{Ring}$$
6		irngval.s	$$⊢\phi \to S\subseteq B$$
7	5	elexd	$$⊢\phi \to R\in \mathrm{V}$$
8	3	fvexi	$$⊢B\in \mathrm{V}$$
9	8	a1i	$$⊢\phi \to B\in \mathrm{V}$$
10	9 6	ssexd	$$⊢\phi \to S\in \mathrm{V}$$
11		fvexd	$$⊢\phi \to {Monic}_{\mathrm{1p}}\left(U\right)\in \mathrm{V}$$
12		fvex	$$⊢O\left(f\right)\in \mathrm{V}$$
13	12	cnvex	$$⊢{O\left(f\right)}^{-1}\in \mathrm{V}$$
14	13	imaex	$$⊢{O\left(f\right)}^{-1}\left[\left\{\underset{\dot{}}{0}\right\}\right]\in \mathrm{V}$$
15	14	rgenw	$$⊢\forall f\in {Monic}_{\mathrm{1p}}\left(U\right){O\left(f\right)}^{-1}\left[\left\{\underset{\dot{}}{0}\right\}\right]\in \mathrm{V}$$
16		iunexg	$$⊢\left({Monic}_{\mathrm{1p}}\left(U\right)\in \mathrm{V}\wedge \forall f\in {Monic}_{\mathrm{1p}}\left(U\right){O\left(f\right)}^{-1}\left[\left\{\underset{\dot{}}{0}\right\}\right]\in \mathrm{V}\right)\to \bigcup _{f\in {Monic}_{\mathrm{1p}}\left(U\right)}{O\left(f\right)}^{-1}\left[\left\{\underset{\dot{}}{0}\right\}\right]\in \mathrm{V}$$
17	11 15 16	sylancl	$$⊢\phi \to \bigcup _{f\in {Monic}_{\mathrm{1p}}\left(U\right)}{O\left(f\right)}^{-1}\left[\left\{\underset{\dot{}}{0}\right\}\right]\in \mathrm{V}$$
18		oveq12	$$⊢\left(r=R\wedge s=S\right)\to r{\upharpoonright }_{𝑠}s=R{\upharpoonright }_{𝑠}S$$
19	18 2	eqtr4di	$$⊢\left(r=R\wedge s=S\right)\to r{\upharpoonright }_{𝑠}s=U$$
20	19	fveq2d	$$⊢\left(r=R\wedge s=S\right)\to {Monic}_{\mathrm{1p}}\left(r{\upharpoonright }_{𝑠}s\right)={Monic}_{\mathrm{1p}}\left(U\right)$$
21		oveq12	$$⊢\left(r=R\wedge s=S\right)\to r{\mathrm{evalSub}}_{1}s=R{\mathrm{evalSub}}_{1}S$$
22	21 1	eqtr4di	$$⊢\left(r=R\wedge s=S\right)\to r{\mathrm{evalSub}}_{1}s=O$$
23	22	fveq1d	$$⊢\left(r=R\wedge s=S\right)\to \left(r{\mathrm{evalSub}}_{1}s\right)\left(f\right)=O\left(f\right)$$
24	23	cnveqd	$$⊢\left(r=R\wedge s=S\right)\to {\left(r{\mathrm{evalSub}}_{1}s\right)\left(f\right)}^{-1}={O\left(f\right)}^{-1}$$
25		simpl	$$⊢\left(r=R\wedge s=S\right)\to r=R$$
26	25	fveq2d	$$⊢\left(r=R\wedge s=S\right)\to 0_r=0_R$$
27	26 4	eqtr4di	$$⊢\left(r=R\wedge s=S\right)\to 0_r=\underset{\dot{}}{0}$$
28	27	sneqd	$$⊢\left(r=R\wedge s=S\right)\to \left\{0_r\right\}=\left\{\underset{\dot{}}{0}\right\}$$
29	24 28	imaeq12d	$$⊢\left(r=R\wedge s=S\right)\to {\left(r{\mathrm{evalSub}}_{1}s\right)\left(f\right)}^{-1}\left[\left\{0_r\right\}\right]={O\left(f\right)}^{-1}\left[\left\{\underset{\dot{}}{0}\right\}\right]$$
30	20 29	iuneq12d	$$⊢\left(r=R\wedge s=S\right)\to \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]=\bigcup _{f\in {Monic}_{\mathrm{1p}}\left(U\right)}{O\left(f\right)}^{-1}\left[\left\{\underset{\dot{}}{0}\right\}\right]$$
31		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)$$
32	30 31	ovmpoga	$$⊢\left(R\in \mathrm{V}\wedge S\in \mathrm{V}\wedge \bigcup _{f\in {Monic}_{\mathrm{1p}}\left(U\right)}{O\left(f\right)}^{-1}\left[\left\{\underset{\dot{}}{0}\right\}\right]\in \mathrm{V}\right)\to R\mathrm{IntgRing}S=\bigcup _{f\in {Monic}_{\mathrm{1p}}\left(U\right)}{O\left(f\right)}^{-1}\left[\left\{\underset{\dot{}}{0}\right\}\right]$$
33	7 10 17 32	syl3anc	$$⊢\phi \to R\mathrm{IntgRing}S=\bigcup _{f\in {Monic}_{\mathrm{1p}}\left(U\right)}{O\left(f\right)}^{-1}\left[\left\{\underset{\dot{}}{0}\right\}\right]$$