Theorem minplyelirng

Description: If the minimial 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	⊢ 𝐵 = ( Base ‘ 𝑅 )
	minplyelirng.m	⊢ 𝑀 = ( 𝑅 minPoly 𝑆 )
	minplyelirng.d	⊢ 𝐷 = ( deg1 ‘ ( 𝑅 ↾s 𝑆 ) )
	minplyelirng.r	⊢ ( 𝜑 → 𝑅 ∈ Field )
	minplyelirng.s	⊢ ( 𝜑 → 𝑆 ∈ ( SubDRing ‘ 𝑅 ) )
	minplyelirng.a	⊢ ( 𝜑 → 𝐴 ∈ 𝐵 )
	minplyelirng.1	⊢ ( 𝜑 → ( 𝐷 ‘ ( 𝑀 ‘ 𝐴 ) ) ∈ ℕ0 )
Assertion	minplyelirng	⊢ ( 𝜑 → 𝐴 ∈ ( 𝑅 IntgRing 𝑆 ) )

Proof

Step	Hyp	Ref	Expression
1		minplyelirng.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		minplyelirng.m	⊢ 𝑀 = ( 𝑅 minPoly 𝑆 )
3		minplyelirng.d	⊢ 𝐷 = ( deg1 ‘ ( 𝑅 ↾s 𝑆 ) )
4		minplyelirng.r	⊢ ( 𝜑 → 𝑅 ∈ Field )
5		minplyelirng.s	⊢ ( 𝜑 → 𝑆 ∈ ( SubDRing ‘ 𝑅 ) )
6		minplyelirng.a	⊢ ( 𝜑 → 𝐴 ∈ 𝐵 )
7		minplyelirng.1	⊢ ( 𝜑 → ( 𝐷 ‘ ( 𝑀 ‘ 𝐴 ) ) ∈ ℕ0 )
8		fveq2	⊢ ( 𝑚 = ( 𝑀 ‘ 𝐴 ) → ( ( 𝑅 evalSub1 𝑆 ) ‘ 𝑚 ) = ( ( 𝑅 evalSub1 𝑆 ) ‘ ( 𝑀 ‘ 𝐴 ) ) )
9	8	fveq1d	⊢ ( 𝑚 = ( 𝑀 ‘ 𝐴 ) → ( ( ( 𝑅 evalSub1 𝑆 ) ‘ 𝑚 ) ‘ 𝐴 ) = ( ( ( 𝑅 evalSub1 𝑆 ) ‘ ( 𝑀 ‘ 𝐴 ) ) ‘ 𝐴 ) )
10	9	eqeq1d	⊢ ( 𝑚 = ( 𝑀 ‘ 𝐴 ) → ( ( ( ( 𝑅 evalSub1 𝑆 ) ‘ 𝑚 ) ‘ 𝐴 ) = ( 0g ‘ 𝑅 ) ↔ ( ( ( 𝑅 evalSub1 𝑆 ) ‘ ( 𝑀 ‘ 𝐴 ) ) ‘ 𝐴 ) = ( 0g ‘ 𝑅 ) ) )
11		eqid	⊢ ( 0g ‘ ( Poly1 ‘ 𝑅 ) ) = ( 0g ‘ ( Poly1 ‘ 𝑅 ) )
12		sdrgsubrg	⊢ ( 𝑆 ∈ ( SubDRing ‘ 𝑅 ) → 𝑆 ∈ ( SubRing ‘ 𝑅 ) )
13	5 12	syl	⊢ ( 𝜑 → 𝑆 ∈ ( SubRing ‘ 𝑅 ) )
14		eqid	⊢ ( 𝑅 ↾s 𝑆 ) = ( 𝑅 ↾s 𝑆 )
15	14	subrgring	⊢ ( 𝑆 ∈ ( SubRing ‘ 𝑅 ) → ( 𝑅 ↾s 𝑆 ) ∈ Ring )
16	13 15	syl	⊢ ( 𝜑 → ( 𝑅 ↾s 𝑆 ) ∈ Ring )
17		eqid	⊢ ( 𝑅 evalSub1 𝑆 ) = ( 𝑅 evalSub1 𝑆 )
18		eqid	⊢ ( Poly1 ‘ ( 𝑅 ↾s 𝑆 ) ) = ( Poly1 ‘ ( 𝑅 ↾s 𝑆 ) )
19		eqid	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
20		eqid	⊢ { 𝑞 ∈ dom ( 𝑅 evalSub1 𝑆 ) ∣ ( ( ( 𝑅 evalSub1 𝑆 ) ‘ 𝑞 ) ‘ 𝐴 ) = ( 0g ‘ 𝑅 ) } = { 𝑞 ∈ dom ( 𝑅 evalSub1 𝑆 ) ∣ ( ( ( 𝑅 evalSub1 𝑆 ) ‘ 𝑞 ) ‘ 𝐴 ) = ( 0g ‘ 𝑅 ) }
21		eqid	⊢ ( RSpan ‘ ( Poly1 ‘ ( 𝑅 ↾s 𝑆 ) ) ) = ( RSpan ‘ ( Poly1 ‘ ( 𝑅 ↾s 𝑆 ) ) )
22		eqid	⊢ ( idlGen1p ‘ ( 𝑅 ↾s 𝑆 ) ) = ( idlGen1p ‘ ( 𝑅 ↾s 𝑆 ) )
23	17 18 1 4 5 6 19 20 21 22 2	minplycl	⊢ ( 𝜑 → ( 𝑀 ‘ 𝐴 ) ∈ ( Base ‘ ( Poly1 ‘ ( 𝑅 ↾s 𝑆 ) ) ) )
24		eqid	⊢ ( 0g ‘ ( Poly1 ‘ ( 𝑅 ↾s 𝑆 ) ) ) = ( 0g ‘ ( Poly1 ‘ ( 𝑅 ↾s 𝑆 ) ) )
25		eqid	⊢ ( Base ‘ ( Poly1 ‘ ( 𝑅 ↾s 𝑆 ) ) ) = ( Base ‘ ( Poly1 ‘ ( 𝑅 ↾s 𝑆 ) ) )
26	3 18 24 25	deg1nn0clb	⊢ ( ( ( 𝑅 ↾s 𝑆 ) ∈ Ring ∧ ( 𝑀 ‘ 𝐴 ) ∈ ( Base ‘ ( Poly1 ‘ ( 𝑅 ↾s 𝑆 ) ) ) ) → ( ( 𝑀 ‘ 𝐴 ) ≠ ( 0g ‘ ( Poly1 ‘ ( 𝑅 ↾s 𝑆 ) ) ) ↔ ( 𝐷 ‘ ( 𝑀 ‘ 𝐴 ) ) ∈ ℕ0 ) )
27	26	biimpar	⊢ ( ( ( ( 𝑅 ↾s 𝑆 ) ∈ Ring ∧ ( 𝑀 ‘ 𝐴 ) ∈ ( Base ‘ ( Poly1 ‘ ( 𝑅 ↾s 𝑆 ) ) ) ) ∧ ( 𝐷 ‘ ( 𝑀 ‘ 𝐴 ) ) ∈ ℕ0 ) → ( 𝑀 ‘ 𝐴 ) ≠ ( 0g ‘ ( Poly1 ‘ ( 𝑅 ↾s 𝑆 ) ) ) )
28	16 23 7 27	syl21anc	⊢ ( 𝜑 → ( 𝑀 ‘ 𝐴 ) ≠ ( 0g ‘ ( Poly1 ‘ ( 𝑅 ↾s 𝑆 ) ) ) )
29		eqid	⊢ ( Poly1 ‘ 𝑅 ) = ( Poly1 ‘ 𝑅 )
30	29 14 18 25 13 11	ressply10g	⊢ ( 𝜑 → ( 0g ‘ ( Poly1 ‘ 𝑅 ) ) = ( 0g ‘ ( Poly1 ‘ ( 𝑅 ↾s 𝑆 ) ) ) )
31	28 30	neeqtrrd	⊢ ( 𝜑 → ( 𝑀 ‘ 𝐴 ) ≠ ( 0g ‘ ( Poly1 ‘ 𝑅 ) ) )
32		eqid	⊢ ( Monic1p ‘ ( 𝑅 ↾s 𝑆 ) ) = ( Monic1p ‘ ( 𝑅 ↾s 𝑆 ) )
33	1 11 4 5 2 6 31 32	minplynzm1p	⊢ ( 𝜑 → ( 𝑀 ‘ 𝐴 ) ∈ ( Monic1p ‘ ( 𝑅 ↾s 𝑆 ) ) )
34	17 18 1 4 5 6 19 2	minplyann	⊢ ( 𝜑 → ( ( ( 𝑅 evalSub1 𝑆 ) ‘ ( 𝑀 ‘ 𝐴 ) ) ‘ 𝐴 ) = ( 0g ‘ 𝑅 ) )
35	10 33 34	rspcedvdw	⊢ ( 𝜑 → ∃ 𝑚 ∈ ( Monic1p ‘ ( 𝑅 ↾s 𝑆 ) ) ( ( ( 𝑅 evalSub1 𝑆 ) ‘ 𝑚 ) ‘ 𝐴 ) = ( 0g ‘ 𝑅 ) )
36	4	fldcrngd	⊢ ( 𝜑 → 𝑅 ∈ CRing )
37	17 14 1 19 36 13	elirng	⊢ ( 𝜑 → ( 𝐴 ∈ ( 𝑅 IntgRing 𝑆 ) ↔ ( 𝐴 ∈ 𝐵 ∧ ∃ 𝑚 ∈ ( Monic1p ‘ ( 𝑅 ↾s 𝑆 ) ) ( ( ( 𝑅 evalSub1 𝑆 ) ‘ 𝑚 ) ‘ 𝐴 ) = ( 0g ‘ 𝑅 ) ) ) )
38	6 35 37	mpbir2and	⊢ ( 𝜑 → 𝐴 ∈ ( 𝑅 IntgRing 𝑆 ) )