| Step | Hyp | Ref
| Expression |
| 1 | | simpl 482 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝜑) |
| 2 | | elirng.s |
. . . . . 6
⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑅)) |
| 3 | | irngval.b |
. . . . . . 7
⊢ 𝐵 = (Base‘𝑅) |
| 4 | 3 | subrgss 20572 |
. . . . . 6
⊢ (𝑆 ∈ (SubRing‘𝑅) → 𝑆 ⊆ 𝐵) |
| 5 | 2, 4 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑆 ⊆ 𝐵) |
| 6 | 5 | sselda 3983 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ 𝐵) |
| 7 | | eqid 2737 |
. . . . . . . . . 10
⊢
(Poly1‘𝑅) = (Poly1‘𝑅) |
| 8 | | irngval.u |
. . . . . . . . . 10
⊢ 𝑈 = (𝑅 ↾s 𝑆) |
| 9 | | eqid 2737 |
. . . . . . . . . 10
⊢
(Poly1‘𝑈) = (Poly1‘𝑈) |
| 10 | | eqid 2737 |
. . . . . . . . . 10
⊢
(Base‘(Poly1‘𝑈)) =
(Base‘(Poly1‘𝑈)) |
| 11 | 2 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑆 ∈ (SubRing‘𝑅)) |
| 12 | | eqid 2737 |
. . . . . . . . . 10
⊢
((Poly1‘𝑅) ↾s
(Base‘(Poly1‘𝑈))) = ((Poly1‘𝑅) ↾s
(Base‘(Poly1‘𝑈))) |
| 13 | | eqid 2737 |
. . . . . . . . . . 11
⊢
(var1‘𝑅) = (var1‘𝑅) |
| 14 | 13, 11, 8, 9, 10 | subrgvr1cl 22265 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (var1‘𝑅) ∈
(Base‘(Poly1‘𝑈))) |
| 15 | | eqid 2737 |
. . . . . . . . . . 11
⊢
(algSc‘(Poly1‘𝑅)) =
(algSc‘(Poly1‘𝑅)) |
| 16 | | simpr 484 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ 𝑆) |
| 17 | 15, 8, 7, 9, 10, 11, 16 | asclply1subcl 22378 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) →
((algSc‘(Poly1‘𝑅))‘𝑥) ∈
(Base‘(Poly1‘𝑈))) |
| 18 | 7, 8, 9, 10, 11, 12, 14, 17 | ressply1sub 33595 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ((var1‘𝑅)(-g‘(Poly1‘𝑈))((algSc‘(Poly1‘𝑅))‘𝑥)) = ((var1‘𝑅)(-g‘((Poly1‘𝑅) ↾s
(Base‘(Poly1‘𝑈))))((algSc‘(Poly1‘𝑅))‘𝑥))) |
| 19 | 7, 8, 9, 10 | subrgply1 22234 |
. . . . . . . . . . . 12
⊢ (𝑆 ∈ (SubRing‘𝑅) →
(Base‘(Poly1‘𝑈)) ∈
(SubRing‘(Poly1‘𝑅))) |
| 20 | | subrgsubg 20577 |
. . . . . . . . . . . 12
⊢
((Base‘(Poly1‘𝑈)) ∈
(SubRing‘(Poly1‘𝑅)) →
(Base‘(Poly1‘𝑈)) ∈
(SubGrp‘(Poly1‘𝑅))) |
| 21 | 2, 19, 20 | 3syl 18 |
. . . . . . . . . . 11
⊢ (𝜑 →
(Base‘(Poly1‘𝑈)) ∈
(SubGrp‘(Poly1‘𝑅))) |
| 22 | 21 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) →
(Base‘(Poly1‘𝑈)) ∈
(SubGrp‘(Poly1‘𝑅))) |
| 23 | | eqid 2737 |
. . . . . . . . . . 11
⊢
(-g‘(Poly1‘𝑅)) =
(-g‘(Poly1‘𝑅)) |
| 24 | | eqid 2737 |
. . . . . . . . . . 11
⊢
(-g‘((Poly1‘𝑅) ↾s
(Base‘(Poly1‘𝑈)))) =
(-g‘((Poly1‘𝑅) ↾s
(Base‘(Poly1‘𝑈)))) |
| 25 | 23, 12, 24 | subgsub 19156 |
. . . . . . . . . 10
⊢
(((Base‘(Poly1‘𝑈)) ∈
(SubGrp‘(Poly1‘𝑅)) ∧ (var1‘𝑅) ∈
(Base‘(Poly1‘𝑈)) ∧
((algSc‘(Poly1‘𝑅))‘𝑥) ∈
(Base‘(Poly1‘𝑈))) → ((var1‘𝑅)(-g‘(Poly1‘𝑅))((algSc‘(Poly1‘𝑅))‘𝑥)) = ((var1‘𝑅)(-g‘((Poly1‘𝑅) ↾s
(Base‘(Poly1‘𝑈))))((algSc‘(Poly1‘𝑅))‘𝑥))) |
| 26 | 22, 14, 17, 25 | syl3anc 1373 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ((var1‘𝑅)(-g‘(Poly1‘𝑅))((algSc‘(Poly1‘𝑅))‘𝑥)) = ((var1‘𝑅)(-g‘((Poly1‘𝑅) ↾s
(Base‘(Poly1‘𝑈))))((algSc‘(Poly1‘𝑅))‘𝑥))) |
| 27 | 18, 26 | eqtr4d 2780 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ((var1‘𝑅)(-g‘(Poly1‘𝑈))((algSc‘(Poly1‘𝑅))‘𝑥)) = ((var1‘𝑅)(-g‘(Poly1‘𝑅))((algSc‘(Poly1‘𝑅))‘𝑥))) |
| 28 | | elirng.r |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑅 ∈ CRing) |
| 29 | 8 | subrgcrng 20575 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ CRing ∧ 𝑆 ∈ (SubRing‘𝑅)) → 𝑈 ∈ CRing) |
| 30 | 28, 2, 29 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑈 ∈ CRing) |
| 31 | 9 | ply1crng 22200 |
. . . . . . . . . . . 12
⊢ (𝑈 ∈ CRing →
(Poly1‘𝑈)
∈ CRing) |
| 32 | 30, 31 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 →
(Poly1‘𝑈)
∈ CRing) |
| 33 | 32 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (Poly1‘𝑈) ∈ CRing) |
| 34 | 33 | crnggrpd 20244 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (Poly1‘𝑈) ∈ Grp) |
| 35 | | eqid 2737 |
. . . . . . . . . 10
⊢
(-g‘(Poly1‘𝑈)) =
(-g‘(Poly1‘𝑈)) |
| 36 | 10, 35 | grpsubcl 19038 |
. . . . . . . . 9
⊢
(((Poly1‘𝑈) ∈ Grp ∧
(var1‘𝑅)
∈ (Base‘(Poly1‘𝑈)) ∧
((algSc‘(Poly1‘𝑅))‘𝑥) ∈
(Base‘(Poly1‘𝑈))) → ((var1‘𝑅)(-g‘(Poly1‘𝑈))((algSc‘(Poly1‘𝑅))‘𝑥)) ∈ (Base‘(Poly1‘𝑈))) |
| 37 | 34, 14, 17, 36 | syl3anc 1373 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ((var1‘𝑅)(-g‘(Poly1‘𝑈))((algSc‘(Poly1‘𝑅))‘𝑥)) ∈ (Base‘(Poly1‘𝑈))) |
| 38 | 27, 37 | eqeltrrd 2842 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ((var1‘𝑅)(-g‘(Poly1‘𝑅))((algSc‘(Poly1‘𝑅))‘𝑥)) ∈ (Base‘(Poly1‘𝑈))) |
| 39 | | eqid 2737 |
. . . . . . . . 9
⊢
(Base‘(Poly1‘𝑅)) =
(Base‘(Poly1‘𝑅)) |
| 40 | | eqid 2737 |
. . . . . . . . 9
⊢
((var1‘𝑅)(-g‘(Poly1‘𝑅))((algSc‘(Poly1‘𝑅))‘𝑥)) = ((var1‘𝑅)(-g‘(Poly1‘𝑅))((algSc‘(Poly1‘𝑅))‘𝑥)) |
| 41 | | eqid 2737 |
. . . . . . . . 9
⊢
(eval1‘𝑅) = (eval1‘𝑅) |
| 42 | | irngss.1 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑅 ∈ NzRing) |
| 43 | 42 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑅 ∈ NzRing) |
| 44 | 28 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑅 ∈ CRing) |
| 45 | | eqid 2737 |
. . . . . . . . 9
⊢
(Monic1p‘𝑅) = (Monic1p‘𝑅) |
| 46 | | eqid 2737 |
. . . . . . . . 9
⊢
(deg1‘𝑅) = (deg1‘𝑅) |
| 47 | | irngval.0 |
. . . . . . . . 9
⊢ 0 =
(0g‘𝑅) |
| 48 | 7, 39, 3, 13, 23, 15, 40, 41, 43, 44, 6, 45, 46, 47 | ply1remlem 26204 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (((var1‘𝑅)(-g‘(Poly1‘𝑅))((algSc‘(Poly1‘𝑅))‘𝑥)) ∈ (Monic1p‘𝑅) ∧ ((deg1‘𝑅)‘((var1‘𝑅)(-g‘(Poly1‘𝑅))((algSc‘(Poly1‘𝑅))‘𝑥))) = 1 ∧ (◡((eval1‘𝑅)‘((var1‘𝑅)(-g‘(Poly1‘𝑅))((algSc‘(Poly1‘𝑅))‘𝑥))) “ { 0 }) = {𝑥})) |
| 49 | 48 | simp1d 1143 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ((var1‘𝑅)(-g‘(Poly1‘𝑅))((algSc‘(Poly1‘𝑅))‘𝑥)) ∈ (Monic1p‘𝑅)) |
| 50 | 38, 49 | elind 4200 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ((var1‘𝑅)(-g‘(Poly1‘𝑅))((algSc‘(Poly1‘𝑅))‘𝑥)) ∈ ((Base‘(Poly1‘𝑈)) ∩
(Monic1p‘𝑅))) |
| 51 | | eqid 2737 |
. . . . . . . 8
⊢
(Monic1p‘𝑈) = (Monic1p‘𝑈) |
| 52 | 7, 8, 9, 10, 2, 45, 51 | ressply1mon1p 33593 |
. . . . . . 7
⊢ (𝜑 →
(Monic1p‘𝑈) =
((Base‘(Poly1‘𝑈)) ∩ (Monic1p‘𝑅))) |
| 53 | 52 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (Monic1p‘𝑈) =
((Base‘(Poly1‘𝑈)) ∩ (Monic1p‘𝑅))) |
| 54 | 50, 53 | eleqtrrd 2844 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ((var1‘𝑅)(-g‘(Poly1‘𝑅))((algSc‘(Poly1‘𝑅))‘𝑥)) ∈ (Monic1p‘𝑈)) |
| 55 | | fveq2 6906 |
. . . . . . . 8
⊢ (𝑓 = ((var1‘𝑅)(-g‘(Poly1‘𝑅))((algSc‘(Poly1‘𝑅))‘𝑥)) → (𝑂‘𝑓) = (𝑂‘((var1‘𝑅)(-g‘(Poly1‘𝑅))((algSc‘(Poly1‘𝑅))‘𝑥)))) |
| 56 | 55 | fveq1d 6908 |
. . . . . . 7
⊢ (𝑓 = ((var1‘𝑅)(-g‘(Poly1‘𝑅))((algSc‘(Poly1‘𝑅))‘𝑥)) → ((𝑂‘𝑓)‘𝑥) = ((𝑂‘((var1‘𝑅)(-g‘(Poly1‘𝑅))((algSc‘(Poly1‘𝑅))‘𝑥)))‘𝑥)) |
| 57 | 56 | eqeq1d 2739 |
. . . . . 6
⊢ (𝑓 = ((var1‘𝑅)(-g‘(Poly1‘𝑅))((algSc‘(Poly1‘𝑅))‘𝑥)) → (((𝑂‘𝑓)‘𝑥) = 0 ↔ ((𝑂‘((var1‘𝑅)(-g‘(Poly1‘𝑅))((algSc‘(Poly1‘𝑅))‘𝑥)))‘𝑥) = 0 )) |
| 58 | 57 | adantl 481 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑆) ∧ 𝑓 = ((var1‘𝑅)(-g‘(Poly1‘𝑅))((algSc‘(Poly1‘𝑅))‘𝑥))) → (((𝑂‘𝑓)‘𝑥) = 0 ↔ ((𝑂‘((var1‘𝑅)(-g‘(Poly1‘𝑅))((algSc‘(Poly1‘𝑅))‘𝑥)))‘𝑥) = 0 )) |
| 59 | | irngval.o |
. . . . . . . . . 10
⊢ 𝑂 = (𝑅 evalSub1 𝑆) |
| 60 | 59, 3, 9, 8, 10, 41, 44, 11 | ressply1evl 22374 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑂 = ((eval1‘𝑅) ↾
(Base‘(Poly1‘𝑈)))) |
| 61 | 60 | fveq1d 6908 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝑂‘((var1‘𝑅)(-g‘(Poly1‘𝑅))((algSc‘(Poly1‘𝑅))‘𝑥))) = (((eval1‘𝑅) ↾ (Base‘(Poly1‘𝑈)))‘((var1‘𝑅)(-g‘(Poly1‘𝑅))((algSc‘(Poly1‘𝑅))‘𝑥)))) |
| 62 | 38 | fvresd 6926 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (((eval1‘𝑅) ↾
(Base‘(Poly1‘𝑈)))‘((var1‘𝑅)(-g‘(Poly1‘𝑅))((algSc‘(Poly1‘𝑅))‘𝑥))) = ((eval1‘𝑅)‘((var1‘𝑅)(-g‘(Poly1‘𝑅))((algSc‘(Poly1‘𝑅))‘𝑥)))) |
| 63 | 61, 62 | eqtrd 2777 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝑂‘((var1‘𝑅)(-g‘(Poly1‘𝑅))((algSc‘(Poly1‘𝑅))‘𝑥))) = ((eval1‘𝑅)‘((var1‘𝑅)(-g‘(Poly1‘𝑅))((algSc‘(Poly1‘𝑅))‘𝑥)))) |
| 64 | 63 | fveq1d 6908 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ((𝑂‘((var1‘𝑅)(-g‘(Poly1‘𝑅))((algSc‘(Poly1‘𝑅))‘𝑥)))‘𝑥) = (((eval1‘𝑅)‘((var1‘𝑅)(-g‘(Poly1‘𝑅))((algSc‘(Poly1‘𝑅))‘𝑥)))‘𝑥)) |
| 65 | | eqid 2737 |
. . . . . . . . 9
⊢ (𝑅 ↑s 𝐵) = (𝑅 ↑s 𝐵) |
| 66 | | eqid 2737 |
. . . . . . . . 9
⊢
(Base‘(𝑅
↑s 𝐵)) = (Base‘(𝑅 ↑s 𝐵)) |
| 67 | 3 | fvexi 6920 |
. . . . . . . . . 10
⊢ 𝐵 ∈ V |
| 68 | 67 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐵 ∈ V) |
| 69 | 41, 7, 65, 3 | evl1rhm 22336 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ CRing →
(eval1‘𝑅)
∈ ((Poly1‘𝑅) RingHom (𝑅 ↑s 𝐵))) |
| 70 | 39, 66 | rhmf 20485 |
. . . . . . . . . . . 12
⊢
((eval1‘𝑅) ∈ ((Poly1‘𝑅) RingHom (𝑅 ↑s 𝐵)) → (eval1‘𝑅):(Base‘(Poly1‘𝑅))⟶(Base‘(𝑅 ↑s 𝐵))) |
| 71 | 28, 69, 70 | 3syl 18 |
. . . . . . . . . . 11
⊢ (𝜑 →
(eval1‘𝑅):(Base‘(Poly1‘𝑅))⟶(Base‘(𝑅 ↑s 𝐵))) |
| 72 | 71 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (eval1‘𝑅):(Base‘(Poly1‘𝑅))⟶(Base‘(𝑅 ↑s 𝐵))) |
| 73 | | eqid 2737 |
. . . . . . . . . . . . . 14
⊢
(PwSer1‘𝑈) = (PwSer1‘𝑈) |
| 74 | | eqid 2737 |
. . . . . . . . . . . . . 14
⊢
(Base‘(PwSer1‘𝑈)) =
(Base‘(PwSer1‘𝑈)) |
| 75 | 7, 8, 9, 10, 2, 73, 74, 39 | ressply1bas2 22229 |
. . . . . . . . . . . . 13
⊢ (𝜑 →
(Base‘(Poly1‘𝑈)) =
((Base‘(PwSer1‘𝑈)) ∩
(Base‘(Poly1‘𝑅)))) |
| 76 | 75 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) →
(Base‘(Poly1‘𝑈)) =
((Base‘(PwSer1‘𝑈)) ∩
(Base‘(Poly1‘𝑅)))) |
| 77 | 38, 76 | eleqtrd 2843 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ((var1‘𝑅)(-g‘(Poly1‘𝑅))((algSc‘(Poly1‘𝑅))‘𝑥)) ∈
((Base‘(PwSer1‘𝑈)) ∩ (Base‘(Poly1‘𝑅)))) |
| 78 | 77 | elin2d 4205 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ((var1‘𝑅)(-g‘(Poly1‘𝑅))((algSc‘(Poly1‘𝑅))‘𝑥)) ∈ (Base‘(Poly1‘𝑅))) |
| 79 | 72, 78 | ffvelcdmd 7105 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ((eval1‘𝑅)‘((var1‘𝑅)(-g‘(Poly1‘𝑅))((algSc‘(Poly1‘𝑅))‘𝑥))) ∈ (Base‘(𝑅 ↑s 𝐵))) |
| 80 | 65, 3, 66, 43, 68, 79 | pwselbas 17534 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ((eval1‘𝑅)‘((var1‘𝑅)(-g‘(Poly1‘𝑅))((algSc‘(Poly1‘𝑅))‘𝑥))):𝐵⟶𝐵) |
| 81 | 80 | ffnd 6737 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ((eval1‘𝑅)‘((var1‘𝑅)(-g‘(Poly1‘𝑅))((algSc‘(Poly1‘𝑅))‘𝑥))) Fn 𝐵) |
| 82 | | vsnid 4663 |
. . . . . . . 8
⊢ 𝑥 ∈ {𝑥} |
| 83 | 48 | simp3d 1145 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (◡((eval1‘𝑅)‘((var1‘𝑅)(-g‘(Poly1‘𝑅))((algSc‘(Poly1‘𝑅))‘𝑥))) “ { 0 }) = {𝑥}) |
| 84 | 82, 83 | eleqtrrid 2848 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ (◡((eval1‘𝑅)‘((var1‘𝑅)(-g‘(Poly1‘𝑅))((algSc‘(Poly1‘𝑅))‘𝑥))) “ { 0 })) |
| 85 | | fniniseg 7080 |
. . . . . . . 8
⊢
(((eval1‘𝑅)‘((var1‘𝑅)(-g‘(Poly1‘𝑅))((algSc‘(Poly1‘𝑅))‘𝑥))) Fn 𝐵 → (𝑥 ∈ (◡((eval1‘𝑅)‘((var1‘𝑅)(-g‘(Poly1‘𝑅))((algSc‘(Poly1‘𝑅))‘𝑥))) “ { 0 }) ↔ (𝑥 ∈ 𝐵 ∧ (((eval1‘𝑅)‘((var1‘𝑅)(-g‘(Poly1‘𝑅))((algSc‘(Poly1‘𝑅))‘𝑥)))‘𝑥) = 0 ))) |
| 86 | 85 | simplbda 499 |
. . . . . . 7
⊢
((((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 584 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (((eval1‘𝑅)‘((var1‘𝑅)(-g‘(Poly1‘𝑅))((algSc‘(Poly1‘𝑅))‘𝑥)))‘𝑥) = 0 ) |
| 88 | 64, 87 | eqtrd 2777 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ((𝑂‘((var1‘𝑅)(-g‘(Poly1‘𝑅))((algSc‘(Poly1‘𝑅))‘𝑥)))‘𝑥) = 0 ) |
| 89 | 54, 58, 88 | rspcedvd 3624 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ∃𝑓 ∈ (Monic1p‘𝑈)((𝑂‘𝑓)‘𝑥) = 0 ) |
| 90 | 59, 8, 3, 47, 28, 2 | elirng 33736 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ (𝑅 IntgRing 𝑆) ↔ (𝑥 ∈ 𝐵 ∧ ∃𝑓 ∈ (Monic1p‘𝑈)((𝑂‘𝑓)‘𝑥) = 0 ))) |
| 91 | 90 | biimpar 477 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ ∃𝑓 ∈ (Monic1p‘𝑈)((𝑂‘𝑓)‘𝑥) = 0 )) → 𝑥 ∈ (𝑅 IntgRing 𝑆)) |
| 92 | 1, 6, 89, 91 | syl12anc 837 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ (𝑅 IntgRing 𝑆)) |
| 93 | 92 | ex 412 |
. 2
⊢ (𝜑 → (𝑥 ∈ 𝑆 → 𝑥 ∈ (𝑅 IntgRing 𝑆))) |
| 94 | 93 | ssrdv 3989 |
1
⊢ (𝜑 → 𝑆 ⊆ (𝑅 IntgRing 𝑆)) |