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 evalSub1 F )
irngnzply1.z 
|- Z = ( 0g ` ( Poly1 ` E ) )
irngnzply1.1 
|- .0. = ( 0g ` E )
irngnzply1.e 
|- ( ph -> E e. Field )
irngnzply1.f 
|- ( ph -> F e. ( SubDRing ` E ) )
irngnzply1lem.b 
|- B = ( Base ` E )
irngnzply1lem.1 
|- ( ph -> P e. dom O )
irngnzply1lem.2 
|- ( ph -> P =/= Z )
irngnzply1lem.3 
|- ( ph -> ( ( O ` P ) ` X ) = .0. )
irngnzply1lem.x 
|- ( ph -> X e. B )
Assertion irngnzply1lem 
|- ( ph -> X e. ( E IntgRing F ) )

Proof

Step Hyp Ref Expression
1 irngnzply1.o 
 |-  O = ( E evalSub1 F )
2 irngnzply1.z 
 |-  Z = ( 0g ` ( Poly1 ` E ) )
3 irngnzply1.1 
 |-  .0. = ( 0g ` E )
4 irngnzply1.e 
 |-  ( ph -> E e. Field )
5 irngnzply1.f 
 |-  ( ph -> F e. ( SubDRing ` E ) )
6 irngnzply1lem.b 
 |-  B = ( Base ` E )
7 irngnzply1lem.1 
 |-  ( ph -> P e. dom O )
8 irngnzply1lem.2 
 |-  ( ph -> P =/= Z )
9 irngnzply1lem.3 
 |-  ( ph -> ( ( O ` P ) ` X ) = .0. )
10 irngnzply1lem.x 
 |-  ( ph -> X e. B )
11 issdrg 
 |-  ( F e. ( SubDRing ` E ) <-> ( E e. DivRing /\ F e. ( SubRing ` E ) /\ ( E |`s F ) e. DivRing ) )
12 11 simp3bi 
 |-  ( F e. ( SubDRing ` E ) -> ( E |`s F ) e. DivRing )
13 5 12 syl 
 |-  ( ph -> ( E |`s F ) e. DivRing )
14 13 drngringd 
 |-  ( ph -> ( E |`s F ) e. Ring )
15 4 fldcrngd 
 |-  ( ph -> E e. CRing )
16 5 11 sylib 
 |-  ( ph -> ( E e. DivRing /\ F e. ( SubRing ` E ) /\ ( E |`s F ) e. DivRing ) )
17 16 simp2d 
 |-  ( ph -> F e. ( SubRing ` E ) )
18 eqid 
 |-  ( E ^s B ) = ( E ^s B )
19 eqid 
 |-  ( E |`s F ) = ( E |`s F )
20 eqid 
 |-  ( Poly1 ` ( E |`s F ) ) = ( Poly1 ` ( E |`s F ) )
21 1 6 18 19 20 evls1rhm 
 |-  ( ( E e. CRing /\ F e. ( SubRing ` E ) ) -> O e. ( ( Poly1 ` ( E |`s F ) ) RingHom ( E ^s B ) ) )
22 15 17 21 syl2anc 
 |-  ( ph -> O e. ( ( Poly1 ` ( E |`s F ) ) RingHom ( E ^s B ) ) )
23 eqid 
 |-  ( Base ` ( Poly1 ` ( E |`s F ) ) ) = ( Base ` ( Poly1 ` ( E |`s F ) ) )
24 eqid 
 |-  ( Base ` ( E ^s B ) ) = ( Base ` ( E ^s B ) )
25 23 24 rhmf 
 |-  ( O e. ( ( Poly1 ` ( E |`s F ) ) RingHom ( E ^s B ) ) -> O : ( Base ` ( Poly1 ` ( E |`s F ) ) ) --> ( Base ` ( E ^s B ) ) )
26 22 25 syl 
 |-  ( ph -> O : ( Base ` ( Poly1 ` ( E |`s F ) ) ) --> ( Base ` ( E ^s B ) ) )
27 26 fdmd 
 |-  ( ph -> dom O = ( Base ` ( Poly1 ` ( E |`s F ) ) ) )
28 7 27 eleqtrd 
 |-  ( ph -> P e. ( Base ` ( Poly1 ` ( E |`s F ) ) ) )
29 eqid 
 |-  ( Poly1 ` E ) = ( Poly1 ` E )
30 29 19 20 23 17 2 ressply10g 
 |-  ( ph -> Z = ( 0g ` ( Poly1 ` ( E |`s F ) ) ) )
31 8 30 neeqtrd 
 |-  ( ph -> P =/= ( 0g ` ( Poly1 ` ( E |`s F ) ) ) )
32 eqid 
 |-  ( 0g ` ( Poly1 ` ( E |`s F ) ) ) = ( 0g ` ( Poly1 ` ( E |`s F ) ) )
33 eqid 
 |-  ( Unic1p ` ( E |`s F ) ) = ( Unic1p ` ( E |`s F ) )
34 20 23 32 33 drnguc1p 
 |-  ( ( ( E |`s F ) e. DivRing /\ P e. ( Base ` ( Poly1 ` ( E |`s F ) ) ) /\ P =/= ( 0g ` ( Poly1 ` ( E |`s F ) ) ) ) -> P e. ( Unic1p ` ( E |`s F ) ) )
35 13 28 31 34 syl3anc 
 |-  ( ph -> P e. ( Unic1p ` ( E |`s F ) ) )
36 eqid 
 |-  ( Monic1p ` ( E |`s F ) ) = ( Monic1p ` ( E |`s F ) )
37 eqid 
 |-  ( .r ` ( Poly1 ` ( E |`s F ) ) ) = ( .r ` ( Poly1 ` ( E |`s F ) ) )
38 eqid 
 |-  ( algSc ` ( Poly1 ` ( E |`s F ) ) ) = ( algSc ` ( Poly1 ` ( E |`s F ) ) )
39 eqid 
 |-  ( deg1 ` ( E |`s F ) ) = ( deg1 ` ( E |`s F ) )
40 eqid 
 |-  ( invr ` ( E |`s F ) ) = ( invr ` ( E |`s F ) )
41 33 36 20 37 38 39 40 uc1pmon1p 
 |-  ( ( ( E |`s F ) e. Ring /\ P e. ( Unic1p ` ( E |`s F ) ) ) -> ( ( ( algSc ` ( Poly1 ` ( E |`s F ) ) ) ` ( ( invr ` ( E |`s F ) ) ` ( ( coe1 ` P ) ` ( ( deg1 ` ( E |`s F ) ) ` P ) ) ) ) ( .r ` ( Poly1 ` ( E |`s F ) ) ) P ) e. ( Monic1p ` ( E |`s F ) ) )
42 14 35 41 syl2anc 
 |-  ( ph -> ( ( ( algSc ` ( Poly1 ` ( E |`s F ) ) ) ` ( ( invr ` ( E |`s F ) ) ` ( ( coe1 ` P ) ` ( ( deg1 ` ( E |`s F ) ) ` P ) ) ) ) ( .r ` ( Poly1 ` ( E |`s F ) ) ) P ) e. ( Monic1p ` ( E |`s F ) ) )
43 simpr 
 |-  ( ( ph /\ p = ( ( ( algSc ` ( Poly1 ` ( E |`s F ) ) ) ` ( ( invr ` ( E |`s F ) ) ` ( ( coe1 ` P ) ` ( ( deg1 ` ( E |`s F ) ) ` P ) ) ) ) ( .r ` ( Poly1 ` ( E |`s F ) ) ) P ) ) -> p = ( ( ( algSc ` ( Poly1 ` ( E |`s F ) ) ) ` ( ( invr ` ( E |`s F ) ) ` ( ( coe1 ` P ) ` ( ( deg1 ` ( E |`s F ) ) ` P ) ) ) ) ( .r ` ( Poly1 ` ( E |`s F ) ) ) P ) )
44 43 fveq2d 
 |-  ( ( ph /\ p = ( ( ( algSc ` ( Poly1 ` ( E |`s F ) ) ) ` ( ( invr ` ( E |`s F ) ) ` ( ( coe1 ` P ) ` ( ( deg1 ` ( E |`s F ) ) ` P ) ) ) ) ( .r ` ( Poly1 ` ( E |`s F ) ) ) P ) ) -> ( O ` p ) = ( O ` ( ( ( algSc ` ( Poly1 ` ( E |`s F ) ) ) ` ( ( invr ` ( E |`s F ) ) ` ( ( coe1 ` P ) ` ( ( deg1 ` ( E |`s F ) ) ` P ) ) ) ) ( .r ` ( Poly1 ` ( E |`s F ) ) ) P ) ) )
45 44 fveq1d 
 |-  ( ( ph /\ p = ( ( ( algSc ` ( Poly1 ` ( E |`s F ) ) ) ` ( ( invr ` ( E |`s F ) ) ` ( ( coe1 ` P ) ` ( ( deg1 ` ( E |`s F ) ) ` P ) ) ) ) ( .r ` ( Poly1 ` ( E |`s F ) ) ) P ) ) -> ( ( O ` p ) ` X ) = ( ( O ` ( ( ( algSc ` ( Poly1 ` ( E |`s F ) ) ) ` ( ( invr ` ( E |`s F ) ) ` ( ( coe1 ` P ) ` ( ( deg1 ` ( E |`s F ) ) ` P ) ) ) ) ( .r ` ( Poly1 ` ( E |`s F ) ) ) P ) ) ` X ) )
46 45 eqeq1d 
 |-  ( ( ph /\ p = ( ( ( algSc ` ( Poly1 ` ( E |`s F ) ) ) ` ( ( invr ` ( E |`s F ) ) ` ( ( coe1 ` P ) ` ( ( deg1 ` ( E |`s F ) ) ` P ) ) ) ) ( .r ` ( Poly1 ` ( E |`s F ) ) ) P ) ) -> ( ( ( O ` p ) ` X ) = .0. <-> ( ( O ` ( ( ( algSc ` ( Poly1 ` ( E |`s F ) ) ) ` ( ( invr ` ( E |`s F ) ) ` ( ( coe1 ` P ) ` ( ( deg1 ` ( E |`s F ) ) ` P ) ) ) ) ( .r ` ( Poly1 ` ( E |`s F ) ) ) P ) ) ` X ) = .0. ) )
47 eqid 
 |-  ( .r ` E ) = ( .r ` E )
48 eqid 
 |-  ( Scalar ` ( Poly1 ` ( E |`s F ) ) ) = ( Scalar ` ( Poly1 ` ( E |`s F ) ) )
49 fldsdrgfld 
 |-  ( ( E e. Field /\ F e. ( SubDRing ` E ) ) -> ( E |`s F ) e. Field )
50 4 5 49 syl2anc 
 |-  ( ph -> ( E |`s F ) e. Field )
51 50 fldcrngd 
 |-  ( ph -> ( E |`s F ) e. CRing )
52 20 ply1assa 
 |-  ( ( E |`s F ) e. CRing -> ( Poly1 ` ( E |`s F ) ) e. AssAlg )
53 51 52 syl 
 |-  ( ph -> ( Poly1 ` ( E |`s F ) ) e. AssAlg )
54 assaring 
 |-  ( ( Poly1 ` ( E |`s F ) ) e. AssAlg -> ( Poly1 ` ( E |`s F ) ) e. Ring )
55 53 54 syl 
 |-  ( ph -> ( Poly1 ` ( E |`s F ) ) e. Ring )
56 20 ply1lmod 
 |-  ( ( E |`s F ) e. Ring -> ( Poly1 ` ( E |`s F ) ) e. LMod )
57 14 56 syl 
 |-  ( ph -> ( Poly1 ` ( E |`s F ) ) e. LMod )
58 eqid 
 |-  ( Base ` ( Scalar ` ( Poly1 ` ( E |`s F ) ) ) ) = ( Base ` ( Scalar ` ( Poly1 ` ( E |`s F ) ) ) )
59 38 48 55 57 58 23 asclf 
 |-  ( ph -> ( algSc ` ( Poly1 ` ( E |`s F ) ) ) : ( Base ` ( Scalar ` ( Poly1 ` ( E |`s F ) ) ) ) --> ( Base ` ( Poly1 ` ( E |`s F ) ) ) )
60 eqid 
 |-  ( Base ` ( E |`s F ) ) = ( Base ` ( E |`s F ) )
61 eqid 
 |-  ( 0g ` ( E |`s F ) ) = ( 0g ` ( E |`s F ) )
62 39 20 32 23 deg1nn0cl 
 |-  ( ( ( E |`s F ) e. Ring /\ P e. ( Base ` ( Poly1 ` ( E |`s F ) ) ) /\ P =/= ( 0g ` ( Poly1 ` ( E |`s F ) ) ) ) -> ( ( deg1 ` ( E |`s F ) ) ` P ) e. NN0 )
63 14 28 31 62 syl3anc 
 |-  ( ph -> ( ( deg1 ` ( E |`s F ) ) ` P ) e. NN0 )
64 eqid 
 |-  ( coe1 ` P ) = ( coe1 ` P )
65 64 23 20 60 coe1fvalcl 
 |-  ( ( P e. ( Base ` ( Poly1 ` ( E |`s F ) ) ) /\ ( ( deg1 ` ( E |`s F ) ) ` P ) e. NN0 ) -> ( ( coe1 ` P ) ` ( ( deg1 ` ( E |`s F ) ) ` P ) ) e. ( Base ` ( E |`s F ) ) )
66 28 63 65 syl2anc 
 |-  ( ph -> ( ( coe1 ` P ) ` ( ( deg1 ` ( E |`s F ) ) ` P ) ) e. ( Base ` ( E |`s F ) ) )
67 39 20 32 23 61 64 deg1ldg 
 |-  ( ( ( E |`s F ) e. Ring /\ P e. ( Base ` ( Poly1 ` ( E |`s F ) ) ) /\ P =/= ( 0g ` ( Poly1 ` ( E |`s F ) ) ) ) -> ( ( coe1 ` P ) ` ( ( deg1 ` ( E |`s F ) ) ` P ) ) =/= ( 0g ` ( E |`s F ) ) )
68 14 28 31 67 syl3anc 
 |-  ( ph -> ( ( coe1 ` P ) ` ( ( deg1 ` ( E |`s F ) ) ` P ) ) =/= ( 0g ` ( E |`s F ) ) )
69 60 61 40 13 66 68 drnginvrcld 
 |-  ( ph -> ( ( invr ` ( E |`s F ) ) ` ( ( coe1 ` P ) ` ( ( deg1 ` ( E |`s F ) ) ` P ) ) ) e. ( Base ` ( E |`s F ) ) )
70 20 ply1sca 
 |-  ( ( E |`s F ) e. Field -> ( E |`s F ) = ( Scalar ` ( Poly1 ` ( E |`s F ) ) ) )
71 50 70 syl 
 |-  ( ph -> ( E |`s F ) = ( Scalar ` ( Poly1 ` ( E |`s F ) ) ) )
72 71 fveq2d 
 |-  ( ph -> ( Base ` ( E |`s F ) ) = ( Base ` ( Scalar ` ( Poly1 ` ( E |`s F ) ) ) ) )
73 69 72 eleqtrd 
 |-  ( ph -> ( ( invr ` ( E |`s F ) ) ` ( ( coe1 ` P ) ` ( ( deg1 ` ( E |`s F ) ) ` P ) ) ) e. ( Base ` ( Scalar ` ( Poly1 ` ( E |`s F ) ) ) ) )
74 59 73 ffvelcdmd 
 |-  ( ph -> ( ( algSc ` ( Poly1 ` ( E |`s F ) ) ) ` ( ( invr ` ( E |`s F ) ) ` ( ( coe1 ` P ) ` ( ( deg1 ` ( E |`s F ) ) ` P ) ) ) ) e. ( Base ` ( Poly1 ` ( E |`s F ) ) ) )
75 1 6 20 19 23 37 47 15 17 74 28 10 evls1muld 
 |-  ( ph -> ( ( O ` ( ( ( algSc ` ( Poly1 ` ( E |`s F ) ) ) ` ( ( invr ` ( E |`s F ) ) ` ( ( coe1 ` P ) ` ( ( deg1 ` ( E |`s F ) ) ` P ) ) ) ) ( .r ` ( Poly1 ` ( E |`s F ) ) ) P ) ) ` X ) = ( ( ( O ` ( ( algSc ` ( Poly1 ` ( E |`s F ) ) ) ` ( ( invr ` ( E |`s F ) ) ` ( ( coe1 ` P ) ` ( ( deg1 ` ( E |`s F ) ) ` P ) ) ) ) ) ` X ) ( .r ` E ) ( ( O ` P ) ` X ) ) )
76 9 oveq2d 
 |-  ( ph -> ( ( ( O ` ( ( algSc ` ( Poly1 ` ( E |`s F ) ) ) ` ( ( invr ` ( E |`s F ) ) ` ( ( coe1 ` P ) ` ( ( deg1 ` ( E |`s F ) ) ` P ) ) ) ) ) ` X ) ( .r ` E ) ( ( O ` P ) ` X ) ) = ( ( ( O ` ( ( algSc ` ( Poly1 ` ( E |`s F ) ) ) ` ( ( invr ` ( E |`s F ) ) ` ( ( coe1 ` P ) ` ( ( deg1 ` ( E |`s F ) ) ` P ) ) ) ) ) ` X ) ( .r ` E ) .0. ) )
77 15 crngringd 
 |-  ( ph -> E e. Ring )
78 6 fvexi 
 |-  B e. _V
79 78 a1i 
 |-  ( ph -> B e. _V )
80 26 74 ffvelcdmd 
 |-  ( ph -> ( O ` ( ( algSc ` ( Poly1 ` ( E |`s F ) ) ) ` ( ( invr ` ( E |`s F ) ) ` ( ( coe1 ` P ) ` ( ( deg1 ` ( E |`s F ) ) ` P ) ) ) ) ) e. ( Base ` ( E ^s B ) ) )
81 18 6 24 4 79 80 pwselbas 
 |-  ( ph -> ( O ` ( ( algSc ` ( Poly1 ` ( E |`s F ) ) ) ` ( ( invr ` ( E |`s F ) ) ` ( ( coe1 ` P ) ` ( ( deg1 ` ( E |`s F ) ) ` P ) ) ) ) ) : B --> B )
82 81 10 ffvelcdmd 
 |-  ( ph -> ( ( O ` ( ( algSc ` ( Poly1 ` ( E |`s F ) ) ) ` ( ( invr ` ( E |`s F ) ) ` ( ( coe1 ` P ) ` ( ( deg1 ` ( E |`s F ) ) ` P ) ) ) ) ) ` X ) e. B )
83 6 47 3 ringrz 
 |-  ( ( E e. Ring /\ ( ( O ` ( ( algSc ` ( Poly1 ` ( E |`s F ) ) ) ` ( ( invr ` ( E |`s F ) ) ` ( ( coe1 ` P ) ` ( ( deg1 ` ( E |`s F ) ) ` P ) ) ) ) ) ` X ) e. B ) -> ( ( ( O ` ( ( algSc ` ( Poly1 ` ( E |`s F ) ) ) ` ( ( invr ` ( E |`s F ) ) ` ( ( coe1 ` P ) ` ( ( deg1 ` ( E |`s F ) ) ` P ) ) ) ) ) ` X ) ( .r ` E ) .0. ) = .0. )
84 77 82 83 syl2anc 
 |-  ( ph -> ( ( ( O ` ( ( algSc ` ( Poly1 ` ( E |`s F ) ) ) ` ( ( invr ` ( E |`s F ) ) ` ( ( coe1 ` P ) ` ( ( deg1 ` ( E |`s F ) ) ` P ) ) ) ) ) ` X ) ( .r ` E ) .0. ) = .0. )
85 75 76 84 3eqtrd 
 |-  ( ph -> ( ( O ` ( ( ( algSc ` ( Poly1 ` ( E |`s F ) ) ) ` ( ( invr ` ( E |`s F ) ) ` ( ( coe1 ` P ) ` ( ( deg1 ` ( E |`s F ) ) ` P ) ) ) ) ( .r ` ( Poly1 ` ( E |`s F ) ) ) P ) ) ` X ) = .0. )
86 42 46 85 rspcedvd 
 |-  ( ph -> E. p e. ( Monic1p ` ( E |`s F ) ) ( ( O ` p ) ` X ) = .0. )
87 1 19 6 3 15 17 elirng 
 |-  ( ph -> ( X e. ( E IntgRing F ) <-> ( X e. B /\ E. p e. ( Monic1p ` ( E |`s F ) ) ( ( O ` p ) ` X ) = .0. ) ) )
88 10 86 87 mpbir2and 
 |-  ( ph -> X e. ( E IntgRing F ) )