Metamath Proof Explorer

Theorem irngss

Description: All elements of a subring S are integral over S . This is only true in the case of a nonzero ring, since there are no integral elements in a zero ring (see 0ringirng ). (Contributed by Thierry Arnoux, 28-Jan-2025)

Ref Expression
Hypotheses irngval.o 
|- O = ( R evalSub1 S )
irngval.u 
|- U = ( R |`s S )
irngval.b 
|- B = ( Base ` R )
irngval.0 
|- .0. = ( 0g ` R )
elirng.r 
|- ( ph -> R e. CRing )
elirng.s 
|- ( ph -> S e. ( SubRing ` R ) )
irngss.1 
|- ( ph -> R e. NzRing )
Assertion irngss 
|- ( ph -> S C_ ( R IntgRing S ) )

Proof

Step Hyp Ref Expression
1 irngval.o 
 |-  O = ( R evalSub1 S )
2 irngval.u 
 |-  U = ( R |`s S )
3 irngval.b 
 |-  B = ( Base ` R )
4 irngval.0 
 |-  .0. = ( 0g ` R )
5 elirng.r 
 |-  ( ph -> R e. CRing )
6 elirng.s 
 |-  ( ph -> S e. ( SubRing ` R ) )
7 irngss.1 
 |-  ( ph -> R e. NzRing )
8 simpl 
 |-  ( ( ph /\ x e. S ) -> ph )
9 3 subrgss 
 |-  ( S e. ( SubRing ` R ) -> S C_ B )
10 6 9 syl 
 |-  ( ph -> S C_ B )
11 10 sselda 
 |-  ( ( ph /\ x e. S ) -> x e. B )
12 eqid 
 |-  ( Poly1 ` R ) = ( Poly1 ` R )
13 eqid 
 |-  ( Poly1 ` U ) = ( Poly1 ` U )
14 eqid 
 |-  ( Base ` ( Poly1 ` U ) ) = ( Base ` ( Poly1 ` U ) )
15 6 adantr 
 |-  ( ( ph /\ x e. S ) -> S e. ( SubRing ` R ) )
16 eqid 
 |-  ( ( Poly1 ` R ) |`s ( Base ` ( Poly1 ` U ) ) ) = ( ( Poly1 ` R ) |`s ( Base ` ( Poly1 ` U ) ) )
17 eqid 
 |-  ( var1 ` R ) = ( var1 ` R )
18 17 15 2 13 14 subrgvr1cl 
 |-  ( ( ph /\ x e. S ) -> ( var1 ` R ) e. ( Base ` ( Poly1 ` U ) ) )
19 eqid 
 |-  ( algSc ` ( Poly1 ` R ) ) = ( algSc ` ( Poly1 ` R ) )
20 simpr 
 |-  ( ( ph /\ x e. S ) -> x e. S )
21 19 2 12 13 14 15 20 asclply1subcl 
 |-  ( ( ph /\ x e. S ) -> ( ( algSc ` ( Poly1 ` R ) ) ` x ) e. ( Base ` ( Poly1 ` U ) ) )
22 12 2 13 14 15 16 18 21 ressply1sub 
 |-  ( ( ph /\ x e. S ) -> ( ( var1 ` R ) ( -g ` ( Poly1 ` U ) ) ( ( algSc ` ( Poly1 ` R ) ) ` x ) ) = ( ( var1 ` R ) ( -g ` ( ( Poly1 ` R ) |`s ( Base ` ( Poly1 ` U ) ) ) ) ( ( algSc ` ( Poly1 ` R ) ) ` x ) ) )
23 12 2 13 14 subrgply1 
 |-  ( S e. ( SubRing ` R ) -> ( Base ` ( Poly1 ` U ) ) e. ( SubRing ` ( Poly1 ` R ) ) )
24 subrgsubg 
 |-  ( ( Base ` ( Poly1 ` U ) ) e. ( SubRing ` ( Poly1 ` R ) ) -> ( Base ` ( Poly1 ` U ) ) e. ( SubGrp ` ( Poly1 ` R ) ) )
25 6 23 24 3syl 
 |-  ( ph -> ( Base ` ( Poly1 ` U ) ) e. ( SubGrp ` ( Poly1 ` R ) ) )
26 25 adantr 
 |-  ( ( ph /\ x e. S ) -> ( Base ` ( Poly1 ` U ) ) e. ( SubGrp ` ( Poly1 ` R ) ) )
27 eqid 
 |-  ( -g ` ( Poly1 ` R ) ) = ( -g ` ( Poly1 ` R ) )
28 eqid 
 |-  ( -g ` ( ( Poly1 ` R ) |`s ( Base ` ( Poly1 ` U ) ) ) ) = ( -g ` ( ( Poly1 ` R ) |`s ( Base ` ( Poly1 ` U ) ) ) )
29 27 16 28 subgsub 
 |-  ( ( ( Base ` ( Poly1 ` U ) ) e. ( SubGrp ` ( Poly1 ` R ) ) /\ ( var1 ` R ) e. ( Base ` ( Poly1 ` U ) ) /\ ( ( algSc ` ( Poly1 ` R ) ) ` x ) e. ( Base ` ( Poly1 ` U ) ) ) -> ( ( var1 ` R ) ( -g ` ( Poly1 ` R ) ) ( ( algSc ` ( Poly1 ` R ) ) ` x ) ) = ( ( var1 ` R ) ( -g ` ( ( Poly1 ` R ) |`s ( Base ` ( Poly1 ` U ) ) ) ) ( ( algSc ` ( Poly1 ` R ) ) ` x ) ) )
30 26 18 21 29 syl3anc 
 |-  ( ( ph /\ x e. S ) -> ( ( var1 ` R ) ( -g ` ( Poly1 ` R ) ) ( ( algSc ` ( Poly1 ` R ) ) ` x ) ) = ( ( var1 ` R ) ( -g ` ( ( Poly1 ` R ) |`s ( Base ` ( Poly1 ` U ) ) ) ) ( ( algSc ` ( Poly1 ` R ) ) ` x ) ) )
31 22 30 eqtr4d 
 |-  ( ( ph /\ x e. S ) -> ( ( var1 ` R ) ( -g ` ( Poly1 ` U ) ) ( ( algSc ` ( Poly1 ` R ) ) ` x ) ) = ( ( var1 ` R ) ( -g ` ( Poly1 ` R ) ) ( ( algSc ` ( Poly1 ` R ) ) ` x ) ) )
32 2 subrgcrng 
 |-  ( ( R e. CRing /\ S e. ( SubRing ` R ) ) -> U e. CRing )
33 5 6 32 syl2anc 
 |-  ( ph -> U e. CRing )
34 13 ply1crng 
 |-  ( U e. CRing -> ( Poly1 ` U ) e. CRing )
35 33 34 syl 
 |-  ( ph -> ( Poly1 ` U ) e. CRing )
36 35 adantr 
 |-  ( ( ph /\ x e. S ) -> ( Poly1 ` U ) e. CRing )
37 36 crnggrpd 
 |-  ( ( ph /\ x e. S ) -> ( Poly1 ` U ) e. Grp )
38 eqid 
 |-  ( -g ` ( Poly1 ` U ) ) = ( -g ` ( Poly1 ` U ) )
39 14 38 grpsubcl 
 |-  ( ( ( Poly1 ` U ) e. Grp /\ ( var1 ` R ) e. ( Base ` ( Poly1 ` U ) ) /\ ( ( algSc ` ( Poly1 ` R ) ) ` x ) e. ( Base ` ( Poly1 ` U ) ) ) -> ( ( var1 ` R ) ( -g ` ( Poly1 ` U ) ) ( ( algSc ` ( Poly1 ` R ) ) ` x ) ) e. ( Base ` ( Poly1 ` U ) ) )
40 37 18 21 39 syl3anc 
 |-  ( ( ph /\ x e. S ) -> ( ( var1 ` R ) ( -g ` ( Poly1 ` U ) ) ( ( algSc ` ( Poly1 ` R ) ) ` x ) ) e. ( Base ` ( Poly1 ` U ) ) )
41 31 40 eqeltrrd 
 |-  ( ( ph /\ x e. S ) -> ( ( var1 ` R ) ( -g ` ( Poly1 ` R ) ) ( ( algSc ` ( Poly1 ` R ) ) ` x ) ) e. ( Base ` ( Poly1 ` U ) ) )
42 eqid 
 |-  ( Base ` ( Poly1 ` R ) ) = ( Base ` ( Poly1 ` R ) )
43 eqid 
 |-  ( ( var1 ` R ) ( -g ` ( Poly1 ` R ) ) ( ( algSc ` ( Poly1 ` R ) ) ` x ) ) = ( ( var1 ` R ) ( -g ` ( Poly1 ` R ) ) ( ( algSc ` ( Poly1 ` R ) ) ` x ) )
44 eqid 
 |-  ( eval1 ` R ) = ( eval1 ` R )
45 7 adantr 
 |-  ( ( ph /\ x e. S ) -> R e. NzRing )
46 5 adantr 
 |-  ( ( ph /\ x e. S ) -> R e. CRing )
47 eqid 
 |-  ( Monic1p ` R ) = ( Monic1p ` R )
48 eqid 
 |-  ( deg1 ` R ) = ( deg1 ` R )
49 12 42 3 17 27 19 43 44 45 46 11 47 48 4 ply1remlem 
 |-  ( ( ph /\ x e. S ) -> ( ( ( var1 ` R ) ( -g ` ( Poly1 ` R ) ) ( ( algSc ` ( Poly1 ` R ) ) ` x ) ) e. ( Monic1p ` R ) /\ ( ( deg1 ` R ) ` ( ( var1 ` R ) ( -g ` ( Poly1 ` R ) ) ( ( algSc ` ( Poly1 ` R ) ) ` x ) ) ) = 1 /\ ( `' ( ( eval1 ` R ) ` ( ( var1 ` R ) ( -g ` ( Poly1 ` R ) ) ( ( algSc ` ( Poly1 ` R ) ) ` x ) ) ) " { .0. } ) = { x } ) )
50 49 simp1d 
 |-  ( ( ph /\ x e. S ) -> ( ( var1 ` R ) ( -g ` ( Poly1 ` R ) ) ( ( algSc ` ( Poly1 ` R ) ) ` x ) ) e. ( Monic1p ` R ) )
51 41 50 elind 
 |-  ( ( ph /\ x e. S ) -> ( ( var1 ` R ) ( -g ` ( Poly1 ` R ) ) ( ( algSc ` ( Poly1 ` R ) ) ` x ) ) e. ( ( Base ` ( Poly1 ` U ) ) i^i ( Monic1p ` R ) ) )
52 eqid 
 |-  ( Monic1p ` U ) = ( Monic1p ` U )
53 12 2 13 14 6 47 52 ressply1mon1p 
 |-  ( ph -> ( Monic1p ` U ) = ( ( Base ` ( Poly1 ` U ) ) i^i ( Monic1p ` R ) ) )
54 53 adantr 
 |-  ( ( ph /\ x e. S ) -> ( Monic1p ` U ) = ( ( Base ` ( Poly1 ` U ) ) i^i ( Monic1p ` R ) ) )
55 51 54 eleqtrrd 
 |-  ( ( ph /\ x e. S ) -> ( ( var1 ` R ) ( -g ` ( Poly1 ` R ) ) ( ( algSc ` ( Poly1 ` R ) ) ` x ) ) e. ( Monic1p ` U ) )
56 fveq2 
 |-  ( f = ( ( var1 ` R ) ( -g ` ( Poly1 ` R ) ) ( ( algSc ` ( Poly1 ` R ) ) ` x ) ) -> ( O ` f ) = ( O ` ( ( var1 ` R ) ( -g ` ( Poly1 ` R ) ) ( ( algSc ` ( Poly1 ` R ) ) ` x ) ) ) )
57 56 fveq1d 
 |-  ( f = ( ( var1 ` R ) ( -g ` ( Poly1 ` R ) ) ( ( algSc ` ( Poly1 ` R ) ) ` x ) ) -> ( ( O ` f ) ` x ) = ( ( O ` ( ( var1 ` R ) ( -g ` ( Poly1 ` R ) ) ( ( algSc ` ( Poly1 ` R ) ) ` x ) ) ) ` x ) )
58 57 eqeq1d 
 |-  ( f = ( ( var1 ` R ) ( -g ` ( Poly1 ` R ) ) ( ( algSc ` ( Poly1 ` R ) ) ` x ) ) -> ( ( ( O ` f ) ` x ) = .0. <-> ( ( O ` ( ( var1 ` R ) ( -g ` ( Poly1 ` R ) ) ( ( algSc ` ( Poly1 ` R ) ) ` x ) ) ) ` x ) = .0. ) )
59 58 adantl 
 |-  ( ( ( ph /\ x e. S ) /\ f = ( ( var1 ` R ) ( -g ` ( Poly1 ` R ) ) ( ( algSc ` ( Poly1 ` R ) ) ` x ) ) ) -> ( ( ( O ` f ) ` x ) = .0. <-> ( ( O ` ( ( var1 ` R ) ( -g ` ( Poly1 ` R ) ) ( ( algSc ` ( Poly1 ` R ) ) ` x ) ) ) ` x ) = .0. ) )
60 1 3 13 2 14 44 46 15 ressply1evl 
 |-  ( ( ph /\ x e. S ) -> O = ( ( eval1 ` R ) |` ( Base ` ( Poly1 ` U ) ) ) )
61 60 fveq1d 
 |-  ( ( ph /\ x e. S ) -> ( O ` ( ( var1 ` R ) ( -g ` ( Poly1 ` R ) ) ( ( algSc ` ( Poly1 ` R ) ) ` x ) ) ) = ( ( ( eval1 ` R ) |` ( Base ` ( Poly1 ` U ) ) ) ` ( ( var1 ` R ) ( -g ` ( Poly1 ` R ) ) ( ( algSc ` ( Poly1 ` R ) ) ` x ) ) ) )
62 41 fvresd 
 |-  ( ( ph /\ x e. S ) -> ( ( ( eval1 ` R ) |` ( Base ` ( Poly1 ` U ) ) ) ` ( ( var1 ` R ) ( -g ` ( Poly1 ` R ) ) ( ( algSc ` ( Poly1 ` R ) ) ` x ) ) ) = ( ( eval1 ` R ) ` ( ( var1 ` R ) ( -g ` ( Poly1 ` R ) ) ( ( algSc ` ( Poly1 ` R ) ) ` x ) ) ) )
63 61 62 eqtrd 
 |-  ( ( ph /\ x e. S ) -> ( O ` ( ( var1 ` R ) ( -g ` ( Poly1 ` R ) ) ( ( algSc ` ( Poly1 ` R ) ) ` x ) ) ) = ( ( eval1 ` R ) ` ( ( var1 ` R ) ( -g ` ( Poly1 ` R ) ) ( ( algSc ` ( Poly1 ` R ) ) ` x ) ) ) )
64 63 fveq1d 
 |-  ( ( ph /\ x e. S ) -> ( ( O ` ( ( var1 ` R ) ( -g ` ( Poly1 ` R ) ) ( ( algSc ` ( Poly1 ` R ) ) ` x ) ) ) ` x ) = ( ( ( eval1 ` R ) ` ( ( var1 ` R ) ( -g ` ( Poly1 ` R ) ) ( ( algSc ` ( Poly1 ` R ) ) ` x ) ) ) ` x ) )
65 eqid 
 |-  ( R ^s B ) = ( R ^s B )
66 eqid 
 |-  ( Base ` ( R ^s B ) ) = ( Base ` ( R ^s B ) )
67 3 fvexi 
 |-  B e. _V
68 67 a1i 
 |-  ( ( ph /\ x e. S ) -> B e. _V )
69 44 12 65 3 evl1rhm 
 |-  ( R e. CRing -> ( eval1 ` R ) e. ( ( Poly1 ` R ) RingHom ( R ^s B ) ) )
70 42 66 rhmf 
 |-  ( ( eval1 ` R ) e. ( ( Poly1 ` R ) RingHom ( R ^s B ) ) -> ( eval1 ` R ) : ( Base ` ( Poly1 ` R ) ) --> ( Base ` ( R ^s B ) ) )
71 5 69 70 3syl 
 |-  ( ph -> ( eval1 ` R ) : ( Base ` ( Poly1 ` R ) ) --> ( Base ` ( R ^s B ) ) )
72 71 adantr 
 |-  ( ( ph /\ x e. S ) -> ( eval1 ` R ) : ( Base ` ( Poly1 ` R ) ) --> ( Base ` ( R ^s B ) ) )
73 eqid 
 |-  ( PwSer1 ` U ) = ( PwSer1 ` U )
74 eqid 
 |-  ( Base ` ( PwSer1 ` U ) ) = ( Base ` ( PwSer1 ` U ) )
75 12 2 13 14 6 73 74 42 ressply1bas2 
 |-  ( ph -> ( Base ` ( Poly1 ` U ) ) = ( ( Base ` ( PwSer1 ` U ) ) i^i ( Base ` ( Poly1 ` R ) ) ) )
76 75 adantr 
 |-  ( ( ph /\ x e. S ) -> ( Base ` ( Poly1 ` U ) ) = ( ( Base ` ( PwSer1 ` U ) ) i^i ( Base ` ( Poly1 ` R ) ) ) )
77 41 76 eleqtrd 
 |-  ( ( ph /\ x e. S ) -> ( ( var1 ` R ) ( -g ` ( Poly1 ` R ) ) ( ( algSc ` ( Poly1 ` R ) ) ` x ) ) e. ( ( Base ` ( PwSer1 ` U ) ) i^i ( Base ` ( Poly1 ` R ) ) ) )
78 77 elin2d 
 |-  ( ( ph /\ x e. S ) -> ( ( var1 ` R ) ( -g ` ( Poly1 ` R ) ) ( ( algSc ` ( Poly1 ` R ) ) ` x ) ) e. ( Base ` ( Poly1 ` R ) ) )
79 72 78 ffvelcdmd 
 |-  ( ( ph /\ x e. S ) -> ( ( eval1 ` R ) ` ( ( var1 ` R ) ( -g ` ( Poly1 ` R ) ) ( ( algSc ` ( Poly1 ` R ) ) ` x ) ) ) e. ( Base ` ( R ^s B ) ) )
80 65 3 66 45 68 79 pwselbas 
 |-  ( ( ph /\ x e. S ) -> ( ( eval1 ` R ) ` ( ( var1 ` R ) ( -g ` ( Poly1 ` R ) ) ( ( algSc ` ( Poly1 ` R ) ) ` x ) ) ) : B --> B )
81 80 ffnd 
 |-  ( ( ph /\ x e. S ) -> ( ( eval1 ` R ) ` ( ( var1 ` R ) ( -g ` ( Poly1 ` R ) ) ( ( algSc ` ( Poly1 ` R ) ) ` x ) ) ) Fn B )
82 vsnid 
 |-  x e. { x }
83 49 simp3d 
 |-  ( ( ph /\ x e. S ) -> ( `' ( ( eval1 ` R ) ` ( ( var1 ` R ) ( -g ` ( Poly1 ` R ) ) ( ( algSc ` ( Poly1 ` R ) ) ` x ) ) ) " { .0. } ) = { x } )
84 82 83 eleqtrrid 
 |-  ( ( ph /\ x e. S ) -> x e. ( `' ( ( eval1 ` R ) ` ( ( var1 ` R ) ( -g ` ( Poly1 ` R ) ) ( ( algSc ` ( Poly1 ` R ) ) ` x ) ) ) " { .0. } ) )
85 fniniseg 
 |-  ( ( ( eval1 ` R ) ` ( ( var1 ` R ) ( -g ` ( Poly1 ` R ) ) ( ( algSc ` ( Poly1 ` R ) ) ` x ) ) ) Fn B -> ( x e. ( `' ( ( eval1 ` R ) ` ( ( var1 ` R ) ( -g ` ( Poly1 ` R ) ) ( ( algSc ` ( Poly1 ` R ) ) ` x ) ) ) " { .0. } ) <-> ( x e. B /\ ( ( ( eval1 ` R ) ` ( ( var1 ` R ) ( -g ` ( Poly1 ` R ) ) ( ( algSc ` ( Poly1 ` R ) ) ` x ) ) ) ` x ) = .0. ) ) )
86 85 simplbda 
 |-  ( ( ( ( eval1 ` R ) ` ( ( var1 ` R ) ( -g ` ( Poly1 ` R ) ) ( ( algSc ` ( Poly1 ` R ) ) ` x ) ) ) Fn B /\ x e. ( `' ( ( eval1 ` R ) ` ( ( var1 ` R ) ( -g ` ( Poly1 ` R ) ) ( ( algSc ` ( Poly1 ` R ) ) ` x ) ) ) " { .0. } ) ) -> ( ( ( eval1 ` R ) ` ( ( var1 ` R ) ( -g ` ( Poly1 ` R ) ) ( ( algSc ` ( Poly1 ` R ) ) ` x ) ) ) ` x ) = .0. )
87 81 84 86 syl2anc 
 |-  ( ( ph /\ x e. S ) -> ( ( ( eval1 ` R ) ` ( ( var1 ` R ) ( -g ` ( Poly1 ` R ) ) ( ( algSc ` ( Poly1 ` R ) ) ` x ) ) ) ` x ) = .0. )
88 64 87 eqtrd 
 |-  ( ( ph /\ x e. S ) -> ( ( O ` ( ( var1 ` R ) ( -g ` ( Poly1 ` R ) ) ( ( algSc ` ( Poly1 ` R ) ) ` x ) ) ) ` x ) = .0. )
89 55 59 88 rspcedvd 
 |-  ( ( ph /\ x e. S ) -> E. f e. ( Monic1p ` U ) ( ( O ` f ) ` x ) = .0. )
90 1 2 3 4 5 6 elirng 
 |-  ( ph -> ( x e. ( R IntgRing S ) <-> ( x e. B /\ E. f e. ( Monic1p ` U ) ( ( O ` f ) ` x ) = .0. ) ) )
91 90 biimpar 
 |-  ( ( ph /\ ( x e. B /\ E. f e. ( Monic1p ` U ) ( ( O ` f ) ` x ) = .0. ) ) -> x e. ( R IntgRing S ) )
92 8 11 89 91 syl12anc 
 |-  ( ( ph /\ x e. S ) -> x e. ( R IntgRing S ) )
93 92 ex 
 |-  ( ph -> ( x e. S -> x e. ( R IntgRing S ) ) )
94 93 ssrdv 
 |-  ( ph -> S C_ ( R IntgRing S ) )