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 ⊢ 𝑂 = ( exp ‘ ( ( i · ( 2 · π ) ) / 3 ) )
cos9thpiminplylem4.2 ⊢ 𝑍 = ( 𝑂 ↑𝑐 ( 1 / 3 ) )
cos9thpiminplylem5.3 ⊢ 𝐴 = ( 𝑍 + ( 1 / 𝑍 ) )
cos9thpiminply.q ⊢ 𝑄 = ( ℂfld ↾s ℚ )
cos9thpiminply.4 ⊢ + = ( +g ‘ 𝑃 )
cos9thpiminply.5 ⊢ · = ( .r ‘ 𝑃 )
cos9thpiminply.6 ⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑃 ) )
cos9thpiminply.p ⊢ 𝑃 = ( Poly1 ‘ 𝑄 )
cos9thpiminply.k ⊢ 𝐾 = ( algSc ‘ 𝑃 )
cos9thpiminply.x ⊢ 𝑋 = ( var1 ‘ 𝑄 )
cos9thpiminply.d ⊢ 𝐷 = ( deg1 ‘ 𝑄 )
cos9thpiminply.f ⊢ 𝐹 = ( ( 3 ↑ 𝑋 ) + ( ( ( 𝐾 ‘ - 3 ) · 𝑋 ) + ( 𝐾 ‘ 1 ) ) )
cos9thpiminply.m ⊢ 𝑀 = ( ℂfld minPoly ℚ )
Assertion cos9thpiminply ( 𝐹 = ( 𝑀 ‘ 𝐴 ) ∧ ( 𝐷 ‘ 𝐹 ) = 3 )

Proof

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