Metamath Proof Explorer

Theorem mpaaeu

Description: An algebraic number has exactly one monic polynomial of the least degree. (Contributed by Stefan O'Rear, 25-Nov-2014)

Ref Expression
Assertion mpaaeu 
|- ( A e. AA -> E! p e. ( Poly ` QQ ) ( ( deg ` p ) = ( degAA ` A ) /\ ( p ` A ) = 0 /\ ( ( coeff ` p ) ` ( degAA ` A ) ) = 1 ) )

Proof

Step Hyp Ref Expression
1 qsscn 
 |-  QQ C_ CC
2 eldifi 
 |-  ( a e. ( ( Poly ` QQ ) \ { 0p } ) -> a e. ( Poly ` QQ ) )
3 2 ad2antlr 
 |-  ( ( ( A e. AA /\ a e. ( ( Poly ` QQ ) \ { 0p } ) ) /\ ( ( deg ` a ) = ( degAA ` A ) /\ ( a ` A ) = 0 ) ) -> a e. ( Poly ` QQ ) )
4 zssq 
 |-  ZZ C_ QQ
5 0z 
 |-  0 e. ZZ
6 4 5 sselii 
 |-  0 e. QQ
7 eqid 
 |-  ( coeff ` a ) = ( coeff ` a )
8 7 coef2 
 |-  ( ( a e. ( Poly ` QQ ) /\ 0 e. QQ ) -> ( coeff ` a ) : NN0 --> QQ )
9 3 6 8 sylancl 
 |-  ( ( ( A e. AA /\ a e. ( ( Poly ` QQ ) \ { 0p } ) ) /\ ( ( deg ` a ) = ( degAA ` A ) /\ ( a ` A ) = 0 ) ) -> ( coeff ` a ) : NN0 --> QQ )
10 dgrcl 
 |-  ( a e. ( Poly ` QQ ) -> ( deg ` a ) e. NN0 )
11 3 10 syl 
 |-  ( ( ( A e. AA /\ a e. ( ( Poly ` QQ ) \ { 0p } ) ) /\ ( ( deg ` a ) = ( degAA ` A ) /\ ( a ` A ) = 0 ) ) -> ( deg ` a ) e. NN0 )
12 9 11 ffvelrnd 
 |-  ( ( ( A e. AA /\ a e. ( ( Poly ` QQ ) \ { 0p } ) ) /\ ( ( deg ` a ) = ( degAA ` A ) /\ ( a ` A ) = 0 ) ) -> ( ( coeff ` a ) ` ( deg ` a ) ) e. QQ )
13 eldifsni 
 |-  ( a e. ( ( Poly ` QQ ) \ { 0p } ) -> a =/= 0p )
14 13 ad2antlr 
 |-  ( ( ( A e. AA /\ a e. ( ( Poly ` QQ ) \ { 0p } ) ) /\ ( ( deg ` a ) = ( degAA ` A ) /\ ( a ` A ) = 0 ) ) -> a =/= 0p )
15 eqid 
 |-  ( deg ` a ) = ( deg ` a )
16 15 7 dgreq0 
 |-  ( a e. ( Poly ` QQ ) -> ( a = 0p <-> ( ( coeff ` a ) ` ( deg ` a ) ) = 0 ) )
17 16 necon3bid 
 |-  ( a e. ( Poly ` QQ ) -> ( a =/= 0p <-> ( ( coeff ` a ) ` ( deg ` a ) ) =/= 0 ) )
18 3 17 syl 
 |-  ( ( ( A e. AA /\ a e. ( ( Poly ` QQ ) \ { 0p } ) ) /\ ( ( deg ` a ) = ( degAA ` A ) /\ ( a ` A ) = 0 ) ) -> ( a =/= 0p <-> ( ( coeff ` a ) ` ( deg ` a ) ) =/= 0 ) )
19 14 18 mpbid 
 |-  ( ( ( A e. AA /\ a e. ( ( Poly ` QQ ) \ { 0p } ) ) /\ ( ( deg ` a ) = ( degAA ` A ) /\ ( a ` A ) = 0 ) ) -> ( ( coeff ` a ) ` ( deg ` a ) ) =/= 0 )
20 qreccl 
 |-  ( ( ( ( coeff ` a ) ` ( deg ` a ) ) e. QQ /\ ( ( coeff ` a ) ` ( deg ` a ) ) =/= 0 ) -> ( 1 / ( ( coeff ` a ) ` ( deg ` a ) ) ) e. QQ )
21 12 19 20 syl2anc 
 |-  ( ( ( A e. AA /\ a e. ( ( Poly ` QQ ) \ { 0p } ) ) /\ ( ( deg ` a ) = ( degAA ` A ) /\ ( a ` A ) = 0 ) ) -> ( 1 / ( ( coeff ` a ) ` ( deg ` a ) ) ) e. QQ )
22 plyconst 
 |-  ( ( QQ C_ CC /\ ( 1 / ( ( coeff ` a ) ` ( deg ` a ) ) ) e. QQ ) -> ( CC X. { ( 1 / ( ( coeff ` a ) ` ( deg ` a ) ) ) } ) e. ( Poly ` QQ ) )
23 1 21 22 sylancr 
 |-  ( ( ( A e. AA /\ a e. ( ( Poly ` QQ ) \ { 0p } ) ) /\ ( ( deg ` a ) = ( degAA ` A ) /\ ( a ` A ) = 0 ) ) -> ( CC X. { ( 1 / ( ( coeff ` a ) ` ( deg ` a ) ) ) } ) e. ( Poly ` QQ ) )
24 simpl 
 |-  ( ( ( CC X. { ( 1 / ( ( coeff ` a ) ` ( deg ` a ) ) ) } ) e. ( Poly ` QQ ) /\ a e. ( Poly ` QQ ) ) -> ( CC X. { ( 1 / ( ( coeff ` a ) ` ( deg ` a ) ) ) } ) e. ( Poly ` QQ ) )
25 simpr 
 |-  ( ( ( CC X. { ( 1 / ( ( coeff ` a ) ` ( deg ` a ) ) ) } ) e. ( Poly ` QQ ) /\ a e. ( Poly ` QQ ) ) -> a e. ( Poly ` QQ ) )
26 qaddcl 
 |-  ( ( b e. QQ /\ c e. QQ ) -> ( b + c ) e. QQ )
27 26 adantl 
 |-  ( ( ( ( CC X. { ( 1 / ( ( coeff ` a ) ` ( deg ` a ) ) ) } ) e. ( Poly ` QQ ) /\ a e. ( Poly ` QQ ) ) /\ ( b e. QQ /\ c e. QQ ) ) -> ( b + c ) e. QQ )
28 qmulcl 
 |-  ( ( b e. QQ /\ c e. QQ ) -> ( b x. c ) e. QQ )
29 28 adantl 
 |-  ( ( ( ( CC X. { ( 1 / ( ( coeff ` a ) ` ( deg ` a ) ) ) } ) e. ( Poly ` QQ ) /\ a e. ( Poly ` QQ ) ) /\ ( b e. QQ /\ c e. QQ ) ) -> ( b x. c ) e. QQ )
30 24 25 27 29 plymul 
 |-  ( ( ( CC X. { ( 1 / ( ( coeff ` a ) ` ( deg ` a ) ) ) } ) e. ( Poly ` QQ ) /\ a e. ( Poly ` QQ ) ) -> ( ( CC X. { ( 1 / ( ( coeff ` a ) ` ( deg ` a ) ) ) } ) oF x. a ) e. ( Poly ` QQ ) )
31 23 3 30 syl2anc 
 |-  ( ( ( A e. AA /\ a e. ( ( Poly ` QQ ) \ { 0p } ) ) /\ ( ( deg ` a ) = ( degAA ` A ) /\ ( a ` A ) = 0 ) ) -> ( ( CC X. { ( 1 / ( ( coeff ` a ) ` ( deg ` a ) ) ) } ) oF x. a ) e. ( Poly ` QQ ) )
32 7 coef3 
 |-  ( a e. ( Poly ` QQ ) -> ( coeff ` a ) : NN0 --> CC )
33 3 32 syl 
 |-  ( ( ( A e. AA /\ a e. ( ( Poly ` QQ ) \ { 0p } ) ) /\ ( ( deg ` a ) = ( degAA ` A ) /\ ( a ` A ) = 0 ) ) -> ( coeff ` a ) : NN0 --> CC )
34 33 11 ffvelrnd 
 |-  ( ( ( A e. AA /\ a e. ( ( Poly ` QQ ) \ { 0p } ) ) /\ ( ( deg ` a ) = ( degAA ` A ) /\ ( a ` A ) = 0 ) ) -> ( ( coeff ` a ) ` ( deg ` a ) ) e. CC )
35 34 19 reccld 
 |-  ( ( ( A e. AA /\ a e. ( ( Poly ` QQ ) \ { 0p } ) ) /\ ( ( deg ` a ) = ( degAA ` A ) /\ ( a ` A ) = 0 ) ) -> ( 1 / ( ( coeff ` a ) ` ( deg ` a ) ) ) e. CC )
36 34 19 recne0d 
 |-  ( ( ( A e. AA /\ a e. ( ( Poly ` QQ ) \ { 0p } ) ) /\ ( ( deg ` a ) = ( degAA ` A ) /\ ( a ` A ) = 0 ) ) -> ( 1 / ( ( coeff ` a ) ` ( deg ` a ) ) ) =/= 0 )
37 dgrmulc 
 |-  ( ( ( 1 / ( ( coeff ` a ) ` ( deg ` a ) ) ) e. CC /\ ( 1 / ( ( coeff ` a ) ` ( deg ` a ) ) ) =/= 0 /\ a e. ( Poly ` QQ ) ) -> ( deg ` ( ( CC X. { ( 1 / ( ( coeff ` a ) ` ( deg ` a ) ) ) } ) oF x. a ) ) = ( deg ` a ) )
38 35 36 3 37 syl3anc 
 |-  ( ( ( A e. AA /\ a e. ( ( Poly ` QQ ) \ { 0p } ) ) /\ ( ( deg ` a ) = ( degAA ` A ) /\ ( a ` A ) = 0 ) ) -> ( deg ` ( ( CC X. { ( 1 / ( ( coeff ` a ) ` ( deg ` a ) ) ) } ) oF x. a ) ) = ( deg ` a ) )
39 simprl 
 |-  ( ( ( A e. AA /\ a e. ( ( Poly ` QQ ) \ { 0p } ) ) /\ ( ( deg ` a ) = ( degAA ` A ) /\ ( a ` A ) = 0 ) ) -> ( deg ` a ) = ( degAA ` A ) )
40 38 39 eqtrd 
 |-  ( ( ( A e. AA /\ a e. ( ( Poly ` QQ ) \ { 0p } ) ) /\ ( ( deg ` a ) = ( degAA ` A ) /\ ( a ` A ) = 0 ) ) -> ( deg ` ( ( CC X. { ( 1 / ( ( coeff ` a ) ` ( deg ` a ) ) ) } ) oF x. a ) ) = ( degAA ` A ) )
41 aacn 
 |-  ( A e. AA -> A e. CC )
42 41 ad2antrr 
 |-  ( ( ( A e. AA /\ a e. ( ( Poly ` QQ ) \ { 0p } ) ) /\ ( ( deg ` a ) = ( degAA ` A ) /\ ( a ` A ) = 0 ) ) -> A e. CC )
43 ovex 
 |-  ( 1 / ( ( coeff ` a ) ` ( deg ` a ) ) ) e. _V
44 fnconstg 
 |-  ( ( 1 / ( ( coeff ` a ) ` ( deg ` a ) ) ) e. _V -> ( CC X. { ( 1 / ( ( coeff ` a ) ` ( deg ` a ) ) ) } ) Fn CC )
45 43 44 mp1i 
 |-  ( ( ( A e. AA /\ a e. ( ( Poly ` QQ ) \ { 0p } ) ) /\ ( ( deg ` a ) = ( degAA ` A ) /\ ( a ` A ) = 0 ) ) -> ( CC X. { ( 1 / ( ( coeff ` a ) ` ( deg ` a ) ) ) } ) Fn CC )
46 plyf 
 |-  ( a e. ( Poly ` QQ ) -> a : CC --> CC )
47 ffn 
 |-  ( a : CC --> CC -> a Fn CC )
48 3 46 47 3syl 
 |-  ( ( ( A e. AA /\ a e. ( ( Poly ` QQ ) \ { 0p } ) ) /\ ( ( deg ` a ) = ( degAA ` A ) /\ ( a ` A ) = 0 ) ) -> a Fn CC )
49 cnex 
 |-  CC e. _V
50 49 a1i 
 |-  ( ( ( A e. AA /\ a e. ( ( Poly ` QQ ) \ { 0p } ) ) /\ ( ( deg ` a ) = ( degAA ` A ) /\ ( a ` A ) = 0 ) ) -> CC e. _V )
51 inidm 
 |-  ( CC i^i CC ) = CC
52 43 fvconst2 
 |-  ( A e. CC -> ( ( CC X. { ( 1 / ( ( coeff ` a ) ` ( deg ` a ) ) ) } ) ` A ) = ( 1 / ( ( coeff ` a ) ` ( deg ` a ) ) ) )
53 52 adantl 
 |-  ( ( ( ( A e. AA /\ a e. ( ( Poly ` QQ ) \ { 0p } ) ) /\ ( ( deg ` a ) = ( degAA ` A ) /\ ( a ` A ) = 0 ) ) /\ A e. CC ) -> ( ( CC X. { ( 1 / ( ( coeff ` a ) ` ( deg ` a ) ) ) } ) ` A ) = ( 1 / ( ( coeff ` a ) ` ( deg ` a ) ) ) )
54 simplrr 
 |-  ( ( ( ( A e. AA /\ a e. ( ( Poly ` QQ ) \ { 0p } ) ) /\ ( ( deg ` a ) = ( degAA ` A ) /\ ( a ` A ) = 0 ) ) /\ A e. CC ) -> ( a ` A ) = 0 )
55 45 48 50 50 51 53 54 ofval 
 |-  ( ( ( ( A e. AA /\ a e. ( ( Poly ` QQ ) \ { 0p } ) ) /\ ( ( deg ` a ) = ( degAA ` A ) /\ ( a ` A ) = 0 ) ) /\ A e. CC ) -> ( ( ( CC X. { ( 1 / ( ( coeff ` a ) ` ( deg ` a ) ) ) } ) oF x. a ) ` A ) = ( ( 1 / ( ( coeff ` a ) ` ( deg ` a ) ) ) x. 0 ) )
56 42 55 mpdan 
 |-  ( ( ( A e. AA /\ a e. ( ( Poly ` QQ ) \ { 0p } ) ) /\ ( ( deg ` a ) = ( degAA ` A ) /\ ( a ` A ) = 0 ) ) -> ( ( ( CC X. { ( 1 / ( ( coeff ` a ) ` ( deg ` a ) ) ) } ) oF x. a ) ` A ) = ( ( 1 / ( ( coeff ` a ) ` ( deg ` a ) ) ) x. 0 ) )
57 35 mul01d 
 |-  ( ( ( A e. AA /\ a e. ( ( Poly ` QQ ) \ { 0p } ) ) /\ ( ( deg ` a ) = ( degAA ` A ) /\ ( a ` A ) = 0 ) ) -> ( ( 1 / ( ( coeff ` a ) ` ( deg ` a ) ) ) x. 0 ) = 0 )
58 56 57 eqtrd 
 |-  ( ( ( A e. AA /\ a e. ( ( Poly ` QQ ) \ { 0p } ) ) /\ ( ( deg ` a ) = ( degAA ` A ) /\ ( a ` A ) = 0 ) ) -> ( ( ( CC X. { ( 1 / ( ( coeff ` a ) ` ( deg ` a ) ) ) } ) oF x. a ) ` A ) = 0 )
59 coemulc 
 |-  ( ( ( 1 / ( ( coeff ` a ) ` ( deg ` a ) ) ) e. CC /\ a e. ( Poly ` QQ ) ) -> ( coeff ` ( ( CC X. { ( 1 / ( ( coeff ` a ) ` ( deg ` a ) ) ) } ) oF x. a ) ) = ( ( NN0 X. { ( 1 / ( ( coeff ` a ) ` ( deg ` a ) ) ) } ) oF x. ( coeff ` a ) ) )
60 35 3 59 syl2anc 
 |-  ( ( ( A e. AA /\ a e. ( ( Poly ` QQ ) \ { 0p } ) ) /\ ( ( deg ` a ) = ( degAA ` A ) /\ ( a ` A ) = 0 ) ) -> ( coeff ` ( ( CC X. { ( 1 / ( ( coeff ` a ) ` ( deg ` a ) ) ) } ) oF x. a ) ) = ( ( NN0 X. { ( 1 / ( ( coeff ` a ) ` ( deg ` a ) ) ) } ) oF x. ( coeff ` a ) ) )
61 60 fveq1d 
 |-  ( ( ( A e. AA /\ a e. ( ( Poly ` QQ ) \ { 0p } ) ) /\ ( ( deg ` a ) = ( degAA ` A ) /\ ( a ` A ) = 0 ) ) -> ( ( coeff ` ( ( CC X. { ( 1 / ( ( coeff ` a ) ` ( deg ` a ) ) ) } ) oF x. a ) ) ` ( degAA ` A ) ) = ( ( ( NN0 X. { ( 1 / ( ( coeff ` a ) ` ( deg ` a ) ) ) } ) oF x. ( coeff ` a ) ) ` ( degAA ` A ) ) )
62 dgraacl 
 |-  ( A e. AA -> ( degAA ` A ) e. NN )
63 62 ad2antrr 
 |-  ( ( ( A e. AA /\ a e. ( ( Poly ` QQ ) \ { 0p } ) ) /\ ( ( deg ` a ) = ( degAA ` A ) /\ ( a ` A ) = 0 ) ) -> ( degAA ` A ) e. NN )
64 63 nnnn0d 
 |-  ( ( ( A e. AA /\ a e. ( ( Poly ` QQ ) \ { 0p } ) ) /\ ( ( deg ` a ) = ( degAA ` A ) /\ ( a ` A ) = 0 ) ) -> ( degAA ` A ) e. NN0 )
65 fnconstg 
 |-  ( ( 1 / ( ( coeff ` a ) ` ( deg ` a ) ) ) e. _V -> ( NN0 X. { ( 1 / ( ( coeff ` a ) ` ( deg ` a ) ) ) } ) Fn NN0 )
66 43 65 mp1i 
 |-  ( ( ( A e. AA /\ a e. ( ( Poly ` QQ ) \ { 0p } ) ) /\ ( ( deg ` a ) = ( degAA ` A ) /\ ( a ` A ) = 0 ) ) -> ( NN0 X. { ( 1 / ( ( coeff ` a ) ` ( deg ` a ) ) ) } ) Fn NN0 )
67 33 ffnd 
 |-  ( ( ( A e. AA /\ a e. ( ( Poly ` QQ ) \ { 0p } ) ) /\ ( ( deg ` a ) = ( degAA ` A ) /\ ( a ` A ) = 0 ) ) -> ( coeff ` a ) Fn NN0 )
68 nn0ex 
 |-  NN0 e. _V
69 68 a1i 
 |-  ( ( ( A e. AA /\ a e. ( ( Poly ` QQ ) \ { 0p } ) ) /\ ( ( deg ` a ) = ( degAA ` A ) /\ ( a ` A ) = 0 ) ) -> NN0 e. _V )
70 inidm 
 |-  ( NN0 i^i NN0 ) = NN0
71 43 fvconst2 
 |-  ( ( degAA ` A ) e. NN0 -> ( ( NN0 X. { ( 1 / ( ( coeff ` a ) ` ( deg ` a ) ) ) } ) ` ( degAA ` A ) ) = ( 1 / ( ( coeff ` a ) ` ( deg ` a ) ) ) )
72 71 adantl 
 |-  ( ( ( ( A e. AA /\ a e. ( ( Poly ` QQ ) \ { 0p } ) ) /\ ( ( deg ` a ) = ( degAA ` A ) /\ ( a ` A ) = 0 ) ) /\ ( degAA ` A ) e. NN0 ) -> ( ( NN0 X. { ( 1 / ( ( coeff ` a ) ` ( deg ` a ) ) ) } ) ` ( degAA ` A ) ) = ( 1 / ( ( coeff ` a ) ` ( deg ` a ) ) ) )
73 simplrl 
 |-  ( ( ( ( A e. AA /\ a e. ( ( Poly ` QQ ) \ { 0p } ) ) /\ ( ( deg ` a ) = ( degAA ` A ) /\ ( a ` A ) = 0 ) ) /\ ( degAA ` A ) e. NN0 ) -> ( deg ` a ) = ( degAA ` A ) )
74 73 eqcomd 
 |-  ( ( ( ( A e. AA /\ a e. ( ( Poly ` QQ ) \ { 0p } ) ) /\ ( ( deg ` a ) = ( degAA ` A ) /\ ( a ` A ) = 0 ) ) /\ ( degAA ` A ) e. NN0 ) -> ( degAA ` A ) = ( deg ` a ) )
75 74 fveq2d 
 |-  ( ( ( ( A e. AA /\ a e. ( ( Poly ` QQ ) \ { 0p } ) ) /\ ( ( deg ` a ) = ( degAA ` A ) /\ ( a ` A ) = 0 ) ) /\ ( degAA ` A ) e. NN0 ) -> ( ( coeff ` a ) ` ( degAA ` A ) ) = ( ( coeff ` a ) ` ( deg ` a ) ) )
76 66 67 69 69 70 72 75 ofval 
 |-  ( ( ( ( A e. AA /\ a e. ( ( Poly ` QQ ) \ { 0p } ) ) /\ ( ( deg ` a ) = ( degAA ` A ) /\ ( a ` A ) = 0 ) ) /\ ( degAA ` A ) e. NN0 ) -> ( ( ( NN0 X. { ( 1 / ( ( coeff ` a ) ` ( deg ` a ) ) ) } ) oF x. ( coeff ` a ) ) ` ( degAA ` A ) ) = ( ( 1 / ( ( coeff ` a ) ` ( deg ` a ) ) ) x. ( ( coeff ` a ) ` ( deg ` a ) ) ) )
77 64 76 mpdan 
 |-  ( ( ( A e. AA /\ a e. ( ( Poly ` QQ ) \ { 0p } ) ) /\ ( ( deg ` a ) = ( degAA ` A ) /\ ( a ` A ) = 0 ) ) -> ( ( ( NN0 X. { ( 1 / ( ( coeff ` a ) ` ( deg ` a ) ) ) } ) oF x. ( coeff ` a ) ) ` ( degAA ` A ) ) = ( ( 1 / ( ( coeff ` a ) ` ( deg ` a ) ) ) x. ( ( coeff ` a ) ` ( deg ` a ) ) ) )
78 34 19 recid2d 
 |-  ( ( ( A e. AA /\ a e. ( ( Poly ` QQ ) \ { 0p } ) ) /\ ( ( deg ` a ) = ( degAA ` A ) /\ ( a ` A ) = 0 ) ) -> ( ( 1 / ( ( coeff ` a ) ` ( deg ` a ) ) ) x. ( ( coeff ` a ) ` ( deg ` a ) ) ) = 1 )
79 61 77 78 3eqtrd 
 |-  ( ( ( A e. AA /\ a e. ( ( Poly ` QQ ) \ { 0p } ) ) /\ ( ( deg ` a ) = ( degAA ` A ) /\ ( a ` A ) = 0 ) ) -> ( ( coeff ` ( ( CC X. { ( 1 / ( ( coeff ` a ) ` ( deg ` a ) ) ) } ) oF x. a ) ) ` ( degAA ` A ) ) = 1 )
80 fveqeq2 
 |-  ( p = ( ( CC X. { ( 1 / ( ( coeff ` a ) ` ( deg ` a ) ) ) } ) oF x. a ) -> ( ( deg ` p ) = ( degAA ` A ) <-> ( deg ` ( ( CC X. { ( 1 / ( ( coeff ` a ) ` ( deg ` a ) ) ) } ) oF x. a ) ) = ( degAA ` A ) ) )
81 fveq1 
 |-  ( p = ( ( CC X. { ( 1 / ( ( coeff ` a ) ` ( deg ` a ) ) ) } ) oF x. a ) -> ( p ` A ) = ( ( ( CC X. { ( 1 / ( ( coeff ` a ) ` ( deg ` a ) ) ) } ) oF x. a ) ` A ) )
82 81 eqeq1d 
 |-  ( p = ( ( CC X. { ( 1 / ( ( coeff ` a ) ` ( deg ` a ) ) ) } ) oF x. a ) -> ( ( p ` A ) = 0 <-> ( ( ( CC X. { ( 1 / ( ( coeff ` a ) ` ( deg ` a ) ) ) } ) oF x. a ) ` A ) = 0 ) )
83 fveq2 
 |-  ( p = ( ( CC X. { ( 1 / ( ( coeff ` a ) ` ( deg ` a ) ) ) } ) oF x. a ) -> ( coeff ` p ) = ( coeff ` ( ( CC X. { ( 1 / ( ( coeff ` a ) ` ( deg ` a ) ) ) } ) oF x. a ) ) )
84 83 fveq1d 
 |-  ( p = ( ( CC X. { ( 1 / ( ( coeff ` a ) ` ( deg ` a ) ) ) } ) oF x. a ) -> ( ( coeff ` p ) ` ( degAA ` A ) ) = ( ( coeff ` ( ( CC X. { ( 1 / ( ( coeff ` a ) ` ( deg ` a ) ) ) } ) oF x. a ) ) ` ( degAA ` A ) ) )
85 84 eqeq1d 
 |-  ( p = ( ( CC X. { ( 1 / ( ( coeff ` a ) ` ( deg ` a ) ) ) } ) oF x. a ) -> ( ( ( coeff ` p ) ` ( degAA ` A ) ) = 1 <-> ( ( coeff ` ( ( CC X. { ( 1 / ( ( coeff ` a ) ` ( deg ` a ) ) ) } ) oF x. a ) ) ` ( degAA ` A ) ) = 1 ) )
86 80 82 85 3anbi123d 
 |-  ( p = ( ( CC X. { ( 1 / ( ( coeff ` a ) ` ( deg ` a ) ) ) } ) oF x. a ) -> ( ( ( deg ` p ) = ( degAA ` A ) /\ ( p ` A ) = 0 /\ ( ( coeff ` p ) ` ( degAA ` A ) ) = 1 ) <-> ( ( deg ` ( ( CC X. { ( 1 / ( ( coeff ` a ) ` ( deg ` a ) ) ) } ) oF x. a ) ) = ( degAA ` A ) /\ ( ( ( CC X. { ( 1 / ( ( coeff ` a ) ` ( deg ` a ) ) ) } ) oF x. a ) ` A ) = 0 /\ ( ( coeff ` ( ( CC X. { ( 1 / ( ( coeff ` a ) ` ( deg ` a ) ) ) } ) oF x. a ) ) ` ( degAA ` A ) ) = 1 ) ) )
87 86 rspcev 
 |-  ( ( ( ( CC X. { ( 1 / ( ( coeff ` a ) ` ( deg ` a ) ) ) } ) oF x. a ) e. ( Poly ` QQ ) /\ ( ( deg ` ( ( CC X. { ( 1 / ( ( coeff ` a ) ` ( deg ` a ) ) ) } ) oF x. a ) ) = ( degAA ` A ) /\ ( ( ( CC X. { ( 1 / ( ( coeff ` a ) ` ( deg ` a ) ) ) } ) oF x. a ) ` A ) = 0 /\ ( ( coeff ` ( ( CC X. { ( 1 / ( ( coeff ` a ) ` ( deg ` a ) ) ) } ) oF x. a ) ) ` ( degAA ` A ) ) = 1 ) ) -> E. p e. ( Poly ` QQ ) ( ( deg ` p ) = ( degAA ` A ) /\ ( p ` A ) = 0 /\ ( ( coeff ` p ) ` ( degAA ` A ) ) = 1 ) )
88 31 40 58 79 87 syl13anc 
 |-  ( ( ( A e. AA /\ a e. ( ( Poly ` QQ ) \ { 0p } ) ) /\ ( ( deg ` a ) = ( degAA ` A ) /\ ( a ` A ) = 0 ) ) -> E. p e. ( Poly ` QQ ) ( ( deg ` p ) = ( degAA ` A ) /\ ( p ` A ) = 0 /\ ( ( coeff ` p ) ` ( degAA ` A ) ) = 1 ) )
89 dgraalem 
 |-  ( A e. AA -> ( ( degAA ` A ) e. NN /\ E. a e. ( ( Poly ` QQ ) \ { 0p } ) ( ( deg ` a ) = ( degAA ` A ) /\ ( a ` A ) = 0 ) ) )
90 89 simprd 
 |-  ( A e. AA -> E. a e. ( ( Poly ` QQ ) \ { 0p } ) ( ( deg ` a ) = ( degAA ` A ) /\ ( a ` A ) = 0 ) )
91 88 90 r19.29a 
 |-  ( A e. AA -> E. p e. ( Poly ` QQ ) ( ( deg ` p ) = ( degAA ` A ) /\ ( p ` A ) = 0 /\ ( ( coeff ` p ) ` ( degAA ` A ) ) = 1 ) )
92 simp2 
 |-  ( ( ( deg ` p ) = ( degAA ` A ) /\ ( p ` A ) = 0 /\ ( ( coeff ` p ) ` ( degAA ` A ) ) = 1 ) -> ( p ` A ) = 0 )
93 simp2 
 |-  ( ( ( deg ` a ) = ( degAA ` A ) /\ ( a ` A ) = 0 /\ ( ( coeff ` a ) ` ( degAA ` A ) ) = 1 ) -> ( a ` A ) = 0 )
94 92 93 anim12i 
 |-  ( ( ( ( deg ` p ) = ( degAA ` A ) /\ ( p ` A ) = 0 /\ ( ( coeff ` p ) ` ( degAA ` A ) ) = 1 ) /\ ( ( deg ` a ) = ( degAA ` A ) /\ ( a ` A ) = 0 /\ ( ( coeff ` a ) ` ( degAA ` A ) ) = 1 ) ) -> ( ( p ` A ) = 0 /\ ( a ` A ) = 0 ) )
95 plyf 
 |-  ( p e. ( Poly ` QQ ) -> p : CC --> CC )
96 95 ffnd 
 |-  ( p e. ( Poly ` QQ ) -> p Fn CC )
97 96 ad2antrr 
 |-  ( ( ( p e. ( Poly ` QQ ) /\ a e. ( Poly ` QQ ) ) /\ ( ( p ` A ) = 0 /\ ( a ` A ) = 0 ) ) -> p Fn CC )
98 46 ffnd 
 |-  ( a e. ( Poly ` QQ ) -> a Fn CC )
99 98 ad2antlr 
 |-  ( ( ( p e. ( Poly ` QQ ) /\ a e. ( Poly ` QQ ) ) /\ ( ( p ` A ) = 0 /\ ( a ` A ) = 0 ) ) -> a Fn CC )
100 49 a1i 
 |-  ( ( ( p e. ( Poly ` QQ ) /\ a e. ( Poly ` QQ ) ) /\ ( ( p ` A ) = 0 /\ ( a ` A ) = 0 ) ) -> CC e. _V )
101 simplrl 
 |-  ( ( ( ( p e. ( Poly ` QQ ) /\ a e. ( Poly ` QQ ) ) /\ ( ( p ` A ) = 0 /\ ( a ` A ) = 0 ) ) /\ A e. CC ) -> ( p ` A ) = 0 )
102 simplrr 
 |-  ( ( ( ( p e. ( Poly ` QQ ) /\ a e. ( Poly ` QQ ) ) /\ ( ( p ` A ) = 0 /\ ( a ` A ) = 0 ) ) /\ A e. CC ) -> ( a ` A ) = 0 )
103 97 99 100 100 51 101 102 ofval 
 |-  ( ( ( ( p e. ( Poly ` QQ ) /\ a e. ( Poly ` QQ ) ) /\ ( ( p ` A ) = 0 /\ ( a ` A ) = 0 ) ) /\ A e. CC ) -> ( ( p oF - a ) ` A ) = ( 0 - 0 ) )
104 41 103 sylan2 
 |-  ( ( ( ( p e. ( Poly ` QQ ) /\ a e. ( Poly ` QQ ) ) /\ ( ( p ` A ) = 0 /\ ( a ` A ) = 0 ) ) /\ A e. AA ) -> ( ( p oF - a ) ` A ) = ( 0 - 0 ) )
105 0m0e0 
 |-  ( 0 - 0 ) = 0
106 104 105 eqtrdi 
 |-  ( ( ( ( p e. ( Poly ` QQ ) /\ a e. ( Poly ` QQ ) ) /\ ( ( p ` A ) = 0 /\ ( a ` A ) = 0 ) ) /\ A e. AA ) -> ( ( p oF - a ) ` A ) = 0 )
107 106 ex 
 |-  ( ( ( p e. ( Poly ` QQ ) /\ a e. ( Poly ` QQ ) ) /\ ( ( p ` A ) = 0 /\ ( a ` A ) = 0 ) ) -> ( A e. AA -> ( ( p oF - a ) ` A ) = 0 ) )
108 94 107 sylan2 
 |-  ( ( ( p e. ( Poly ` QQ ) /\ a e. ( Poly ` QQ ) ) /\ ( ( ( deg ` p ) = ( degAA ` A ) /\ ( p ` A ) = 0 /\ ( ( coeff ` p ) ` ( degAA ` A ) ) = 1 ) /\ ( ( deg ` a ) = ( degAA ` A ) /\ ( a ` A ) = 0 /\ ( ( coeff ` a ) ` ( degAA ` A ) ) = 1 ) ) ) -> ( A e. AA -> ( ( p oF - a ) ` A ) = 0 ) )
109 108 com12 
 |-  ( A e. AA -> ( ( ( p e. ( Poly ` QQ ) /\ a e. ( Poly ` QQ ) ) /\ ( ( ( deg ` p ) = ( degAA ` A ) /\ ( p ` A ) = 0 /\ ( ( coeff ` p ) ` ( degAA ` A ) ) = 1 ) /\ ( ( deg ` a ) = ( degAA ` A ) /\ ( a ` A ) = 0 /\ ( ( coeff ` a ) ` ( degAA ` A ) ) = 1 ) ) ) -> ( ( p oF - a ) ` A ) = 0 ) )
110 109 impl 
 |-  ( ( ( A e. AA /\ ( p e. ( Poly ` QQ ) /\ a e. ( Poly ` QQ ) ) ) /\ ( ( ( deg ` p ) = ( degAA ` A ) /\ ( p ` A ) = 0 /\ ( ( coeff ` p ) ` ( degAA ` A ) ) = 1 ) /\ ( ( deg ` a ) = ( degAA ` A ) /\ ( a ` A ) = 0 /\ ( ( coeff ` a ) ` ( degAA ` A ) ) = 1 ) ) ) -> ( ( p oF - a ) ` A ) = 0 )
111 simpll 
 |-  ( ( ( A e. AA /\ ( p e. ( Poly ` QQ ) /\ a e. ( Poly ` QQ ) ) ) /\ ( ( ( deg ` p ) = ( degAA ` A ) /\ ( p ` A ) = 0 /\ ( ( coeff ` p ) ` ( degAA ` A ) ) = 1 ) /\ ( ( deg ` a ) = ( degAA ` A ) /\ ( a ` A ) = 0 /\ ( ( coeff ` a ) ` ( degAA ` A ) ) = 1 ) ) ) -> A e. AA )
112 simpl 
 |-  ( ( p e. ( Poly ` QQ ) /\ a e. ( Poly ` QQ ) ) -> p e. ( Poly ` QQ ) )
113 simpr 
 |-  ( ( p e. ( Poly ` QQ ) /\ a e. ( Poly ` QQ ) ) -> a e. ( Poly ` QQ ) )
114 26 adantl 
 |-  ( ( ( p e. ( Poly ` QQ ) /\ a e. ( Poly ` QQ ) ) /\ ( b e. QQ /\ c e. QQ ) ) -> ( b + c ) e. QQ )
115 28 adantl 
 |-  ( ( ( p e. ( Poly ` QQ ) /\ a e. ( Poly ` QQ ) ) /\ ( b e. QQ /\ c e. QQ ) ) -> ( b x. c ) e. QQ )
116 1z 
 |-  1 e. ZZ
117 zq 
 |-  ( 1 e. ZZ -> 1 e. QQ )
118 qnegcl 
 |-  ( 1 e. QQ -> -u 1 e. QQ )
119 116 117 118 mp2b 
 |-  -u 1 e. QQ
120 119 a1i 
 |-  ( ( p e. ( Poly ` QQ ) /\ a e. ( Poly ` QQ ) ) -> -u 1 e. QQ )
121 112 113 114 115 120 plysub 
 |-  ( ( p e. ( Poly ` QQ ) /\ a e. ( Poly ` QQ ) ) -> ( p oF - a ) e. ( Poly ` QQ ) )
122 121 ad2antlr 
 |-  ( ( ( A e. AA /\ ( p e. ( Poly ` QQ ) /\ a e. ( Poly ` QQ ) ) ) /\ ( ( ( deg ` p ) = ( degAA ` A ) /\ ( p ` A ) = 0 /\ ( ( coeff ` p ) ` ( degAA ` A ) ) = 1 ) /\ ( ( deg ` a ) = ( degAA ` A ) /\ ( a ` A ) = 0 /\ ( ( coeff ` a ) ` ( degAA ` A ) ) = 1 ) ) ) -> ( p oF - a ) e. ( Poly ` QQ ) )
123 simplrl 
 |-  ( ( ( A e. AA /\ ( p e. ( Poly ` QQ ) /\ a e. ( Poly ` QQ ) ) ) /\ ( ( ( deg ` p ) = ( degAA ` A ) /\ ( p ` A ) = 0 /\ ( ( coeff ` p ) ` ( degAA ` A ) ) = 1 ) /\ ( ( deg ` a ) = ( degAA ` A ) /\ ( a ` A ) = 0 /\ ( ( coeff ` a ) ` ( degAA ` A ) ) = 1 ) ) ) -> p e. ( Poly ` QQ ) )
124 simplrr 
 |-  ( ( ( A e. AA /\ ( p e. ( Poly ` QQ ) /\ a e. ( Poly ` QQ ) ) ) /\ ( ( ( deg ` p ) = ( degAA ` A ) /\ ( p ` A ) = 0 /\ ( ( coeff ` p ) ` ( degAA ` A ) ) = 1 ) /\ ( ( deg ` a ) = ( degAA ` A ) /\ ( a ` A ) = 0 /\ ( ( coeff ` a ) ` ( degAA ` A ) ) = 1 ) ) ) -> a e. ( Poly ` QQ ) )
125 simprr1 
 |-  ( ( ( A e. AA /\ ( p e. ( Poly ` QQ ) /\ a e. ( Poly ` QQ ) ) ) /\ ( ( ( deg ` p ) = ( degAA ` A ) /\ ( p ` A ) = 0 /\ ( ( coeff ` p ) ` ( degAA ` A ) ) = 1 ) /\ ( ( deg ` a ) = ( degAA ` A ) /\ ( a ` A ) = 0 /\ ( ( coeff ` a ) ` ( degAA ` A ) ) = 1 ) ) ) -> ( deg ` a ) = ( degAA ` A ) )
126 simprl1 
 |-  ( ( ( A e. AA /\ ( p e. ( Poly ` QQ ) /\ a e. ( Poly ` QQ ) ) ) /\ ( ( ( deg ` p ) = ( degAA ` A ) /\ ( p ` A ) = 0 /\ ( ( coeff ` p ) ` ( degAA ` A ) ) = 1 ) /\ ( ( deg ` a ) = ( degAA ` A ) /\ ( a ` A ) = 0 /\ ( ( coeff ` a ) ` ( degAA ` A ) ) = 1 ) ) ) -> ( deg ` p ) = ( degAA ` A ) )
127 125 126 eqtr4d 
 |-  ( ( ( A e. AA /\ ( p e. ( Poly ` QQ ) /\ a e. ( Poly ` QQ ) ) ) /\ ( ( ( deg ` p ) = ( degAA ` A ) /\ ( p ` A ) = 0 /\ ( ( coeff ` p ) ` ( degAA ` A ) ) = 1 ) /\ ( ( deg ` a ) = ( degAA ` A ) /\ ( a ` A ) = 0 /\ ( ( coeff ` a ) ` ( degAA ` A ) ) = 1 ) ) ) -> ( deg ` a ) = ( deg ` p ) )
128 62 ad2antrr 
 |-  ( ( ( A e. AA /\ ( p e. ( Poly ` QQ ) /\ a e. ( Poly ` QQ ) ) ) /\ ( ( ( deg ` p ) = ( degAA ` A ) /\ ( p ` A ) = 0 /\ ( ( coeff ` p ) ` ( degAA ` A ) ) = 1 ) /\ ( ( deg ` a ) = ( degAA ` A ) /\ ( a ` A ) = 0 /\ ( ( coeff ` a ) ` ( degAA ` A ) ) = 1 ) ) ) -> ( degAA ` A ) e. NN )
129 126 128 eqeltrd 
 |-  ( ( ( A e. AA /\ ( p e. ( Poly ` QQ ) /\ a e. ( Poly ` QQ ) ) ) /\ ( ( ( deg ` p ) = ( degAA ` A ) /\ ( p ` A ) = 0 /\ ( ( coeff ` p ) ` ( degAA ` A ) ) = 1 ) /\ ( ( deg ` a ) = ( degAA ` A ) /\ ( a ` A ) = 0 /\ ( ( coeff ` a ) ` ( degAA ` A ) ) = 1 ) ) ) -> ( deg ` p ) e. NN )
130 simprl3 
 |-  ( ( ( A e. AA /\ ( p e. ( Poly ` QQ ) /\ a e. ( Poly ` QQ ) ) ) /\ ( ( ( deg ` p ) = ( degAA ` A ) /\ ( p ` A ) = 0 /\ ( ( coeff ` p ) ` ( degAA ` A ) ) = 1 ) /\ ( ( deg ` a ) = ( degAA ` A ) /\ ( a ` A ) = 0 /\ ( ( coeff ` a ) ` ( degAA ` A ) ) = 1 ) ) ) -> ( ( coeff ` p ) ` ( degAA ` A ) ) = 1 )
131 126 fveq2d 
 |-  ( ( ( A e. AA /\ ( p e. ( Poly ` QQ ) /\ a e. ( Poly ` QQ ) ) ) /\ ( ( ( deg ` p ) = ( degAA ` A ) /\ ( p ` A ) = 0 /\ ( ( coeff ` p ) ` ( degAA ` A ) ) = 1 ) /\ ( ( deg ` a ) = ( degAA ` A ) /\ ( a ` A ) = 0 /\ ( ( coeff ` a ) ` ( degAA ` A ) ) = 1 ) ) ) -> ( ( coeff ` p ) ` ( deg ` p ) ) = ( ( coeff ` p ) ` ( degAA ` A ) ) )
132 126 fveq2d 
 |-  ( ( ( A e. AA /\ ( p e. ( Poly ` QQ ) /\ a e. ( Poly ` QQ ) ) ) /\ ( ( ( deg ` p ) = ( degAA ` A ) /\ ( p ` A ) = 0 /\ ( ( coeff ` p ) ` ( degAA ` A ) ) = 1 ) /\ ( ( deg ` a ) = ( degAA ` A ) /\ ( a ` A ) = 0 /\ ( ( coeff ` a ) ` ( degAA ` A ) ) = 1 ) ) ) -> ( ( coeff ` a ) ` ( deg ` p ) ) = ( ( coeff ` a ) ` ( degAA ` A ) ) )
133 simprr3 
 |-  ( ( ( A e. AA /\ ( p e. ( Poly ` QQ ) /\ a e. ( Poly ` QQ ) ) ) /\ ( ( ( deg ` p ) = ( degAA ` A ) /\ ( p ` A ) = 0 /\ ( ( coeff ` p ) ` ( degAA ` A ) ) = 1 ) /\ ( ( deg ` a ) = ( degAA ` A ) /\ ( a ` A ) = 0 /\ ( ( coeff ` a ) ` ( degAA ` A ) ) = 1 ) ) ) -> ( ( coeff ` a ) ` ( degAA ` A ) ) = 1 )
134 132 133 eqtrd 
 |-  ( ( ( A e. AA /\ ( p e. ( Poly ` QQ ) /\ a e. ( Poly ` QQ ) ) ) /\ ( ( ( deg ` p ) = ( degAA ` A ) /\ ( p ` A ) = 0 /\ ( ( coeff ` p ) ` ( degAA ` A ) ) = 1 ) /\ ( ( deg ` a ) = ( degAA ` A ) /\ ( a ` A ) = 0 /\ ( ( coeff ` a ) ` ( degAA ` A ) ) = 1 ) ) ) -> ( ( coeff ` a ) ` ( deg ` p ) ) = 1 )
135 130 131 134 3eqtr4d 
 |-  ( ( ( A e. AA /\ ( p e. ( Poly ` QQ ) /\ a e. ( Poly ` QQ ) ) ) /\ ( ( ( deg ` p ) = ( degAA ` A ) /\ ( p ` A ) = 0 /\ ( ( coeff ` p ) ` ( degAA ` A ) ) = 1 ) /\ ( ( deg ` a ) = ( degAA ` A ) /\ ( a ` A ) = 0 /\ ( ( coeff ` a ) ` ( degAA ` A ) ) = 1 ) ) ) -> ( ( coeff ` p ) ` ( deg ` p ) ) = ( ( coeff ` a ) ` ( deg ` p ) ) )
136 eqid 
 |-  ( deg ` p ) = ( deg ` p )
137 136 dgrsub2 
 |-  ( ( ( p e. ( Poly ` QQ ) /\ a e. ( Poly ` QQ ) ) /\ ( ( deg ` a ) = ( deg ` p ) /\ ( deg ` p ) e. NN /\ ( ( coeff ` p ) ` ( deg ` p ) ) = ( ( coeff ` a ) ` ( deg ` p ) ) ) ) -> ( deg ` ( p oF - a ) ) < ( deg ` p ) )
138 123 124 127 129 135 137 syl23anc 
 |-  ( ( ( A e. AA /\ ( p e. ( Poly ` QQ ) /\ a e. ( Poly ` QQ ) ) ) /\ ( ( ( deg ` p ) = ( degAA ` A ) /\ ( p ` A ) = 0 /\ ( ( coeff ` p ) ` ( degAA ` A ) ) = 1 ) /\ ( ( deg ` a ) = ( degAA ` A ) /\ ( a ` A ) = 0 /\ ( ( coeff ` a ) ` ( degAA ` A ) ) = 1 ) ) ) -> ( deg ` ( p oF - a ) ) < ( deg ` p ) )
139 138 126 breqtrd 
 |-  ( ( ( A e. AA /\ ( p e. ( Poly ` QQ ) /\ a e. ( Poly ` QQ ) ) ) /\ ( ( ( deg ` p ) = ( degAA ` A ) /\ ( p ` A ) = 0 /\ ( ( coeff ` p ) ` ( degAA ` A ) ) = 1 ) /\ ( ( deg ` a ) = ( degAA ` A ) /\ ( a ` A ) = 0 /\ ( ( coeff ` a ) ` ( degAA ` A ) ) = 1 ) ) ) -> ( deg ` ( p oF - a ) ) < ( degAA ` A ) )
140 dgraa0p 
 |-  ( ( A e. AA /\ ( p oF - a ) e. ( Poly ` QQ ) /\ ( deg ` ( p oF - a ) ) < ( degAA ` A ) ) -> ( ( ( p oF - a ) ` A ) = 0 <-> ( p oF - a ) = 0p ) )
141 111 122 139 140 syl3anc 
 |-  ( ( ( A e. AA /\ ( p e. ( Poly ` QQ ) /\ a e. ( Poly ` QQ ) ) ) /\ ( ( ( deg ` p ) = ( degAA ` A ) /\ ( p ` A ) = 0 /\ ( ( coeff ` p ) ` ( degAA ` A ) ) = 1 ) /\ ( ( deg ` a ) = ( degAA ` A ) /\ ( a ` A ) = 0 /\ ( ( coeff ` a ) ` ( degAA ` A ) ) = 1 ) ) ) -> ( ( ( p oF - a ) ` A ) = 0 <-> ( p oF - a ) = 0p ) )
142 110 141 mpbid 
 |-  ( ( ( A e. AA /\ ( p e. ( Poly ` QQ ) /\ a e. ( Poly ` QQ ) ) ) /\ ( ( ( deg ` p ) = ( degAA ` A ) /\ ( p ` A ) = 0 /\ ( ( coeff ` p ) ` ( degAA ` A ) ) = 1 ) /\ ( ( deg ` a ) = ( degAA ` A ) /\ ( a ` A ) = 0 /\ ( ( coeff ` a ) ` ( degAA ` A ) ) = 1 ) ) ) -> ( p oF - a ) = 0p )
143 df-0p 
 |-  0p = ( CC X. { 0 } )
144 142 143 eqtrdi 
 |-  ( ( ( A e. AA /\ ( p e. ( Poly ` QQ ) /\ a e. ( Poly ` QQ ) ) ) /\ ( ( ( deg ` p ) = ( degAA ` A ) /\ ( p ` A ) = 0 /\ ( ( coeff ` p ) ` ( degAA ` A ) ) = 1 ) /\ ( ( deg ` a ) = ( degAA ` A ) /\ ( a ` A ) = 0 /\ ( ( coeff ` a ) ` ( degAA ` A ) ) = 1 ) ) ) -> ( p oF - a ) = ( CC X. { 0 } ) )
145 ofsubeq0 
 |-  ( ( CC e. _V /\ p : CC --> CC /\ a : CC --> CC ) -> ( ( p oF - a ) = ( CC X. { 0 } ) <-> p = a ) )
146 49 145 mp3an1 
 |-  ( ( p : CC --> CC /\ a : CC --> CC ) -> ( ( p oF - a ) = ( CC X. { 0 } ) <-> p = a ) )
147 95 46 146 syl2an 
 |-  ( ( p e. ( Poly ` QQ ) /\ a e. ( Poly ` QQ ) ) -> ( ( p oF - a ) = ( CC X. { 0 } ) <-> p = a ) )
148 147 ad2antlr 
 |-  ( ( ( A e. AA /\ ( p e. ( Poly ` QQ ) /\ a e. ( Poly ` QQ ) ) ) /\ ( ( ( deg ` p ) = ( degAA ` A ) /\ ( p ` A ) = 0 /\ ( ( coeff ` p ) ` ( degAA ` A ) ) = 1 ) /\ ( ( deg ` a ) = ( degAA ` A ) /\ ( a ` A ) = 0 /\ ( ( coeff ` a ) ` ( degAA ` A ) ) = 1 ) ) ) -> ( ( p oF - a ) = ( CC X. { 0 } ) <-> p = a ) )
149 144 148 mpbid 
 |-  ( ( ( A e. AA /\ ( p e. ( Poly ` QQ ) /\ a e. ( Poly ` QQ ) ) ) /\ ( ( ( deg ` p ) = ( degAA ` A ) /\ ( p ` A ) = 0 /\ ( ( coeff ` p ) ` ( degAA ` A ) ) = 1 ) /\ ( ( deg ` a ) = ( degAA ` A ) /\ ( a ` A ) = 0 /\ ( ( coeff ` a ) ` ( degAA ` A ) ) = 1 ) ) ) -> p = a )
150 149 ex 
 |-  ( ( A e. AA /\ ( p e. ( Poly ` QQ ) /\ a e. ( Poly ` QQ ) ) ) -> ( ( ( ( deg ` p ) = ( degAA ` A ) /\ ( p ` A ) = 0 /\ ( ( coeff ` p ) ` ( degAA ` A ) ) = 1 ) /\ ( ( deg ` a ) = ( degAA ` A ) /\ ( a ` A ) = 0 /\ ( ( coeff ` a ) ` ( degAA ` A ) ) = 1 ) ) -> p = a ) )
151 150 ralrimivva 
 |-  ( A e. AA -> A. p e. ( Poly ` QQ ) A. a e. ( Poly ` QQ ) ( ( ( ( deg ` p ) = ( degAA ` A ) /\ ( p ` A ) = 0 /\ ( ( coeff ` p ) ` ( degAA ` A ) ) = 1 ) /\ ( ( deg ` a ) = ( degAA ` A ) /\ ( a ` A ) = 0 /\ ( ( coeff ` a ) ` ( degAA ` A ) ) = 1 ) ) -> p = a ) )
152 fveqeq2 
 |-  ( p = a -> ( ( deg ` p ) = ( degAA ` A ) <-> ( deg ` a ) = ( degAA ` A ) ) )
153 fveq1 
 |-  ( p = a -> ( p ` A ) = ( a ` A ) )
154 153 eqeq1d 
 |-  ( p = a -> ( ( p ` A ) = 0 <-> ( a ` A ) = 0 ) )
155 fveq2 
 |-  ( p = a -> ( coeff ` p ) = ( coeff ` a ) )
156 155 fveq1d 
 |-  ( p = a -> ( ( coeff ` p ) ` ( degAA ` A ) ) = ( ( coeff ` a ) ` ( degAA ` A ) ) )
157 156 eqeq1d 
 |-  ( p = a -> ( ( ( coeff ` p ) ` ( degAA ` A ) ) = 1 <-> ( ( coeff ` a ) ` ( degAA ` A ) ) = 1 ) )
158 152 154 157 3anbi123d 
 |-  ( p = a -> ( ( ( deg ` p ) = ( degAA ` A ) /\ ( p ` A ) = 0 /\ ( ( coeff ` p ) ` ( degAA ` A ) ) = 1 ) <-> ( ( deg ` a ) = ( degAA ` A ) /\ ( a ` A ) = 0 /\ ( ( coeff ` a ) ` ( degAA ` A ) ) = 1 ) ) )
159 158 reu4 
 |-  ( E! p e. ( Poly ` QQ ) ( ( deg ` p ) = ( degAA ` A ) /\ ( p ` A ) = 0 /\ ( ( coeff ` p ) ` ( degAA ` A ) ) = 1 ) <-> ( E. p e. ( Poly ` QQ ) ( ( deg ` p ) = ( degAA ` A ) /\ ( p ` A ) = 0 /\ ( ( coeff ` p ) ` ( degAA ` A ) ) = 1 ) /\ A. p e. ( Poly ` QQ ) A. a e. ( Poly ` QQ ) ( ( ( ( deg ` p ) = ( degAA ` A ) /\ ( p ` A ) = 0 /\ ( ( coeff ` p ) ` ( degAA ` A ) ) = 1 ) /\ ( ( deg ` a ) = ( degAA ` A ) /\ ( a ` A ) = 0 /\ ( ( coeff ` a ) ` ( degAA ` A ) ) = 1 ) ) -> p = a ) ) )
160 91 151 159 sylanbrc 
 |-  ( A e. AA -> E! p e. ( Poly ` QQ ) ( ( deg ` p ) = ( degAA ` A ) /\ ( p ` A ) = 0 /\ ( ( coeff ` p ) ` ( degAA ` A ) ) = 1 ) )