Metamath Proof Explorer

Theorem irngnzply1lem

Description: In the case of a field E , a root X of some nonzero polynomial P with coefficients in a subfield F is integral over F . (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
irngnzply1lem.b ⊢ B = Base E
irngnzply1lem.1 ⊢ φ → P ∈ dom ⁡ O
irngnzply1lem.2 ⊢ φ → P ≠ Z
irngnzply1lem.3 ⊢ φ → O ⁡ P ⁡ X = 0 ˙
irngnzply1lem.x ⊢ φ → X ∈ B
Assertion irngnzply1lem ⊢ φ → X ∈ E IntgRing F

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 irngnzply1lem.b ⊢ B = Base E
7 irngnzply1lem.1 ⊢ φ → P ∈ dom ⁡ O
8 irngnzply1lem.2 ⊢ φ → P ≠ Z
9 irngnzply1lem.3 ⊢ φ → O ⁡ P ⁡ X = 0 ˙
10 irngnzply1lem.x ⊢ φ → X ∈ B
11 issdrg ⊢ F ∈ SubDRing ⁡ E ↔ E ∈ DivRing ∧ F ∈ SubRing ⁡ E ∧ E ↾ 𝑠 F ∈ DivRing
12 11 simp3bi ⊢ F ∈ SubDRing ⁡ E → E ↾ 𝑠 F ∈ DivRing
13 5 12 syl ⊢ φ → E ↾ 𝑠 F ∈ DivRing
14 13 drngringd ⊢ φ → E ↾ 𝑠 F ∈ Ring
15 4 fldcrngd ⊢ φ → E ∈ CRing
16 5 11 sylib ⊢ φ → E ∈ DivRing ∧ F ∈ SubRing ⁡ E ∧ E ↾ 𝑠 F ∈ DivRing
17 16 simp2d ⊢ φ → F ∈ SubRing ⁡ E
18 eqid ⊢ E ↑ 𝑠 B = E ↑ 𝑠 B
19 eqid ⊢ E ↾ 𝑠 F = E ↾ 𝑠 F
20 eqid ⊢ Poly 1 ⁡ E ↾ 𝑠 F = Poly 1 ⁡ E ↾ 𝑠 F
21 1 6 18 19 20 evls1rhm ⊢ E ∈ CRing ∧ F ∈ SubRing ⁡ E → O ∈ Poly 1 ⁡ E ↾ 𝑠 F RingHom E ↑ 𝑠 B
22 15 17 21 syl2anc ⊢ φ → O ∈ Poly 1 ⁡ E ↾ 𝑠 F RingHom E ↑ 𝑠 B
23 eqid ⊢ Base Poly 1 ⁡ E ↾ 𝑠 F = Base Poly 1 ⁡ E ↾ 𝑠 F
24 eqid ⊢ Base E ↑ 𝑠 B = Base E ↑ 𝑠 B
25 23 24 rhmf ⊢ O ∈ Poly 1 ⁡ E ↾ 𝑠 F RingHom E ↑ 𝑠 B → O : Base Poly 1 ⁡ E ↾ 𝑠 F ⟶ Base E ↑ 𝑠 B
26 22 25 syl ⊢ φ → O : Base Poly 1 ⁡ E ↾ 𝑠 F ⟶ Base E ↑ 𝑠 B
27 26 fdmd ⊢ φ → dom ⁡ O = Base Poly 1 ⁡ E ↾ 𝑠 F
28 7 27 eleqtrd ⊢ φ → P ∈ Base Poly 1 ⁡ E ↾ 𝑠 F
29 eqid ⊢ Poly 1 ⁡ E = Poly 1 ⁡ E
30 29 19 20 23 17 2 ressply10g ⊢ φ → Z = 0 Poly 1 ⁡ E ↾ 𝑠 F
31 8 30 neeqtrd ⊢ φ → P ≠ 0 Poly 1 ⁡ E ↾ 𝑠 F
32 eqid ⊢ 0 Poly 1 ⁡ E ↾ 𝑠 F = 0 Poly 1 ⁡ E ↾ 𝑠 F
33 eqid ⊢ Unic 1p ⁡ E ↾ 𝑠 F = Unic 1p ⁡ E ↾ 𝑠 F
34 20 23 32 33 drnguc1p ⊢ E ↾ 𝑠 F ∈ DivRing ∧ P ∈ Base Poly 1 ⁡ E ↾ 𝑠 F ∧ P ≠ 0 Poly 1 ⁡ E ↾ 𝑠 F → P ∈ Unic 1p ⁡ E ↾ 𝑠 F
35 13 28 31 34 syl3anc ⊢ φ → P ∈ Unic 1p ⁡ E ↾ 𝑠 F
36 eqid ⊢ Monic 1p ⁡ E ↾ 𝑠 F = Monic 1p ⁡ E ↾ 𝑠 F
37 eqid ⊢ ⋅ Poly 1 ⁡ E ↾ 𝑠 F = ⋅ Poly 1 ⁡ E ↾ 𝑠 F
38 eqid ⊢ algSc ⁡ Poly 1 ⁡ E ↾ 𝑠 F = algSc ⁡ Poly 1 ⁡ E ↾ 𝑠 F
39 eqid ⊢ deg 1 ⁡ E ↾ 𝑠 F = deg 1 ⁡ E ↾ 𝑠 F
40 eqid ⊢ inv r ⁡ E ↾ 𝑠 F = inv r ⁡ E ↾ 𝑠 F
41 33 36 20 37 38 39 40 uc1pmon1p ⊢ E ↾ 𝑠 F ∈ Ring ∧ P ∈ Unic 1p ⁡ E ↾ 𝑠 F → algSc ⁡ Poly 1 ⁡ E ↾ 𝑠 F ⁡ inv r ⁡ E ↾ 𝑠 F ⁡ coe 1 ⁡ P ⁡ deg 1 ⁡ E ↾ 𝑠 F ⁡ P ⋅ Poly 1 ⁡ E ↾ 𝑠 F P ∈ Monic 1p ⁡ E ↾ 𝑠 F
42 14 35 41 syl2anc ⊢ φ → algSc ⁡ Poly 1 ⁡ E ↾ 𝑠 F ⁡ inv r ⁡ E ↾ 𝑠 F ⁡ coe 1 ⁡ P ⁡ deg 1 ⁡ E ↾ 𝑠 F ⁡ P ⋅ Poly 1 ⁡ E ↾ 𝑠 F P ∈ Monic 1p ⁡ E ↾ 𝑠 F
43 simpr ⊢ φ ∧ p = algSc ⁡ Poly 1 ⁡ E ↾ 𝑠 F ⁡ inv r ⁡ E ↾ 𝑠 F ⁡ coe 1 ⁡ P ⁡ deg 1 ⁡ E ↾ 𝑠 F ⁡ P ⋅ Poly 1 ⁡ E ↾ 𝑠 F P → p = algSc ⁡ Poly 1 ⁡ E ↾ 𝑠 F ⁡ inv r ⁡ E ↾ 𝑠 F ⁡ coe 1 ⁡ P ⁡ deg 1 ⁡ E ↾ 𝑠 F ⁡ P ⋅ Poly 1 ⁡ E ↾ 𝑠 F P
44 43 fveq2d ⊢ φ ∧ p = algSc ⁡ Poly 1 ⁡ E ↾ 𝑠 F ⁡ inv r ⁡ E ↾ 𝑠 F ⁡ coe 1 ⁡ P ⁡ deg 1 ⁡ E ↾ 𝑠 F ⁡ P ⋅ Poly 1 ⁡ E ↾ 𝑠 F P → O ⁡ p = O ⁡ algSc ⁡ Poly 1 ⁡ E ↾ 𝑠 F ⁡ inv r ⁡ E ↾ 𝑠 F ⁡ coe 1 ⁡ P ⁡ deg 1 ⁡ E ↾ 𝑠 F ⁡ P ⋅ Poly 1 ⁡ E ↾ 𝑠 F P
45 44 fveq1d ⊢ φ ∧ p = algSc ⁡ Poly 1 ⁡ E ↾ 𝑠 F ⁡ inv r ⁡ E ↾ 𝑠 F ⁡ coe 1 ⁡ P ⁡ deg 1 ⁡ E ↾ 𝑠 F ⁡ P ⋅ Poly 1 ⁡ E ↾ 𝑠 F P → O ⁡ p ⁡ X = O ⁡ algSc ⁡ Poly 1 ⁡ E ↾ 𝑠 F ⁡ inv r ⁡ E ↾ 𝑠 F ⁡ coe 1 ⁡ P ⁡ deg 1 ⁡ E ↾ 𝑠 F ⁡ P ⋅ Poly 1 ⁡ E ↾ 𝑠 F P ⁡ X
46 45 eqeq1d ⊢ φ ∧ p = algSc ⁡ Poly 1 ⁡ E ↾ 𝑠 F ⁡ inv r ⁡ E ↾ 𝑠 F ⁡ coe 1 ⁡ P ⁡ deg 1 ⁡ E ↾ 𝑠 F ⁡ P ⋅ Poly 1 ⁡ E ↾ 𝑠 F P → O ⁡ p ⁡ X = 0 ˙ ↔ O ⁡ algSc ⁡ Poly 1 ⁡ E ↾ 𝑠 F ⁡ inv r ⁡ E ↾ 𝑠 F ⁡ coe 1 ⁡ P ⁡ deg 1 ⁡ E ↾ 𝑠 F ⁡ P ⋅ Poly 1 ⁡ E ↾ 𝑠 F P ⁡ X = 0 ˙
47 eqid ⊢ ⋅ E = ⋅ E
48 eqid ⊢ Scalar ⁡ Poly 1 ⁡ E ↾ 𝑠 F = Scalar ⁡ Poly 1 ⁡ E ↾ 𝑠 F
49 fldsdrgfld ⊢ E ∈ Field ∧ F ∈ SubDRing ⁡ E → E ↾ 𝑠 F ∈ Field
50 4 5 49 syl2anc ⊢ φ → E ↾ 𝑠 F ∈ Field
51 50 fldcrngd ⊢ φ → E ↾ 𝑠 F ∈ CRing
52 20 ply1assa ⊢ E ↾ 𝑠 F ∈ CRing → Poly 1 ⁡ E ↾ 𝑠 F ∈ AssAlg
53 51 52 syl ⊢ φ → Poly 1 ⁡ E ↾ 𝑠 F ∈ AssAlg
54 assaring ⊢ Poly 1 ⁡ E ↾ 𝑠 F ∈ AssAlg → Poly 1 ⁡ E ↾ 𝑠 F ∈ Ring
55 53 54 syl ⊢ φ → Poly 1 ⁡ E ↾ 𝑠 F ∈ Ring
56 20 ply1lmod ⊢ E ↾ 𝑠 F ∈ Ring → Poly 1 ⁡ E ↾ 𝑠 F ∈ LMod
57 14 56 syl ⊢ φ → Poly 1 ⁡ E ↾ 𝑠 F ∈ LMod
58 eqid ⊢ Base Scalar ⁡ Poly 1 ⁡ E ↾ 𝑠 F = Base Scalar ⁡ Poly 1 ⁡ E ↾ 𝑠 F
59 38 48 55 57 58 23 asclf ⊢ φ → algSc ⁡ Poly 1 ⁡ E ↾ 𝑠 F : Base Scalar ⁡ Poly 1 ⁡ E ↾ 𝑠 F ⟶ Base Poly 1 ⁡ E ↾ 𝑠 F
60 eqid ⊢ Base E ↾ 𝑠 F = Base E ↾ 𝑠 F
61 eqid ⊢ 0 E ↾ 𝑠 F = 0 E ↾ 𝑠 F
62 39 20 32 23 deg1nn0cl ⊢ E ↾ 𝑠 F ∈ Ring ∧ P ∈ Base Poly 1 ⁡ E ↾ 𝑠 F ∧ P ≠ 0 Poly 1 ⁡ E ↾ 𝑠 F → deg 1 ⁡ E ↾ 𝑠 F ⁡ P ∈ ℕ 0
63 14 28 31 62 syl3anc ⊢ φ → deg 1 ⁡ E ↾ 𝑠 F ⁡ P ∈ ℕ 0
64 eqid ⊢ coe 1 ⁡ P = coe 1 ⁡ P
65 64 23 20 60 coe1fvalcl ⊢ P ∈ Base Poly 1 ⁡ E ↾ 𝑠 F ∧ deg 1 ⁡ E ↾ 𝑠 F ⁡ P ∈ ℕ 0 → coe 1 ⁡ P ⁡ deg 1 ⁡ E ↾ 𝑠 F ⁡ P ∈ Base E ↾ 𝑠 F
66 28 63 65 syl2anc ⊢ φ → coe 1 ⁡ P ⁡ deg 1 ⁡ E ↾ 𝑠 F ⁡ P ∈ Base E ↾ 𝑠 F
67 39 20 32 23 61 64 deg1ldg ⊢ E ↾ 𝑠 F ∈ Ring ∧ P ∈ Base Poly 1 ⁡ E ↾ 𝑠 F ∧ P ≠ 0 Poly 1 ⁡ E ↾ 𝑠 F → coe 1 ⁡ P ⁡ deg 1 ⁡ E ↾ 𝑠 F ⁡ P ≠ 0 E ↾ 𝑠 F
68 14 28 31 67 syl3anc ⊢ φ → coe 1 ⁡ P ⁡ deg 1 ⁡ E ↾ 𝑠 F ⁡ P ≠ 0 E ↾ 𝑠 F
69 60 61 40 13 66 68 drnginvrcld ⊢ φ → inv r ⁡ E ↾ 𝑠 F ⁡ coe 1 ⁡ P ⁡ deg 1 ⁡ E ↾ 𝑠 F ⁡ P ∈ Base E ↾ 𝑠 F
70 20 ply1sca ⊢ E ↾ 𝑠 F ∈ Field → E ↾ 𝑠 F = Scalar ⁡ Poly 1 ⁡ E ↾ 𝑠 F
71 50 70 syl ⊢ φ → E ↾ 𝑠 F = Scalar ⁡ Poly 1 ⁡ E ↾ 𝑠 F
72 71 fveq2d ⊢ φ → Base E ↾ 𝑠 F = Base Scalar ⁡ Poly 1 ⁡ E ↾ 𝑠 F
73 69 72 eleqtrd ⊢ φ → inv r ⁡ E ↾ 𝑠 F ⁡ coe 1 ⁡ P ⁡ deg 1 ⁡ E ↾ 𝑠 F ⁡ P ∈ Base Scalar ⁡ Poly 1 ⁡ E ↾ 𝑠 F
74 59 73 ffvelcdmd ⊢ φ → algSc ⁡ Poly 1 ⁡ E ↾ 𝑠 F ⁡ inv r ⁡ E ↾ 𝑠 F ⁡ coe 1 ⁡ P ⁡ deg 1 ⁡ E ↾ 𝑠 F ⁡ P ∈ Base Poly 1 ⁡ E ↾ 𝑠 F
75 1 6 20 19 23 37 47 15 17 74 28 10 evls1muld ⊢ φ → O ⁡ algSc ⁡ Poly 1 ⁡ E ↾ 𝑠 F ⁡ inv r ⁡ E ↾ 𝑠 F ⁡ coe 1 ⁡ P ⁡ deg 1 ⁡ E ↾ 𝑠 F ⁡ P ⋅ Poly 1 ⁡ E ↾ 𝑠 F P ⁡ X = O ⁡ algSc ⁡ Poly 1 ⁡ E ↾ 𝑠 F ⁡ inv r ⁡ E ↾ 𝑠 F ⁡ coe 1 ⁡ P ⁡ deg 1 ⁡ E ↾ 𝑠 F ⁡ P ⁡ X ⋅ E O ⁡ P ⁡ X
76 9 oveq2d ⊢ φ → O ⁡ algSc ⁡ Poly 1 ⁡ E ↾ 𝑠 F ⁡ inv r ⁡ E ↾ 𝑠 F ⁡ coe 1 ⁡ P ⁡ deg 1 ⁡ E ↾ 𝑠 F ⁡ P ⁡ X ⋅ E O ⁡ P ⁡ X = O ⁡ algSc ⁡ Poly 1 ⁡ E ↾ 𝑠 F ⁡ inv r ⁡ E ↾ 𝑠 F ⁡ coe 1 ⁡ P ⁡ deg 1 ⁡ E ↾ 𝑠 F ⁡ P ⁡ X ⋅ E 0 ˙
77 15 crngringd ⊢ φ → E ∈ Ring
78 6 fvexi ⊢ B ∈ V
79 78 a1i ⊢ φ → B ∈ V
80 26 74 ffvelcdmd ⊢ φ → O ⁡ algSc ⁡ Poly 1 ⁡ E ↾ 𝑠 F ⁡ inv r ⁡ E ↾ 𝑠 F ⁡ coe 1 ⁡ P ⁡ deg 1 ⁡ E ↾ 𝑠 F ⁡ P ∈ Base E ↑ 𝑠 B
81 18 6 24 4 79 80 pwselbas ⊢ φ → O ⁡ algSc ⁡ Poly 1 ⁡ E ↾ 𝑠 F ⁡ inv r ⁡ E ↾ 𝑠 F ⁡ coe 1 ⁡ P ⁡ deg 1 ⁡ E ↾ 𝑠 F ⁡ P : B ⟶ B
82 81 10 ffvelcdmd ⊢ φ → O ⁡ algSc ⁡ Poly 1 ⁡ E ↾ 𝑠 F ⁡ inv r ⁡ E ↾ 𝑠 F ⁡ coe 1 ⁡ P ⁡ deg 1 ⁡ E ↾ 𝑠 F ⁡ P ⁡ X ∈ B
83 6 47 3 ringrz ⊢ E ∈ Ring ∧ O ⁡ algSc ⁡ Poly 1 ⁡ E ↾ 𝑠 F ⁡ inv r ⁡ E ↾ 𝑠 F ⁡ coe 1 ⁡ P ⁡ deg 1 ⁡ E ↾ 𝑠 F ⁡ P ⁡ X ∈ B → O ⁡ algSc ⁡ Poly 1 ⁡ E ↾ 𝑠 F ⁡ inv r ⁡ E ↾ 𝑠 F ⁡ coe 1 ⁡ P ⁡ deg 1 ⁡ E ↾ 𝑠 F ⁡ P ⁡ X ⋅ E 0 ˙ = 0 ˙
84 77 82 83 syl2anc ⊢ φ → O ⁡ algSc ⁡ Poly 1 ⁡ E ↾ 𝑠 F ⁡ inv r ⁡ E ↾ 𝑠 F ⁡ coe 1 ⁡ P ⁡ deg 1 ⁡ E ↾ 𝑠 F ⁡ P ⁡ X ⋅ E 0 ˙ = 0 ˙
85 75 76 84 3eqtrd ⊢ φ → O ⁡ algSc ⁡ Poly 1 ⁡ E ↾ 𝑠 F ⁡ inv r ⁡ E ↾ 𝑠 F ⁡ coe 1 ⁡ P ⁡ deg 1 ⁡ E ↾ 𝑠 F ⁡ P ⋅ Poly 1 ⁡ E ↾ 𝑠 F P ⁡ X = 0 ˙
86 42 46 85 rspcedvd ⊢ φ → ∃ p ∈ Monic 1p ⁡ E ↾ 𝑠 F O ⁡ p ⁡ X = 0 ˙
87 1 19 6 3 15 17 elirng ⊢ φ → X ∈ E IntgRing F ↔ X ∈ B ∧ ∃ p ∈ Monic 1p ⁡ E ↾ 𝑠 F O ⁡ p ⁡ X = 0 ˙
88 10 86 87 mpbir2and ⊢ φ → X ∈ E IntgRing F