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∈𝔸→∃!p∈Poly⁡ℚdeg⁡p=deg𝔸⁡A∧p⁡A=0∧coeff⁡p⁡deg𝔸⁡A=1

Proof

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