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 ( 𝐴 ∈ 𝔸 → ∃! 𝑝 ∈ ( Poly ‘ ℚ ) ( ( deg ‘ 𝑝 ) = ( degAA ‘ 𝐴 ) ∧ ( 𝑝 ‘ 𝐴 ) = 0 ∧ ( ( coeff ‘ 𝑝 ) ‘ ( degAA ‘ 𝐴 ) ) = 1 ) )

Proof

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