Step | Hyp | Ref
| Expression |
1 | | rngunsnply.s |
. . 3
RingSpanℂfld |
2 | 1 | eleq2d 2687 |
. 2
RingSpanℂfld |
3 | | cnring 19768 |
. . . . . . 7
ℂfld |
4 | 3 | a1i 11 |
. . . . . 6
ℂfld |
5 | | cnfldbas 19750 |
. . . . . . 7
ℂfld |
6 | 5 | a1i 11 |
. . . . . 6
ℂfld |
7 | | rngunsnply.b |
. . . . . . . 8
SubRingℂfld |
8 | 5 | subrgss 18781 |
. . . . . . . 8
SubRingℂfld
|
9 | 7, 8 | syl 17 |
. . . . . . 7
|
10 | | rngunsnply.x |
. . . . . . . 8
|
11 | 10 | snssd 4340 |
. . . . . . 7
|
12 | 9, 11 | unssd 3789 |
. . . . . 6
|
13 | | eqidd 2623 |
. . . . . 6
RingSpanℂfld
RingSpanℂfld |
14 | | eqidd 2623 |
. . . . . 6
RingSpanℂfld RingSpanℂfld |
15 | | eqidd 2623 |
. . . . . . 7
ℂfld ↾s Poly ℂfld
↾s
Poly |
16 | | cnfld0 19770 |
. . . . . . . 8
ℂfld |
17 | 16 | a1i 11 |
. . . . . . 7
ℂfld |
18 | | cnfldadd 19751 |
. . . . . . . 8
ℂfld |
19 | 18 | a1i 11 |
. . . . . . 7
ℂfld |
20 | | plyf 23954 |
. . . . . . . . . . . 12
Poly
|
21 | | ffvelrn 6357 |
. . . . . . . . . . . 12
|
22 | 20, 10, 21 | syl2anr 495 |
. . . . . . . . . . 11
Poly |
23 | | eleq1 2689 |
. . . . . . . . . . 11
|
24 | 22, 23 | syl5ibrcom 237 |
. . . . . . . . . 10
Poly
|
25 | 24 | rexlimdva 3031 |
. . . . . . . . 9
Poly |
26 | 25 | ss2abdv 3675 |
. . . . . . . 8
Poly
|
27 | | abid2 2745 |
. . . . . . . . 9
|
28 | 27, 5 | eqtri 2644 |
. . . . . . . 8
ℂfld |
29 | 26, 28 | syl6sseq 3651 |
. . . . . . 7
Poly
ℂfld |
30 | | abid2 2745 |
. . . . . . . . 9
|
31 | | plyconst 23962 |
. . . . . . . . . . . . 13
Poly |
32 | 9, 31 | sylan 488 |
. . . . . . . . . . . 12
Poly |
33 | 10 | adantr 481 |
. . . . . . . . . . . . . 14
|
34 | | vex 3203 |
. . . . . . . . . . . . . . 15
|
35 | 34 | fvconst2 6469 |
. . . . . . . . . . . . . 14
|
36 | 33, 35 | syl 17 |
. . . . . . . . . . . . 13
|
37 | 36 | eqcomd 2628 |
. . . . . . . . . . . 12
|
38 | | fveq1 6190 |
. . . . . . . . . . . . . 14
|
39 | 38 | eqeq2d 2632 |
. . . . . . . . . . . . 13
|
40 | 39 | rspcev 3309 |
. . . . . . . . . . . 12
Poly
Poly |
41 | 32, 37, 40 | syl2anc 693 |
. . . . . . . . . . 11
Poly |
42 | 41 | ex 450 |
. . . . . . . . . 10
Poly |
43 | 42 | ss2abdv 3675 |
. . . . . . . . 9
Poly |
44 | 30, 43 | syl5eqssr 3650 |
. . . . . . . 8
Poly |
45 | | subrgsubg 18786 |
. . . . . . . . . 10
SubRingℂfld
SubGrpℂfld |
46 | 7, 45 | syl 17 |
. . . . . . . . 9
SubGrpℂfld |
47 | 16 | subg0cl 17602 |
. . . . . . . . 9
SubGrpℂfld
|
48 | 46, 47 | syl 17 |
. . . . . . . 8
|
49 | 44, 48 | sseldd 3604 |
. . . . . . 7
Poly |
50 | | biid 251 |
. . . . . . . . 9
|
51 | | vex 3203 |
. . . . . . . . . 10
|
52 | | eqeq1 2626 |
. . . . . . . . . . . 12
|
53 | 52 | rexbidv 3052 |
. . . . . . . . . . 11
Poly Poly |
54 | | fveq1 6190 |
. . . . . . . . . . . . 13
|
55 | 54 | eqeq2d 2632 |
. . . . . . . . . . . 12
|
56 | 55 | cbvrexv 3172 |
. . . . . . . . . . 11
Poly Poly |
57 | 53, 56 | syl6bb 276 |
. . . . . . . . . 10
Poly Poly |
58 | 51, 57 | elab 3350 |
. . . . . . . . 9
Poly
Poly |
59 | | vex 3203 |
. . . . . . . . . 10
|
60 | | eqeq1 2626 |
. . . . . . . . . . . 12
|
61 | 60 | rexbidv 3052 |
. . . . . . . . . . 11
Poly Poly |
62 | | fveq1 6190 |
. . . . . . . . . . . . 13
|
63 | 62 | eqeq2d 2632 |
. . . . . . . . . . . 12
|
64 | 63 | cbvrexv 3172 |
. . . . . . . . . . 11
Poly Poly |
65 | 61, 64 | syl6bb 276 |
. . . . . . . . . 10
Poly Poly |
66 | 59, 65 | elab 3350 |
. . . . . . . . 9
Poly
Poly |
67 | | simplr 792 |
. . . . . . . . . . . . . . . 16
Poly
Poly Poly |
68 | | simpr 477 |
. . . . . . . . . . . . . . . 16
Poly
Poly Poly |
69 | 18 | subrgacl 18791 |
. . . . . . . . . . . . . . . . . . . 20
SubRingℂfld
|
70 | 69 | 3expb 1266 |
. . . . . . . . . . . . . . . . . . 19
SubRingℂfld
|
71 | 7, 70 | sylan 488 |
. . . . . . . . . . . . . . . . . 18
|
72 | 71 | adantlr 751 |
. . . . . . . . . . . . . . . . 17
Poly
|
73 | 72 | adantlr 751 |
. . . . . . . . . . . . . . . 16
Poly Poly
|
74 | 67, 68, 73 | plyadd 23973 |
. . . . . . . . . . . . . . 15
Poly
Poly Poly |
75 | | plyf 23954 |
. . . . . . . . . . . . . . . . . . 19
Poly
|
76 | | ffn 6045 |
. . . . . . . . . . . . . . . . . . 19
|
77 | 75, 76 | syl 17 |
. . . . . . . . . . . . . . . . . 18
Poly
|
78 | 77 | ad2antlr 763 |
. . . . . . . . . . . . . . . . 17
Poly
Poly |
79 | | plyf 23954 |
. . . . . . . . . . . . . . . . . . 19
Poly
|
80 | | ffn 6045 |
. . . . . . . . . . . . . . . . . . 19
|
81 | 79, 80 | syl 17 |
. . . . . . . . . . . . . . . . . 18
Poly
|
82 | 81 | adantl 482 |
. . . . . . . . . . . . . . . . 17
Poly
Poly |
83 | | cnex 10017 |
. . . . . . . . . . . . . . . . . 18
|
84 | 83 | a1i 11 |
. . . . . . . . . . . . . . . . 17
Poly
Poly |
85 | 10 | ad2antrr 762 |
. . . . . . . . . . . . . . . . 17
Poly
Poly |
86 | | fnfvof 6911 |
. . . . . . . . . . . . . . . . 17
|
87 | 78, 82, 84, 85, 86 | syl22anc 1327 |
. . . . . . . . . . . . . . . 16
Poly
Poly |
88 | 87 | eqcomd 2628 |
. . . . . . . . . . . . . . 15
Poly
Poly |
89 | | fveq1 6190 |
. . . . . . . . . . . . . . . . 17
|
90 | 89 | eqeq2d 2632 |
. . . . . . . . . . . . . . . 16
|
91 | 90 | rspcev 3309 |
. . . . . . . . . . . . . . 15
Poly Poly |
92 | 74, 88, 91 | syl2anc 693 |
. . . . . . . . . . . . . 14
Poly
Poly Poly |
93 | | oveq2 6658 |
. . . . . . . . . . . . . . . 16
|
94 | 93 | eqeq1d 2624 |
. . . . . . . . . . . . . . 15
|
95 | 94 | rexbidv 3052 |
. . . . . . . . . . . . . 14
Poly Poly |
96 | 92, 95 | syl5ibrcom 237 |
. . . . . . . . . . . . 13
Poly
Poly
Poly |
97 | 96 | rexlimdva 3031 |
. . . . . . . . . . . 12
Poly Poly
Poly |
98 | | oveq1 6657 |
. . . . . . . . . . . . . . 15
|
99 | 98 | eqeq1d 2624 |
. . . . . . . . . . . . . 14
|
100 | 99 | rexbidv 3052 |
. . . . . . . . . . . . 13
Poly Poly |
101 | 100 | imbi2d 330 |
. . . . . . . . . . . 12
Poly
Poly
Poly Poly |
102 | 97, 101 | syl5ibrcom 237 |
. . . . . . . . . . 11
Poly
Poly Poly |
103 | 102 | rexlimdva 3031 |
. . . . . . . . . 10
Poly Poly
Poly |
104 | 103 | 3imp 1256 |
. . . . . . . . 9
Poly Poly Poly |
105 | 50, 58, 66, 104 | syl3anb 1369 |
. . . . . . . 8
Poly Poly
Poly |
106 | | ovex 6678 |
. . . . . . . . 9
|
107 | | eqeq1 2626 |
. . . . . . . . . 10
|
108 | 107 | rexbidv 3052 |
. . . . . . . . 9
Poly Poly |
109 | 106, 108 | elab 3350 |
. . . . . . . 8
Poly
Poly |
110 | 105, 109 | sylibr 224 |
. . . . . . 7
Poly Poly
Poly |
111 | | ax-1cn 9994 |
. . . . . . . . . . . . . . . . . 18
|
112 | | cnfldneg 19772 |
. . . . . . . . . . . . . . . . . 18
ℂfld |
113 | 111, 112 | mp1i 13 |
. . . . . . . . . . . . . . . . 17
ℂfld |
114 | | cnfld1 19771 |
. . . . . . . . . . . . . . . . . . . 20
ℂfld |
115 | 114 | subrg1cl 18788 |
. . . . . . . . . . . . . . . . . . 19
SubRingℂfld
|
116 | 7, 115 | syl 17 |
. . . . . . . . . . . . . . . . . 18
|
117 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . 19
ℂfld
ℂfld |
118 | 117 | subginvcl 17603 |
. . . . . . . . . . . . . . . . . 18
SubGrpℂfld
ℂfld |
119 | 46, 116, 118 | syl2anc 693 |
. . . . . . . . . . . . . . . . 17
ℂfld |
120 | 113, 119 | eqeltrrd 2702 |
. . . . . . . . . . . . . . . 16
|
121 | | plyconst 23962 |
. . . . . . . . . . . . . . . 16
Poly |
122 | 9, 120, 121 | syl2anc 693 |
. . . . . . . . . . . . . . 15
Poly |
123 | 122 | adantr 481 |
. . . . . . . . . . . . . 14
Poly Poly |
124 | | simpr 477 |
. . . . . . . . . . . . . 14
Poly Poly |
125 | | cnfldmul 19752 |
. . . . . . . . . . . . . . . . . 18
ℂfld |
126 | 125 | subrgmcl 18792 |
. . . . . . . . . . . . . . . . 17
SubRingℂfld
|
127 | 126 | 3expb 1266 |
. . . . . . . . . . . . . . . 16
SubRingℂfld
|
128 | 7, 127 | sylan 488 |
. . . . . . . . . . . . . . 15
|
129 | 128 | adantlr 751 |
. . . . . . . . . . . . . 14
Poly
|
130 | 123, 124,
72, 129 | plymul 23974 |
. . . . . . . . . . . . 13
Poly Poly |
131 | | ffvelrn 6357 |
. . . . . . . . . . . . . . . 16
|
132 | 75, 10, 131 | syl2anr 495 |
. . . . . . . . . . . . . . 15
Poly |
133 | | cnfldneg 19772 |
. . . . . . . . . . . . . . 15
ℂfld |
134 | 132, 133 | syl 17 |
. . . . . . . . . . . . . 14
Poly ℂfld |
135 | | negex 10279 |
. . . . . . . . . . . . . . . . 17
|
136 | | fnconstg 6093 |
. . . . . . . . . . . . . . . . 17
|
137 | 135, 136 | mp1i 13 |
. . . . . . . . . . . . . . . 16
Poly |
138 | 77 | adantl 482 |
. . . . . . . . . . . . . . . 16
Poly |
139 | 83 | a1i 11 |
. . . . . . . . . . . . . . . 16
Poly |
140 | 10 | adantr 481 |
. . . . . . . . . . . . . . . 16
Poly |
141 | | fnfvof 6911 |
. . . . . . . . . . . . . . . 16
|
142 | 137, 138,
139, 140, 141 | syl22anc 1327 |
. . . . . . . . . . . . . . 15
Poly |
143 | 135 | fvconst2 6469 |
. . . . . . . . . . . . . . . . 17
|
144 | 140, 143 | syl 17 |
. . . . . . . . . . . . . . . 16
Poly |
145 | 144 | oveq1d 6665 |
. . . . . . . . . . . . . . 15
Poly |
146 | 132 | mulm1d 10482 |
. . . . . . . . . . . . . . 15
Poly |
147 | 142, 145,
146 | 3eqtrd 2660 |
. . . . . . . . . . . . . 14
Poly |
148 | 134, 147 | eqtr4d 2659 |
. . . . . . . . . . . . 13
Poly ℂfld |
149 | | fveq1 6190 |
. . . . . . . . . . . . . . 15
|
150 | 149 | eqeq2d 2632 |
. . . . . . . . . . . . . 14
ℂfld
ℂfld |
151 | 150 | rspcev 3309 |
. . . . . . . . . . . . 13
Poly ℂfld
Polyℂfld |
152 | 130, 148,
151 | syl2anc 693 |
. . . . . . . . . . . 12
Poly Polyℂfld |
153 | | fveq2 6191 |
. . . . . . . . . . . . . 14
ℂfld ℂfld |
154 | 153 | eqeq1d 2624 |
. . . . . . . . . . . . 13
ℂfld
ℂfld |
155 | 154 | rexbidv 3052 |
. . . . . . . . . . . 12
Polyℂfld
Polyℂfld |
156 | 152, 155 | syl5ibrcom 237 |
. . . . . . . . . . 11
Poly
Polyℂfld |
157 | 156 | rexlimdva 3031 |
. . . . . . . . . 10
Poly
Polyℂfld |
158 | 157 | imp 445 |
. . . . . . . . 9
Poly Polyℂfld |
159 | 58, 158 | sylan2b 492 |
. . . . . . . 8
Poly
Polyℂfld |
160 | | fvex 6201 |
. . . . . . . . 9
ℂfld |
161 | | eqeq1 2626 |
. . . . . . . . . 10
ℂfld ℂfld |
162 | 161 | rexbidv 3052 |
. . . . . . . . 9
ℂfld Poly
Polyℂfld |
163 | 160, 162 | elab 3350 |
. . . . . . . 8
ℂfld Poly
Polyℂfld |
164 | 159, 163 | sylibr 224 |
. . . . . . 7
Poly
ℂfld Poly |
165 | 114 | a1i 11 |
. . . . . . 7
ℂfld |
166 | 125 | a1i 11 |
. . . . . . 7
ℂfld |
167 | 44, 116 | sseldd 3604 |
. . . . . . 7
Poly |
168 | 129 | adantlr 751 |
. . . . . . . . . . . . . . . 16
Poly Poly
|
169 | 67, 68, 73, 168 | plymul 23974 |
. . . . . . . . . . . . . . 15
Poly
Poly Poly |
170 | | fnfvof 6911 |
. . . . . . . . . . . . . . . . 17
|
171 | 78, 82, 84, 85, 170 | syl22anc 1327 |
. . . . . . . . . . . . . . . 16
Poly
Poly |
172 | 171 | eqcomd 2628 |
. . . . . . . . . . . . . . 15
Poly
Poly |
173 | | fveq1 6190 |
. . . . . . . . . . . . . . . . 17
|
174 | 173 | eqeq2d 2632 |
. . . . . . . . . . . . . . . 16
|
175 | 174 | rspcev 3309 |
. . . . . . . . . . . . . . 15
Poly Poly |
176 | 169, 172,
175 | syl2anc 693 |
. . . . . . . . . . . . . 14
Poly
Poly Poly |
177 | | oveq2 6658 |
. . . . . . . . . . . . . . . 16
|
178 | 177 | eqeq1d 2624 |
. . . . . . . . . . . . . . 15
|
179 | 178 | rexbidv 3052 |
. . . . . . . . . . . . . 14
Poly Poly |
180 | 176, 179 | syl5ibrcom 237 |
. . . . . . . . . . . . 13
Poly
Poly
Poly |
181 | 180 | rexlimdva 3031 |
. . . . . . . . . . . 12
Poly Poly
Poly |
182 | | oveq1 6657 |
. . . . . . . . . . . . . . 15
|
183 | 182 | eqeq1d 2624 |
. . . . . . . . . . . . . 14
|
184 | 183 | rexbidv 3052 |
. . . . . . . . . . . . 13
Poly Poly |
185 | 184 | imbi2d 330 |
. . . . . . . . . . . 12
Poly
Poly
Poly Poly |
186 | 181, 185 | syl5ibrcom 237 |
. . . . . . . . . . 11
Poly
Poly Poly |
187 | 186 | rexlimdva 3031 |
. . . . . . . . . 10
Poly Poly
Poly |
188 | 187 | 3imp 1256 |
. . . . . . . . 9
Poly Poly Poly |
189 | 50, 58, 66, 188 | syl3anb 1369 |
. . . . . . . 8
Poly Poly
Poly |
190 | | ovex 6678 |
. . . . . . . . 9
|
191 | | eqeq1 2626 |
. . . . . . . . . 10
|
192 | 191 | rexbidv 3052 |
. . . . . . . . 9
Poly Poly |
193 | 190, 192 | elab 3350 |
. . . . . . . 8
Poly
Poly |
194 | 189, 193 | sylibr 224 |
. . . . . . 7
Poly Poly
Poly |
195 | 15, 17, 19, 29, 49, 110, 164, 165, 166, 167, 194, 4 | issubrngd2 19189 |
. . . . . 6
Poly SubRingℂfld |
196 | | plyid 23965 |
. . . . . . . . . . 11
Poly |
197 | 9, 116, 196 | syl2anc 693 |
. . . . . . . . . 10
Poly |
198 | | df-idp 23945 |
. . . . . . . . . . . 12
|
199 | 198 | fveq1i 6192 |
. . . . . . . . . . 11
|
200 | | fvresi 6439 |
. . . . . . . . . . . 12
|
201 | 10, 200 | syl 17 |
. . . . . . . . . . 11
|
202 | 199, 201 | syl5req 2669 |
. . . . . . . . . 10
|
203 | | fveq1 6190 |
. . . . . . . . . . . 12
|
204 | 203 | eqeq2d 2632 |
. . . . . . . . . . 11
|
205 | 204 | rspcev 3309 |
. . . . . . . . . 10
Poly Poly |
206 | 197, 202,
205 | syl2anc 693 |
. . . . . . . . 9
Poly |
207 | | eqeq1 2626 |
. . . . . . . . . . . 12
|
208 | 207 | rexbidv 3052 |
. . . . . . . . . . 11
Poly Poly |
209 | 208 | elabg 3351 |
. . . . . . . . . 10
Poly
Poly
|
210 | 10, 209 | syl 17 |
. . . . . . . . 9
Poly
Poly |
211 | 206, 210 | mpbird 247 |
. . . . . . . 8
Poly |
212 | 211 | snssd 4340 |
. . . . . . 7
Poly |
213 | 44, 212 | unssd 3789 |
. . . . . 6
Poly |
214 | 4, 6, 12, 13, 14, 195, 213 | rgspnmin 37741 |
. . . . 5
RingSpanℂfld Poly |
215 | 214 | sseld 3602 |
. . . 4
RingSpanℂfld
Poly |
216 | | fvex 6201 |
. . . . . . 7
|
217 | | eleq1 2689 |
. . . . . . 7
|
218 | 216, 217 | mpbiri 248 |
. . . . . 6
|
219 | 218 | rexlimivw 3029 |
. . . . 5
Poly
|
220 | | eqeq1 2626 |
. . . . . 6
|
221 | 220 | rexbidv 3052 |
. . . . 5
Poly Poly |
222 | 219, 221 | elab3 3358 |
. . . 4
Poly
Poly
|
223 | 215, 222 | syl6ib 241 |
. . 3
RingSpanℂfld Poly
|
224 | 4, 6, 12, 13, 14 | rgspncl 37739 |
. . . . . . 7
RingSpanℂfld SubRingℂfld |
225 | 224 | adantr 481 |
. . . . . 6
Poly RingSpanℂfld SubRingℂfld |
226 | | simpr 477 |
. . . . . 6
Poly Poly |
227 | 4, 6, 12, 13, 14 | rgspnssid 37740 |
. . . . . . . . 9
RingSpanℂfld |
228 | 227 | unssbd 3791 |
. . . . . . . 8
RingSpanℂfld |
229 | | snidg 4206 |
. . . . . . . . 9
|
230 | 10, 229 | syl 17 |
. . . . . . . 8
|
231 | 228, 230 | sseldd 3604 |
. . . . . . 7
RingSpanℂfld |
232 | 231 | adantr 481 |
. . . . . 6
Poly RingSpanℂfld |
233 | 227 | unssad 3790 |
. . . . . . 7
RingSpanℂfld |
234 | 233 | adantr 481 |
. . . . . 6
Poly RingSpanℂfld |
235 | 225, 226,
232, 234 | cnsrplycl 37737 |
. . . . 5
Poly RingSpanℂfld |
236 | | eleq1 2689 |
. . . . 5
RingSpanℂfld RingSpanℂfld |
237 | 235, 236 | syl5ibrcom 237 |
. . . 4
Poly
RingSpanℂfld |
238 | 237 | rexlimdva 3031 |
. . 3
Poly
RingSpanℂfld |
239 | 223, 238 | impbid 202 |
. 2
RingSpanℂfld
Poly
|
240 | 2, 239 | bitrd 268 |
1
Poly |