Metamath Proof Explorer

Theorem cos9thpiminply

Description: The polynomial ( ( X ^ 3 ) + ( ( -u 3 x. X ) + 1 ) ) is the minimal polynomial for A over QQ , and its degree is 3 . (Contributed by Thierry Arnoux, 14-Nov-2025)

Ref Expression
Hypotheses cos9thpiminplylem3.1 
|- O = ( exp ` ( ( _i x. ( 2 x. _pi ) ) / 3 ) )
cos9thpiminplylem4.2 
|- Z = ( O ^c ( 1 / 3 ) )
cos9thpiminplylem5.3 
|- A = ( Z + ( 1 / Z ) )
cos9thpiminply.q 
|- Q = ( CCfld |`s QQ )
cos9thpiminply.4 
|- .+ = ( +g ` P )
cos9thpiminply.5 
|- .x. = ( .r ` P )
cos9thpiminply.6 
|- .^ = ( .g ` ( mulGrp ` P ) )
cos9thpiminply.p 
|- P = ( Poly1 ` Q )
cos9thpiminply.k 
|- K = ( algSc ` P )
cos9thpiminply.x 
|- X = ( var1 ` Q )
cos9thpiminply.d 
|- D = ( deg1 ` Q )
cos9thpiminply.f 
|- F = ( ( 3 .^ X ) .+ ( ( ( K ` -u 3 ) .x. X ) .+ ( K ` 1 ) ) )
cos9thpiminply.m 
|- M = ( CCfld minPoly QQ )
Assertion cos9thpiminply 
|- ( F = ( M ` A ) /\ ( D ` F ) = 3 )

Proof

Step Hyp Ref Expression
1 cos9thpiminplylem3.1 
 |-  O = ( exp ` ( ( _i x. ( 2 x. _pi ) ) / 3 ) )
2 cos9thpiminplylem4.2 
 |-  Z = ( O ^c ( 1 / 3 ) )
3 cos9thpiminplylem5.3 
 |-  A = ( Z + ( 1 / Z ) )
4 cos9thpiminply.q 
 |-  Q = ( CCfld |`s QQ )
5 cos9thpiminply.4 
 |-  .+ = ( +g ` P )
6 cos9thpiminply.5 
 |-  .x. = ( .r ` P )
7 cos9thpiminply.6 
 |-  .^ = ( .g ` ( mulGrp ` P ) )
8 cos9thpiminply.p 
 |-  P = ( Poly1 ` Q )
9 cos9thpiminply.k 
 |-  K = ( algSc ` P )
10 cos9thpiminply.x 
 |-  X = ( var1 ` Q )
11 cos9thpiminply.d 
 |-  D = ( deg1 ` Q )
12 cos9thpiminply.f 
 |-  F = ( ( 3 .^ X ) .+ ( ( ( K ` -u 3 ) .x. X ) .+ ( K ` 1 ) ) )
13 cos9thpiminply.m 
 |-  M = ( CCfld minPoly QQ )
14 eqid 
 |-  ( CCfld evalSub1 QQ ) = ( CCfld evalSub1 QQ )
15 4 fveq2i 
 |-  ( Poly1 ` Q ) = ( Poly1 ` ( CCfld |`s QQ ) )
16 8 15 eqtri 
 |-  P = ( Poly1 ` ( CCfld |`s QQ ) )
17 cnfldbas 
 |-  CC = ( Base ` CCfld )
18 cnfldfld 
 |-  CCfld e. Field
19 18 a1i 
 |-  ( T. -> CCfld e. Field )
20 cndrng 
 |-  CCfld e. DivRing
21 qsubdrg 
 |-  ( QQ e. ( SubRing ` CCfld ) /\ ( CCfld |`s QQ ) e. DivRing )
22 21 simpli 
 |-  QQ e. ( SubRing ` CCfld )
23 21 simpri 
 |-  ( CCfld |`s QQ ) e. DivRing
24 issdrg 
 |-  ( QQ e. ( SubDRing ` CCfld ) <-> ( CCfld e. DivRing /\ QQ e. ( SubRing ` CCfld ) /\ ( CCfld |`s QQ ) e. DivRing ) )
25 20 22 23 24 mpbir3an 
 |-  QQ e. ( SubDRing ` CCfld )
26 25 a1i 
 |-  ( T. -> QQ e. ( SubDRing ` CCfld ) )
27 ax-icn 
 |-  _i e. CC
28 27 a1i 
 |-  ( T. -> _i e. CC )
29 2cnd 
 |-  ( T. -> 2 e. CC )
30 picn 
 |-  _pi e. CC
31 30 a1i 
 |-  ( T. -> _pi e. CC )
32 29 31 mulcld 
 |-  ( T. -> ( 2 x. _pi ) e. CC )
33 28 32 mulcld 
 |-  ( T. -> ( _i x. ( 2 x. _pi ) ) e. CC )
34 3cn 
 |-  3 e. CC
35 34 a1i 
 |-  ( T. -> 3 e. CC )
36 3ne0 
 |-  3 =/= 0
37 36 a1i 
 |-  ( T. -> 3 =/= 0 )
38 33 35 37 divcld 
 |-  ( T. -> ( ( _i x. ( 2 x. _pi ) ) / 3 ) e. CC )
39 38 efcld 
 |-  ( T. -> ( exp ` ( ( _i x. ( 2 x. _pi ) ) / 3 ) ) e. CC )
40 1 39 eqeltrid 
 |-  ( T. -> O e. CC )
41 35 37 reccld 
 |-  ( T. -> ( 1 / 3 ) e. CC )
42 40 41 cxpcld 
 |-  ( T. -> ( O ^c ( 1 / 3 ) ) e. CC )
43 2 42 eqeltrid 
 |-  ( T. -> Z e. CC )
44 2 a1i 
 |-  ( T. -> Z = ( O ^c ( 1 / 3 ) ) )
45 1 a1i 
 |-  ( T. -> O = ( exp ` ( ( _i x. ( 2 x. _pi ) ) / 3 ) ) )
46 38 efne0d 
 |-  ( T. -> ( exp ` ( ( _i x. ( 2 x. _pi ) ) / 3 ) ) =/= 0 )
47 45 46 eqnetrd 
 |-  ( T. -> O =/= 0 )
48 40 47 41 cxpne0d 
 |-  ( T. -> ( O ^c ( 1 / 3 ) ) =/= 0 )
49 44 48 eqnetrd 
 |-  ( T. -> Z =/= 0 )
50 43 49 reccld 
 |-  ( T. -> ( 1 / Z ) e. CC )
51 43 50 addcld 
 |-  ( T. -> ( Z + ( 1 / Z ) ) e. CC )
52 3 51 eqeltrid 
 |-  ( T. -> A e. CC )
53 cnfld0 
 |-  0 = ( 0g ` CCfld )
54 eqid 
 |-  ( 0g ` P ) = ( 0g ` P )
55 1 2 3 4 5 6 7 8 9 10 11 12 52 cos9thpiminplylem6 
 |-  ( T. -> ( ( ( CCfld evalSub1 QQ ) ` F ) ` A ) = ( ( A ^ 3 ) + ( ( -u 3 x. A ) + 1 ) ) )
56 1 2 3 cos9thpiminplylem5 
 |-  ( ( A ^ 3 ) + ( ( -u 3 x. A ) + 1 ) ) = 0
57 55 56 eqtrdi 
 |-  ( T. -> ( ( ( CCfld evalSub1 QQ ) ` F ) ` A ) = 0 )
58 4 qrng0 
 |-  0 = ( 0g ` Q )
59 eqid 
 |-  ( eval1 ` Q ) = ( eval1 ` Q )
60 eqid 
 |-  ( Base ` P ) = ( Base ` P )
61 4 qfld 
 |-  Q e. Field
62 61 a1i 
 |-  ( T. -> Q e. Field )
63 4 qdrng 
 |-  Q e. DivRing
64 63 a1i 
 |-  ( T. -> Q e. DivRing )
65 64 drngringd 
 |-  ( T. -> Q e. Ring )
66 8 ply1ring 
 |-  ( Q e. Ring -> P e. Ring )
67 65 66 syl 
 |-  ( T. -> P e. Ring )
68 67 ringgrpd 
 |-  ( T. -> P e. Grp )
69 eqid 
 |-  ( mulGrp ` P ) = ( mulGrp ` P )
70 69 60 mgpbas 
 |-  ( Base ` P ) = ( Base ` ( mulGrp ` P ) )
71 69 ringmgp 
 |-  ( P e. Ring -> ( mulGrp ` P ) e. Mnd )
72 67 71 syl 
 |-  ( T. -> ( mulGrp ` P ) e. Mnd )
73 3nn0 
 |-  3 e. NN0
74 73 a1i 
 |-  ( T. -> 3 e. NN0 )
75 10 8 60 vr1cl 
 |-  ( Q e. Ring -> X e. ( Base ` P ) )
76 65 75 syl 
 |-  ( T. -> X e. ( Base ` P ) )
77 70 7 72 74 76 mulgnn0cld 
 |-  ( T. -> ( 3 .^ X ) e. ( Base ` P ) )
78 8 ply1sca 
 |-  ( Q e. DivRing -> Q = ( Scalar ` P ) )
79 63 78 ax-mp 
 |-  Q = ( Scalar ` P )
80 8 ply1lmod 
 |-  ( Q e. Ring -> P e. LMod )
81 65 80 syl 
 |-  ( T. -> P e. LMod )
82 4 qrngbas 
 |-  QQ = ( Base ` Q )
83 9 79 67 81 82 60 asclf 
 |-  ( T. -> K : QQ --> ( Base ` P ) )
84 74 nn0zd 
 |-  ( T. -> 3 e. ZZ )
85 zq 
 |-  ( 3 e. ZZ -> 3 e. QQ )
86 qnegcl 
 |-  ( 3 e. QQ -> -u 3 e. QQ )
87 84 85 86 3syl 
 |-  ( T. -> -u 3 e. QQ )
88 83 87 ffvelcdmd 
 |-  ( T. -> ( K ` -u 3 ) e. ( Base ` P ) )
89 60 6 67 88 76 ringcld 
 |-  ( T. -> ( ( K ` -u 3 ) .x. X ) e. ( Base ` P ) )
90 1zzd 
 |-  ( T. -> 1 e. ZZ )
91 zq 
 |-  ( 1 e. ZZ -> 1 e. QQ )
92 90 91 syl 
 |-  ( T. -> 1 e. QQ )
93 83 92 ffvelcdmd 
 |-  ( T. -> ( K ` 1 ) e. ( Base ` P ) )
94 60 5 68 89 93 grpcld 
 |-  ( T. -> ( ( ( K ` -u 3 ) .x. X ) .+ ( K ` 1 ) ) e. ( Base ` P ) )
95 60 5 68 77 94 grpcld 
 |-  ( T. -> ( ( 3 .^ X ) .+ ( ( ( K ` -u 3 ) .x. X ) .+ ( K ` 1 ) ) ) e. ( Base ` P ) )
96 12 95 eqeltrid 
 |-  ( T. -> F e. ( Base ` P ) )
97 62 fldcrngd 
 |-  ( T. -> Q e. CRing )
98 59 8 60 97 82 96 evl1fvf 
 |-  ( T. -> ( ( eval1 ` Q ) ` F ) : QQ --> QQ )
99 98 ffnd 
 |-  ( T. -> ( ( eval1 ` Q ) ` F ) Fn QQ )
100 fniniseg2 
 |-  ( ( ( eval1 ` Q ) ` F ) Fn QQ -> ( `' ( ( eval1 ` Q ) ` F ) " { 0 } ) = { x e. QQ | ( ( ( eval1 ` Q ) ` F ) ` x ) = 0 } )
101 99 100 syl 
 |-  ( T. -> ( `' ( ( eval1 ` Q ) ` F ) " { 0 } ) = { x e. QQ | ( ( ( eval1 ` Q ) ` F ) ` x ) = 0 } )
102 59 82 evl1fval1 
 |-  ( eval1 ` Q ) = ( Q evalSub1 QQ )
103 102 a1i 
 |-  ( x e. QQ -> ( eval1 ` Q ) = ( Q evalSub1 QQ ) )
104 103 fveq1d 
 |-  ( x e. QQ -> ( ( eval1 ` Q ) ` F ) = ( ( Q evalSub1 QQ ) ` F ) )
105 104 fveq1d 
 |-  ( x e. QQ -> ( ( ( eval1 ` Q ) ` F ) ` x ) = ( ( ( Q evalSub1 QQ ) ` F ) ` x ) )
106 eqid 
 |-  ( Q evalSub1 QQ ) = ( Q evalSub1 QQ )
107 cncrng 
 |-  CCfld e. CRing
108 107 a1i 
 |-  ( x e. QQ -> CCfld e. CRing )
109 22 a1i 
 |-  ( x e. QQ -> QQ e. ( SubRing ` CCfld ) )
110 97 mptru 
 |-  Q e. CRing
111 110 a1i 
 |-  ( x e. QQ -> Q e. CRing )
112 111 crngringd 
 |-  ( x e. QQ -> Q e. Ring )
113 82 subrgid 
 |-  ( Q e. Ring -> QQ e. ( SubRing ` Q ) )
114 112 113 syl 
 |-  ( x e. QQ -> QQ e. ( SubRing ` Q ) )
115 96 mptru 
 |-  F e. ( Base ` P )
116 115 a1i 
 |-  ( x e. QQ -> F e. ( Base ` P ) )
117 4 14 106 8 4 60 108 109 114 116 ressply1evls1 
 |-  ( x e. QQ -> ( ( Q evalSub1 QQ ) ` F ) = ( ( ( CCfld evalSub1 QQ ) ` F ) |` QQ ) )
118 117 fveq1d 
 |-  ( x e. QQ -> ( ( ( Q evalSub1 QQ ) ` F ) ` x ) = ( ( ( ( CCfld evalSub1 QQ ) ` F ) |` QQ ) ` x ) )
119 fvres 
 |-  ( x e. QQ -> ( ( ( ( CCfld evalSub1 QQ ) ` F ) |` QQ ) ` x ) = ( ( ( CCfld evalSub1 QQ ) ` F ) ` x ) )
120 118 119 eqtr2d 
 |-  ( x e. QQ -> ( ( ( CCfld evalSub1 QQ ) ` F ) ` x ) = ( ( ( Q evalSub1 QQ ) ` F ) ` x ) )
121 qcn 
 |-  ( x e. QQ -> x e. CC )
122 1 2 3 4 5 6 7 8 9 10 11 12 121 cos9thpiminplylem6 
 |-  ( x e. QQ -> ( ( ( CCfld evalSub1 QQ ) ` F ) ` x ) = ( ( x ^ 3 ) + ( ( -u 3 x. x ) + 1 ) ) )
123 105 120 122 3eqtr2d 
 |-  ( x e. QQ -> ( ( ( eval1 ` Q ) ` F ) ` x ) = ( ( x ^ 3 ) + ( ( -u 3 x. x ) + 1 ) ) )
124 id 
 |-  ( x e. QQ -> x e. QQ )
125 124 cos9thpiminplylem2 
 |-  ( x e. QQ -> ( ( x ^ 3 ) + ( ( -u 3 x. x ) + 1 ) ) =/= 0 )
126 123 125 eqnetrd 
 |-  ( x e. QQ -> ( ( ( eval1 ` Q ) ` F ) ` x ) =/= 0 )
127 126 neneqd 
 |-  ( x e. QQ -> -. ( ( ( eval1 ` Q ) ` F ) ` x ) = 0 )
128 127 rgen 
 |-  A. x e. QQ -. ( ( ( eval1 ` Q ) ` F ) ` x ) = 0
129 128 a1i 
 |-  ( T. -> A. x e. QQ -. ( ( ( eval1 ` Q ) ` F ) ` x ) = 0 )
130 rabeq0 
 |-  ( { x e. QQ | ( ( ( eval1 ` Q ) ` F ) ` x ) = 0 } = (/) <-> A. x e. QQ -. ( ( ( eval1 ` Q ) ` F ) ` x ) = 0 )
131 129 130 sylibr 
 |-  ( T. -> { x e. QQ | ( ( ( eval1 ` Q ) ` F ) ` x ) = 0 } = (/) )
132 101 131 eqtrd 
 |-  ( T. -> ( `' ( ( eval1 ` Q ) ` F ) " { 0 } ) = (/) )
133 12 a1i 
 |-  ( T. -> F = ( ( 3 .^ X ) .+ ( ( ( K ` -u 3 ) .x. X ) .+ ( K ` 1 ) ) ) )
134 133 fveq2d 
 |-  ( T. -> ( D ` F ) = ( D ` ( ( 3 .^ X ) .+ ( ( ( K ` -u 3 ) .x. X ) .+ ( K ` 1 ) ) ) ) )
135 1lt3 
 |-  1 < 3
136 135 a1i 
 |-  ( T. -> 1 < 3 )
137 0lt1 
 |-  0 < 1
138 137 a1i 
 |-  ( T. -> 0 < 1 )
139 138 gt0ne0d 
 |-  ( T. -> 1 =/= 0 )
140 11 8 82 9 58 deg1scl 
 |-  ( ( Q e. Ring /\ 1 e. QQ /\ 1 =/= 0 ) -> ( D ` ( K ` 1 ) ) = 0 )
141 65 92 139 140 syl3anc 
 |-  ( T. -> ( D ` ( K ` 1 ) ) = 0 )
142 drngdomn 
 |-  ( Q e. DivRing -> Q e. Domn )
143 63 142 mp1i 
 |-  ( T. -> Q e. Domn )
144 35 37 negne0d 
 |-  ( T. -> -u 3 =/= 0 )
145 8 9 58 54 82 ply1scln0 
 |-  ( ( Q e. Ring /\ -u 3 e. QQ /\ -u 3 =/= 0 ) -> ( K ` -u 3 ) =/= ( 0g ` P ) )
146 65 87 144 145 syl3anc 
 |-  ( T. -> ( K ` -u 3 ) =/= ( 0g ` P ) )
147 107 a1i 
 |-  ( T. -> CCfld e. CRing )
148 drngnzr 
 |-  ( CCfld e. DivRing -> CCfld e. NzRing )
149 20 148 mp1i 
 |-  ( T. -> CCfld e. NzRing )
150 22 a1i 
 |-  ( T. -> QQ e. ( SubRing ` CCfld ) )
151 10 54 4 8 147 149 150 vr1nz 
 |-  ( T. -> X =/= ( 0g ` P ) )
152 11 8 60 6 54 143 88 146 76 151 deg1mul 
 |-  ( T. -> ( D ` ( ( K ` -u 3 ) .x. X ) ) = ( ( D ` ( K ` -u 3 ) ) + ( D ` X ) ) )
153 11 8 82 9 58 deg1scl 
 |-  ( ( Q e. Ring /\ -u 3 e. QQ /\ -u 3 =/= 0 ) -> ( D ` ( K ` -u 3 ) ) = 0 )
154 65 87 144 153 syl3anc 
 |-  ( T. -> ( D ` ( K ` -u 3 ) ) = 0 )
155 drngnzr 
 |-  ( Q e. DivRing -> Q e. NzRing )
156 63 155 mp1i 
 |-  ( T. -> Q e. NzRing )
157 11 8 10 156 deg1vr 
 |-  ( T. -> ( D ` X ) = 1 )
158 154 157 oveq12d 
 |-  ( T. -> ( ( D ` ( K ` -u 3 ) ) + ( D ` X ) ) = ( 0 + 1 ) )
159 1cnd 
 |-  ( T. -> 1 e. CC )
160 159 addlidd 
 |-  ( T. -> ( 0 + 1 ) = 1 )
161 152 158 160 3eqtrd 
 |-  ( T. -> ( D ` ( ( K ` -u 3 ) .x. X ) ) = 1 )
162 138 141 161 3brtr4d 
 |-  ( T. -> ( D ` ( K ` 1 ) ) < ( D ` ( ( K ` -u 3 ) .x. X ) ) )
163 8 11 65 60 5 89 93 162 deg1add 
 |-  ( T. -> ( D ` ( ( ( K ` -u 3 ) .x. X ) .+ ( K ` 1 ) ) ) = ( D ` ( ( K ` -u 3 ) .x. X ) ) )
164 163 161 eqtrd 
 |-  ( T. -> ( D ` ( ( ( K ` -u 3 ) .x. X ) .+ ( K ` 1 ) ) ) = 1 )
165 11 8 10 69 7 deg1pw 
 |-  ( ( Q e. NzRing /\ 3 e. NN0 ) -> ( D ` ( 3 .^ X ) ) = 3 )
166 156 74 165 syl2anc 
 |-  ( T. -> ( D ` ( 3 .^ X ) ) = 3 )
167 136 164 166 3brtr4d 
 |-  ( T. -> ( D ` ( ( ( K ` -u 3 ) .x. X ) .+ ( K ` 1 ) ) ) < ( D ` ( 3 .^ X ) ) )
168 8 11 65 60 5 77 94 167 deg1add 
 |-  ( T. -> ( D ` ( ( 3 .^ X ) .+ ( ( ( K ` -u 3 ) .x. X ) .+ ( K ` 1 ) ) ) ) = ( D ` ( 3 .^ X ) ) )
169 134 168 166 3eqtrd 
 |-  ( T. -> ( D ` F ) = 3 )
170 58 59 11 8 60 62 96 132 169 ply1dg3rt0irred 
 |-  ( T. -> F e. ( Irred ` P ) )
171 eqid 
 |-  ( Irred ` P ) = ( Irred ` P )
172 171 54 irredn0 
 |-  ( ( P e. Ring /\ F e. ( Irred ` P ) ) -> F =/= ( 0g ` P ) )
173 67 170 172 syl2anc 
 |-  ( T. -> F =/= ( 0g ` P ) )
174 169 fveq2d 
 |-  ( T. -> ( ( coe1 ` F ) ` ( D ` F ) ) = ( ( coe1 ` F ) ` 3 ) )
175 133 fveq2d 
 |-  ( T. -> ( coe1 ` F ) = ( coe1 ` ( ( 3 .^ X ) .+ ( ( ( K ` -u 3 ) .x. X ) .+ ( K ` 1 ) ) ) ) )
176 175 fveq1d 
 |-  ( T. -> ( ( coe1 ` F ) ` 3 ) = ( ( coe1 ` ( ( 3 .^ X ) .+ ( ( ( K ` -u 3 ) .x. X ) .+ ( K ` 1 ) ) ) ) ` 3 ) )
177 cnfldadd 
 |-  + = ( +g ` CCfld )
178 4 177 ressplusg 
 |-  ( QQ e. ( SubRing ` CCfld ) -> + = ( +g ` Q ) )
179 22 178 ax-mp 
 |-  + = ( +g ` Q )
180 8 60 5 179 coe1addfv 
 |-  ( ( ( Q e. Ring /\ ( 3 .^ X ) e. ( Base ` P ) /\ ( ( ( K ` -u 3 ) .x. X ) .+ ( K ` 1 ) ) e. ( Base ` P ) ) /\ 3 e. NN0 ) -> ( ( coe1 ` ( ( 3 .^ X ) .+ ( ( ( K ` -u 3 ) .x. X ) .+ ( K ` 1 ) ) ) ) ` 3 ) = ( ( ( coe1 ` ( 3 .^ X ) ) ` 3 ) + ( ( coe1 ` ( ( ( K ` -u 3 ) .x. X ) .+ ( K ` 1 ) ) ) ` 3 ) ) )
181 65 77 94 74 180 syl31anc 
 |-  ( T. -> ( ( coe1 ` ( ( 3 .^ X ) .+ ( ( ( K ` -u 3 ) .x. X ) .+ ( K ` 1 ) ) ) ) ` 3 ) = ( ( ( coe1 ` ( 3 .^ X ) ) ` 3 ) + ( ( coe1 ` ( ( ( K ` -u 3 ) .x. X ) .+ ( K ` 1 ) ) ) ` 3 ) ) )
182 iftrue 
 |-  ( i = 3 -> if ( i = 3 , 1 , 0 ) = 1 )
183 4 qrng1 
 |-  1 = ( 1r ` Q )
184 8 10 7 65 74 58 183 coe1mon 
 |-  ( T. -> ( coe1 ` ( 3 .^ X ) ) = ( i e. NN0 |-> if ( i = 3 , 1 , 0 ) ) )
185 182 184 74 159 fvmptd4 
 |-  ( T. -> ( ( coe1 ` ( 3 .^ X ) ) ` 3 ) = 1 )
186 8 60 5 179 coe1addfv 
 |-  ( ( ( Q e. Ring /\ ( ( K ` -u 3 ) .x. X ) e. ( Base ` P ) /\ ( K ` 1 ) e. ( Base ` P ) ) /\ 3 e. NN0 ) -> ( ( coe1 ` ( ( ( K ` -u 3 ) .x. X ) .+ ( K ` 1 ) ) ) ` 3 ) = ( ( ( coe1 ` ( ( K ` -u 3 ) .x. X ) ) ` 3 ) + ( ( coe1 ` ( K ` 1 ) ) ` 3 ) ) )
187 65 89 93 74 186 syl31anc 
 |-  ( T. -> ( ( coe1 ` ( ( ( K ` -u 3 ) .x. X ) .+ ( K ` 1 ) ) ) ` 3 ) = ( ( ( coe1 ` ( ( K ` -u 3 ) .x. X ) ) ` 3 ) + ( ( coe1 ` ( K ` 1 ) ) ` 3 ) ) )
188 8 ply1assa 
 |-  ( Q e. CRing -> P e. AssAlg )
189 97 188 syl 
 |-  ( T. -> P e. AssAlg )
190 eqid 
 |-  ( .s ` P ) = ( .s ` P )
191 9 79 82 60 6 190 asclmul1 
 |-  ( ( P e. AssAlg /\ -u 3 e. QQ /\ X e. ( Base ` P ) ) -> ( ( K ` -u 3 ) .x. X ) = ( -u 3 ( .s ` P ) X ) )
192 189 87 76 191 syl3anc 
 |-  ( T. -> ( ( K ` -u 3 ) .x. X ) = ( -u 3 ( .s ` P ) X ) )
193 70 7 mulg1 
 |-  ( X e. ( Base ` P ) -> ( 1 .^ X ) = X )
194 76 193 syl 
 |-  ( T. -> ( 1 .^ X ) = X )
195 194 oveq2d 
 |-  ( T. -> ( -u 3 ( .s ` P ) ( 1 .^ X ) ) = ( -u 3 ( .s ` P ) X ) )
196 192 195 eqtr4d 
 |-  ( T. -> ( ( K ` -u 3 ) .x. X ) = ( -u 3 ( .s ` P ) ( 1 .^ X ) ) )
197 196 fveq2d 
 |-  ( T. -> ( coe1 ` ( ( K ` -u 3 ) .x. X ) ) = ( coe1 ` ( -u 3 ( .s ` P ) ( 1 .^ X ) ) ) )
198 197 fveq1d 
 |-  ( T. -> ( ( coe1 ` ( ( K ` -u 3 ) .x. X ) ) ` 3 ) = ( ( coe1 ` ( -u 3 ( .s ` P ) ( 1 .^ X ) ) ) ` 3 ) )
199 1nn0 
 |-  1 e. NN0
200 199 a1i 
 |-  ( T. -> 1 e. NN0 )
201 1red 
 |-  ( T. -> 1 e. RR )
202 201 136 ltned 
 |-  ( T. -> 1 =/= 3 )
203 58 82 8 10 190 69 7 65 87 200 74 202 coe1tmfv2 
 |-  ( T. -> ( ( coe1 ` ( -u 3 ( .s ` P ) ( 1 .^ X ) ) ) ` 3 ) = 0 )
204 198 203 eqtrd 
 |-  ( T. -> ( ( coe1 ` ( ( K ` -u 3 ) .x. X ) ) ` 3 ) = 0 )
205 8 9 82 58 coe1scl 
 |-  ( ( Q e. Ring /\ 1 e. QQ ) -> ( coe1 ` ( K ` 1 ) ) = ( i e. NN0 |-> if ( i = 0 , 1 , 0 ) ) )
206 65 92 205 syl2anc 
 |-  ( T. -> ( coe1 ` ( K ` 1 ) ) = ( i e. NN0 |-> if ( i = 0 , 1 , 0 ) ) )
207 simpr 
 |-  ( ( T. /\ i = 3 ) -> i = 3 )
208 36 a1i 
 |-  ( ( T. /\ i = 3 ) -> 3 =/= 0 )
209 207 208 eqnetrd 
 |-  ( ( T. /\ i = 3 ) -> i =/= 0 )
210 209 neneqd 
 |-  ( ( T. /\ i = 3 ) -> -. i = 0 )
211 210 iffalsed 
 |-  ( ( T. /\ i = 3 ) -> if ( i = 0 , 1 , 0 ) = 0 )
212 0zd 
 |-  ( T. -> 0 e. ZZ )
213 206 211 74 212 fvmptd 
 |-  ( T. -> ( ( coe1 ` ( K ` 1 ) ) ` 3 ) = 0 )
214 204 213 oveq12d 
 |-  ( T. -> ( ( ( coe1 ` ( ( K ` -u 3 ) .x. X ) ) ` 3 ) + ( ( coe1 ` ( K ` 1 ) ) ` 3 ) ) = ( 0 + 0 ) )
215 00id 
 |-  ( 0 + 0 ) = 0
216 215 a1i 
 |-  ( T. -> ( 0 + 0 ) = 0 )
217 187 214 216 3eqtrd 
 |-  ( T. -> ( ( coe1 ` ( ( ( K ` -u 3 ) .x. X ) .+ ( K ` 1 ) ) ) ` 3 ) = 0 )
218 185 217 oveq12d 
 |-  ( T. -> ( ( ( coe1 ` ( 3 .^ X ) ) ` 3 ) + ( ( coe1 ` ( ( ( K ` -u 3 ) .x. X ) .+ ( K ` 1 ) ) ) ` 3 ) ) = ( 1 + 0 ) )
219 159 addridd 
 |-  ( T. -> ( 1 + 0 ) = 1 )
220 218 219 eqtrd 
 |-  ( T. -> ( ( ( coe1 ` ( 3 .^ X ) ) ` 3 ) + ( ( coe1 ` ( ( ( K ` -u 3 ) .x. X ) .+ ( K ` 1 ) ) ) ` 3 ) ) = 1 )
221 176 181 220 3eqtrd 
 |-  ( T. -> ( ( coe1 ` F ) ` 3 ) = 1 )
222 174 221 eqtrd 
 |-  ( T. -> ( ( coe1 ` F ) ` ( D ` F ) ) = 1 )
223 4 fveq2i 
 |-  ( Monic1p ` Q ) = ( Monic1p ` ( CCfld |`s QQ ) )
224 223 eqcomi 
 |-  ( Monic1p ` ( CCfld |`s QQ ) ) = ( Monic1p ` Q )
225 8 60 54 11 224 183 ismon1p 
 |-  ( F e. ( Monic1p ` ( CCfld |`s QQ ) ) <-> ( F e. ( Base ` P ) /\ F =/= ( 0g ` P ) /\ ( ( coe1 ` F ) ` ( D ` F ) ) = 1 ) )
226 96 173 222 225 syl3anbrc 
 |-  ( T. -> F e. ( Monic1p ` ( CCfld |`s QQ ) ) )
227 14 16 17 19 26 52 53 13 54 57 170 226 irredminply 
 |-  ( T. -> F = ( M ` A ) )
228 227 169 jca 
 |-  ( T. -> ( F = ( M ` A ) /\ ( D ` F ) = 3 ) )
229 228 mptru 
 |-  ( F = ( M ` A ) /\ ( D ` F ) = 3 )