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=EevalSub1F
irngnzply1.z ⊢Z=0Poly1⁡E
irngnzply1.1 ⊢0˙=0E
irngnzply1.e ⊢φ→E∈Field
irngnzply1.f ⊢φ→F∈SubDRing⁡E
irngnzply1lem.b ⊢B=BaseE
irngnzply1lem.1 ⊢φ→P∈dom⁡O
irngnzply1lem.2 ⊢φ→P≠Z
irngnzply1lem.3 ⊢φ→O⁡P⁡X=0˙
irngnzply1lem.x ⊢φ→X∈B
Assertion irngnzply1lem ⊢φ→X∈EIntgRingF

Proof

Step Hyp Ref Expression
1 irngnzply1.o ⊢O=EevalSub1F
2 irngnzply1.z ⊢Z=0Poly1⁡E
3 irngnzply1.1 ⊢0˙=0E
4 irngnzply1.e ⊢φ→E∈Field
5 irngnzply1.f ⊢φ→F∈SubDRing⁡E
6 irngnzply1lem.b ⊢B=BaseE
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 ⊢Poly1⁡E↾𝑠F=Poly1⁡E↾𝑠F
21 1 6 18 19 20 evls1rhm ⊢E∈CRing∧F∈SubRing⁡E→O∈Poly1⁡E↾𝑠FRingHomE↑𝑠B
22 15 17 21 syl2anc ⊢φ→O∈Poly1⁡E↾𝑠FRingHomE↑𝑠B
23 eqid ⊢BasePoly1⁡E↾𝑠F=BasePoly1⁡E↾𝑠F
24 eqid ⊢BaseE↑𝑠B=BaseE↑𝑠B
25 23 24 rhmf ⊢O∈Poly1⁡E↾𝑠FRingHomE↑𝑠B→O:BasePoly1⁡E↾𝑠F⟶BaseE↑𝑠B
26 22 25 syl ⊢φ→O:BasePoly1⁡E↾𝑠F⟶BaseE↑𝑠B
27 26 fdmd ⊢φ→dom⁡O=BasePoly1⁡E↾𝑠F
28 7 27 eleqtrd ⊢φ→P∈BasePoly1⁡E↾𝑠F
29 eqid ⊢Poly1⁡E=Poly1⁡E
30 29 19 20 23 17 2 ressply10g ⊢φ→Z=0Poly1⁡E↾𝑠F
31 8 30 neeqtrd ⊢φ→P≠0Poly1⁡E↾𝑠F
32 eqid ⊢0Poly1⁡E↾𝑠F=0Poly1⁡E↾𝑠F
33 eqid ⊢Unic1p⁡E↾𝑠F=Unic1p⁡E↾𝑠F
34 20 23 32 33 drnguc1p ⊢E↾𝑠F∈DivRing∧P∈BasePoly1⁡E↾𝑠F∧P≠0Poly1⁡E↾𝑠F→P∈Unic1p⁡E↾𝑠F
35 13 28 31 34 syl3anc ⊢φ→P∈Unic1p⁡E↾𝑠F
36 eqid ⊢Monic1p⁡E↾𝑠F=Monic1p⁡E↾𝑠F
37 eqid ⊢⋅Poly1⁡E↾𝑠F=⋅Poly1⁡E↾𝑠F
38 eqid ⊢algSc⁡Poly1⁡E↾𝑠F=algSc⁡Poly1⁡E↾𝑠F
39 eqid ⊢deg1⁡E↾𝑠F=deg1⁡E↾𝑠F
40 eqid ⊢invr⁡E↾𝑠F=invr⁡E↾𝑠F
41 33 36 20 37 38 39 40 uc1pmon1p ⊢E↾𝑠F∈Ring∧P∈Unic1p⁡E↾𝑠F→algSc⁡Poly1⁡E↾𝑠F⁡invr⁡E↾𝑠F⁡coe1⁡P⁡deg1⁡E↾𝑠F⁡P⋅Poly1⁡E↾𝑠FP∈Monic1p⁡E↾𝑠F
42 14 35 41 syl2anc ⊢φ→algSc⁡Poly1⁡E↾𝑠F⁡invr⁡E↾𝑠F⁡coe1⁡P⁡deg1⁡E↾𝑠F⁡P⋅Poly1⁡E↾𝑠FP∈Monic1p⁡E↾𝑠F
43 simpr ⊢φ∧p=algSc⁡Poly1⁡E↾𝑠F⁡invr⁡E↾𝑠F⁡coe1⁡P⁡deg1⁡E↾𝑠F⁡P⋅Poly1⁡E↾𝑠FP→p=algSc⁡Poly1⁡E↾𝑠F⁡invr⁡E↾𝑠F⁡coe1⁡P⁡deg1⁡E↾𝑠F⁡P⋅Poly1⁡E↾𝑠FP
44 43 fveq2d ⊢φ∧p=algSc⁡Poly1⁡E↾𝑠F⁡invr⁡E↾𝑠F⁡coe1⁡P⁡deg1⁡E↾𝑠F⁡P⋅Poly1⁡E↾𝑠FP→O⁡p=O⁡algSc⁡Poly1⁡E↾𝑠F⁡invr⁡E↾𝑠F⁡coe1⁡P⁡deg1⁡E↾𝑠F⁡P⋅Poly1⁡E↾𝑠FP
45 44 fveq1d ⊢φ∧p=algSc⁡Poly1⁡E↾𝑠F⁡invr⁡E↾𝑠F⁡coe1⁡P⁡deg1⁡E↾𝑠F⁡P⋅Poly1⁡E↾𝑠FP→O⁡p⁡X=O⁡algSc⁡Poly1⁡E↾𝑠F⁡invr⁡E↾𝑠F⁡coe1⁡P⁡deg1⁡E↾𝑠F⁡P⋅Poly1⁡E↾𝑠FP⁡X
46 45 eqeq1d ⊢φ∧p=algSc⁡Poly1⁡E↾𝑠F⁡invr⁡E↾𝑠F⁡coe1⁡P⁡deg1⁡E↾𝑠F⁡P⋅Poly1⁡E↾𝑠FP→O⁡p⁡X=0˙↔O⁡algSc⁡Poly1⁡E↾𝑠F⁡invr⁡E↾𝑠F⁡coe1⁡P⁡deg1⁡E↾𝑠F⁡P⋅Poly1⁡E↾𝑠FP⁡X=0˙
47 eqid ⊢⋅E=⋅E
48 eqid ⊢Scalar⁡Poly1⁡E↾𝑠F=Scalar⁡Poly1⁡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→Poly1⁡E↾𝑠F∈AssAlg
53 51 52 syl ⊢φ→Poly1⁡E↾𝑠F∈AssAlg
54 assaring ⊢Poly1⁡E↾𝑠F∈AssAlg→Poly1⁡E↾𝑠F∈Ring
55 53 54 syl ⊢φ→Poly1⁡E↾𝑠F∈Ring
56 20 ply1lmod ⊢E↾𝑠F∈Ring→Poly1⁡E↾𝑠F∈LMod
57 14 56 syl ⊢φ→Poly1⁡E↾𝑠F∈LMod
58 eqid ⊢BaseScalar⁡Poly1⁡E↾𝑠F=BaseScalar⁡Poly1⁡E↾𝑠F
59 38 48 55 57 58 23 asclf ⊢φ→algSc⁡Poly1⁡E↾𝑠F:BaseScalar⁡Poly1⁡E↾𝑠F⟶BasePoly1⁡E↾𝑠F
60 eqid ⊢BaseE↾𝑠F=BaseE↾𝑠F
61 eqid ⊢0E↾𝑠F=0E↾𝑠F
62 39 20 32 23 deg1nn0cl ⊢E↾𝑠F∈Ring∧P∈BasePoly1⁡E↾𝑠F∧P≠0Poly1⁡E↾𝑠F→deg1⁡E↾𝑠F⁡P∈ℕ0
63 14 28 31 62 syl3anc ⊢φ→deg1⁡E↾𝑠F⁡P∈ℕ0
64 eqid ⊢coe1⁡P=coe1⁡P
65 64 23 20 60 coe1fvalcl ⊢P∈BasePoly1⁡E↾𝑠F∧deg1⁡E↾𝑠F⁡P∈ℕ0→coe1⁡P⁡deg1⁡E↾𝑠F⁡P∈BaseE↾𝑠F
66 28 63 65 syl2anc ⊢φ→coe1⁡P⁡deg1⁡E↾𝑠F⁡P∈BaseE↾𝑠F
67 39 20 32 23 61 64 deg1ldg ⊢E↾𝑠F∈Ring∧P∈BasePoly1⁡E↾𝑠F∧P≠0Poly1⁡E↾𝑠F→coe1⁡P⁡deg1⁡E↾𝑠F⁡P≠0E↾𝑠F
68 14 28 31 67 syl3anc ⊢φ→coe1⁡P⁡deg1⁡E↾𝑠F⁡P≠0E↾𝑠F
69 60 61 40 13 66 68 drnginvrcld ⊢φ→invr⁡E↾𝑠F⁡coe1⁡P⁡deg1⁡E↾𝑠F⁡P∈BaseE↾𝑠F
70 20 ply1sca ⊢E↾𝑠F∈Field→E↾𝑠F=Scalar⁡Poly1⁡E↾𝑠F
71 50 70 syl ⊢φ→E↾𝑠F=Scalar⁡Poly1⁡E↾𝑠F
72 71 fveq2d ⊢φ→BaseE↾𝑠F=BaseScalar⁡Poly1⁡E↾𝑠F
73 69 72 eleqtrd ⊢φ→invr⁡E↾𝑠F⁡coe1⁡P⁡deg1⁡E↾𝑠F⁡P∈BaseScalar⁡Poly1⁡E↾𝑠F
74 59 73 ffvelcdmd ⊢φ→algSc⁡Poly1⁡E↾𝑠F⁡invr⁡E↾𝑠F⁡coe1⁡P⁡deg1⁡E↾𝑠F⁡P∈BasePoly1⁡E↾𝑠F
75 1 6 20 19 23 37 47 15 17 74 28 10 evls1muld ⊢φ→O⁡algSc⁡Poly1⁡E↾𝑠F⁡invr⁡E↾𝑠F⁡coe1⁡P⁡deg1⁡E↾𝑠F⁡P⋅Poly1⁡E↾𝑠FP⁡X=O⁡algSc⁡Poly1⁡E↾𝑠F⁡invr⁡E↾𝑠F⁡coe1⁡P⁡deg1⁡E↾𝑠F⁡P⁡X⋅EO⁡P⁡X
76 9 oveq2d ⊢φ→O⁡algSc⁡Poly1⁡E↾𝑠F⁡invr⁡E↾𝑠F⁡coe1⁡P⁡deg1⁡E↾𝑠F⁡P⁡X⋅EO⁡P⁡X=O⁡algSc⁡Poly1⁡E↾𝑠F⁡invr⁡E↾𝑠F⁡coe1⁡P⁡deg1⁡E↾𝑠F⁡P⁡X⋅E0˙
77 15 crngringd ⊢φ→E∈Ring
78 6 fvexi ⊢B∈V
79 78 a1i ⊢φ→B∈V
80 26 74 ffvelcdmd ⊢φ→O⁡algSc⁡Poly1⁡E↾𝑠F⁡invr⁡E↾𝑠F⁡coe1⁡P⁡deg1⁡E↾𝑠F⁡P∈BaseE↑𝑠B
81 18 6 24 4 79 80 pwselbas ⊢φ→O⁡algSc⁡Poly1⁡E↾𝑠F⁡invr⁡E↾𝑠F⁡coe1⁡P⁡deg1⁡E↾𝑠F⁡P:B⟶B
82 81 10 ffvelcdmd ⊢φ→O⁡algSc⁡Poly1⁡E↾𝑠F⁡invr⁡E↾𝑠F⁡coe1⁡P⁡deg1⁡E↾𝑠F⁡P⁡X∈B
83 6 47 3 ringrz ⊢E∈Ring∧O⁡algSc⁡Poly1⁡E↾𝑠F⁡invr⁡E↾𝑠F⁡coe1⁡P⁡deg1⁡E↾𝑠F⁡P⁡X∈B→O⁡algSc⁡Poly1⁡E↾𝑠F⁡invr⁡E↾𝑠F⁡coe1⁡P⁡deg1⁡E↾𝑠F⁡P⁡X⋅E0˙=0˙
84 77 82 83 syl2anc ⊢φ→O⁡algSc⁡Poly1⁡E↾𝑠F⁡invr⁡E↾𝑠F⁡coe1⁡P⁡deg1⁡E↾𝑠F⁡P⁡X⋅E0˙=0˙
85 75 76 84 3eqtrd ⊢φ→O⁡algSc⁡Poly1⁡E↾𝑠F⁡invr⁡E↾𝑠F⁡coe1⁡P⁡deg1⁡E↾𝑠F⁡P⋅Poly1⁡E↾𝑠FP⁡X=0˙
86 42 46 85 rspcedvd ⊢φ→∃p∈Monic1p⁡E↾𝑠FO⁡p⁡X=0˙
87 1 19 6 3 15 17 elirng ⊢φ→X∈EIntgRingF↔X∈B∧∃p∈Monic1p⁡E↾𝑠FO⁡p⁡X=0˙
88 10 86 87 mpbir2and ⊢φ→X∈EIntgRingF