Step | Hyp | Ref
| Expression |
1 | | simpl 483 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝜑) |
2 | | elirng.s |
. . . . . 6
⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑅)) |
3 | | irngval.b |
. . . . . . 7
⊢ 𝐵 = (Base‘𝑅) |
4 | 3 | subrgss 20315 |
. . . . . 6
⊢ (𝑆 ∈ (SubRing‘𝑅) → 𝑆 ⊆ 𝐵) |
5 | 2, 4 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑆 ⊆ 𝐵) |
6 | 5 | sselda 3979 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ 𝐵) |
7 | | eqid 2732 |
. . . . . . . . . 10
⊢
(Poly1‘𝑅) = (Poly1‘𝑅) |
8 | | irngval.u |
. . . . . . . . . 10
⊢ 𝑈 = (𝑅 ↾s 𝑆) |
9 | | eqid 2732 |
. . . . . . . . . 10
⊢
(Poly1‘𝑈) = (Poly1‘𝑈) |
10 | | eqid 2732 |
. . . . . . . . . 10
⊢
(Base‘(Poly1‘𝑈)) =
(Base‘(Poly1‘𝑈)) |
11 | 2 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑆 ∈ (SubRing‘𝑅)) |
12 | | eqid 2732 |
. . . . . . . . . 10
⊢
((Poly1‘𝑅) ↾s
(Base‘(Poly1‘𝑈))) = ((Poly1‘𝑅) ↾s
(Base‘(Poly1‘𝑈))) |
13 | | eqid 2732 |
. . . . . . . . . . 11
⊢
(var1‘𝑅) = (var1‘𝑅) |
14 | 13, 11, 8, 9, 10 | subrgvr1cl 21717 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (var1‘𝑅) ∈
(Base‘(Poly1‘𝑈))) |
15 | | eqid 2732 |
. . . . . . . . . . 11
⊢
(algSc‘(Poly1‘𝑅)) =
(algSc‘(Poly1‘𝑅)) |
16 | | simpr 485 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ 𝑆) |
17 | 15, 8, 7, 9, 10, 11, 16 | asclply1subcl 32564 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) →
((algSc‘(Poly1‘𝑅))‘𝑥) ∈
(Base‘(Poly1‘𝑈))) |
18 | 7, 8, 9, 10, 11, 12, 14, 17 | ressply1sub 32563 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ((var1‘𝑅)(-g‘(Poly1‘𝑈))((algSc‘(Poly1‘𝑅))‘𝑥)) = ((var1‘𝑅)(-g‘((Poly1‘𝑅) ↾s
(Base‘(Poly1‘𝑈))))((algSc‘(Poly1‘𝑅))‘𝑥))) |
19 | 7, 8, 9, 10 | subrgply1 21688 |
. . . . . . . . . . . 12
⊢ (𝑆 ∈ (SubRing‘𝑅) →
(Base‘(Poly1‘𝑈)) ∈
(SubRing‘(Poly1‘𝑅))) |
20 | | subrgsubg 20320 |
. . . . . . . . . . . 12
⊢
((Base‘(Poly1‘𝑈)) ∈
(SubRing‘(Poly1‘𝑅)) →
(Base‘(Poly1‘𝑈)) ∈
(SubGrp‘(Poly1‘𝑅))) |
21 | 2, 19, 20 | 3syl 18 |
. . . . . . . . . . 11
⊢ (𝜑 →
(Base‘(Poly1‘𝑈)) ∈
(SubGrp‘(Poly1‘𝑅))) |
22 | 21 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) →
(Base‘(Poly1‘𝑈)) ∈
(SubGrp‘(Poly1‘𝑅))) |
23 | | eqid 2732 |
. . . . . . . . . . 11
⊢
(-g‘(Poly1‘𝑅)) =
(-g‘(Poly1‘𝑅)) |
24 | | eqid 2732 |
. . . . . . . . . . 11
⊢
(-g‘((Poly1‘𝑅) ↾s
(Base‘(Poly1‘𝑈)))) =
(-g‘((Poly1‘𝑅) ↾s
(Base‘(Poly1‘𝑈)))) |
25 | 23, 12, 24 | subgsub 18992 |
. . . . . . . . . 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 1371 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ((var1‘𝑅)(-g‘(Poly1‘𝑅))((algSc‘(Poly1‘𝑅))‘𝑥)) = ((var1‘𝑅)(-g‘((Poly1‘𝑅) ↾s
(Base‘(Poly1‘𝑈))))((algSc‘(Poly1‘𝑅))‘𝑥))) |
27 | 18, 26 | eqtr4d 2775 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ((var1‘𝑅)(-g‘(Poly1‘𝑈))((algSc‘(Poly1‘𝑅))‘𝑥)) = ((var1‘𝑅)(-g‘(Poly1‘𝑅))((algSc‘(Poly1‘𝑅))‘𝑥))) |
28 | | elirng.r |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑅 ∈ CRing) |
29 | 8 | subrgcrng 20318 |
. . . . . . . . . . . . 13
⊢ ((𝑅 ∈ CRing ∧ 𝑆 ∈ (SubRing‘𝑅)) → 𝑈 ∈ CRing) |
30 | 28, 2, 29 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑈 ∈ CRing) |
31 | 9 | ply1crng 21653 |
. . . . . . . . . . . 12
⊢ (𝑈 ∈ CRing →
(Poly1‘𝑈)
∈ CRing) |
32 | 30, 31 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 →
(Poly1‘𝑈)
∈ CRing) |
33 | 32 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (Poly1‘𝑈) ∈ CRing) |
34 | 33 | crnggrpd 20030 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (Poly1‘𝑈) ∈ Grp) |
35 | | eqid 2732 |
. . . . . . . . . 10
⊢
(-g‘(Poly1‘𝑈)) =
(-g‘(Poly1‘𝑈)) |
36 | 10, 35 | grpsubcl 18879 |
. . . . . . . . 9
⊢
(((Poly1‘𝑈) ∈ Grp ∧
(var1‘𝑅)
∈ (Base‘(Poly1‘𝑈)) ∧
((algSc‘(Poly1‘𝑅))‘𝑥) ∈
(Base‘(Poly1‘𝑈))) → ((var1‘𝑅)(-g‘(Poly1‘𝑈))((algSc‘(Poly1‘𝑅))‘𝑥)) ∈ (Base‘(Poly1‘𝑈))) |
37 | 34, 14, 17, 36 | syl3anc 1371 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ((var1‘𝑅)(-g‘(Poly1‘𝑈))((algSc‘(Poly1‘𝑅))‘𝑥)) ∈ (Base‘(Poly1‘𝑈))) |
38 | 27, 37 | eqeltrrd 2834 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ((var1‘𝑅)(-g‘(Poly1‘𝑅))((algSc‘(Poly1‘𝑅))‘𝑥)) ∈ (Base‘(Poly1‘𝑈))) |
39 | | eqid 2732 |
. . . . . . . . 9
⊢
(Base‘(Poly1‘𝑅)) =
(Base‘(Poly1‘𝑅)) |
40 | | eqid 2732 |
. . . . . . . . 9
⊢
((var1‘𝑅)(-g‘(Poly1‘𝑅))((algSc‘(Poly1‘𝑅))‘𝑥)) = ((var1‘𝑅)(-g‘(Poly1‘𝑅))((algSc‘(Poly1‘𝑅))‘𝑥)) |
41 | | eqid 2732 |
. . . . . . . . 9
⊢
(eval1‘𝑅) = (eval1‘𝑅) |
42 | | irngss.1 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑅 ∈ NzRing) |
43 | 42 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑅 ∈ NzRing) |
44 | 28 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑅 ∈ CRing) |
45 | | eqid 2732 |
. . . . . . . . 9
⊢
(Monic1p‘𝑅) = (Monic1p‘𝑅) |
46 | | eqid 2732 |
. . . . . . . . 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 25611 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (((var1‘𝑅)(-g‘(Poly1‘𝑅))((algSc‘(Poly1‘𝑅))‘𝑥)) ∈ (Monic1p‘𝑅) ∧ (( deg1 ‘𝑅)‘((var1‘𝑅)(-g‘(Poly1‘𝑅))((algSc‘(Poly1‘𝑅))‘𝑥))) = 1 ∧ (◡((eval1‘𝑅)‘((var1‘𝑅)(-g‘(Poly1‘𝑅))((algSc‘(Poly1‘𝑅))‘𝑥))) “ { 0 }) = {𝑥})) |
49 | 48 | simp1d 1142 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ((var1‘𝑅)(-g‘(Poly1‘𝑅))((algSc‘(Poly1‘𝑅))‘𝑥)) ∈ (Monic1p‘𝑅)) |
50 | 38, 49 | elind 4191 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ((var1‘𝑅)(-g‘(Poly1‘𝑅))((algSc‘(Poly1‘𝑅))‘𝑥)) ∈ ((Base‘(Poly1‘𝑈)) ∩
(Monic1p‘𝑅))) |
51 | | eqid 2732 |
. . . . . . . 8
⊢
(Monic1p‘𝑈) = (Monic1p‘𝑈) |
52 | 7, 8, 9, 10, 2, 45, 51 | ressply1mon1p 32561 |
. . . . . . 7
⊢ (𝜑 →
(Monic1p‘𝑈) =
((Base‘(Poly1‘𝑈)) ∩ (Monic1p‘𝑅))) |
53 | 52 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (Monic1p‘𝑈) =
((Base‘(Poly1‘𝑈)) ∩ (Monic1p‘𝑅))) |
54 | 50, 53 | eleqtrrd 2836 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ((var1‘𝑅)(-g‘(Poly1‘𝑅))((algSc‘(Poly1‘𝑅))‘𝑥)) ∈ (Monic1p‘𝑈)) |
55 | | fveq2 6879 |
. . . . . . . 8
⊢ (𝑓 = ((var1‘𝑅)(-g‘(Poly1‘𝑅))((algSc‘(Poly1‘𝑅))‘𝑥)) → (𝑂‘𝑓) = (𝑂‘((var1‘𝑅)(-g‘(Poly1‘𝑅))((algSc‘(Poly1‘𝑅))‘𝑥)))) |
56 | 55 | fveq1d 6881 |
. . . . . . 7
⊢ (𝑓 = ((var1‘𝑅)(-g‘(Poly1‘𝑅))((algSc‘(Poly1‘𝑅))‘𝑥)) → ((𝑂‘𝑓)‘𝑥) = ((𝑂‘((var1‘𝑅)(-g‘(Poly1‘𝑅))((algSc‘(Poly1‘𝑅))‘𝑥)))‘𝑥)) |
57 | 56 | eqeq1d 2734 |
. . . . . 6
⊢ (𝑓 = ((var1‘𝑅)(-g‘(Poly1‘𝑅))((algSc‘(Poly1‘𝑅))‘𝑥)) → (((𝑂‘𝑓)‘𝑥) = 0 ↔ ((𝑂‘((var1‘𝑅)(-g‘(Poly1‘𝑅))((algSc‘(Poly1‘𝑅))‘𝑥)))‘𝑥) = 0 )) |
58 | 57 | adantl 482 |
. . . . 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 32554 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑂 = ((eval1‘𝑅) ↾
(Base‘(Poly1‘𝑈)))) |
61 | 60 | fveq1d 6881 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝑂‘((var1‘𝑅)(-g‘(Poly1‘𝑅))((algSc‘(Poly1‘𝑅))‘𝑥))) = (((eval1‘𝑅) ↾ (Base‘(Poly1‘𝑈)))‘((var1‘𝑅)(-g‘(Poly1‘𝑅))((algSc‘(Poly1‘𝑅))‘𝑥)))) |
62 | 38 | fvresd 6899 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (((eval1‘𝑅) ↾
(Base‘(Poly1‘𝑈)))‘((var1‘𝑅)(-g‘(Poly1‘𝑅))((algSc‘(Poly1‘𝑅))‘𝑥))) = ((eval1‘𝑅)‘((var1‘𝑅)(-g‘(Poly1‘𝑅))((algSc‘(Poly1‘𝑅))‘𝑥)))) |
63 | 61, 62 | eqtrd 2772 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝑂‘((var1‘𝑅)(-g‘(Poly1‘𝑅))((algSc‘(Poly1‘𝑅))‘𝑥))) = ((eval1‘𝑅)‘((var1‘𝑅)(-g‘(Poly1‘𝑅))((algSc‘(Poly1‘𝑅))‘𝑥)))) |
64 | 63 | fveq1d 6881 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ((𝑂‘((var1‘𝑅)(-g‘(Poly1‘𝑅))((algSc‘(Poly1‘𝑅))‘𝑥)))‘𝑥) = (((eval1‘𝑅)‘((var1‘𝑅)(-g‘(Poly1‘𝑅))((algSc‘(Poly1‘𝑅))‘𝑥)))‘𝑥)) |
65 | | eqid 2732 |
. . . . . . . . 9
⊢ (𝑅 ↑s 𝐵) = (𝑅 ↑s 𝐵) |
66 | | eqid 2732 |
. . . . . . . . 9
⊢
(Base‘(𝑅
↑s 𝐵)) = (Base‘(𝑅 ↑s 𝐵)) |
67 | 3 | fvexi 6893 |
. . . . . . . . . 10
⊢ 𝐵 ∈ V |
68 | 67 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝐵 ∈ V) |
69 | 41, 7, 65, 3 | evl1rhm 21782 |
. . . . . . . . . . . 12
⊢ (𝑅 ∈ CRing →
(eval1‘𝑅)
∈ ((Poly1‘𝑅) RingHom (𝑅 ↑s 𝐵))) |
70 | 39, 66 | rhmf 20215 |
. . . . . . . . . . . 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 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (eval1‘𝑅):(Base‘(Poly1‘𝑅))⟶(Base‘(𝑅 ↑s 𝐵))) |
73 | | eqid 2732 |
. . . . . . . . . . . . . 14
⊢
(PwSer1‘𝑈) = (PwSer1‘𝑈) |
74 | | eqid 2732 |
. . . . . . . . . . . . . 14
⊢
(Base‘(PwSer1‘𝑈)) =
(Base‘(PwSer1‘𝑈)) |
75 | 7, 8, 9, 10, 2, 73, 74, 39 | ressply1bas2 21683 |
. . . . . . . . . . . . 13
⊢ (𝜑 →
(Base‘(Poly1‘𝑈)) =
((Base‘(PwSer1‘𝑈)) ∩
(Base‘(Poly1‘𝑅)))) |
76 | 75 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) →
(Base‘(Poly1‘𝑈)) =
((Base‘(PwSer1‘𝑈)) ∩
(Base‘(Poly1‘𝑅)))) |
77 | 38, 76 | eleqtrd 2835 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ((var1‘𝑅)(-g‘(Poly1‘𝑅))((algSc‘(Poly1‘𝑅))‘𝑥)) ∈
((Base‘(PwSer1‘𝑈)) ∩ (Base‘(Poly1‘𝑅)))) |
78 | 77 | elin2d 4196 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ((var1‘𝑅)(-g‘(Poly1‘𝑅))((algSc‘(Poly1‘𝑅))‘𝑥)) ∈ (Base‘(Poly1‘𝑅))) |
79 | 72, 78 | ffvelcdmd 7073 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ((eval1‘𝑅)‘((var1‘𝑅)(-g‘(Poly1‘𝑅))((algSc‘(Poly1‘𝑅))‘𝑥))) ∈ (Base‘(𝑅 ↑s 𝐵))) |
80 | 65, 3, 66, 43, 68, 79 | pwselbas 17419 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ((eval1‘𝑅)‘((var1‘𝑅)(-g‘(Poly1‘𝑅))((algSc‘(Poly1‘𝑅))‘𝑥))):𝐵⟶𝐵) |
81 | 80 | ffnd 6706 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ((eval1‘𝑅)‘((var1‘𝑅)(-g‘(Poly1‘𝑅))((algSc‘(Poly1‘𝑅))‘𝑥))) Fn 𝐵) |
82 | | vsnid 4660 |
. . . . . . . 8
⊢ 𝑥 ∈ {𝑥} |
83 | 48 | simp3d 1144 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (◡((eval1‘𝑅)‘((var1‘𝑅)(-g‘(Poly1‘𝑅))((algSc‘(Poly1‘𝑅))‘𝑥))) “ { 0 }) = {𝑥}) |
84 | 82, 83 | eleqtrrid 2840 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ (◡((eval1‘𝑅)‘((var1‘𝑅)(-g‘(Poly1‘𝑅))((algSc‘(Poly1‘𝑅))‘𝑥))) “ { 0 })) |
85 | | fniniseg 7047 |
. . . . . . . 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 500 |
. . . . . . 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 2772 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ((𝑂‘((var1‘𝑅)(-g‘(Poly1‘𝑅))((algSc‘(Poly1‘𝑅))‘𝑥)))‘𝑥) = 0 ) |
89 | 54, 58, 88 | rspcedvd 3612 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → ∃𝑓 ∈ (Monic1p‘𝑈)((𝑂‘𝑓)‘𝑥) = 0 ) |
90 | 59, 8, 3, 47, 28, 2 | elirng 32652 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ (𝑅 IntgRing 𝑆) ↔ (𝑥 ∈ 𝐵 ∧ ∃𝑓 ∈ (Monic1p‘𝑈)((𝑂‘𝑓)‘𝑥) = 0 ))) |
91 | 90 | biimpar 478 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ ∃𝑓 ∈ (Monic1p‘𝑈)((𝑂‘𝑓)‘𝑥) = 0 )) → 𝑥 ∈ (𝑅 IntgRing 𝑆)) |
92 | 1, 6, 89, 91 | syl12anc 835 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ (𝑅 IntgRing 𝑆)) |
93 | 92 | ex 413 |
. 2
⊢ (𝜑 → (𝑥 ∈ 𝑆 → 𝑥 ∈ (𝑅 IntgRing 𝑆))) |
94 | 93 | ssrdv 3985 |
1
⊢ (𝜑 → 𝑆 ⊆ (𝑅 IntgRing 𝑆)) |