Theorem minplyelirng

Description: If the minimal polynomial F of an element X of a field R has nonnegative degree, then X is integral. (Contributed by Thierry Arnoux, 26-Oct-2025)

	Ref	Expression
Hypotheses	minplyelirng.b	$$⊢B={\mathrm{Base}}_R$$
	minplyelirng.m	$$⊢M=R\mathrm{minPoly}S$$
	minplyelirng.d	$$⊢D={\mathrm{deg}}_1\left(R{\upharpoonright }_{𝑠}S\right)$$
	minplyelirng.r	$$⊢\phi \to R\in \mathrm{Field}$$
	minplyelirng.s	$$⊢\phi \to S\in \mathrm{SubDRing}\left(R\right)$$
	minplyelirng.a	$$⊢\phi \to A\in B$$
	minplyelirng.1	$$⊢\phi \to D\left(M\left(A\right)\right)\in {\mathbb{N}}_0$$
Assertion	minplyelirng	$$⊢\phi \to A\in \left(R\mathrm{IntgRing}S\right)$$

Proof

Step	Hyp	Ref	Expression
1		minplyelirng.b	$$⊢B={\mathrm{Base}}_R$$
2		minplyelirng.m	$$⊢M=R\mathrm{minPoly}S$$
3		minplyelirng.d	$$⊢D={\mathrm{deg}}_1\left(R{\upharpoonright }_{𝑠}S\right)$$
4		minplyelirng.r	$$⊢\phi \to R\in \mathrm{Field}$$
5		minplyelirng.s	$$⊢\phi \to S\in \mathrm{SubDRing}\left(R\right)$$
6		minplyelirng.a	$$⊢\phi \to A\in B$$
7		minplyelirng.1	$$⊢\phi \to D\left(M\left(A\right)\right)\in {\mathbb{N}}_0$$
8		fveq2	$$⊢m=M\left(A\right)\to \left(R{\mathrm{evalSub}}_{1}S\right)\left(m\right)=\left(R{\mathrm{evalSub}}_{1}S\right)\left(M\left(A\right)\right)$$
9	8	fveq1d	$$⊢m=M\left(A\right)\to \left(R{\mathrm{evalSub}}_{1}S\right)\left(m\right)\left(A\right)=\left(R{\mathrm{evalSub}}_{1}S\right)\left(M\left(A\right)\right)\left(A\right)$$
10	9	eqeq1d	$$⊢m=M\left(A\right)\to \left(\left(R{\mathrm{evalSub}}_{1}S\right)\left(m\right)\left(A\right)=0_R\leftrightarrow \left(R{\mathrm{evalSub}}_{1}S\right)\left(M\left(A\right)\right)\left(A\right)=0_R\right)$$
11		eqid	$$⊢0_{{\mathrm{Poly}}_1\left(R\right)}=0_{{\mathrm{Poly}}_1\left(R\right)}$$
12		sdrgsubrg	$$⊢S\in \mathrm{SubDRing}\left(R\right)\to S\in \mathrm{SubRing}\left(R\right)$$
13	5 12	syl	$$⊢\phi \to S\in \mathrm{SubRing}\left(R\right)$$
14		eqid	$$⊢R{\upharpoonright }_{𝑠}S=R{\upharpoonright }_{𝑠}S$$
15	14	subrgring	$$⊢S\in \mathrm{SubRing}\left(R\right)\to R{\upharpoonright }_{𝑠}S\in \mathrm{Ring}$$
16	13 15	syl	$$⊢\phi \to R{\upharpoonright }_{𝑠}S\in \mathrm{Ring}$$
17		eqid	$$⊢R{\mathrm{evalSub}}_{1}S=R{\mathrm{evalSub}}_{1}S$$
18		eqid	$$⊢{\mathrm{Poly}}_1\left(R{\upharpoonright }_{𝑠}S\right)={\mathrm{Poly}}_1\left(R{\upharpoonright }_{𝑠}S\right)$$
19		eqid	$$⊢0_R=0_R$$
20		eqid	$$⊢\left\{q\in \mathrm{dom}\left(R{\mathrm{evalSub}}_{1}S\right)|\left(R{\mathrm{evalSub}}_{1}S\right)\left(q\right)\left(A\right)=0_R\right\}=\left\{q\in \mathrm{dom}\left(R{\mathrm{evalSub}}_{1}S\right)|\left(R{\mathrm{evalSub}}_{1}S\right)\left(q\right)\left(A\right)=0_R\right\}$$
21		eqid	$$⊢\mathrm{RSpan}\left({\mathrm{Poly}}_1\left(R{\upharpoonright }_{𝑠}S\right)\right)=\mathrm{RSpan}\left({\mathrm{Poly}}_1\left(R{\upharpoonright }_{𝑠}S\right)\right)$$
22		eqid	$$⊢{idlGen}_{\mathrm{1p}}\left(R{\upharpoonright }_{𝑠}S\right)={idlGen}_{\mathrm{1p}}\left(R{\upharpoonright }_{𝑠}S\right)$$
23	17 18 1 4 5 6 19 20 21 22 2	minplycl	$$⊢\phi \to M\left(A\right)\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R{\upharpoonright }_{𝑠}S\right)}$$
24		eqid	$$⊢0_{{\mathrm{Poly}}_1\left(R{\upharpoonright }_{𝑠}S\right)}=0_{{\mathrm{Poly}}_1\left(R{\upharpoonright }_{𝑠}S\right)}$$
25		eqid	$$⊢{\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R{\upharpoonright }_{𝑠}S\right)}={\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R{\upharpoonright }_{𝑠}S\right)}$$
26	3 18 24 25	deg1nn0clb	$$⊢\left(R{\upharpoonright }_{𝑠}S\in \mathrm{Ring}\wedge M\left(A\right)\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R{\upharpoonright }_{𝑠}S\right)}\right)\to \left(M\left(A\right)\ne 0_{{\mathrm{Poly}}_1\left(R{\upharpoonright }_{𝑠}S\right)}\leftrightarrow D\left(M\left(A\right)\right)\in {\mathbb{N}}_0\right)$$
27	26	biimpar	$$⊢\left(\left(R{\upharpoonright }_{𝑠}S\in \mathrm{Ring}\wedge M\left(A\right)\in {\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R{\upharpoonright }_{𝑠}S\right)}\right)\wedge D\left(M\left(A\right)\right)\in {\mathbb{N}}_0\right)\to M\left(A\right)\ne 0_{{\mathrm{Poly}}_1\left(R{\upharpoonright }_{𝑠}S\right)}$$
28	16 23 7 27	syl21anc	$$⊢\phi \to M\left(A\right)\ne 0_{{\mathrm{Poly}}_1\left(R{\upharpoonright }_{𝑠}S\right)}$$
29		eqid	$$⊢{\mathrm{Poly}}_1\left(R\right)={\mathrm{Poly}}_1\left(R\right)$$
30	29 14 18 25 13 11	ressply10g	$$⊢\phi \to 0_{{\mathrm{Poly}}_1\left(R\right)}=0_{{\mathrm{Poly}}_1\left(R{\upharpoonright }_{𝑠}S\right)}$$
31	28 30	neeqtrrd	$$⊢\phi \to M\left(A\right)\ne 0_{{\mathrm{Poly}}_1\left(R\right)}$$
32		eqid	$$⊢{Monic}_{\mathrm{1p}}\left(R{\upharpoonright }_{𝑠}S\right)={Monic}_{\mathrm{1p}}\left(R{\upharpoonright }_{𝑠}S\right)$$
33	1 11 4 5 2 6 31 32	minplynzm1p	$$⊢\phi \to M\left(A\right)\in {Monic}_{\mathrm{1p}}\left(R{\upharpoonright }_{𝑠}S\right)$$
34	17 18 1 4 5 6 19 2	minplyann	$$⊢\phi \to \left(R{\mathrm{evalSub}}_{1}S\right)\left(M\left(A\right)\right)\left(A\right)=0_R$$
35	10 33 34	rspcedvdw	$$⊢\phi \to \exists m\in {Monic}_{\mathrm{1p}}\left(R{\upharpoonright }_{𝑠}S\right)\left(R{\mathrm{evalSub}}_{1}S\right)\left(m\right)\left(A\right)=0_R$$
36	4	fldcrngd	$$⊢\phi \to R\in \mathrm{CRing}$$
37	17 14 1 19 36 13	elirng	$$⊢\phi \to \left(A\in \left(R\mathrm{IntgRing}S\right)\leftrightarrow \left(A\in B\wedge \exists m\in {Monic}_{\mathrm{1p}}\left(R{\upharpoonright }_{𝑠}S\right)\left(R{\mathrm{evalSub}}_{1}S\right)\left(m\right)\left(A\right)=0_R\right)\right)$$
38	6 35 37	mpbir2and	$$⊢\phi \to A\in \left(R\mathrm{IntgRing}S\right)$$