Metamath Proof Explorer


Theorem aannenlem2

Description: Lemma for aannen . (Contributed by Stefan O'Rear, 16-Nov-2014)

Ref Expression
Hypothesis aannenlem.a H = a 0 b | c d Poly | d 0 𝑝 deg d a e 0 coeff d e a c b = 0
Assertion aannenlem2 𝔸 = ran H

Proof

Step Hyp Ref Expression
1 aannenlem.a H = a 0 b | c d Poly | d 0 𝑝 deg d a e 0 coeff d e a c b = 0
2 fveqeq2 b = g c b = 0 c g = 0
3 2 rexbidv b = g c d Poly | d 0 𝑝 deg d sup 0 deg h g 0 | i 0 deg h g = coeff h i * < e 0 coeff d e sup 0 deg h g 0 | i 0 deg h g = coeff h i * < c b = 0 c d Poly | d 0 𝑝 deg d sup 0 deg h g 0 | i 0 deg h g = coeff h i * < e 0 coeff d e sup 0 deg h g 0 | i 0 deg h g = coeff h i * < c g = 0
4 simp3 h Poly 0 𝑝 h g = 0 g g
5 neeq1 d = h d 0 𝑝 h 0 𝑝
6 fveq2 d = h deg d = deg h
7 6 breq1d d = h deg d sup 0 deg h g 0 | i 0 deg h g = coeff h i * < deg h sup 0 deg h g 0 | i 0 deg h g = coeff h i * <
8 fveq2 d = h coeff d = coeff h
9 8 fveq1d d = h coeff d e = coeff h e
10 9 fveq2d d = h coeff d e = coeff h e
11 10 breq1d d = h coeff d e sup 0 deg h g 0 | i 0 deg h g = coeff h i * < coeff h e sup 0 deg h g 0 | i 0 deg h g = coeff h i * <
12 11 ralbidv d = h e 0 coeff d e sup 0 deg h g 0 | i 0 deg h g = coeff h i * < e 0 coeff h e sup 0 deg h g 0 | i 0 deg h g = coeff h i * <
13 5 7 12 3anbi123d d = h d 0 𝑝 deg d sup 0 deg h g 0 | i 0 deg h g = coeff h i * < e 0 coeff d e sup 0 deg h g 0 | i 0 deg h g = coeff h i * < h 0 𝑝 deg h sup 0 deg h g 0 | i 0 deg h g = coeff h i * < e 0 coeff h e sup 0 deg h g 0 | i 0 deg h g = coeff h i * <
14 eldifi h Poly 0 𝑝 h Poly
15 14 adantr h Poly 0 𝑝 g h Poly
16 15 3adant2 h Poly 0 𝑝 h g = 0 g h Poly
17 eldifsni h Poly 0 𝑝 h 0 𝑝
18 17 adantr h Poly 0 𝑝 g h 0 𝑝
19 0nn0 0 0
20 dgrcl h Poly deg h 0
21 15 20 syl h Poly 0 𝑝 g deg h 0
22 prssi 0 0 deg h 0 0 deg h 0
23 19 21 22 sylancr h Poly 0 𝑝 g 0 deg h 0
24 ssrab2 g 0 | i 0 deg h g = coeff h i 0
25 24 a1i h Poly 0 𝑝 g g 0 | i 0 deg h g = coeff h i 0
26 23 25 unssd h Poly 0 𝑝 g 0 deg h g 0 | i 0 deg h g = coeff h i 0
27 nn0ssre 0
28 ressxr *
29 27 28 sstri 0 *
30 26 29 sstrdi h Poly 0 𝑝 g 0 deg h g 0 | i 0 deg h g = coeff h i *
31 fvex deg h V
32 31 prid2 deg h 0 deg h
33 elun1 deg h 0 deg h deg h 0 deg h g 0 | i 0 deg h g = coeff h i
34 32 33 ax-mp deg h 0 deg h g 0 | i 0 deg h g = coeff h i
35 supxrub 0 deg h g 0 | i 0 deg h g = coeff h i * deg h 0 deg h g 0 | i 0 deg h g = coeff h i deg h sup 0 deg h g 0 | i 0 deg h g = coeff h i * <
36 30 34 35 sylancl h Poly 0 𝑝 g deg h sup 0 deg h g 0 | i 0 deg h g = coeff h i * <
37 30 adantr h Poly 0 𝑝 g e 0 0 deg h g 0 | i 0 deg h g = coeff h i *
38 fveq2 coeff h e = 0 coeff h e = 0
39 abs0 0 = 0
40 38 39 eqtrdi coeff h e = 0 coeff h e = 0
41 c0ex 0 V
42 41 prid1 0 0 deg h
43 elun1 0 0 deg h 0 0 deg h g 0 | i 0 deg h g = coeff h i
44 42 43 ax-mp 0 0 deg h g 0 | i 0 deg h g = coeff h i
45 40 44 eqeltrdi coeff h e = 0 coeff h e 0 deg h g 0 | i 0 deg h g = coeff h i
46 45 adantl h Poly 0 𝑝 g e 0 coeff h e = 0 coeff h e 0 deg h g 0 | i 0 deg h g = coeff h i
47 eqeq1 g = coeff h e g = coeff h i coeff h e = coeff h i
48 47 rexbidv g = coeff h e i 0 deg h g = coeff h i i 0 deg h coeff h e = coeff h i
49 0z 0
50 eqid coeff h = coeff h
51 50 coef2 h Poly 0 coeff h : 0
52 15 49 51 sylancl h Poly 0 𝑝 g coeff h : 0
53 52 ffvelrnda h Poly 0 𝑝 g e 0 coeff h e
54 nn0abscl coeff h e coeff h e 0
55 53 54 syl h Poly 0 𝑝 g e 0 coeff h e 0
56 55 adantr h Poly 0 𝑝 g e 0 coeff h e 0 coeff h e 0
57 simplr h Poly 0 𝑝 g e 0 coeff h e 0 e 0
58 21 ad2antrr h Poly 0 𝑝 g e 0 coeff h e 0 deg h 0
59 15 ad2antrr h Poly 0 𝑝 g e 0 coeff h e 0 h Poly
60 simpr h Poly 0 𝑝 g e 0 coeff h e 0 coeff h e 0
61 eqid deg h = deg h
62 50 61 dgrub h Poly e 0 coeff h e 0 e deg h
63 59 57 60 62 syl3anc h Poly 0 𝑝 g e 0 coeff h e 0 e deg h
64 elfz2nn0 e 0 deg h e 0 deg h 0 e deg h
65 57 58 63 64 syl3anbrc h Poly 0 𝑝 g e 0 coeff h e 0 e 0 deg h
66 eqid coeff h e = coeff h e
67 2fveq3 i = e coeff h i = coeff h e
68 67 rspceeqv e 0 deg h coeff h e = coeff h e i 0 deg h coeff h e = coeff h i
69 65 66 68 sylancl h Poly 0 𝑝 g e 0 coeff h e 0 i 0 deg h coeff h e = coeff h i
70 48 56 69 elrabd h Poly 0 𝑝 g e 0 coeff h e 0 coeff h e g 0 | i 0 deg h g = coeff h i
71 elun2 coeff h e g 0 | i 0 deg h g = coeff h i coeff h e 0 deg h g 0 | i 0 deg h g = coeff h i
72 70 71 syl h Poly 0 𝑝 g e 0 coeff h e 0 coeff h e 0 deg h g 0 | i 0 deg h g = coeff h i
73 46 72 pm2.61dane h Poly 0 𝑝 g e 0 coeff h e 0 deg h g 0 | i 0 deg h g = coeff h i
74 supxrub 0 deg h g 0 | i 0 deg h g = coeff h i * coeff h e 0 deg h g 0 | i 0 deg h g = coeff h i coeff h e sup 0 deg h g 0 | i 0 deg h g = coeff h i * <
75 37 73 74 syl2anc h Poly 0 𝑝 g e 0 coeff h e sup 0 deg h g 0 | i 0 deg h g = coeff h i * <
76 75 ralrimiva h Poly 0 𝑝 g e 0 coeff h e sup 0 deg h g 0 | i 0 deg h g = coeff h i * <
77 18 36 76 3jca h Poly 0 𝑝 g h 0 𝑝 deg h sup 0 deg h g 0 | i 0 deg h g = coeff h i * < e 0 coeff h e sup 0 deg h g 0 | i 0 deg h g = coeff h i * <
78 77 3adant2 h Poly 0 𝑝 h g = 0 g h 0 𝑝 deg h sup 0 deg h g 0 | i 0 deg h g = coeff h i * < e 0 coeff h e sup 0 deg h g 0 | i 0 deg h g = coeff h i * <
79 13 16 78 elrabd h Poly 0 𝑝 h g = 0 g h d Poly | d 0 𝑝 deg d sup 0 deg h g 0 | i 0 deg h g = coeff h i * < e 0 coeff d e sup 0 deg h g 0 | i 0 deg h g = coeff h i * <
80 simp2 h Poly 0 𝑝 h g = 0 g h g = 0
81 fveq1 c = h c g = h g
82 81 eqeq1d c = h c g = 0 h g = 0
83 82 rspcev h d Poly | d 0 𝑝 deg d sup 0 deg h g 0 | i 0 deg h g = coeff h i * < e 0 coeff d e sup 0 deg h g 0 | i 0 deg h g = coeff h i * < h g = 0 c d Poly | d 0 𝑝 deg d sup 0 deg h g 0 | i 0 deg h g = coeff h i * < e 0 coeff d e sup 0 deg h g 0 | i 0 deg h g = coeff h i * < c g = 0
84 79 80 83 syl2anc h Poly 0 𝑝 h g = 0 g c d Poly | d 0 𝑝 deg d sup 0 deg h g 0 | i 0 deg h g = coeff h i * < e 0 coeff d e sup 0 deg h g 0 | i 0 deg h g = coeff h i * < c g = 0
85 3 4 84 elrabd h Poly 0 𝑝 h g = 0 g g b | c d Poly | d 0 𝑝 deg d sup 0 deg h g 0 | i 0 deg h g = coeff h i * < e 0 coeff d e sup 0 deg h g 0 | i 0 deg h g = coeff h i * < c b = 0
86 prfi 0 deg h Fin
87 fzfi 0 deg h Fin
88 abrexfi 0 deg h Fin g | i 0 deg h g = coeff h i Fin
89 87 88 ax-mp g | i 0 deg h g = coeff h i Fin
90 rabssab g 0 | i 0 deg h g = coeff h i g | i 0 deg h g = coeff h i
91 ssfi g | i 0 deg h g = coeff h i Fin g 0 | i 0 deg h g = coeff h i g | i 0 deg h g = coeff h i g 0 | i 0 deg h g = coeff h i Fin
92 89 90 91 mp2an g 0 | i 0 deg h g = coeff h i Fin
93 unfi 0 deg h Fin g 0 | i 0 deg h g = coeff h i Fin 0 deg h g 0 | i 0 deg h g = coeff h i Fin
94 86 92 93 mp2an 0 deg h g 0 | i 0 deg h g = coeff h i Fin
95 34 ne0ii 0 deg h g 0 | i 0 deg h g = coeff h i
96 xrltso < Or *
97 fisupcl < Or * 0 deg h g 0 | i 0 deg h g = coeff h i Fin 0 deg h g 0 | i 0 deg h g = coeff h i 0 deg h g 0 | i 0 deg h g = coeff h i * sup 0 deg h g 0 | i 0 deg h g = coeff h i * < 0 deg h g 0 | i 0 deg h g = coeff h i
98 96 97 mpan 0 deg h g 0 | i 0 deg h g = coeff h i Fin 0 deg h g 0 | i 0 deg h g = coeff h i 0 deg h g 0 | i 0 deg h g = coeff h i * sup 0 deg h g 0 | i 0 deg h g = coeff h i * < 0 deg h g 0 | i 0 deg h g = coeff h i
99 94 95 30 98 mp3an12i h Poly 0 𝑝 g sup 0 deg h g 0 | i 0 deg h g = coeff h i * < 0 deg h g 0 | i 0 deg h g = coeff h i
100 26 99 sseldd h Poly 0 𝑝 g sup 0 deg h g 0 | i 0 deg h g = coeff h i * < 0
101 100 3adant2 h Poly 0 𝑝 h g = 0 g sup 0 deg h g 0 | i 0 deg h g = coeff h i * < 0
102 eqidd h Poly 0 𝑝 h g = 0 g b | c d Poly | d 0 𝑝 deg d sup 0 deg h g 0 | i 0 deg h g = coeff h i * < e 0 coeff d e sup 0 deg h g 0 | i 0 deg h g = coeff h i * < c b = 0 = b | c d Poly | d 0 𝑝 deg d sup 0 deg h g 0 | i 0 deg h g = coeff h i * < e 0 coeff d e sup 0 deg h g 0 | i 0 deg h g = coeff h i * < c b = 0
103 breq2 a = sup 0 deg h g 0 | i 0 deg h g = coeff h i * < deg d a deg d sup 0 deg h g 0 | i 0 deg h g = coeff h i * <
104 breq2 a = sup 0 deg h g 0 | i 0 deg h g = coeff h i * < coeff d e a coeff d e sup 0 deg h g 0 | i 0 deg h g = coeff h i * <
105 104 ralbidv a = sup 0 deg h g 0 | i 0 deg h g = coeff h i * < e 0 coeff d e a e 0 coeff d e sup 0 deg h g 0 | i 0 deg h g = coeff h i * <
106 103 105 3anbi23d a = sup 0 deg h g 0 | i 0 deg h g = coeff h i * < d 0 𝑝 deg d a e 0 coeff d e a d 0 𝑝 deg d sup 0 deg h g 0 | i 0 deg h g = coeff h i * < e 0 coeff d e sup 0 deg h g 0 | i 0 deg h g = coeff h i * <
107 106 rabbidv a = sup 0 deg h g 0 | i 0 deg h g = coeff h i * < d Poly | d 0 𝑝 deg d a e 0 coeff d e a = d Poly | d 0 𝑝 deg d sup 0 deg h g 0 | i 0 deg h g = coeff h i * < e 0 coeff d e sup 0 deg h g 0 | i 0 deg h g = coeff h i * <
108 107 rexeqdv a = sup 0 deg h g 0 | i 0 deg h g = coeff h i * < c d Poly | d 0 𝑝 deg d a e 0 coeff d e a c b = 0 c d Poly | d 0 𝑝 deg d sup 0 deg h g 0 | i 0 deg h g = coeff h i * < e 0 coeff d e sup 0 deg h g 0 | i 0 deg h g = coeff h i * < c b = 0
109 108 rabbidv a = sup 0 deg h g 0 | i 0 deg h g = coeff h i * < b | c d Poly | d 0 𝑝 deg d a e 0 coeff d e a c b = 0 = b | c d Poly | d 0 𝑝 deg d sup 0 deg h g 0 | i 0 deg h g = coeff h i * < e 0 coeff d e sup 0 deg h g 0 | i 0 deg h g = coeff h i * < c b = 0
110 109 rspceeqv sup 0 deg h g 0 | i 0 deg h g = coeff h i * < 0 b | c d Poly | d 0 𝑝 deg d sup 0 deg h g 0 | i 0 deg h g = coeff h i * < e 0 coeff d e sup 0 deg h g 0 | i 0 deg h g = coeff h i * < c b = 0 = b | c d Poly | d 0 𝑝 deg d sup 0 deg h g 0 | i 0 deg h g = coeff h i * < e 0 coeff d e sup 0 deg h g 0 | i 0 deg h g = coeff h i * < c b = 0 a 0 b | c d Poly | d 0 𝑝 deg d sup 0 deg h g 0 | i 0 deg h g = coeff h i * < e 0 coeff d e sup 0 deg h g 0 | i 0 deg h g = coeff h i * < c b = 0 = b | c d Poly | d 0 𝑝 deg d a e 0 coeff d e a c b = 0
111 101 102 110 syl2anc h Poly 0 𝑝 h g = 0 g a 0 b | c d Poly | d 0 𝑝 deg d sup 0 deg h g 0 | i 0 deg h g = coeff h i * < e 0 coeff d e sup 0 deg h g 0 | i 0 deg h g = coeff h i * < c b = 0 = b | c d Poly | d 0 𝑝 deg d a e 0 coeff d e a c b = 0
112 cnex V
113 112 rabex b | c d Poly | d 0 𝑝 deg d sup 0 deg h g 0 | i 0 deg h g = coeff h i * < e 0 coeff d e sup 0 deg h g 0 | i 0 deg h g = coeff h i * < c b = 0 V
114 eleq2 f = b | c d Poly | d 0 𝑝 deg d sup 0 deg h g 0 | i 0 deg h g = coeff h i * < e 0 coeff d e sup 0 deg h g 0 | i 0 deg h g = coeff h i * < c b = 0 g f g b | c d Poly | d 0 𝑝 deg d sup 0 deg h g 0 | i 0 deg h g = coeff h i * < e 0 coeff d e sup 0 deg h g 0 | i 0 deg h g = coeff h i * < c b = 0
115 eqeq1 f = b | c d Poly | d 0 𝑝 deg d sup 0 deg h g 0 | i 0 deg h g = coeff h i * < e 0 coeff d e sup 0 deg h g 0 | i 0 deg h g = coeff h i * < c b = 0 f = b | c d Poly | d 0 𝑝 deg d a e 0 coeff d e a c b = 0 b | c d Poly | d 0 𝑝 deg d sup 0 deg h g 0 | i 0 deg h g = coeff h i * < e 0 coeff d e sup 0 deg h g 0 | i 0 deg h g = coeff h i * < c b = 0 = b | c d Poly | d 0 𝑝 deg d a e 0 coeff d e a c b = 0
116 115 rexbidv f = b | c d Poly | d 0 𝑝 deg d sup 0 deg h g 0 | i 0 deg h g = coeff h i * < e 0 coeff d e sup 0 deg h g 0 | i 0 deg h g = coeff h i * < c b = 0 a 0 f = b | c d Poly | d 0 𝑝 deg d a e 0 coeff d e a c b = 0 a 0 b | c d Poly | d 0 𝑝 deg d sup 0 deg h g 0 | i 0 deg h g = coeff h i * < e 0 coeff d e sup 0 deg h g 0 | i 0 deg h g = coeff h i * < c b = 0 = b | c d Poly | d 0 𝑝 deg d a e 0 coeff d e a c b = 0
117 114 116 anbi12d f = b | c d Poly | d 0 𝑝 deg d sup 0 deg h g 0 | i 0 deg h g = coeff h i * < e 0 coeff d e sup 0 deg h g 0 | i 0 deg h g = coeff h i * < c b = 0 g f a 0 f = b | c d Poly | d 0 𝑝 deg d a e 0 coeff d e a c b = 0 g b | c d Poly | d 0 𝑝 deg d sup 0 deg h g 0 | i 0 deg h g = coeff h i * < e 0 coeff d e sup 0 deg h g 0 | i 0 deg h g = coeff h i * < c b = 0 a 0 b | c d Poly | d 0 𝑝 deg d sup 0 deg h g 0 | i 0 deg h g = coeff h i * < e 0 coeff d e sup 0 deg h g 0 | i 0 deg h g = coeff h i * < c b = 0 = b | c d Poly | d 0 𝑝 deg d a e 0 coeff d e a c b = 0
118 113 117 spcev g b | c d Poly | d 0 𝑝 deg d sup 0 deg h g 0 | i 0 deg h g = coeff h i * < e 0 coeff d e sup 0 deg h g 0 | i 0 deg h g = coeff h i * < c b = 0 a 0 b | c d Poly | d 0 𝑝 deg d sup 0 deg h g 0 | i 0 deg h g = coeff h i * < e 0 coeff d e sup 0 deg h g 0 | i 0 deg h g = coeff h i * < c b = 0 = b | c d Poly | d 0 𝑝 deg d a e 0 coeff d e a c b = 0 f g f a 0 f = b | c d Poly | d 0 𝑝 deg d a e 0 coeff d e a c b = 0
119 85 111 118 syl2anc h Poly 0 𝑝 h g = 0 g f g f a 0 f = b | c d Poly | d 0 𝑝 deg d a e 0 coeff d e a c b = 0
120 119 3exp h Poly 0 𝑝 h g = 0 g f g f a 0 f = b | c d Poly | d 0 𝑝 deg d a e 0 coeff d e a c b = 0
121 120 rexlimiv h Poly 0 𝑝 h g = 0 g f g f a 0 f = b | c d Poly | d 0 𝑝 deg d a e 0 coeff d e a c b = 0
122 121 impcom g h Poly 0 𝑝 h g = 0 f g f a 0 f = b | c d Poly | d 0 𝑝 deg d a e 0 coeff d e a c b = 0
123 eleq2 f = b | c d Poly | d 0 𝑝 deg d a e 0 coeff d e a c b = 0 g f g b | c d Poly | d 0 𝑝 deg d a e 0 coeff d e a c b = 0
124 2 rexbidv b = g c d Poly | d 0 𝑝 deg d a e 0 coeff d e a c b = 0 c d Poly | d 0 𝑝 deg d a e 0 coeff d e a c g = 0
125 124 elrab g b | c d Poly | d 0 𝑝 deg d a e 0 coeff d e a c b = 0 g c d Poly | d 0 𝑝 deg d a e 0 coeff d e a c g = 0
126 simp1 h 0 𝑝 deg h a e 0 coeff h e a h 0 𝑝
127 126 anim2i h Poly h 0 𝑝 deg h a e 0 coeff h e a h Poly h 0 𝑝
128 6 breq1d d = h deg d a deg h a
129 10 breq1d d = h coeff d e a coeff h e a
130 129 ralbidv d = h e 0 coeff d e a e 0 coeff h e a
131 5 128 130 3anbi123d d = h d 0 𝑝 deg d a e 0 coeff d e a h 0 𝑝 deg h a e 0 coeff h e a
132 131 elrab h d Poly | d 0 𝑝 deg d a e 0 coeff d e a h Poly h 0 𝑝 deg h a e 0 coeff h e a
133 eldifsn h Poly 0 𝑝 h Poly h 0 𝑝
134 127 132 133 3imtr4i h d Poly | d 0 𝑝 deg d a e 0 coeff d e a h Poly 0 𝑝
135 134 ssriv d Poly | d 0 𝑝 deg d a e 0 coeff d e a Poly 0 𝑝
136 ssrexv d Poly | d 0 𝑝 deg d a e 0 coeff d e a Poly 0 𝑝 c d Poly | d 0 𝑝 deg d a e 0 coeff d e a c g = 0 c Poly 0 𝑝 c g = 0
137 82 cbvrexvw c Poly 0 𝑝 c g = 0 h Poly 0 𝑝 h g = 0
138 136 137 syl6ib d Poly | d 0 𝑝 deg d a e 0 coeff d e a Poly 0 𝑝 c d Poly | d 0 𝑝 deg d a e 0 coeff d e a c g = 0 h Poly 0 𝑝 h g = 0
139 135 138 ax-mp c d Poly | d 0 𝑝 deg d a e 0 coeff d e a c g = 0 h Poly 0 𝑝 h g = 0
140 139 anim2i g c d Poly | d 0 𝑝 deg d a e 0 coeff d e a c g = 0 g h Poly 0 𝑝 h g = 0
141 125 140 sylbi g b | c d Poly | d 0 𝑝 deg d a e 0 coeff d e a c b = 0 g h Poly 0 𝑝 h g = 0
142 123 141 syl6bi f = b | c d Poly | d 0 𝑝 deg d a e 0 coeff d e a c b = 0 g f g h Poly 0 𝑝 h g = 0
143 142 rexlimivw a 0 f = b | c d Poly | d 0 𝑝 deg d a e 0 coeff d e a c b = 0 g f g h Poly 0 𝑝 h g = 0
144 143 impcom g f a 0 f = b | c d Poly | d 0 𝑝 deg d a e 0 coeff d e a c b = 0 g h Poly 0 𝑝 h g = 0
145 144 exlimiv f g f a 0 f = b | c d Poly | d 0 𝑝 deg d a e 0 coeff d e a c b = 0 g h Poly 0 𝑝 h g = 0
146 122 145 impbii g h Poly 0 𝑝 h g = 0 f g f a 0 f = b | c d Poly | d 0 𝑝 deg d a e 0 coeff d e a c b = 0
147 elaa g 𝔸 g h Poly 0 𝑝 h g = 0
148 eluniab g f | a 0 f = b | c d Poly | d 0 𝑝 deg d a e 0 coeff d e a c b = 0 f g f a 0 f = b | c d Poly | d 0 𝑝 deg d a e 0 coeff d e a c b = 0
149 146 147 148 3bitr4i g 𝔸 g f | a 0 f = b | c d Poly | d 0 𝑝 deg d a e 0 coeff d e a c b = 0
150 149 eqriv 𝔸 = f | a 0 f = b | c d Poly | d 0 𝑝 deg d a e 0 coeff d e a c b = 0
151 1 rnmpt ran H = f | a 0 f = b | c d Poly | d 0 𝑝 deg d a e 0 coeff d e a c b = 0
152 151 unieqi ran H = f | a 0 f = b | c d Poly | d 0 𝑝 deg d a e 0 coeff d e a c b = 0
153 150 152 eqtr4i 𝔸 = ran H