Theorem mpaaeu 29352

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

Assertion

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

Distinct variable group:   A, p

Proof of Theorem mpaaeu

Dummy variables a b c are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		dgraalem 29347	. . . 4 |- ( A e. AA -> ( (degAA ` A ) e. NN /\ E. a e. ( (Poly ` QQ ) \ { 0p } ) ( (deg ` a ) = (degAA ` A ) /\ ( a ` A ) = 0 ) ) )
2	1	simprd 460	. . 3 |- ( A e. AA -> E. a e. ( (Poly ` QQ ) \ { 0p } ) ( (deg ` a ) = (degAA ` A ) /\ ( a ` A ) = 0 ) )
3		qsscn 10952	. . . . . . . 8 |- QQ C_ CC
4		eldifi 3466	. . . . . . . . . . . 12 |- ( a e. ( (Poly ` QQ ) \ { 0p } ) -> a e. (Poly ` QQ ) )
5	4	ad2antlr 719	. . . . . . . . . . 11 |- ( ( ( A e. AA /\ a e. ( (Poly ` QQ ) \ { 0p } ) ) /\ ( (deg ` a ) = (degAA ` A ) /\ ( a ` A ) = 0 ) ) -> a e. (Poly ` QQ ) )
6		zssq 10948	. . . . . . . . . . . 12 |- ZZ C_ QQ
7		0z 10645	. . . . . . . . . . . 12 |- 0 e. ZZ
8	6, 7	sselii 3341	. . . . . . . . . . 11 |- 0 e. QQ
9		eqid 2433	. . . . . . . . . . . 12 |- (coeff ` a ) = (coeff ` a )
10	9	coef2 21584	. . . . . . . . . . 11 |- ( ( a e. (Poly ` QQ ) /\ 0 e. QQ ) -> (coeff ` a ) : NN0 --> QQ )
11	5, 8, 10	sylancl 655	. . . . . . . . . 10 |- ( ( ( A e. AA /\ a e. ( (Poly ` QQ ) \ { 0p } ) ) /\ ( (deg ` a ) = (degAA ` A ) /\ ( a ` A ) = 0 ) ) -> (coeff ` a ) : NN0 --> QQ )
12		dgrcl 21586	. . . . . . . . . . 11 |- ( a e. (Poly ` QQ ) -> (deg ` a ) e. NN0 )
13	5, 12	syl 16	. . . . . . . . . 10 |- ( ( ( A e. AA /\ a e. ( (Poly ` QQ ) \ { 0p } ) ) /\ ( (deg ` a ) = (degAA ` A ) /\ ( a ` A ) = 0 ) ) -> (deg ` a ) e. NN0 )
14	11, 13	ffvelrnd 5832	. . . . . . . . 9 |- ( ( ( A e. AA /\ a e. ( (Poly ` QQ ) \ { 0p } ) ) /\ ( (deg ` a ) = (degAA ` A ) /\ ( a ` A ) = 0 ) ) -> ( (coeff ` a ) ` (deg ` a ) ) e. QQ )
15		eldifsni 3989	. . . . . . . . . . 11 |- ( a e. ( (Poly ` QQ ) \ { 0p } ) -> a =/= 0p )
16	15	ad2antlr 719	. . . . . . . . . 10 |- ( ( ( A e. AA /\ a e. ( (Poly ` QQ ) \ { 0p } ) ) /\ ( (deg ` a ) = (degAA ` A ) /\ ( a ` A ) = 0 ) ) -> a =/= 0p )
17		eqid 2433	. . . . . . . . . . . . 13 |- (deg ` a ) = (deg ` a )
18	17, 9	dgreq0 21617	. . . . . . . . . . . 12 |- ( a e. (Poly ` QQ ) -> ( a = 0p <-> ( (coeff ` a ) ` (deg ` a ) ) = 0 ) )
19	18	necon3bid 2633	. . . . . . . . . . 11 |- ( a e. (Poly ` QQ ) -> ( a =/= 0p <-> ( (coeff ` a ) ` (deg ` a ) ) =/= 0 ) )
20	5, 19	syl 16	. . . . . . . . . 10 |- ( ( ( A e. AA /\ a e. ( (Poly ` QQ ) \ { 0p } ) ) /\ ( (deg ` a ) = (degAA ` A ) /\ ( a ` A ) = 0 ) ) -> ( a =/= 0p <-> ( (coeff ` a ) ` (deg ` a ) ) =/= 0 ) )
21	16, 20	mpbid 210	. . . . . . . . 9 |- ( ( ( A e. AA /\ a e. ( (Poly ` QQ ) \ { 0p } ) ) /\ ( (deg ` a ) = (degAA ` A ) /\ ( a ` A ) = 0 ) ) -> ( (coeff ` a ) ` (deg ` a ) ) =/= 0 )
22		qreccl 10961	. . . . . . . . 9 |- ( ( ( (coeff ` a ) ` (deg ` a ) ) e. QQ /\ ( (coeff ` a ) ` (deg ` a ) ) =/= 0 ) -> ( 1 / ( (coeff ` a ) ` (deg ` a ) ) ) e. QQ )
23	14, 21, 22	syl2anc 654	. . . . . . . 8 |- ( ( ( A e. AA /\ a e. ( (Poly ` QQ ) \ { 0p } ) ) /\ ( (deg ` a ) = (degAA ` A ) /\ ( a ` A ) = 0 ) ) -> ( 1 / ( (coeff ` a ) ` (deg ` a ) ) ) e. QQ )
24		plyconst 21559	. . . . . . . 8 |- ( ( QQ C_ CC /\ ( 1 / ( (coeff ` a ) ` (deg ` a ) ) ) e. QQ ) -> ( CC X. { ( 1 / ( (coeff ` a ) ` (deg ` a ) ) ) } ) e. (Poly ` QQ ) )
25	3, 23, 24	sylancr 656	. . . . . . 7 |- ( ( ( 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 ) )
26		simpl 454	. . . . . . . 8 |- ( ( ( CC X. { ( 1 / ( (coeff ` a ) ` (deg ` a ) ) ) } ) e. (Poly ` QQ ) /\ a e. (Poly ` QQ ) ) -> ( CC X. { ( 1 / ( (coeff ` a ) ` (deg ` a ) ) ) } ) e. (Poly ` QQ ) )
27		simpr 458	. . . . . . . 8 |- ( ( ( CC X. { ( 1 / ( (coeff ` a ) ` (deg ` a ) ) ) } ) e. (Poly ` QQ ) /\ a e. (Poly ` QQ ) ) -> a e. (Poly ` QQ ) )
28		qaddcl 10957	. . . . . . . . 9 |- ( ( b e. QQ /\ c e. QQ ) -> ( b + c ) e. QQ )
29	28	adantl 463	. . . . . . . 8 |- ( ( ( ( CC X. { ( 1 / ( (coeff ` a ) ` (deg ` a ) ) ) } ) e. (Poly ` QQ ) /\ a e. (Poly ` QQ ) ) /\ ( b e. QQ /\ c e. QQ ) ) -> ( b + c ) e. QQ )
30		qmulcl 10959	. . . . . . . . 9 |- ( ( b e. QQ /\ c e. QQ ) -> ( b x. c ) e. QQ )
31	30	adantl 463	. . . . . . . 8 |- ( ( ( ( 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 )
32	26, 27, 29, 31	plymul 21571	. . . . . . 7 |- ( ( ( 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 ) )
33	25, 5, 32	syl2anc 654	. . . . . 6 |- ( ( ( 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 ) )
34	9	coef3 21585	. . . . . . . . . . 11 |- ( a e. (Poly ` QQ ) -> (coeff ` a ) : NN0 --> CC )
35	5, 34	syl 16	. . . . . . . . . 10 |- ( ( ( A e. AA /\ a e. ( (Poly ` QQ ) \ { 0p } ) ) /\ ( (deg ` a ) = (degAA ` A ) /\ ( a ` A ) = 0 ) ) -> (coeff ` a ) : NN0 --> CC )
36	35, 13	ffvelrnd 5832	. . . . . . . . 9 |- ( ( ( A e. AA /\ a e. ( (Poly ` QQ ) \ { 0p } ) ) /\ ( (deg ` a ) = (degAA ` A ) /\ ( a ` A ) = 0 ) ) -> ( (coeff ` a ) ` (deg ` a ) ) e. CC )
37	36, 21	reccld 10088	. . . . . . . 8 |- ( ( ( A e. AA /\ a e. ( (Poly ` QQ ) \ { 0p } ) ) /\ ( (deg ` a ) = (degAA ` A ) /\ ( a ` A ) = 0 ) ) -> ( 1 / ( (coeff ` a ) ` (deg ` a ) ) ) e. CC )
38	36, 21	recne0d 10089	. . . . . . . 8 |- ( ( ( A e. AA /\ a e. ( (Poly ` QQ ) \ { 0p } ) ) /\ ( (deg ` a ) = (degAA ` A ) /\ ( a ` A ) = 0 ) ) -> ( 1 / ( (coeff ` a ) ` (deg ` a ) ) ) =/= 0 )
39		dgrmulc 21623	. . . . . . . 8 |- ( ( ( 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 ) )
40	37, 38, 5, 39	syl3anc 1211	. . . . . . 7 |- ( ( ( 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 ) )
41		simprl 748	. . . . . . 7 |- ( ( ( A e. AA /\ a e. ( (Poly ` QQ ) \ { 0p } ) ) /\ ( (deg ` a ) = (degAA ` A ) /\ ( a ` A ) = 0 ) ) -> (deg ` a ) = (degAA ` A ) )
42	40, 41	eqtrd 2465	. . . . . 6 |- ( ( ( 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 ) )
43		aacn 21668	. . . . . . . . 9 |- ( A e. AA -> A e. CC )
44	43	ad2antrr 718	. . . . . . . 8 |- ( ( ( A e. AA /\ a e. ( (Poly ` QQ ) \ { 0p } ) ) /\ ( (deg ` a ) = (degAA ` A ) /\ ( a ` A ) = 0 ) ) -> A e. CC )
45		ovex 6105	. . . . . . . . . 10 |- ( 1 / ( (coeff ` a ) ` (deg ` a ) ) ) e. _V
46		fnconstg 5586	. . . . . . . . . 10 |- ( ( 1 / ( (coeff ` a ) ` (deg ` a ) ) ) e. _V -> ( CC X. { ( 1 / ( (coeff ` a ) ` (deg ` a ) ) ) } ) Fn CC )
47	45, 46	mp1i 12	. . . . . . . . 9 |- ( ( ( A e. AA /\ a e. ( (Poly ` QQ ) \ { 0p } ) ) /\ ( (deg ` a ) = (degAA ` A ) /\ ( a ` A ) = 0 ) ) -> ( CC X. { ( 1 / ( (coeff ` a ) ` (deg ` a ) ) ) } ) Fn CC )
48		plyf 21551	. . . . . . . . . 10 |- ( a e. (Poly ` QQ ) -> a : CC --> CC )
49		ffn 5547	. . . . . . . . . 10 |- ( a : CC --> CC -> a Fn CC )
50	5, 48, 49	3syl 20	. . . . . . . . 9 |- ( ( ( A e. AA /\ a e. ( (Poly ` QQ ) \ { 0p } ) ) /\ ( (deg ` a ) = (degAA ` A ) /\ ( a ` A ) = 0 ) ) -> a Fn CC )
51		cnex 9351	. . . . . . . . . 10 |- CC e. _V
52	51	a1i 11	. . . . . . . . 9 |- ( ( ( A e. AA /\ a e. ( (Poly ` QQ ) \ { 0p } ) ) /\ ( (deg ` a ) = (degAA ` A ) /\ ( a ` A ) = 0 ) ) -> CC e. _V )
53		inidm 3547	. . . . . . . . 9 |- ( CC i^i CC ) = CC
54	45	fvconst2 5920	. . . . . . . . . 10 |- ( A e. CC -> ( ( CC X. { ( 1 / ( (coeff ` a ) ` (deg ` a ) ) ) } ) ` A ) = ( 1 / ( (coeff ` a ) ` (deg ` a ) ) ) )
55	54	adantl 463	. . . . . . . . 9 |- ( ( ( ( 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 ) ) ) )
56		simplrr 753	. . . . . . . . 9 |- ( ( ( ( A e. AA /\ a e. ( (Poly ` QQ ) \ { 0p } ) ) /\ ( (deg ` a ) = (degAA ` A ) /\ ( a ` A ) = 0 ) ) /\ A e. CC ) -> ( a ` A ) = 0 )
57	47, 50, 52, 52, 53, 55, 56	ofval 6318	. . . . . . . 8 |- ( ( ( ( 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 ) )
58	44, 57	mpdan 661	. . . . . . 7 |- ( ( ( 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 ) )
59	37	mul01d 9556	. . . . . . 7 |- ( ( ( A e. AA /\ a e. ( (Poly ` QQ ) \ { 0p } ) ) /\ ( (deg ` a ) = (degAA ` A ) /\ ( a ` A ) = 0 ) ) -> ( ( 1 / ( (coeff ` a ) ` (deg ` a ) ) ) x. 0 ) = 0 )
60	58, 59	eqtrd 2465	. . . . . 6 |- ( ( ( 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 )
61		coemulc 21607	. . . . . . . . 9 |- ( ( ( 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 ) ) )
62	37, 5, 61	syl2anc 654	. . . . . . . 8 |- ( ( ( 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 ) ) )
63	62	fveq1d 5681	. . . . . . 7 |- ( ( ( 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 ) ) )
64		dgraacl 29348	. . . . . . . . . 10 |- ( A e. AA -> (degAA ` A ) e. NN )
65	64	ad2antrr 718	. . . . . . . . 9 |- ( ( ( A e. AA /\ a e. ( (Poly ` QQ ) \ { 0p } ) ) /\ ( (deg ` a ) = (degAA ` A ) /\ ( a ` A ) = 0 ) ) -> (degAA ` A ) e. NN )
66	65	nnnn0d 10624	. . . . . . . 8 |- ( ( ( A e. AA /\ a e. ( (Poly ` QQ ) \ { 0p } ) ) /\ ( (deg ` a ) = (degAA ` A ) /\ ( a ` A ) = 0 ) ) -> (degAA ` A ) e. NN0 )
67		fnconstg 5586	. . . . . . . . . 10 |- ( ( 1 / ( (coeff ` a ) ` (deg ` a ) ) ) e. _V -> ( NN0 X. { ( 1 / ( (coeff ` a ) ` (deg ` a ) ) ) } ) Fn NN0 )
68	45, 67	mp1i 12	. . . . . . . . 9 |- ( ( ( A e. AA /\ a e. ( (Poly ` QQ ) \ { 0p } ) ) /\ ( (deg ` a ) = (degAA ` A ) /\ ( a ` A ) = 0 ) ) -> ( NN0 X. { ( 1 / ( (coeff ` a ) ` (deg ` a ) ) ) } ) Fn NN0 )
69		ffn 5547	. . . . . . . . . 10 |- ( (coeff ` a ) : NN0 --> CC -> (coeff ` a ) Fn NN0 )
70	35, 69	syl 16	. . . . . . . . 9 |- ( ( ( A e. AA /\ a e. ( (Poly ` QQ ) \ { 0p } ) ) /\ ( (deg ` a ) = (degAA ` A ) /\ ( a ` A ) = 0 ) ) -> (coeff ` a ) Fn NN0 )
71		nn0ex 10573	. . . . . . . . . 10 |- NN0 e. _V
72	71	a1i 11	. . . . . . . . 9 |- ( ( ( A e. AA /\ a e. ( (Poly ` QQ ) \ { 0p } ) ) /\ ( (deg ` a ) = (degAA ` A ) /\ ( a ` A ) = 0 ) ) -> NN0 e. _V )
73		inidm 3547	. . . . . . . . 9 |- ( NN0 i^i NN0 ) = NN0
74	45	fvconst2 5920	. . . . . . . . . 10 |- ( (degAA ` A ) e. NN0 -> ( ( NN0 X. { ( 1 / ( (coeff ` a ) ` (deg ` a ) ) ) } ) ` (degAA ` A ) ) = ( 1 / ( (coeff ` a ) ` (deg ` a ) ) ) )
75	74	adantl 463	. . . . . . . . 9 |- ( ( ( ( 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 ) ) ) )
76		simplrl 752	. . . . . . . . . . 11 |- ( ( ( ( A e. AA /\ a e. ( (Poly ` QQ ) \ { 0p } ) ) /\ ( (deg ` a ) = (degAA ` A ) /\ ( a ` A ) = 0 ) ) /\ (degAA ` A ) e. NN0 ) -> (deg ` a ) = (degAA ` A ) )
77	76	eqcomd 2438	. . . . . . . . . 10 |- ( ( ( ( A e. AA /\ a e. ( (Poly ` QQ ) \ { 0p } ) ) /\ ( (deg ` a ) = (degAA ` A ) /\ ( a ` A ) = 0 ) ) /\ (degAA ` A ) e. NN0 ) -> (degAA ` A ) = (deg ` a ) )
78	77	fveq2d 5683	. . . . . . . . 9 |- ( ( ( ( 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 ) ) )
79	68, 70, 72, 72, 73, 75, 78	ofval 6318	. . . . . . . 8 |- ( ( ( ( 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 ) ) ) )
80	66, 79	mpdan 661	. . . . . . 7 |- ( ( ( 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 ) ) ) )
81	36, 21	recid2d 10091	. . . . . . 7 |- ( ( ( 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 )
82	63, 80, 81	3eqtrd 2469	. . . . . 6 |- ( ( ( 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 )
83		fveq2 5679	. . . . . . . . 9 |- ( p = ( ( CC X. { ( 1 / ( (coeff ` a ) ` (deg ` a ) ) ) } ) oF x. a ) -> (deg ` p ) = (deg ` ( ( CC X. { ( 1 / ( (coeff ` a ) ` (deg ` a ) ) ) } ) oF x. a ) ) )
84	83	eqeq1d 2441	. . . . . . . 8 |- ( 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 ) ) )
85		fveq1 5678	. . . . . . . . 9 |- ( p = ( ( CC X. { ( 1 / ( (coeff ` a ) ` (deg ` a ) ) ) } ) oF x. a ) -> ( p ` A ) = ( ( ( CC X. { ( 1 / ( (coeff ` a ) ` (deg ` a ) ) ) } ) oF x. a ) ` A ) )
86	85	eqeq1d 2441	. . . . . . . 8 |- ( 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 ) )
87		fveq2 5679	. . . . . . . . . 10 |- ( p = ( ( CC X. { ( 1 / ( (coeff ` a ) ` (deg ` a ) ) ) } ) oF x. a ) -> (coeff ` p ) = (coeff ` ( ( CC X. { ( 1 / ( (coeff ` a ) ` (deg ` a ) ) ) } ) oF x. a ) ) )
88	87	fveq1d 5681	. . . . . . . . 9 |- ( 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 ) ) )
89	88	eqeq1d 2441	. . . . . . . 8 |- ( 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 ) )
90	84, 86, 89	3anbi123d 1282	. . . . . . 7 |- ( 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 ) ) )
91	90	rspcev 3062	. . . . . 6 |- ( ( ( ( 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 ) )
92	33, 42, 60, 82, 91	syl13anc 1213	. . . . 5 |- ( ( ( 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 ) )
93	92	ex 434	. . . 4 |- ( ( 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 ) ) )
94	93	rexlimdva 2831	. . 3 |- ( A e. AA -> ( E. 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 ) ) )
95	2, 94	mpd 15	. 2 |- ( A e. AA -> E. p e. (Poly ` QQ ) ( (deg ` p ) = (degAA ` A ) /\ ( p ` A ) = 0 /\ ( (coeff ` p ) ` (degAA ` A ) ) = 1 ) )
96		simp2 982	. . . . . . . . . . 11 |- ( ( (deg ` p ) = (degAA ` A ) /\ ( p ` A ) = 0 /\ ( (coeff ` p ) ` (degAA ` A ) ) = 1 ) -> ( p ` A ) = 0 )
97		simp2 982	. . . . . . . . . . 11 |- ( ( (deg ` a ) = (degAA ` A ) /\ ( a ` A ) = 0 /\ ( (coeff ` a ) ` (degAA ` A ) ) = 1 ) -> ( a ` A ) = 0 )
98	96, 97	anim12i 561	. . . . . . . . . 10 |- ( ( ( (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 ) )
99		plyf 21551	. . . . . . . . . . . . . . . 16 |- ( p e. (Poly ` QQ ) -> p : CC --> CC )
100		ffn 5547	. . . . . . . . . . . . . . . 16 |- ( p : CC --> CC -> p Fn CC )
101	99, 100	syl 16	. . . . . . . . . . . . . . 15 |- ( p e. (Poly ` QQ ) -> p Fn CC )
102	101	ad2antrr 718	. . . . . . . . . . . . . 14 |- ( ( ( p e. (Poly ` QQ ) /\ a e. (Poly ` QQ ) ) /\ ( ( p ` A ) = 0 /\ ( a ` A ) = 0 ) ) -> p Fn CC )
103	48, 49	syl 16	. . . . . . . . . . . . . . 15 |- ( a e. (Poly ` QQ ) -> a Fn CC )
104	103	ad2antlr 719	. . . . . . . . . . . . . 14 |- ( ( ( p e. (Poly ` QQ ) /\ a e. (Poly ` QQ ) ) /\ ( ( p ` A ) = 0 /\ ( a ` A ) = 0 ) ) -> a Fn CC )
105	51	a1i 11	. . . . . . . . . . . . . 14 |- ( ( ( p e. (Poly ` QQ ) /\ a e. (Poly ` QQ ) ) /\ ( ( p ` A ) = 0 /\ ( a ` A ) = 0 ) ) -> CC e. _V )
106		simplrl 752	. . . . . . . . . . . . . 14 |- ( ( ( ( p e. (Poly ` QQ ) /\ a e. (Poly ` QQ ) ) /\ ( ( p ` A ) = 0 /\ ( a ` A ) = 0 ) ) /\ A e. CC ) -> ( p ` A ) = 0 )
107		simplrr 753	. . . . . . . . . . . . . 14 |- ( ( ( ( p e. (Poly ` QQ ) /\ a e. (Poly ` QQ ) ) /\ ( ( p ` A ) = 0 /\ ( a ` A ) = 0 ) ) /\ A e. CC ) -> ( a ` A ) = 0 )
108	102, 104, 105, 105, 53, 106, 107	ofval 6318	. . . . . . . . . . . . 13 |- ( ( ( ( p e. (Poly ` QQ ) /\ a e. (Poly ` QQ ) ) /\ ( ( p ` A ) = 0 /\ ( a ` A ) = 0 ) ) /\ A e. CC ) -> ( ( p oF - a ) ` A ) = ( 0 - 0 ) )
109	43, 108	sylan2 471	. . . . . . . . . . . 12 |- ( ( ( ( p e. (Poly ` QQ ) /\ a e. (Poly ` QQ ) ) /\ ( ( p ` A ) = 0 /\ ( a ` A ) = 0 ) ) /\ A e. AA ) -> ( ( p oF - a ) ` A ) = ( 0 - 0 ) )
110		0m0e0 10419	. . . . . . . . . . . 12 |- ( 0 - 0 ) = 0
111	109, 110	syl6eq 2481	. . . . . . . . . . 11 |- ( ( ( ( p e. (Poly ` QQ ) /\ a e. (Poly ` QQ ) ) /\ ( ( p ` A ) = 0 /\ ( a ` A ) = 0 ) ) /\ A e. AA ) -> ( ( p oF - a ) ` A ) = 0 )
112	111	ex 434	. . . . . . . . . 10 |- ( ( ( p e. (Poly ` QQ ) /\ a e. (Poly ` QQ ) ) /\ ( ( p ` A ) = 0 /\ ( a ` A ) = 0 ) ) -> ( A e. AA -> ( ( p oF - a ) ` A ) = 0 ) )
113	98, 112	sylan2 471	. . . . . . . . 9 |- ( ( ( 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 ) )
114	113	com12 31	. . . . . . . 8 |- ( 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 ) )
115	114	impl 615	. . . . . . 7 |- ( ( ( 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 )
116		simpll 746	. . . . . . . 8 |- ( ( ( 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 )
117		simpl 454	. . . . . . . . . 10 |- ( ( p e. (Poly ` QQ ) /\ a e. (Poly ` QQ ) ) -> p e. (Poly ` QQ ) )
118		simpr 458	. . . . . . . . . 10 |- ( ( p e. (Poly ` QQ ) /\ a e. (Poly ` QQ ) ) -> a e. (Poly ` QQ ) )
119	28	adantl 463	. . . . . . . . . 10 |- ( ( ( p e. (Poly ` QQ ) /\ a e. (Poly ` QQ ) ) /\ ( b e. QQ /\ c e. QQ ) ) -> ( b + c ) e. QQ )
120	30	adantl 463	. . . . . . . . . 10 |- ( ( ( p e. (Poly ` QQ ) /\ a e. (Poly ` QQ ) ) /\ ( b e. QQ /\ c e. QQ ) ) -> ( b x. c ) e. QQ )
121		1z 10664	. . . . . . . . . . . 12 |- 1 e. ZZ
122		zq 10947	. . . . . . . . . . . 12 |- ( 1 e. ZZ -> 1 e. QQ )
123		qnegcl 10958	. . . . . . . . . . . 12 |- ( 1 e. QQ -> -u 1 e. QQ )
124	121, 122, 123	mp2b 10	. . . . . . . . . . 11 |- -u 1 e. QQ
125	124	a1i 11	. . . . . . . . . 10 |- ( ( p e. (Poly ` QQ ) /\ a e. (Poly ` QQ ) ) -> -u 1 e. QQ )
126	117, 118, 119, 120, 125	plysub 21572	. . . . . . . . 9 |- ( ( p e. (Poly ` QQ ) /\ a e. (Poly ` QQ ) ) -> ( p oF - a ) e. (Poly ` QQ ) )
127	126	ad2antlr 719	. . . . . . . 8 |- ( ( ( 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 ) )
128		simplrl 752	. . . . . . . . . 10 |- ( ( ( 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 ) )
129		simplrr 753	. . . . . . . . . 10 |- ( ( ( 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 ) )
130		simprr1 1029	. . . . . . . . . . 11 |- ( ( ( 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 ) )
131		simprl1 1026	. . . . . . . . . . 11 |- ( ( ( 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 ) )
132	130, 131	eqtr4d 2468	. . . . . . . . . 10 |- ( ( ( 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 ) )
133	64	ad2antrr 718	. . . . . . . . . . 11 |- ( ( ( 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 )
134	131, 133	eqeltrd 2507	. . . . . . . . . 10 |- ( ( ( 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 )
135		simprl3 1028	. . . . . . . . . . 11 |- ( ( ( 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 )
136	131	fveq2d 5683	. . . . . . . . . . 11 |- ( ( ( 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 ) ) )
137	131	fveq2d 5683	. . . . . . . . . . . 12 |- ( ( ( 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 ) ) )
138		simprr3 1031	. . . . . . . . . . . 12 |- ( ( ( 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 )
139	137, 138	eqtrd 2465	. . . . . . . . . . 11 |- ( ( ( 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 )
140	135, 136, 139	3eqtr4d 2475	. . . . . . . . . 10 |- ( ( ( 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 ) ) )
141		eqid 2433	. . . . . . . . . . 11 |- (deg ` p ) = (deg ` p )
142	141	dgrsub2 29336	. . . . . . . . . 10 |- ( ( ( 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 ) )
143	128, 129, 132, 134, 140, 142	syl23anc 1218	. . . . . . . . 9 |- ( ( ( 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 ) )
144	143, 131	breqtrd 4304	. . . . . . . 8 |- ( ( ( 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 ) )
145		dgraa0p 29351	. . . . . . . 8 |- ( ( A e. AA /\ ( p oF - a ) e. (Poly ` QQ ) /\ (deg ` ( p oF - a ) ) < (degAA ` A ) ) -> ( ( ( p oF - a ) ` A ) = 0 <-> ( p oF - a ) = 0p ) )
146	116, 127, 144, 145	syl3anc 1211	. . . . . . 7 |- ( ( ( 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 ) )
147	115, 146	mpbid 210	. . . . . 6 |- ( ( ( 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 )
148		df-0p 20990	. . . . . 6 |- 0p = ( CC X. { 0 } )
149	147, 148	syl6eq 2481	. . . . 5 |- ( ( ( 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 } ) )
150		ofsubeq0 10307	. . . . . . . 8 |- ( ( CC e. _V /\ p : CC --> CC /\ a : CC --> CC ) -> ( ( p oF - a ) = ( CC X. { 0 } ) <-> p = a ) )
151	51, 150	mp3an1 1294	. . . . . . 7 |- ( ( p : CC --> CC /\ a : CC --> CC ) -> ( ( p oF - a ) = ( CC X. { 0 } ) <-> p = a ) )
152	99, 48, 151	syl2an 474	. . . . . 6 |- ( ( p e. (Poly ` QQ ) /\ a e. (Poly ` QQ ) ) -> ( ( p oF - a ) = ( CC X. { 0 } ) <-> p = a ) )
153	152	ad2antlr 719	. . . . 5 |- ( ( ( 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 ) )
154	149, 153	mpbid 210	. . . 4 |- ( ( ( 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 )
155	154	ex 434	. . 3 |- ( ( 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 ) )
156	155	ralrimivva 2798	. 2 |- ( 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 ) )
157		fveq2 5679	. . . . 5 |- ( p = a -> (deg ` p ) = (deg ` a ) )
158	157	eqeq1d 2441	. . . 4 |- ( p = a -> ( (deg ` p ) = (degAA ` A ) <-> (deg ` a ) = (degAA ` A ) ) )
159		fveq1 5678	. . . . 5 |- ( p = a -> ( p ` A ) = ( a ` A ) )
160	159	eqeq1d 2441	. . . 4 |- ( p = a -> ( ( p ` A ) = 0 <-> ( a ` A ) = 0 ) )
161		fveq2 5679	. . . . . 6 |- ( p = a -> (coeff ` p ) = (coeff ` a ) )
162	161	fveq1d 5681	. . . . 5 |- ( p = a -> ( (coeff ` p ) ` (degAA ` A ) ) = ( (coeff ` a ) ` (degAA ` A ) ) )
163	162	eqeq1d 2441	. . . 4 |- ( p = a -> ( ( (coeff ` p ) ` (degAA ` A ) ) = 1 <-> ( (coeff ` a ) ` (degAA ` A ) ) = 1 ) )
164	158, 160, 163	3anbi123d 1282	. . 3 |- ( 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 ) ) )
165	164	reu4 3142	. 2 |- ( 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 ) ) )
166	95, 156, 165	sylanbrc 657	1 |- ( A e. AA -> E! p e. (Poly ` QQ ) ( (deg ` p ) = (degAA ` A ) /\ ( p ` A ) = 0 /\ ( (coeff ` p ) ` (degAA ` A ) ) = 1 ) )

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 369   /\ w3a 958   = wceq 1362   e. wcel 1755   =/= wne 2596   A.wral 2705   E.wrex 2706   E!wreu 2707   _Vcvv 2962   \ cdif 3313   C_ wss 3316   {csn 3865   class class class wbr 4280   X. cxp 4825   Fn wfn 5401   -->wf 5402   ` cfv 5406  (class class class)co 6080   oFcof 6307   CCcc 9268   0cc0 9270   1c1 9271   + caddc 9273   x. cmul 9275   < clt 9406   - cmin 9583   -ucneg 9584   / cdiv 9981   NNcn 10310   NN0cn0 10567   ZZcz 10634   QQcq 10941   0pc0p 20989  Polycply 21537  coeffccoe 21539  degcdgr 21540   AAcaa 21665  deg_AAcdgraa 29342

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-8 1757  ax-9 1759  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414  ax-rep 4391  ax-sep 4401  ax-nul 4409  ax-pow 4458  ax-pr 4519  ax-un 6361  ax-inf2 7835  ax-cnex 9326  ax-resscn 9327  ax-1cn 9328  ax-icn 9329  ax-addcl 9330  ax-addrcl 9331  ax-mulcl 9332  ax-mulrcl 9333  ax-mulcom 9334  ax-addass 9335  ax-mulass 9336  ax-distr 9337  ax-i2m1 9338  ax-1ne0 9339  ax-1rid 9340  ax-rnegex 9341  ax-rrecex 9342  ax-cnre 9343  ax-pre-lttri 9344  ax-pre-lttrn 9345  ax-pre-ltadd 9346  ax-pre-mulgt0 9347  ax-pre-sup 9348  ax-addf 9349

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 959  df-3an 960  df-tru 1365  df-fal 1368  df-ex 1590  df-nf 1593  df-sb 1700  df-eu 2258  df-mo 2259  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ne 2598  df-nel 2599  df-ral 2710  df-rex 2711  df-reu 2712  df-rmo 2713  df-rab 2714  df-v 2964  df-sbc 3176  df-csb 3277  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-pss 3332  df-nul 3626  df-if 3780  df-pw 3850  df-sn 3866  df-pr 3868  df-tp 3870  df-op 3872  df-uni 4080  df-int 4117  df-iun 4161  df-br 4281  df-opab 4339  df-mpt 4340  df-tr 4374  df-eprel 4619  df-id 4623  df-po 4628  df-so 4629  df-fr 4666  df-se 4667  df-we 4668  df-ord 4709  df-on 4710  df-lim 4711  df-suc 4712  df-xp 4833  df-rel 4834  df-cnv 4835  df-co 4836  df-dm 4837  df-rn 4838  df-res 4839  df-ima 4840  df-iota 5369  df-fun 5408  df-fn 5409  df-f 5410  df-f1 5411  df-fo 5412  df-f1o 5413  df-fv 5414  df-isom 5415  df-riota 6039  df-ov 6083  df-oprab 6084  df-mpt2 6085  df-of 6309  df-om 6466  df-1st 6566  df-2nd 6567  df-recs 6818  df-rdg 6852  df-1o 6908  df-oadd 6912  df-er 7089  df-map 7204  df-pm 7205  df-en 7299  df-dom 7300  df-sdom 7301  df-fin 7302  df-sup 7679  df-oi 7712  df-card 8097  df-pnf 9408  df-mnf 9409  df-xr 9410  df-ltxr 9411  df-le 9412  df-sub 9585  df-neg 9586  df-div 9982  df-nn 10311  df-2 10368  df-3 10369  df-n0 10568  df-z 10635  df-uz 10850  df-q 10942  df-rp 10980  df-fz 11425  df-fzo 11533  df-fl 11626  df-mod 11693  df-seq 11791  df-exp 11850  df-hash 12088  df-cj 12572  df-re 12573  df-im 12574  df-sqr 12708  df-abs 12709  df-clim 12950  df-rlim 12951  df-sum 13148  df-0p 20990  df-ply 21541  df-coe 21543  df-dgr 21544  df-aa 21666  df-dgraa 29344

This theorem is referenced by:  mpaalem  29354