Theorem elirng

Description: Property for an element X of a field R to be integral over a subring 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$$
	elirng.r	$$⊢\phi \to R\in \mathrm{CRing}$$
	elirng.s	$$⊢\phi \to S\in \mathrm{SubRing}\left(R\right)$$
Assertion	elirng	$$⊢\phi \to \left(X\in \left(R\mathrm{IntgRing}S\right)\leftrightarrow \left(X\in B\wedge \exists f\in {Monic}_{\mathrm{1p}}\left(U\right)O\left(f\right)\left(X\right)=\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		elirng.r	$$⊢\phi \to R\in \mathrm{CRing}$$
6		elirng.s	$$⊢\phi \to S\in \mathrm{SubRing}\left(R\right)$$
7	5	crngringd	$$⊢\phi \to R\in \mathrm{Ring}$$
8	3	subrgss	$$⊢S\in \mathrm{SubRing}\left(R\right)\to S\subseteq B$$
9	6 8	syl	$$⊢\phi \to S\subseteq B$$
10	1 2 3 4 7 9	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]$$
11	10	eleq2d	$$⊢\phi \to \left(X\in \left(R\mathrm{IntgRing}S\right)\leftrightarrow X\in \bigcup _{f\in {Monic}_{\mathrm{1p}}\left(U\right)}{O\left(f\right)}^{-1}\left[\left\{\underset{\dot{}}{0}\right\}\right]\right)$$
12		eliun	$$⊢X\in \bigcup _{f\in {Monic}_{\mathrm{1p}}\left(U\right)}{O\left(f\right)}^{-1}\left[\left\{\underset{\dot{}}{0}\right\}\right]\leftrightarrow \exists f\in {Monic}_{\mathrm{1p}}\left(U\right)X\in {O\left(f\right)}^{-1}\left[\left\{\underset{\dot{}}{0}\right\}\right]$$
13	11 12	bitrdi	$$⊢\phi \to \left(X\in \left(R\mathrm{IntgRing}S\right)\leftrightarrow \exists f\in {Monic}_{\mathrm{1p}}\left(U\right)X\in {O\left(f\right)}^{-1}\left[\left\{\underset{\dot{}}{0}\right\}\right]\right)$$
14		eqid	$$⊢R{\uparrow }_{𝑠}B=R{\uparrow }_{𝑠}B$$
15		eqid	$$⊢{\mathrm{Base}}_{\left(R{\uparrow }_{𝑠}B\right)}={\mathrm{Base}}_{\left(R{\uparrow }_{𝑠}B\right)}$$
16	7	adantr	$$⊢\left(\phi \wedge f\in {Monic}_{\mathrm{1p}}\left(U\right)\right)\to R\in \mathrm{Ring}$$
17	3	fvexi	$$⊢B\in \mathrm{V}$$
18	17	a1i	$$⊢\left(\phi \wedge f\in {Monic}_{\mathrm{1p}}\left(U\right)\right)\to B\in \mathrm{V}$$
19		eqid	$$⊢{\mathrm{Poly}}_1\left(U\right)={\mathrm{Poly}}_1\left(U\right)$$
20	1 3 14 2 19	evls1rhm	$$⊢\left(R\in \mathrm{CRing}\wedge S\in \mathrm{SubRing}\left(R\right)\right)\to O\in \left({\mathrm{Poly}}_1\left(U\right)\mathrm{RingHom}\left(R{\uparrow }_{𝑠}B\right)\right)$$
21	5 6 20	syl2anc	$$⊢\phi \to O\in \left({\mathrm{Poly}}_1\left(U\right)\mathrm{RingHom}\left(R{\uparrow }_{𝑠}B\right)\right)$$
22		eqid	$$⊢{\mathrm{Base}}_{{\mathrm{Poly}}_1\left(U\right)}={\mathrm{Base}}_{{\mathrm{Poly}}_1\left(U\right)}$$
23	22 15	rhmf	$$⊢O\in \left({\mathrm{Poly}}_1\left(U\right)\mathrm{RingHom}\left(R{\uparrow }_{𝑠}B\right)\right)\to O:{\mathrm{Base}}_{{\mathrm{Poly}}_1\left(U\right)}⟶{\mathrm{Base}}_{\left(R{\uparrow }_{𝑠}B\right)}$$
24	21 23	syl	$$⊢\phi \to O:{\mathrm{Base}}_{{\mathrm{Poly}}_1\left(U\right)}⟶{\mathrm{Base}}_{\left(R{\uparrow }_{𝑠}B\right)}$$
25	24	adantr	$$⊢\left(\phi \wedge f\in {Monic}_{\mathrm{1p}}\left(U\right)\right)\to O:{\mathrm{Base}}_{{\mathrm{Poly}}_1\left(U\right)}⟶{\mathrm{Base}}_{\left(R{\uparrow }_{𝑠}B\right)}$$
26		eqid	$$⊢{Monic}_{\mathrm{1p}}\left(U\right)={Monic}_{\mathrm{1p}}\left(U\right)$$
27	19 22 26	mon1pcl	$$⊢f\in {Monic}_{\mathrm{1p}}\left(U\right)\to f\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(U\right)}$$
28	27	adantl	$$⊢\left(\phi \wedge f\in {Monic}_{\mathrm{1p}}\left(U\right)\right)\to f\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(U\right)}$$
29	25 28	ffvelcdmd	$$⊢\left(\phi \wedge f\in {Monic}_{\mathrm{1p}}\left(U\right)\right)\to O\left(f\right)\in {\mathrm{Base}}_{\left(R{\uparrow }_{𝑠}B\right)}$$
30	14 3 15 16 18 29	pwselbas	$$⊢\left(\phi \wedge f\in {Monic}_{\mathrm{1p}}\left(U\right)\right)\to O\left(f\right):B⟶B$$
31		ffn	$$⊢O\left(f\right):B⟶B\to O\left(f\right)FnB$$
32		fniniseg	$$⊢O\left(f\right)FnB\to \left(X\in {O\left(f\right)}^{-1}\left[\left\{\underset{\dot{}}{0}\right\}\right]\leftrightarrow \left(X\in B\wedge O\left(f\right)\left(X\right)=\underset{\dot{}}{0}\right)\right)$$
33	30 31 32	3syl	$$⊢\left(\phi \wedge f\in {Monic}_{\mathrm{1p}}\left(U\right)\right)\to \left(X\in {O\left(f\right)}^{-1}\left[\left\{\underset{\dot{}}{0}\right\}\right]\leftrightarrow \left(X\in B\wedge O\left(f\right)\left(X\right)=\underset{\dot{}}{0}\right)\right)$$
34	33	rexbidva	$$⊢\phi \to \left(\exists f\in {Monic}_{\mathrm{1p}}\left(U\right)X\in {O\left(f\right)}^{-1}\left[\left\{\underset{\dot{}}{0}\right\}\right]\leftrightarrow \exists f\in {Monic}_{\mathrm{1p}}\left(U\right)\left(X\in B\wedge O\left(f\right)\left(X\right)=\underset{\dot{}}{0}\right)\right)$$
35	13 34	bitrd	$$⊢\phi \to \left(X\in \left(R\mathrm{IntgRing}S\right)\leftrightarrow \exists f\in {Monic}_{\mathrm{1p}}\left(U\right)\left(X\in B\wedge O\left(f\right)\left(X\right)=\underset{\dot{}}{0}\right)\right)$$
36		r19.42v	$$⊢\exists f\in {Monic}_{\mathrm{1p}}\left(U\right)\left(X\in B\wedge O\left(f\right)\left(X\right)=\underset{\dot{}}{0}\right)\leftrightarrow \left(X\in B\wedge \exists f\in {Monic}_{\mathrm{1p}}\left(U\right)O\left(f\right)\left(X\right)=\underset{\dot{}}{0}\right)$$
37	35 36	bitrdi	$$⊢\phi \to \left(X\in \left(R\mathrm{IntgRing}S\right)\leftrightarrow \left(X\in B\wedge \exists f\in {Monic}_{\mathrm{1p}}\left(U\right)O\left(f\right)\left(X\right)=\underset{\dot{}}{0}\right)\right)$$