Metamath Proof Explorer


Theorem rngunsnply

Description: Adjoining one element to a ring results in a set of polynomial evaluations. (Contributed by Stefan O'Rear, 30-Nov-2014)

Ref Expression
Hypotheses rngunsnply.b φ B SubRing fld
rngunsnply.x φ X
rngunsnply.s φ S = RingSpan fld B X
Assertion rngunsnply φ V S p Poly B V = p X

Proof

Step Hyp Ref Expression
1 rngunsnply.b φ B SubRing fld
2 rngunsnply.x φ X
3 rngunsnply.s φ S = RingSpan fld B X
4 3 eleq2d φ V S V RingSpan fld B X
5 cnring fld Ring
6 5 a1i φ fld Ring
7 cnfldbas = Base fld
8 7 a1i φ = Base fld
9 7 subrgss B SubRing fld B
10 1 9 syl φ B
11 2 snssd φ X
12 10 11 unssd φ B X
13 eqidd φ RingSpan fld = RingSpan fld
14 eqidd φ RingSpan fld B X = RingSpan fld B X
15 eqidd φ fld 𝑠 a | p Poly B a = p X = fld 𝑠 a | p Poly B a = p X
16 cnfld0 0 = 0 fld
17 16 a1i φ 0 = 0 fld
18 cnfldadd + = + fld
19 18 a1i φ + = + fld
20 plyf p Poly B p :
21 ffvelrn p : X p X
22 20 2 21 syl2anr φ p Poly B p X
23 eleq1 a = p X a p X
24 22 23 syl5ibrcom φ p Poly B a = p X a
25 24 rexlimdva φ p Poly B a = p X a
26 25 ss2abdv φ a | p Poly B a = p X a | a
27 abid2 a | a =
28 27 7 eqtri a | a = Base fld
29 26 28 sseqtrdi φ a | p Poly B a = p X Base fld
30 abid2 a | a B = B
31 plyconst B a B × a Poly B
32 10 31 sylan φ a B × a Poly B
33 2 adantr φ a B X
34 vex a V
35 34 fvconst2 X × a X = a
36 33 35 syl φ a B × a X = a
37 36 eqcomd φ a B a = × a X
38 fveq1 p = × a p X = × a X
39 38 rspceeqv × a Poly B a = × a X p Poly B a = p X
40 32 37 39 syl2anc φ a B p Poly B a = p X
41 40 ex φ a B p Poly B a = p X
42 41 ss2abdv φ a | a B a | p Poly B a = p X
43 30 42 eqsstrrid φ B a | p Poly B a = p X
44 subrgsubg B SubRing fld B SubGrp fld
45 1 44 syl φ B SubGrp fld
46 16 subg0cl B SubGrp fld 0 B
47 45 46 syl φ 0 B
48 43 47 sseldd φ 0 a | p Poly B a = p X
49 biid φ φ
50 vex b V
51 eqeq1 a = b a = p X b = p X
52 51 rexbidv a = b p Poly B a = p X p Poly B b = p X
53 fveq1 p = e p X = e X
54 53 eqeq2d p = e b = p X b = e X
55 54 cbvrexvw p Poly B b = p X e Poly B b = e X
56 52 55 bitrdi a = b p Poly B a = p X e Poly B b = e X
57 50 56 elab b a | p Poly B a = p X e Poly B b = e X
58 vex c V
59 eqeq1 a = c a = p X c = p X
60 59 rexbidv a = c p Poly B a = p X p Poly B c = p X
61 fveq1 p = d p X = d X
62 61 eqeq2d p = d c = p X c = d X
63 62 cbvrexvw p Poly B c = p X d Poly B c = d X
64 60 63 bitrdi a = c p Poly B a = p X d Poly B c = d X
65 58 64 elab c a | p Poly B a = p X d Poly B c = d X
66 simplr φ e Poly B d Poly B e Poly B
67 simpr φ e Poly B d Poly B d Poly B
68 18 subrgacl B SubRing fld a B b B a + b B
69 68 3expb B SubRing fld a B b B a + b B
70 1 69 sylan φ a B b B a + b B
71 70 adantlr φ e Poly B a B b B a + b B
72 71 adantlr φ e Poly B d Poly B a B b B a + b B
73 66 67 72 plyadd φ e Poly B d Poly B e + f d Poly B
74 plyf e Poly B e :
75 74 ffnd e Poly B e Fn
76 75 ad2antlr φ e Poly B d Poly B e Fn
77 plyf d Poly B d :
78 77 ffnd d Poly B d Fn
79 78 adantl φ e Poly B d Poly B d Fn
80 cnex V
81 80 a1i φ e Poly B d Poly B V
82 2 ad2antrr φ e Poly B d Poly B X
83 fnfvof e Fn d Fn V X e + f d X = e X + d X
84 76 79 81 82 83 syl22anc φ e Poly B d Poly B e + f d X = e X + d X
85 84 eqcomd φ e Poly B d Poly B e X + d X = e + f d X
86 fveq1 p = e + f d p X = e + f d X
87 86 rspceeqv e + f d Poly B e X + d X = e + f d X p Poly B e X + d X = p X
88 73 85 87 syl2anc φ e Poly B d Poly B p Poly B e X + d X = p X
89 oveq2 c = d X e X + c = e X + d X
90 89 eqeq1d c = d X e X + c = p X e X + d X = p X
91 90 rexbidv c = d X p Poly B e X + c = p X p Poly B e X + d X = p X
92 88 91 syl5ibrcom φ e Poly B d Poly B c = d X p Poly B e X + c = p X
93 92 rexlimdva φ e Poly B d Poly B c = d X p Poly B e X + c = p X
94 oveq1 b = e X b + c = e X + c
95 94 eqeq1d b = e X b + c = p X e X + c = p X
96 95 rexbidv b = e X p Poly B b + c = p X p Poly B e X + c = p X
97 96 imbi2d b = e X d Poly B c = d X p Poly B b + c = p X d Poly B c = d X p Poly B e X + c = p X
98 93 97 syl5ibrcom φ e Poly B b = e X d Poly B c = d X p Poly B b + c = p X
99 98 rexlimdva φ e Poly B b = e X d Poly B c = d X p Poly B b + c = p X
100 99 3imp φ e Poly B b = e X d Poly B c = d X p Poly B b + c = p X
101 49 57 65 100 syl3anb φ b a | p Poly B a = p X c a | p Poly B a = p X p Poly B b + c = p X
102 ovex b + c V
103 eqeq1 a = b + c a = p X b + c = p X
104 103 rexbidv a = b + c p Poly B a = p X p Poly B b + c = p X
105 102 104 elab b + c a | p Poly B a = p X p Poly B b + c = p X
106 101 105 sylibr φ b a | p Poly B a = p X c a | p Poly B a = p X b + c a | p Poly B a = p X
107 ax-1cn 1
108 cnfldneg 1 inv g fld 1 = 1
109 107 108 mp1i φ inv g fld 1 = 1
110 cnfld1 1 = 1 fld
111 110 subrg1cl B SubRing fld 1 B
112 1 111 syl φ 1 B
113 eqid inv g fld = inv g fld
114 113 subginvcl B SubGrp fld 1 B inv g fld 1 B
115 45 112 114 syl2anc φ inv g fld 1 B
116 109 115 eqeltrrd φ 1 B
117 plyconst B 1 B × 1 Poly B
118 10 116 117 syl2anc φ × 1 Poly B
119 118 adantr φ e Poly B × 1 Poly B
120 simpr φ e Poly B e Poly B
121 cnfldmul × = fld
122 121 subrgmcl B SubRing fld a B b B a b B
123 122 3expb B SubRing fld a B b B a b B
124 1 123 sylan φ a B b B a b B
125 124 adantlr φ e Poly B a B b B a b B
126 119 120 71 125 plymul φ e Poly B × 1 × f e Poly B
127 ffvelrn e : X e X
128 74 2 127 syl2anr φ e Poly B e X
129 cnfldneg e X inv g fld e X = e X
130 128 129 syl φ e Poly B inv g fld e X = e X
131 negex 1 V
132 fnconstg 1 V × 1 Fn
133 131 132 mp1i φ e Poly B × 1 Fn
134 75 adantl φ e Poly B e Fn
135 80 a1i φ e Poly B V
136 2 adantr φ e Poly B X
137 fnfvof × 1 Fn e Fn V X × 1 × f e X = × 1 X e X
138 133 134 135 136 137 syl22anc φ e Poly B × 1 × f e X = × 1 X e X
139 131 fvconst2 X × 1 X = 1
140 136 139 syl φ e Poly B × 1 X = 1
141 140 oveq1d φ e Poly B × 1 X e X = -1 e X
142 128 mulm1d φ e Poly B -1 e X = e X
143 138 141 142 3eqtrd φ e Poly B × 1 × f e X = e X
144 130 143 eqtr4d φ e Poly B inv g fld e X = × 1 × f e X
145 fveq1 p = × 1 × f e p X = × 1 × f e X
146 145 rspceeqv × 1 × f e Poly B inv g fld e X = × 1 × f e X p Poly B inv g fld e X = p X
147 126 144 146 syl2anc φ e Poly B p Poly B inv g fld e X = p X
148 fveqeq2 b = e X inv g fld b = p X inv g fld e X = p X
149 148 rexbidv b = e X p Poly B inv g fld b = p X p Poly B inv g fld e X = p X
150 147 149 syl5ibrcom φ e Poly B b = e X p Poly B inv g fld b = p X
151 150 rexlimdva φ e Poly B b = e X p Poly B inv g fld b = p X
152 151 imp φ e Poly B b = e X p Poly B inv g fld b = p X
153 57 152 sylan2b φ b a | p Poly B a = p X p Poly B inv g fld b = p X
154 fvex inv g fld b V
155 eqeq1 a = inv g fld b a = p X inv g fld b = p X
156 155 rexbidv a = inv g fld b p Poly B a = p X p Poly B inv g fld b = p X
157 154 156 elab inv g fld b a | p Poly B a = p X p Poly B inv g fld b = p X
158 153 157 sylibr φ b a | p Poly B a = p X inv g fld b a | p Poly B a = p X
159 110 a1i φ 1 = 1 fld
160 121 a1i φ × = fld
161 43 112 sseldd φ 1 a | p Poly B a = p X
162 125 adantlr φ e Poly B d Poly B a B b B a b B
163 66 67 72 162 plymul φ e Poly B d Poly B e × f d Poly B
164 fnfvof e Fn d Fn V X e × f d X = e X d X
165 76 79 81 82 164 syl22anc φ e Poly B d Poly B e × f d X = e X d X
166 165 eqcomd φ e Poly B d Poly B e X d X = e × f d X
167 fveq1 p = e × f d p X = e × f d X
168 167 rspceeqv e × f d Poly B e X d X = e × f d X p Poly B e X d X = p X
169 163 166 168 syl2anc φ e Poly B d Poly B p Poly B e X d X = p X
170 oveq2 c = d X e X c = e X d X
171 170 eqeq1d c = d X e X c = p X e X d X = p X
172 171 rexbidv c = d X p Poly B e X c = p X p Poly B e X d X = p X
173 169 172 syl5ibrcom φ e Poly B d Poly B c = d X p Poly B e X c = p X
174 173 rexlimdva φ e Poly B d Poly B c = d X p Poly B e X c = p X
175 oveq1 b = e X b c = e X c
176 175 eqeq1d b = e X b c = p X e X c = p X
177 176 rexbidv b = e X p Poly B b c = p X p Poly B e X c = p X
178 177 imbi2d b = e X d Poly B c = d X p Poly B b c = p X d Poly B c = d X p Poly B e X c = p X
179 174 178 syl5ibrcom φ e Poly B b = e X d Poly B c = d X p Poly B b c = p X
180 179 rexlimdva φ e Poly B b = e X d Poly B c = d X p Poly B b c = p X
181 180 3imp φ e Poly B b = e X d Poly B c = d X p Poly B b c = p X
182 49 57 65 181 syl3anb φ b a | p Poly B a = p X c a | p Poly B a = p X p Poly B b c = p X
183 ovex b c V
184 eqeq1 a = b c a = p X b c = p X
185 184 rexbidv a = b c p Poly B a = p X p Poly B b c = p X
186 183 185 elab b c a | p Poly B a = p X p Poly B b c = p X
187 182 186 sylibr φ b a | p Poly B a = p X c a | p Poly B a = p X b c a | p Poly B a = p X
188 15 17 19 29 48 106 158 159 160 161 187 6 issubrngd2 φ a | p Poly B a = p X SubRing fld
189 plyid B 1 B X p Poly B
190 10 112 189 syl2anc φ X p Poly B
191 df-idp X p = I
192 191 fveq1i X p X = I X
193 fvresi X I X = X
194 2 193 syl φ I X = X
195 192 194 eqtr2id φ X = X p X
196 fveq1 p = X p p X = X p X
197 196 rspceeqv X p Poly B X = X p X p Poly B X = p X
198 190 195 197 syl2anc φ p Poly B X = p X
199 eqeq1 a = X a = p X X = p X
200 199 rexbidv a = X p Poly B a = p X p Poly B X = p X
201 2 198 200 elabd φ X a | p Poly B a = p X
202 201 snssd φ X a | p Poly B a = p X
203 43 202 unssd φ B X a | p Poly B a = p X
204 6 8 12 13 14 188 203 rgspnmin φ RingSpan fld B X a | p Poly B a = p X
205 204 sseld φ V RingSpan fld B X V a | p Poly B a = p X
206 fvex p X V
207 eleq1 V = p X V V p X V
208 206 207 mpbiri V = p X V V
209 208 rexlimivw p Poly B V = p X V V
210 eqeq1 a = V a = p X V = p X
211 210 rexbidv a = V p Poly B a = p X p Poly B V = p X
212 209 211 elab3 V a | p Poly B a = p X p Poly B V = p X
213 205 212 syl6ib φ V RingSpan fld B X p Poly B V = p X
214 6 8 12 13 14 rgspncl φ RingSpan fld B X SubRing fld
215 214 adantr φ p Poly B RingSpan fld B X SubRing fld
216 simpr φ p Poly B p Poly B
217 6 8 12 13 14 rgspnssid φ B X RingSpan fld B X
218 217 unssbd φ X RingSpan fld B X
219 snidg X X X
220 2 219 syl φ X X
221 218 220 sseldd φ X RingSpan fld B X
222 221 adantr φ p Poly B X RingSpan fld B X
223 217 unssad φ B RingSpan fld B X
224 223 adantr φ p Poly B B RingSpan fld B X
225 215 216 222 224 cnsrplycl φ p Poly B p X RingSpan fld B X
226 eleq1 V = p X V RingSpan fld B X p X RingSpan fld B X
227 225 226 syl5ibrcom φ p Poly B V = p X V RingSpan fld B X
228 227 rexlimdva φ p Poly B V = p X V RingSpan fld B X
229 213 228 impbid φ V RingSpan fld B X p Poly B V = p X
230 4 229 bitrd φ V S p Poly B V = p X