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 ⊢ 𝑂 = ( 𝑅 evalSub1 𝑆 )
irngval.u ⊢ 𝑈 = ( 𝑅 ↾s 𝑆 )
irngval.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
irngval.0 ⊢ 0 = ( 0g ‘ 𝑅 )
elirng.r ⊢ ( 𝜑 → 𝑅 ∈ CRing )
elirng.s ⊢ ( 𝜑 → 𝑆 ∈ ( SubRing ‘ 𝑅 ) )
irngss.1 ⊢ ( 𝜑 → 𝑅 ∈ NzRing )
Assertion irngss ( 𝜑 → 𝑆 ⊆ ( 𝑅 IntgRing 𝑆 ) )

Proof

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