This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ 𝐵 = ( 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 𝑆 ) )