Metamath Proof Explorer

Theorem irngnminplynz

Description: Integral elements have nonzero minimal polynomials. (Contributed by Thierry Arnoux, 22-Mar-2025)

Ref Expression
Hypotheses irngnminplynz.z ⊢ Z = 0 Poly 1 ⁡ E
irngnminplynz.e ⊢ φ → E ∈ Field
irngnminplynz.f ⊢ φ → F ∈ SubDRing ⁡ E
irngnminplynz.m ⊢ M = E minPoly F
irngnminplynz.a ⊢ φ → A ∈ E IntgRing F
Assertion irngnminplynz ⊢ φ → M ⁡ A ≠ Z

Proof

Step Hyp Ref Expression
1 irngnminplynz.z ⊢ Z = 0 Poly 1 ⁡ E
2 irngnminplynz.e ⊢ φ → E ∈ Field
3 irngnminplynz.f ⊢ φ → F ∈ SubDRing ⁡ E
4 irngnminplynz.m ⊢ M = E minPoly F
5 irngnminplynz.a ⊢ φ → A ∈ E IntgRing F
6 sdrgsubrg ⊢ F ∈ SubDRing ⁡ E → F ∈ SubRing ⁡ E
7 3 6 syl ⊢ φ → F ∈ SubRing ⁡ E
8 eqid ⊢ E ↾ 𝑠 F = E ↾ 𝑠 F
9 8 subrgring ⊢ F ∈ SubRing ⁡ E → E ↾ 𝑠 F ∈ Ring
10 7 9 syl ⊢ φ → E ↾ 𝑠 F ∈ Ring
11 eqid ⊢ Poly 1 ⁡ E ↾ 𝑠 F = Poly 1 ⁡ E ↾ 𝑠 F
12 11 ply1ring ⊢ E ↾ 𝑠 F ∈ Ring → Poly 1 ⁡ E ↾ 𝑠 F ∈ Ring
13 10 12 syl ⊢ φ → Poly 1 ⁡ E ↾ 𝑠 F ∈ Ring
14 eqid ⊢ E evalSub 1 F = E evalSub 1 F
15 eqid ⊢ Base E = Base E
16 2 fldcrngd ⊢ φ → E ∈ CRing
17 eqid ⊢ 0 E = 0 E
18 14 8 15 17 16 7 irngssv ⊢ φ → E IntgRing F ⊆ Base E
19 18 5 sseldd ⊢ φ → A ∈ Base E
20 eqid ⊢ q ∈ dom ⁡ E evalSub 1 F | E evalSub 1 F ⁡ q ⁡ A = 0 E = q ∈ dom ⁡ E evalSub 1 F | E evalSub 1 F ⁡ q ⁡ A = 0 E
21 14 11 15 16 7 19 17 20 ply1annidl ⊢ φ → q ∈ dom ⁡ E evalSub 1 F | E evalSub 1 F ⁡ q ⁡ A = 0 E ∈ LIdeal ⁡ Poly 1 ⁡ E ↾ 𝑠 F
22 eqid ⊢ Base Poly 1 ⁡ E ↾ 𝑠 F = Base Poly 1 ⁡ E ↾ 𝑠 F
23 eqid ⊢ LIdeal ⁡ Poly 1 ⁡ E ↾ 𝑠 F = LIdeal ⁡ Poly 1 ⁡ E ↾ 𝑠 F
24 22 23 lidlss ⊢ q ∈ dom ⁡ E evalSub 1 F | E evalSub 1 F ⁡ q ⁡ A = 0 E ∈ LIdeal ⁡ Poly 1 ⁡ E ↾ 𝑠 F → q ∈ dom ⁡ E evalSub 1 F | E evalSub 1 F ⁡ q ⁡ A = 0 E ⊆ Base Poly 1 ⁡ E ↾ 𝑠 F
25 21 24 syl ⊢ φ → q ∈ dom ⁡ E evalSub 1 F | E evalSub 1 F ⁡ q ⁡ A = 0 E ⊆ Base Poly 1 ⁡ E ↾ 𝑠 F
26 8 sdrgdrng ⊢ F ∈ SubDRing ⁡ E → E ↾ 𝑠 F ∈ DivRing
27 3 26 syl ⊢ φ → E ↾ 𝑠 F ∈ DivRing
28 eqid ⊢ idlGen 1p ⁡ E ↾ 𝑠 F = idlGen 1p ⁡ E ↾ 𝑠 F
29 11 28 23 ig1pcl ⊢ E ↾ 𝑠 F ∈ DivRing ∧ q ∈ dom ⁡ E evalSub 1 F | E evalSub 1 F ⁡ q ⁡ A = 0 E ∈ LIdeal ⁡ Poly 1 ⁡ E ↾ 𝑠 F → idlGen 1p ⁡ E ↾ 𝑠 F ⁡ q ∈ dom ⁡ E evalSub 1 F | E evalSub 1 F ⁡ q ⁡ A = 0 E ∈ q ∈ dom ⁡ E evalSub 1 F | E evalSub 1 F ⁡ q ⁡ A = 0 E
30 27 21 29 syl2anc ⊢ φ → idlGen 1p ⁡ E ↾ 𝑠 F ⁡ q ∈ dom ⁡ E evalSub 1 F | E evalSub 1 F ⁡ q ⁡ A = 0 E ∈ q ∈ dom ⁡ E evalSub 1 F | E evalSub 1 F ⁡ q ⁡ A = 0 E
31 25 30 sseldd ⊢ φ → idlGen 1p ⁡ E ↾ 𝑠 F ⁡ q ∈ dom ⁡ E evalSub 1 F | E evalSub 1 F ⁡ q ⁡ A = 0 E ∈ Base Poly 1 ⁡ E ↾ 𝑠 F
32 eqid ⊢ RSpan ⁡ Poly 1 ⁡ E ↾ 𝑠 F = RSpan ⁡ Poly 1 ⁡ E ↾ 𝑠 F
33 14 11 15 2 3 19 17 20 32 28 ply1annig1p ⊢ φ → q ∈ dom ⁡ E evalSub 1 F | E evalSub 1 F ⁡ q ⁡ A = 0 E = RSpan ⁡ Poly 1 ⁡ E ↾ 𝑠 F ⁡ idlGen 1p ⁡ E ↾ 𝑠 F ⁡ q ∈ dom ⁡ E evalSub 1 F | E evalSub 1 F ⁡ q ⁡ A = 0 E
34 fveq2 ⊢ q = p → E evalSub 1 F ⁡ q = E evalSub 1 F ⁡ p
35 34 fveq1d ⊢ q = p → E evalSub 1 F ⁡ q ⁡ A = E evalSub 1 F ⁡ p ⁡ A
36 35 eqeq1d ⊢ q = p → E evalSub 1 F ⁡ q ⁡ A = 0 E ↔ E evalSub 1 F ⁡ p ⁡ A = 0 E
37 simplr ⊢ φ ∧ p ∈ dom ⁡ E evalSub 1 F ∖ Z ∧ A ∈ E evalSub 1 F ⁡ p -1 0 E → p ∈ dom ⁡ E evalSub 1 F ∖ Z
38 37 eldifad ⊢ φ ∧ p ∈ dom ⁡ E evalSub 1 F ∖ Z ∧ A ∈ E evalSub 1 F ⁡ p -1 0 E → p ∈ dom ⁡ E evalSub 1 F
39 16 ad2antrr ⊢ φ ∧ p ∈ dom ⁡ E evalSub 1 F ∖ Z ∧ A ∈ E evalSub 1 F ⁡ p -1 0 E → E ∈ CRing
40 7 ad2antrr ⊢ φ ∧ p ∈ dom ⁡ E evalSub 1 F ∖ Z ∧ A ∈ E evalSub 1 F ⁡ p -1 0 E → F ∈ SubRing ⁡ E
41 14 11 22 16 7 evls1dm ⊢ φ → dom ⁡ E evalSub 1 F = Base Poly 1 ⁡ E ↾ 𝑠 F
42 41 ad2antrr ⊢ φ ∧ p ∈ dom ⁡ E evalSub 1 F ∖ Z ∧ A ∈ E evalSub 1 F ⁡ p -1 0 E → dom ⁡ E evalSub 1 F = Base Poly 1 ⁡ E ↾ 𝑠 F
43 38 42 eleqtrd ⊢ φ ∧ p ∈ dom ⁡ E evalSub 1 F ∖ Z ∧ A ∈ E evalSub 1 F ⁡ p -1 0 E → p ∈ Base Poly 1 ⁡ E ↾ 𝑠 F
44 14 11 22 39 40 15 43 evls1fvf ⊢ φ ∧ p ∈ dom ⁡ E evalSub 1 F ∖ Z ∧ A ∈ E evalSub 1 F ⁡ p -1 0 E → E evalSub 1 F ⁡ p : Base E ⟶ Base E
45 44 ffnd ⊢ φ ∧ p ∈ dom ⁡ E evalSub 1 F ∖ Z ∧ A ∈ E evalSub 1 F ⁡ p -1 0 E → E evalSub 1 F ⁡ p Fn Base E
46 elpreima ⊢ E evalSub 1 F ⁡ p Fn Base E → A ∈ E evalSub 1 F ⁡ p -1 0 E ↔ A ∈ Base E ∧ E evalSub 1 F ⁡ p ⁡ A ∈ 0 E
47 46 simplbda ⊢ E evalSub 1 F ⁡ p Fn Base E ∧ A ∈ E evalSub 1 F ⁡ p -1 0 E → E evalSub 1 F ⁡ p ⁡ A ∈ 0 E
48 45 47 sylancom ⊢ φ ∧ p ∈ dom ⁡ E evalSub 1 F ∖ Z ∧ A ∈ E evalSub 1 F ⁡ p -1 0 E → E evalSub 1 F ⁡ p ⁡ A ∈ 0 E
49 elsni ⊢ E evalSub 1 F ⁡ p ⁡ A ∈ 0 E → E evalSub 1 F ⁡ p ⁡ A = 0 E
50 48 49 syl ⊢ φ ∧ p ∈ dom ⁡ E evalSub 1 F ∖ Z ∧ A ∈ E evalSub 1 F ⁡ p -1 0 E → E evalSub 1 F ⁡ p ⁡ A = 0 E
51 36 38 50 elrabd ⊢ φ ∧ p ∈ dom ⁡ E evalSub 1 F ∖ Z ∧ A ∈ E evalSub 1 F ⁡ p -1 0 E → p ∈ q ∈ dom ⁡ E evalSub 1 F | E evalSub 1 F ⁡ q ⁡ A = 0 E
52 eldifsni ⊢ p ∈ dom ⁡ E evalSub 1 F ∖ Z → p ≠ Z
53 37 52 syl ⊢ φ ∧ p ∈ dom ⁡ E evalSub 1 F ∖ Z ∧ A ∈ E evalSub 1 F ⁡ p -1 0 E → p ≠ Z
54 eqid ⊢ Poly 1 ⁡ E = Poly 1 ⁡ E
55 54 8 11 22 7 1 ressply10g ⊢ φ → Z = 0 Poly 1 ⁡ E ↾ 𝑠 F
56 55 ad2antrr ⊢ φ ∧ p ∈ dom ⁡ E evalSub 1 F ∖ Z ∧ A ∈ E evalSub 1 F ⁡ p -1 0 E → Z = 0 Poly 1 ⁡ E ↾ 𝑠 F
57 53 56 neeqtrd ⊢ φ ∧ p ∈ dom ⁡ E evalSub 1 F ∖ Z ∧ A ∈ E evalSub 1 F ⁡ p -1 0 E → p ≠ 0 Poly 1 ⁡ E ↾ 𝑠 F
58 nelsn ⊢ p ≠ 0 Poly 1 ⁡ E ↾ 𝑠 F → ¬ p ∈ 0 Poly 1 ⁡ E ↾ 𝑠 F
59 57 58 syl ⊢ φ ∧ p ∈ dom ⁡ E evalSub 1 F ∖ Z ∧ A ∈ E evalSub 1 F ⁡ p -1 0 E → ¬ p ∈ 0 Poly 1 ⁡ E ↾ 𝑠 F
60 nelne1 ⊢ p ∈ q ∈ dom ⁡ E evalSub 1 F | E evalSub 1 F ⁡ q ⁡ A = 0 E ∧ ¬ p ∈ 0 Poly 1 ⁡ E ↾ 𝑠 F → q ∈ dom ⁡ E evalSub 1 F | E evalSub 1 F ⁡ q ⁡ A = 0 E ≠ 0 Poly 1 ⁡ E ↾ 𝑠 F
61 51 59 60 syl2anc ⊢ φ ∧ p ∈ dom ⁡ E evalSub 1 F ∖ Z ∧ A ∈ E evalSub 1 F ⁡ p -1 0 E → q ∈ dom ⁡ E evalSub 1 F | E evalSub 1 F ⁡ q ⁡ A = 0 E ≠ 0 Poly 1 ⁡ E ↾ 𝑠 F
62 14 1 17 2 3 irngnzply1 ⊢ φ → E IntgRing F = ⋃ p ∈ dom ⁡ E evalSub 1 F ∖ Z E evalSub 1 F ⁡ p -1 0 E
63 5 62 eleqtrd ⊢ φ → A ∈ ⋃ p ∈ dom ⁡ E evalSub 1 F ∖ Z E evalSub 1 F ⁡ p -1 0 E
64 eliun ⊢ A ∈ ⋃ p ∈ dom ⁡ E evalSub 1 F ∖ Z E evalSub 1 F ⁡ p -1 0 E ↔ ∃ p ∈ dom ⁡ E evalSub 1 F ∖ Z A ∈ E evalSub 1 F ⁡ p -1 0 E
65 63 64 sylib ⊢ φ → ∃ p ∈ dom ⁡ E evalSub 1 F ∖ Z A ∈ E evalSub 1 F ⁡ p -1 0 E
66 61 65 r19.29a ⊢ φ → q ∈ dom ⁡ E evalSub 1 F | E evalSub 1 F ⁡ q ⁡ A = 0 E ≠ 0 Poly 1 ⁡ E ↾ 𝑠 F
67 33 66 eqnetrrd ⊢ φ → RSpan ⁡ Poly 1 ⁡ E ↾ 𝑠 F ⁡ idlGen 1p ⁡ E ↾ 𝑠 F ⁡ q ∈ dom ⁡ E evalSub 1 F | E evalSub 1 F ⁡ q ⁡ A = 0 E ≠ 0 Poly 1 ⁡ E ↾ 𝑠 F
68 eqid ⊢ 0 Poly 1 ⁡ E ↾ 𝑠 F = 0 Poly 1 ⁡ E ↾ 𝑠 F
69 22 68 32 pidlnzb ⊢ Poly 1 ⁡ E ↾ 𝑠 F ∈ Ring ∧ idlGen 1p ⁡ E ↾ 𝑠 F ⁡ q ∈ dom ⁡ E evalSub 1 F | E evalSub 1 F ⁡ q ⁡ A = 0 E ∈ Base Poly 1 ⁡ E ↾ 𝑠 F → idlGen 1p ⁡ E ↾ 𝑠 F ⁡ q ∈ dom ⁡ E evalSub 1 F | E evalSub 1 F ⁡ q ⁡ A = 0 E ≠ 0 Poly 1 ⁡ E ↾ 𝑠 F ↔ RSpan ⁡ Poly 1 ⁡ E ↾ 𝑠 F ⁡ idlGen 1p ⁡ E ↾ 𝑠 F ⁡ q ∈ dom ⁡ E evalSub 1 F | E evalSub 1 F ⁡ q ⁡ A = 0 E ≠ 0 Poly 1 ⁡ E ↾ 𝑠 F
70 69 biimpar ⊢ Poly 1 ⁡ E ↾ 𝑠 F ∈ Ring ∧ idlGen 1p ⁡ E ↾ 𝑠 F ⁡ q ∈ dom ⁡ E evalSub 1 F | E evalSub 1 F ⁡ q ⁡ A = 0 E ∈ Base Poly 1 ⁡ E ↾ 𝑠 F ∧ RSpan ⁡ Poly 1 ⁡ E ↾ 𝑠 F ⁡ idlGen 1p ⁡ E ↾ 𝑠 F ⁡ q ∈ dom ⁡ E evalSub 1 F | E evalSub 1 F ⁡ q ⁡ A = 0 E ≠ 0 Poly 1 ⁡ E ↾ 𝑠 F → idlGen 1p ⁡ E ↾ 𝑠 F ⁡ q ∈ dom ⁡ E evalSub 1 F | E evalSub 1 F ⁡ q ⁡ A = 0 E ≠ 0 Poly 1 ⁡ E ↾ 𝑠 F
71 13 31 67 70 syl21anc ⊢ φ → idlGen 1p ⁡ E ↾ 𝑠 F ⁡ q ∈ dom ⁡ E evalSub 1 F | E evalSub 1 F ⁡ q ⁡ A = 0 E ≠ 0 Poly 1 ⁡ E ↾ 𝑠 F
72 14 11 15 2 3 19 17 20 32 28 4 minplyval ⊢ φ → M ⁡ A = idlGen 1p ⁡ E ↾ 𝑠 F ⁡ q ∈ dom ⁡ E evalSub 1 F | E evalSub 1 F ⁡ q ⁡ A = 0 E
73 71 72 55 3netr4d ⊢ φ → M ⁡ A ≠ Z