Metamath Proof Explorer

Theorem irngnzply1

Description: In the case of a field E , the roots of nonzero polynomials p with coefficients in a subfield F are exactly the integral elements over F . Roots of nonzero polynomials are called algebraic numbers, so this shows that in the case of a field, elements integral over F are exactly the algebraic numbers. In this formula, dom O represents the polynomials, and Z the zero polynomial. (Contributed by Thierry Arnoux, 5-Feb-2025)

Ref Expression
Hypotheses irngnzply1.o ⊢ O = E evalSub 1 F
irngnzply1.z ⊢ Z = 0 Poly 1 ⁡ E
irngnzply1.1 ⊢ 0 ˙ = 0 E
irngnzply1.e ⊢ φ → E ∈ Field
irngnzply1.f ⊢ φ → F ∈ SubDRing ⁡ E
Assertion irngnzply1 ⊢ φ → E IntgRing F = ⋃ p ∈ dom ⁡ O ∖ Z O ⁡ p -1 0 ˙

Proof

Step Hyp Ref Expression
1 irngnzply1.o ⊢ O = E evalSub 1 F
2 irngnzply1.z ⊢ Z = 0 Poly 1 ⁡ E
3 irngnzply1.1 ⊢ 0 ˙ = 0 E
4 irngnzply1.e ⊢ φ → E ∈ Field
5 irngnzply1.f ⊢ φ → F ∈ SubDRing ⁡ E
6 eqid ⊢ E ↾ 𝑠 F = E ↾ 𝑠 F
7 eqid ⊢ Base E = Base E
8 4 fldcrngd ⊢ φ → E ∈ CRing
9 issdrg ⊢ F ∈ SubDRing ⁡ E ↔ E ∈ DivRing ∧ F ∈ SubRing ⁡ E ∧ E ↾ 𝑠 F ∈ DivRing
10 5 9 sylib ⊢ φ → E ∈ DivRing ∧ F ∈ SubRing ⁡ E ∧ E ↾ 𝑠 F ∈ DivRing
11 10 simp2d ⊢ φ → F ∈ SubRing ⁡ E
12 1 6 7 3 8 11 elirng ⊢ φ → x ∈ E IntgRing F ↔ x ∈ Base E ∧ ∃ p ∈ Monic 1p ⁡ E ↾ 𝑠 F O ⁡ p ⁡ x = 0 ˙
13 12 biimpa ⊢ φ ∧ x ∈ E IntgRing F → x ∈ Base E ∧ ∃ p ∈ Monic 1p ⁡ E ↾ 𝑠 F O ⁡ p ⁡ x = 0 ˙
14 13 simprd ⊢ φ ∧ x ∈ E IntgRing F → ∃ p ∈ Monic 1p ⁡ E ↾ 𝑠 F O ⁡ p ⁡ x = 0 ˙
15 eqid ⊢ Poly 1 ⁡ E ↾ 𝑠 F = Poly 1 ⁡ E ↾ 𝑠 F
16 eqid ⊢ Base Poly 1 ⁡ E ↾ 𝑠 F = Base Poly 1 ⁡ E ↾ 𝑠 F
17 eqid ⊢ Monic 1p ⁡ E ↾ 𝑠 F = Monic 1p ⁡ E ↾ 𝑠 F
18 15 16 17 mon1pcl ⊢ p ∈ Monic 1p ⁡ E ↾ 𝑠 F → p ∈ Base Poly 1 ⁡ E ↾ 𝑠 F
19 18 adantl ⊢ φ ∧ p ∈ Monic 1p ⁡ E ↾ 𝑠 F → p ∈ Base Poly 1 ⁡ E ↾ 𝑠 F
20 eqid ⊢ E ↑ 𝑠 Base E = E ↑ 𝑠 Base E
21 1 7 20 6 15 evls1rhm ⊢ E ∈ CRing ∧ F ∈ SubRing ⁡ E → O ∈ Poly 1 ⁡ E ↾ 𝑠 F RingHom E ↑ 𝑠 Base E
22 8 11 21 syl2anc ⊢ φ → O ∈ Poly 1 ⁡ E ↾ 𝑠 F RingHom E ↑ 𝑠 Base E
23 eqid ⊢ Base E ↑ 𝑠 Base E = Base E ↑ 𝑠 Base E
24 16 23 rhmf ⊢ O ∈ Poly 1 ⁡ E ↾ 𝑠 F RingHom E ↑ 𝑠 Base E → O : Base Poly 1 ⁡ E ↾ 𝑠 F ⟶ Base E ↑ 𝑠 Base E
25 22 24 syl ⊢ φ → O : Base Poly 1 ⁡ E ↾ 𝑠 F ⟶ Base E ↑ 𝑠 Base E
26 25 fdmd ⊢ φ → dom ⁡ O = Base Poly 1 ⁡ E ↾ 𝑠 F
27 26 adantr ⊢ φ ∧ p ∈ Monic 1p ⁡ E ↾ 𝑠 F → dom ⁡ O = Base Poly 1 ⁡ E ↾ 𝑠 F
28 19 27 eleqtrrd ⊢ φ ∧ p ∈ Monic 1p ⁡ E ↾ 𝑠 F → p ∈ dom ⁡ O
29 eqid ⊢ 0 Poly 1 ⁡ E ↾ 𝑠 F = 0 Poly 1 ⁡ E ↾ 𝑠 F
30 15 29 17 mon1pn0 ⊢ p ∈ Monic 1p ⁡ E ↾ 𝑠 F → p ≠ 0 Poly 1 ⁡ E ↾ 𝑠 F
31 30 adantl ⊢ φ ∧ p ∈ Monic 1p ⁡ E ↾ 𝑠 F → p ≠ 0 Poly 1 ⁡ E ↾ 𝑠 F
32 eqid ⊢ Poly 1 ⁡ E = Poly 1 ⁡ E
33 32 6 15 16 11 2 ressply10g ⊢ φ → Z = 0 Poly 1 ⁡ E ↾ 𝑠 F
34 33 adantr ⊢ φ ∧ p ∈ Monic 1p ⁡ E ↾ 𝑠 F → Z = 0 Poly 1 ⁡ E ↾ 𝑠 F
35 31 34 neeqtrrd ⊢ φ ∧ p ∈ Monic 1p ⁡ E ↾ 𝑠 F → p ≠ Z
36 eldifsn ⊢ p ∈ dom ⁡ O ∖ Z ↔ p ∈ dom ⁡ O ∧ p ≠ Z
37 28 35 36 sylanbrc ⊢ φ ∧ p ∈ Monic 1p ⁡ E ↾ 𝑠 F → p ∈ dom ⁡ O ∖ Z
38 37 ad2ant2r ⊢ φ ∧ x ∈ E IntgRing F ∧ p ∈ Monic 1p ⁡ E ↾ 𝑠 F ∧ O ⁡ p ⁡ x = 0 ˙ → p ∈ dom ⁡ O ∖ Z
39 4 ad2antrr ⊢ φ ∧ x ∈ E IntgRing F ∧ p ∈ Monic 1p ⁡ E ↾ 𝑠 F ∧ O ⁡ p ⁡ x = 0 ˙ → E ∈ Field
40 fvexd ⊢ φ ∧ x ∈ E IntgRing F ∧ p ∈ Monic 1p ⁡ E ↾ 𝑠 F ∧ O ⁡ p ⁡ x = 0 ˙ → Base E ∈ V
41 25 ad2antrr ⊢ φ ∧ x ∈ E IntgRing F ∧ p ∈ Monic 1p ⁡ E ↾ 𝑠 F ∧ O ⁡ p ⁡ x = 0 ˙ → O : Base Poly 1 ⁡ E ↾ 𝑠 F ⟶ Base E ↑ 𝑠 Base E
42 18 ad2antrl ⊢ φ ∧ x ∈ E IntgRing F ∧ p ∈ Monic 1p ⁡ E ↾ 𝑠 F ∧ O ⁡ p ⁡ x = 0 ˙ → p ∈ Base Poly 1 ⁡ E ↾ 𝑠 F
43 41 42 ffvelcdmd ⊢ φ ∧ x ∈ E IntgRing F ∧ p ∈ Monic 1p ⁡ E ↾ 𝑠 F ∧ O ⁡ p ⁡ x = 0 ˙ → O ⁡ p ∈ Base E ↑ 𝑠 Base E
44 20 7 23 39 40 43 pwselbas ⊢ φ ∧ x ∈ E IntgRing F ∧ p ∈ Monic 1p ⁡ E ↾ 𝑠 F ∧ O ⁡ p ⁡ x = 0 ˙ → O ⁡ p : Base E ⟶ Base E
45 44 ffnd ⊢ φ ∧ x ∈ E IntgRing F ∧ p ∈ Monic 1p ⁡ E ↾ 𝑠 F ∧ O ⁡ p ⁡ x = 0 ˙ → O ⁡ p Fn Base E
46 13 simpld ⊢ φ ∧ x ∈ E IntgRing F → x ∈ Base E
47 46 adantr ⊢ φ ∧ x ∈ E IntgRing F ∧ p ∈ Monic 1p ⁡ E ↾ 𝑠 F ∧ O ⁡ p ⁡ x = 0 ˙ → x ∈ Base E
48 simprr ⊢ φ ∧ x ∈ E IntgRing F ∧ p ∈ Monic 1p ⁡ E ↾ 𝑠 F ∧ O ⁡ p ⁡ x = 0 ˙ → O ⁡ p ⁡ x = 0 ˙
49 fniniseg ⊢ O ⁡ p Fn Base E → x ∈ O ⁡ p -1 0 ˙ ↔ x ∈ Base E ∧ O ⁡ p ⁡ x = 0 ˙
50 49 biimpar ⊢ O ⁡ p Fn Base E ∧ x ∈ Base E ∧ O ⁡ p ⁡ x = 0 ˙ → x ∈ O ⁡ p -1 0 ˙
51 45 47 48 50 syl12anc ⊢ φ ∧ x ∈ E IntgRing F ∧ p ∈ Monic 1p ⁡ E ↾ 𝑠 F ∧ O ⁡ p ⁡ x = 0 ˙ → x ∈ O ⁡ p -1 0 ˙
52 14 38 51 reximssdv ⊢ φ ∧ x ∈ E IntgRing F → ∃ p ∈ dom ⁡ O ∖ Z x ∈ O ⁡ p -1 0 ˙
53 eliun ⊢ x ∈ ⋃ p ∈ dom ⁡ O ∖ Z O ⁡ p -1 0 ˙ ↔ ∃ p ∈ dom ⁡ O ∖ Z x ∈ O ⁡ p -1 0 ˙
54 52 53 sylibr ⊢ φ ∧ x ∈ E IntgRing F → x ∈ ⋃ p ∈ dom ⁡ O ∖ Z O ⁡ p -1 0 ˙
55 nfv ⊢ Ⅎ p φ
56 nfiu1 ⊢ Ⅎ _ p ⋃ p ∈ dom ⁡ O ∖ Z O ⁡ p -1 0 ˙
57 56 nfcri ⊢ Ⅎ p x ∈ ⋃ p ∈ dom ⁡ O ∖ Z O ⁡ p -1 0 ˙
58 55 57 nfan ⊢ Ⅎ p φ ∧ x ∈ ⋃ p ∈ dom ⁡ O ∖ Z O ⁡ p -1 0 ˙
59 4 ad2antrr ⊢ φ ∧ p ∈ dom ⁡ O ∖ Z ∧ x ∈ O ⁡ p -1 0 ˙ → E ∈ Field
60 5 ad2antrr ⊢ φ ∧ p ∈ dom ⁡ O ∖ Z ∧ x ∈ O ⁡ p -1 0 ˙ → F ∈ SubDRing ⁡ E
61 eldifi ⊢ p ∈ dom ⁡ O ∖ Z → p ∈ dom ⁡ O
62 61 adantl ⊢ φ ∧ p ∈ dom ⁡ O ∖ Z → p ∈ dom ⁡ O
63 62 adantr ⊢ φ ∧ p ∈ dom ⁡ O ∖ Z ∧ x ∈ O ⁡ p -1 0 ˙ → p ∈ dom ⁡ O
64 eldifsni ⊢ p ∈ dom ⁡ O ∖ Z → p ≠ Z
65 64 adantl ⊢ φ ∧ p ∈ dom ⁡ O ∖ Z → p ≠ Z
66 65 adantr ⊢ φ ∧ p ∈ dom ⁡ O ∖ Z ∧ x ∈ O ⁡ p -1 0 ˙ → p ≠ Z
67 4 adantr ⊢ φ ∧ p ∈ dom ⁡ O ∖ Z → E ∈ Field
68 fvexd ⊢ φ ∧ p ∈ dom ⁡ O ∖ Z → Base E ∈ V
69 25 adantr ⊢ φ ∧ p ∈ dom ⁡ O ∖ Z → O : Base Poly 1 ⁡ E ↾ 𝑠 F ⟶ Base E ↑ 𝑠 Base E
70 26 adantr ⊢ φ ∧ p ∈ dom ⁡ O ∖ Z → dom ⁡ O = Base Poly 1 ⁡ E ↾ 𝑠 F
71 62 70 eleqtrd ⊢ φ ∧ p ∈ dom ⁡ O ∖ Z → p ∈ Base Poly 1 ⁡ E ↾ 𝑠 F
72 69 71 ffvelcdmd ⊢ φ ∧ p ∈ dom ⁡ O ∖ Z → O ⁡ p ∈ Base E ↑ 𝑠 Base E
73 20 7 23 67 68 72 pwselbas ⊢ φ ∧ p ∈ dom ⁡ O ∖ Z → O ⁡ p : Base E ⟶ Base E
74 73 ffnd ⊢ φ ∧ p ∈ dom ⁡ O ∖ Z → O ⁡ p Fn Base E
75 49 biimpa ⊢ O ⁡ p Fn Base E ∧ x ∈ O ⁡ p -1 0 ˙ → x ∈ Base E ∧ O ⁡ p ⁡ x = 0 ˙
76 74 75 sylan ⊢ φ ∧ p ∈ dom ⁡ O ∖ Z ∧ x ∈ O ⁡ p -1 0 ˙ → x ∈ Base E ∧ O ⁡ p ⁡ x = 0 ˙
77 76 simprd ⊢ φ ∧ p ∈ dom ⁡ O ∖ Z ∧ x ∈ O ⁡ p -1 0 ˙ → O ⁡ p ⁡ x = 0 ˙
78 76 simpld ⊢ φ ∧ p ∈ dom ⁡ O ∖ Z ∧ x ∈ O ⁡ p -1 0 ˙ → x ∈ Base E
79 1 2 3 59 60 7 63 66 77 78 irngnzply1lem ⊢ φ ∧ p ∈ dom ⁡ O ∖ Z ∧ x ∈ O ⁡ p -1 0 ˙ → x ∈ E IntgRing F
80 79 adantllr ⊢ φ ∧ x ∈ ⋃ p ∈ dom ⁡ O ∖ Z O ⁡ p -1 0 ˙ ∧ p ∈ dom ⁡ O ∖ Z ∧ x ∈ O ⁡ p -1 0 ˙ → x ∈ E IntgRing F
81 53 biimpi ⊢ x ∈ ⋃ p ∈ dom ⁡ O ∖ Z O ⁡ p -1 0 ˙ → ∃ p ∈ dom ⁡ O ∖ Z x ∈ O ⁡ p -1 0 ˙
82 81 adantl ⊢ φ ∧ x ∈ ⋃ p ∈ dom ⁡ O ∖ Z O ⁡ p -1 0 ˙ → ∃ p ∈ dom ⁡ O ∖ Z x ∈ O ⁡ p -1 0 ˙
83 58 80 82 r19.29af ⊢ φ ∧ x ∈ ⋃ p ∈ dom ⁡ O ∖ Z O ⁡ p -1 0 ˙ → x ∈ E IntgRing F
84 54 83 impbida ⊢ φ → x ∈ E IntgRing F ↔ x ∈ ⋃ p ∈ dom ⁡ O ∖ Z O ⁡ p -1 0 ˙
85 84 eqrdv ⊢ φ → E IntgRing F = ⋃ p ∈ dom ⁡ O ∖ Z O ⁡ p -1 0 ˙