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 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 ) )
Assertion irngnzply1 
|- ( ph -> ( E IntgRing F ) = U_ p e. ( dom O \ { Z } ) ( `' ( O ` p ) " { .0. } ) )

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 eqid 
 |-  ( E |`s F ) = ( E |`s F )
7 eqid 
 |-  ( Base ` E ) = ( Base ` E )
8 4 fldcrngd 
 |-  ( ph -> E e. CRing )
9 issdrg 
 |-  ( F e. ( SubDRing ` E ) <-> ( E e. DivRing /\ F e. ( SubRing ` E ) /\ ( E |`s F ) e. DivRing ) )
10 5 9 sylib 
 |-  ( ph -> ( E e. DivRing /\ F e. ( SubRing ` E ) /\ ( E |`s F ) e. DivRing ) )
11 10 simp2d 
 |-  ( ph -> F e. ( SubRing ` E ) )
12 1 6 7 3 8 11 elirng 
 |-  ( ph -> ( x e. ( E IntgRing F ) <-> ( x e. ( Base ` E ) /\ E. p e. ( Monic1p ` ( E |`s F ) ) ( ( O ` p ) ` x ) = .0. ) ) )
13 12 biimpa 
 |-  ( ( ph /\ x e. ( E IntgRing F ) ) -> ( x e. ( Base ` E ) /\ E. p e. ( Monic1p ` ( E |`s F ) ) ( ( O ` p ) ` x ) = .0. ) )
14 13 simprd 
 |-  ( ( ph /\ x e. ( E IntgRing F ) ) -> E. p e. ( Monic1p ` ( E |`s F ) ) ( ( O ` p ) ` x ) = .0. )
15 eqid 
 |-  ( Poly1 ` ( E |`s F ) ) = ( Poly1 ` ( E |`s F ) )
16 eqid 
 |-  ( Base ` ( Poly1 ` ( E |`s F ) ) ) = ( Base ` ( Poly1 ` ( E |`s F ) ) )
17 eqid 
 |-  ( Monic1p ` ( E |`s F ) ) = ( Monic1p ` ( E |`s F ) )
18 15 16 17 mon1pcl 
 |-  ( p e. ( Monic1p ` ( E |`s F ) ) -> p e. ( Base ` ( Poly1 ` ( E |`s F ) ) ) )
19 18 adantl 
 |-  ( ( ph /\ p e. ( Monic1p ` ( E |`s F ) ) ) -> p e. ( Base ` ( Poly1 ` ( E |`s F ) ) ) )
20 eqid 
 |-  ( E ^s ( Base ` E ) ) = ( E ^s ( Base ` E ) )
21 1 7 20 6 15 evls1rhm 
 |-  ( ( E e. CRing /\ F e. ( SubRing ` E ) ) -> O e. ( ( Poly1 ` ( E |`s F ) ) RingHom ( E ^s ( Base ` E ) ) ) )
22 8 11 21 syl2anc 
 |-  ( ph -> O e. ( ( Poly1 ` ( E |`s F ) ) RingHom ( E ^s ( Base ` E ) ) ) )
23 eqid 
 |-  ( Base ` ( E ^s ( Base ` E ) ) ) = ( Base ` ( E ^s ( Base ` E ) ) )
24 16 23 rhmf 
 |-  ( O e. ( ( Poly1 ` ( E |`s F ) ) RingHom ( E ^s ( Base ` E ) ) ) -> O : ( Base ` ( Poly1 ` ( E |`s F ) ) ) --> ( Base ` ( E ^s ( Base ` E ) ) ) )
25 22 24 syl 
 |-  ( ph -> O : ( Base ` ( Poly1 ` ( E |`s F ) ) ) --> ( Base ` ( E ^s ( Base ` E ) ) ) )
26 25 fdmd 
 |-  ( ph -> dom O = ( Base ` ( Poly1 ` ( E |`s F ) ) ) )
27 26 adantr 
 |-  ( ( ph /\ p e. ( Monic1p ` ( E |`s F ) ) ) -> dom O = ( Base ` ( Poly1 ` ( E |`s F ) ) ) )
28 19 27 eleqtrrd 
 |-  ( ( ph /\ p e. ( Monic1p ` ( E |`s F ) ) ) -> p e. dom O )
29 eqid 
 |-  ( 0g ` ( Poly1 ` ( E |`s F ) ) ) = ( 0g ` ( Poly1 ` ( E |`s F ) ) )
30 15 29 17 mon1pn0 
 |-  ( p e. ( Monic1p ` ( E |`s F ) ) -> p =/= ( 0g ` ( Poly1 ` ( E |`s F ) ) ) )
31 30 adantl 
 |-  ( ( ph /\ p e. ( Monic1p ` ( E |`s F ) ) ) -> p =/= ( 0g ` ( Poly1 ` ( E |`s F ) ) ) )
32 eqid 
 |-  ( Poly1 ` E ) = ( Poly1 ` E )
33 32 6 15 16 11 2 ressply10g 
 |-  ( ph -> Z = ( 0g ` ( Poly1 ` ( E |`s F ) ) ) )
34 33 adantr 
 |-  ( ( ph /\ p e. ( Monic1p ` ( E |`s F ) ) ) -> Z = ( 0g ` ( Poly1 ` ( E |`s F ) ) ) )
35 31 34 neeqtrrd 
 |-  ( ( ph /\ p e. ( Monic1p ` ( E |`s F ) ) ) -> p =/= Z )
36 eldifsn 
 |-  ( p e. ( dom O \ { Z } ) <-> ( p e. dom O /\ p =/= Z ) )
37 28 35 36 sylanbrc 
 |-  ( ( ph /\ p e. ( Monic1p ` ( E |`s F ) ) ) -> p e. ( dom O \ { Z } ) )
38 37 ad2ant2r 
 |-  ( ( ( ph /\ x e. ( E IntgRing F ) ) /\ ( p e. ( Monic1p ` ( E |`s F ) ) /\ ( ( O ` p ) ` x ) = .0. ) ) -> p e. ( dom O \ { Z } ) )
39 4 ad2antrr 
 |-  ( ( ( ph /\ x e. ( E IntgRing F ) ) /\ ( p e. ( Monic1p ` ( E |`s F ) ) /\ ( ( O ` p ) ` x ) = .0. ) ) -> E e. Field )
40 fvexd 
 |-  ( ( ( ph /\ x e. ( E IntgRing F ) ) /\ ( p e. ( Monic1p ` ( E |`s F ) ) /\ ( ( O ` p ) ` x ) = .0. ) ) -> ( Base ` E ) e. _V )
41 25 ad2antrr 
 |-  ( ( ( ph /\ x e. ( E IntgRing F ) ) /\ ( p e. ( Monic1p ` ( E |`s F ) ) /\ ( ( O ` p ) ` x ) = .0. ) ) -> O : ( Base ` ( Poly1 ` ( E |`s F ) ) ) --> ( Base ` ( E ^s ( Base ` E ) ) ) )
42 18 ad2antrl 
 |-  ( ( ( ph /\ x e. ( E IntgRing F ) ) /\ ( p e. ( Monic1p ` ( E |`s F ) ) /\ ( ( O ` p ) ` x ) = .0. ) ) -> p e. ( Base ` ( Poly1 ` ( E |`s F ) ) ) )
43 41 42 ffvelcdmd 
 |-  ( ( ( ph /\ x e. ( E IntgRing F ) ) /\ ( p e. ( Monic1p ` ( E |`s F ) ) /\ ( ( O ` p ) ` x ) = .0. ) ) -> ( O ` p ) e. ( Base ` ( E ^s ( Base ` E ) ) ) )
44 20 7 23 39 40 43 pwselbas 
 |-  ( ( ( ph /\ x e. ( E IntgRing F ) ) /\ ( p e. ( Monic1p ` ( E |`s F ) ) /\ ( ( O ` p ) ` x ) = .0. ) ) -> ( O ` p ) : ( Base ` E ) --> ( Base ` E ) )
45 44 ffnd 
 |-  ( ( ( ph /\ x e. ( E IntgRing F ) ) /\ ( p e. ( Monic1p ` ( E |`s F ) ) /\ ( ( O ` p ) ` x ) = .0. ) ) -> ( O ` p ) Fn ( Base ` E ) )
46 13 simpld 
 |-  ( ( ph /\ x e. ( E IntgRing F ) ) -> x e. ( Base ` E ) )
47 46 adantr 
 |-  ( ( ( ph /\ x e. ( E IntgRing F ) ) /\ ( p e. ( Monic1p ` ( E |`s F ) ) /\ ( ( O ` p ) ` x ) = .0. ) ) -> x e. ( Base ` E ) )
48 simprr 
 |-  ( ( ( ph /\ x e. ( E IntgRing F ) ) /\ ( p e. ( Monic1p ` ( E |`s F ) ) /\ ( ( O ` p ) ` x ) = .0. ) ) -> ( ( O ` p ) ` x ) = .0. )
49 fniniseg 
 |-  ( ( O ` p ) Fn ( Base ` E ) -> ( x e. ( `' ( O ` p ) " { .0. } ) <-> ( x e. ( Base ` E ) /\ ( ( O ` p ) ` x ) = .0. ) ) )
50 49 biimpar 
 |-  ( ( ( O ` p ) Fn ( Base ` E ) /\ ( x e. ( Base ` E ) /\ ( ( O ` p ) ` x ) = .0. ) ) -> x e. ( `' ( O ` p ) " { .0. } ) )
51 45 47 48 50 syl12anc 
 |-  ( ( ( ph /\ x e. ( E IntgRing F ) ) /\ ( p e. ( Monic1p ` ( E |`s F ) ) /\ ( ( O ` p ) ` x ) = .0. ) ) -> x e. ( `' ( O ` p ) " { .0. } ) )
52 14 38 51 reximssdv 
 |-  ( ( ph /\ x e. ( E IntgRing F ) ) -> E. p e. ( dom O \ { Z } ) x e. ( `' ( O ` p ) " { .0. } ) )
53 eliun 
 |-  ( x e. U_ p e. ( dom O \ { Z } ) ( `' ( O ` p ) " { .0. } ) <-> E. p e. ( dom O \ { Z } ) x e. ( `' ( O ` p ) " { .0. } ) )
54 52 53 sylibr 
 |-  ( ( ph /\ x e. ( E IntgRing F ) ) -> x e. U_ p e. ( dom O \ { Z } ) ( `' ( O ` p ) " { .0. } ) )
55 nfv 
 |-  F/ p ph
56 nfiu1 
 |-  F/_ p U_ p e. ( dom O \ { Z } ) ( `' ( O ` p ) " { .0. } )
57 56 nfcri 
 |-  F/ p x e. U_ p e. ( dom O \ { Z } ) ( `' ( O ` p ) " { .0. } )
58 55 57 nfan 
 |-  F/ p ( ph /\ x e. U_ p e. ( dom O \ { Z } ) ( `' ( O ` p ) " { .0. } ) )
59 4 ad2antrr 
 |-  ( ( ( ph /\ p e. ( dom O \ { Z } ) ) /\ x e. ( `' ( O ` p ) " { .0. } ) ) -> E e. Field )
60 5 ad2antrr 
 |-  ( ( ( ph /\ p e. ( dom O \ { Z } ) ) /\ x e. ( `' ( O ` p ) " { .0. } ) ) -> F e. ( SubDRing ` E ) )
61 eldifi 
 |-  ( p e. ( dom O \ { Z } ) -> p e. dom O )
62 61 adantl 
 |-  ( ( ph /\ p e. ( dom O \ { Z } ) ) -> p e. dom O )
63 62 adantr 
 |-  ( ( ( ph /\ p e. ( dom O \ { Z } ) ) /\ x e. ( `' ( O ` p ) " { .0. } ) ) -> p e. dom O )
64 eldifsni 
 |-  ( p e. ( dom O \ { Z } ) -> p =/= Z )
65 64 adantl 
 |-  ( ( ph /\ p e. ( dom O \ { Z } ) ) -> p =/= Z )
66 65 adantr 
 |-  ( ( ( ph /\ p e. ( dom O \ { Z } ) ) /\ x e. ( `' ( O ` p ) " { .0. } ) ) -> p =/= Z )
67 4 adantr 
 |-  ( ( ph /\ p e. ( dom O \ { Z } ) ) -> E e. Field )
68 fvexd 
 |-  ( ( ph /\ p e. ( dom O \ { Z } ) ) -> ( Base ` E ) e. _V )
69 25 adantr 
 |-  ( ( ph /\ p e. ( dom O \ { Z } ) ) -> O : ( Base ` ( Poly1 ` ( E |`s F ) ) ) --> ( Base ` ( E ^s ( Base ` E ) ) ) )
70 26 adantr 
 |-  ( ( ph /\ p e. ( dom O \ { Z } ) ) -> dom O = ( Base ` ( Poly1 ` ( E |`s F ) ) ) )
71 62 70 eleqtrd 
 |-  ( ( ph /\ p e. ( dom O \ { Z } ) ) -> p e. ( Base ` ( Poly1 ` ( E |`s F ) ) ) )
72 69 71 ffvelcdmd 
 |-  ( ( ph /\ p e. ( dom O \ { Z } ) ) -> ( O ` p ) e. ( Base ` ( E ^s ( Base ` E ) ) ) )
73 20 7 23 67 68 72 pwselbas 
 |-  ( ( ph /\ p e. ( dom O \ { Z } ) ) -> ( O ` p ) : ( Base ` E ) --> ( Base ` E ) )
74 73 ffnd 
 |-  ( ( ph /\ p e. ( dom O \ { Z } ) ) -> ( O ` p ) Fn ( Base ` E ) )
75 49 biimpa 
 |-  ( ( ( O ` p ) Fn ( Base ` E ) /\ x e. ( `' ( O ` p ) " { .0. } ) ) -> ( x e. ( Base ` E ) /\ ( ( O ` p ) ` x ) = .0. ) )
76 74 75 sylan 
 |-  ( ( ( ph /\ p e. ( dom O \ { Z } ) ) /\ x e. ( `' ( O ` p ) " { .0. } ) ) -> ( x e. ( Base ` E ) /\ ( ( O ` p ) ` x ) = .0. ) )
77 76 simprd 
 |-  ( ( ( ph /\ p e. ( dom O \ { Z } ) ) /\ x e. ( `' ( O ` p ) " { .0. } ) ) -> ( ( O ` p ) ` x ) = .0. )
78 76 simpld 
 |-  ( ( ( ph /\ p e. ( dom O \ { Z } ) ) /\ x e. ( `' ( O ` p ) " { .0. } ) ) -> x e. ( Base ` E ) )
79 1 2 3 59 60 7 63 66 77 78 irngnzply1lem 
 |-  ( ( ( ph /\ p e. ( dom O \ { Z } ) ) /\ x e. ( `' ( O ` p ) " { .0. } ) ) -> x e. ( E IntgRing F ) )
80 79 adantllr 
 |-  ( ( ( ( ph /\ x e. U_ p e. ( dom O \ { Z } ) ( `' ( O ` p ) " { .0. } ) ) /\ p e. ( dom O \ { Z } ) ) /\ x e. ( `' ( O ` p ) " { .0. } ) ) -> x e. ( E IntgRing F ) )
81 53 biimpi 
 |-  ( x e. U_ p e. ( dom O \ { Z } ) ( `' ( O ` p ) " { .0. } ) -> E. p e. ( dom O \ { Z } ) x e. ( `' ( O ` p ) " { .0. } ) )
82 81 adantl 
 |-  ( ( ph /\ x e. U_ p e. ( dom O \ { Z } ) ( `' ( O ` p ) " { .0. } ) ) -> E. p e. ( dom O \ { Z } ) x e. ( `' ( O ` p ) " { .0. } ) )
83 58 80 82 r19.29af 
 |-  ( ( ph /\ x e. U_ p e. ( dom O \ { Z } ) ( `' ( O ` p ) " { .0. } ) ) -> x e. ( E IntgRing F ) )
84 54 83 impbida 
 |-  ( ph -> ( x e. ( E IntgRing F ) <-> x e. U_ p e. ( dom O \ { Z } ) ( `' ( O ` p ) " { .0. } ) ) )
85 84 eqrdv 
 |-  ( ph -> ( E IntgRing F ) = U_ p e. ( dom O \ { Z } ) ( `' ( O ` p ) " { .0. } ) )