Metamath Proof Explorer

Theorem 2sqr3minply

Description: The polynomial ( ( X ^ 3 ) - 2 ) is the minimal polynomial for ( 2 ^c ( 1 / 3 ) ) over QQ , and its degree is 3 . (Contributed by Thierry Arnoux, 14-Jun-2025)

Ref Expression
Hypotheses 2sqr3minply.q ⊢ 𝑄 = ( ℂfld ↾s ℚ )
2sqr3minply.1 ⊢ − = ( -g ‘ 𝑃 )
2sqr3minply.2 ⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑃 ) )
2sqr3minply.p ⊢ 𝑃 = ( Poly1 ‘ 𝑄 )
2sqr3minply.k ⊢ 𝐾 = ( algSc ‘ 𝑃 )
2sqr3minply.x ⊢ 𝑋 = ( var1 ‘ 𝑄 )
2sqr3minply.d ⊢ 𝐷 = ( deg1 ‘ 𝑄 )
2sqr3minply.f ⊢ 𝐹 = ( ( 3 ↑ 𝑋 ) − ( 𝐾 ‘ 2 ) )
2sqr3minply.a ⊢ 𝐴 = ( 2 ↑𝑐 ( 1 / 3 ) )
2sqr3minply.m ⊢ 𝑀 = ( ℂfld minPoly ℚ )
Assertion 2sqr3minply ( 𝐹 = ( 𝑀 ‘ 𝐴 ) ∧ ( 𝐷 ‘ 𝐹 ) = 3 )

Proof

Step Hyp Ref Expression
1 2sqr3minply.q ⊢ 𝑄 = ( ℂfld ↾s ℚ )
2 2sqr3minply.1 ⊢ − = ( -g ‘ 𝑃 )
3 2sqr3minply.2 ⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑃 ) )
4 2sqr3minply.p ⊢ 𝑃 = ( Poly1 ‘ 𝑄 )
5 2sqr3minply.k ⊢ 𝐾 = ( algSc ‘ 𝑃 )
6 2sqr3minply.x ⊢ 𝑋 = ( var1 ‘ 𝑄 )
7 2sqr3minply.d ⊢ 𝐷 = ( deg1 ‘ 𝑄 )
8 2sqr3minply.f ⊢ 𝐹 = ( ( 3 ↑ 𝑋 ) − ( 𝐾 ‘ 2 ) )
9 2sqr3minply.a ⊢ 𝐴 = ( 2 ↑𝑐 ( 1 / 3 ) )
10 2sqr3minply.m ⊢ 𝑀 = ( ℂfld minPoly ℚ )
11 eqid ⊢ ( ℂfld evalSub1 ℚ ) = ( ℂfld evalSub1 ℚ )
12 1 fveq2i ⊢ ( Poly1 ‘ 𝑄 ) = ( Poly1 ‘ ( ℂfld ↾s ℚ ) )
13 4 12 eqtri ⊢ 𝑃 = ( Poly1 ‘ ( ℂfld ↾s ℚ ) )
14 cnfldbas ⊢ ℂ = ( Base ‘ ℂfld )
15 cndrng ⊢ ℂfld ∈ DivRing
16 cncrng ⊢ ℂfld ∈ CRing
17 isfld ⊢ ( ℂfld ∈ Field ↔ ( ℂfld ∈ DivRing ∧ ℂfld ∈ CRing ) )
18 15 16 17 mpbir2an ⊢ ℂfld ∈ Field
19 18 a1i ⊢ ( ⊤ → ℂfld ∈ Field )
20 qsubdrg ⊢ ( ℚ ∈ ( SubRing ‘ ℂfld ) ∧ ( ℂfld ↾s ℚ ) ∈ DivRing )
21 20 simpli ⊢ ℚ ∈ ( SubRing ‘ ℂfld )
22 20 simpri ⊢ ( ℂfld ↾s ℚ ) ∈ DivRing
23 issdrg ⊢ ( ℚ ∈ ( SubDRing ‘ ℂfld ) ↔ ( ℂfld ∈ DivRing ∧ ℚ ∈ ( SubRing ‘ ℂfld ) ∧ ( ℂfld ↾s ℚ ) ∈ DivRing ) )
24 15 21 22 23 mpbir3an ⊢ ℚ ∈ ( SubDRing ‘ ℂfld )
25 24 a1i ⊢ ( ⊤ → ℚ ∈ ( SubDRing ‘ ℂfld ) )
26 2cn ⊢ 2 ∈ ℂ
27 3cn ⊢ 3 ∈ ℂ
28 3ne0 ⊢ 3 ≠ 0
29 27 28 reccli ⊢ ( 1 / 3 ) ∈ ℂ
30 cxpcl ⊢ ( ( 2 ∈ ℂ ∧ ( 1 / 3 ) ∈ ℂ ) → ( 2 ↑𝑐 ( 1 / 3 ) ) ∈ ℂ )
31 26 29 30 mp2an ⊢ ( 2 ↑𝑐 ( 1 / 3 ) ) ∈ ℂ
32 9 31 eqeltri ⊢ 𝐴 ∈ ℂ
33 32 a1i ⊢ ( ⊤ → 𝐴 ∈ ℂ )
34 cnfld0 ⊢ 0 = ( 0g ‘ ℂfld )
35 eqid ⊢ ( 0g ‘ 𝑃 ) = ( 0g ‘ 𝑃 )
36 8 fveq2i ⊢ ( ( ℂfld evalSub1 ℚ ) ‘ 𝐹 ) = ( ( ℂfld evalSub1 ℚ ) ‘ ( ( 3 ↑ 𝑋 ) − ( 𝐾 ‘ 2 ) ) )
37 36 fveq1i ⊢ ( ( ( ℂfld evalSub1 ℚ ) ‘ 𝐹 ) ‘ 𝐴 ) = ( ( ( ℂfld evalSub1 ℚ ) ‘ ( ( 3 ↑ 𝑋 ) − ( 𝐾 ‘ 2 ) ) ) ‘ 𝐴 )
38 37 a1i ⊢ ( ⊤ → ( ( ( ℂfld evalSub1 ℚ ) ‘ 𝐹 ) ‘ 𝐴 ) = ( ( ( ℂfld evalSub1 ℚ ) ‘ ( ( 3 ↑ 𝑋 ) − ( 𝐾 ‘ 2 ) ) ) ‘ 𝐴 ) )
39 eqid ⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
40 cnfldsub ⊢ − = ( -g ‘ ℂfld )
41 16 a1i ⊢ ( ⊤ → ℂfld ∈ CRing )
42 21 a1i ⊢ ( ⊤ → ℚ ∈ ( SubRing ‘ ℂfld ) )
43 eqid ⊢ ( mulGrp ‘ 𝑃 ) = ( mulGrp ‘ 𝑃 )
44 43 39 mgpbas ⊢ ( Base ‘ 𝑃 ) = ( Base ‘ ( mulGrp ‘ 𝑃 ) )
45 1 qdrng ⊢ 𝑄 ∈ DivRing
46 45 a1i ⊢ ( ⊤ → 𝑄 ∈ DivRing )
47 46 drngringd ⊢ ( ⊤ → 𝑄 ∈ Ring )
48 4 ply1ring ⊢ ( 𝑄 ∈ Ring → 𝑃 ∈ Ring )
49 47 48 syl ⊢ ( ⊤ → 𝑃 ∈ Ring )
50 43 ringmgp ⊢ ( 𝑃 ∈ Ring → ( mulGrp ‘ 𝑃 ) ∈ Mnd )
51 49 50 syl ⊢ ( ⊤ → ( mulGrp ‘ 𝑃 ) ∈ Mnd )
52 3nn0 ⊢ 3 ∈ ℕ0
53 52 a1i ⊢ ( ⊤ → 3 ∈ ℕ0 )
54 6 4 39 vr1cl ⊢ ( 𝑄 ∈ Ring → 𝑋 ∈ ( Base ‘ 𝑃 ) )
55 47 54 syl ⊢ ( ⊤ → 𝑋 ∈ ( Base ‘ 𝑃 ) )
56 44 3 51 53 55 mulgnn0cld ⊢ ( ⊤ → ( 3 ↑ 𝑋 ) ∈ ( Base ‘ 𝑃 ) )
57 47 mptru ⊢ 𝑄 ∈ Ring
58 4 ply1sca ⊢ ( 𝑄 ∈ Ring → 𝑄 = ( Scalar ‘ 𝑃 ) )
59 57 58 ax-mp ⊢ 𝑄 = ( Scalar ‘ 𝑃 )
60 4 ply1lmod ⊢ ( 𝑄 ∈ Ring → 𝑃 ∈ LMod )
61 47 60 syl ⊢ ( ⊤ → 𝑃 ∈ LMod )
62 1 qrngbas ⊢ ℚ = ( Base ‘ 𝑄 )
63 5 59 49 61 62 39 asclf ⊢ ( ⊤ → 𝐾 : ℚ ⟶ ( Base ‘ 𝑃 ) )
64 2z ⊢ 2 ∈ ℤ
65 zq ⊢ ( 2 ∈ ℤ → 2 ∈ ℚ )
66 64 65 mp1i ⊢ ( ⊤ → 2 ∈ ℚ )
67 63 66 ffvelcdmd ⊢ ( ⊤ → ( 𝐾 ‘ 2 ) ∈ ( Base ‘ 𝑃 ) )
68 11 14 4 1 39 2 40 41 42 56 67 33 evls1subd ⊢ ( ⊤ → ( ( ( ℂfld evalSub1 ℚ ) ‘ ( ( 3 ↑ 𝑋 ) − ( 𝐾 ‘ 2 ) ) ) ‘ 𝐴 ) = ( ( ( ( ℂfld evalSub1 ℚ ) ‘ ( 3 ↑ 𝑋 ) ) ‘ 𝐴 ) − ( ( ( ℂfld evalSub1 ℚ ) ‘ ( 𝐾 ‘ 2 ) ) ‘ 𝐴 ) ) )
69 eqid ⊢ ( .g ‘ ( mulGrp ‘ ℂfld ) ) = ( .g ‘ ( mulGrp ‘ ℂfld ) )
70 11 14 4 1 39 41 42 3 69 53 55 33 evls1expd ⊢ ( ⊤ → ( ( ( ℂfld evalSub1 ℚ ) ‘ ( 3 ↑ 𝑋 ) ) ‘ 𝐴 ) = ( 3 ( .g ‘ ( mulGrp ‘ ℂfld ) ) ( ( ( ℂfld evalSub1 ℚ ) ‘ 𝑋 ) ‘ 𝐴 ) ) )
71 11 6 1 14 41 42 evls1var ⊢ ( ⊤ → ( ( ℂfld evalSub1 ℚ ) ‘ 𝑋 ) = ( I ↾ ℂ ) )
72 71 fveq1d ⊢ ( ⊤ → ( ( ( ℂfld evalSub1 ℚ ) ‘ 𝑋 ) ‘ 𝐴 ) = ( ( I ↾ ℂ ) ‘ 𝐴 ) )
73 fvresi ⊢ ( 𝐴 ∈ ℂ → ( ( I ↾ ℂ ) ‘ 𝐴 ) = 𝐴 )
74 32 73 mp1i ⊢ ( ⊤ → ( ( I ↾ ℂ ) ‘ 𝐴 ) = 𝐴 )
75 72 74 eqtrd ⊢ ( ⊤ → ( ( ( ℂfld evalSub1 ℚ ) ‘ 𝑋 ) ‘ 𝐴 ) = 𝐴 )
76 75 oveq2d ⊢ ( ⊤ → ( 3 ( .g ‘ ( mulGrp ‘ ℂfld ) ) ( ( ( ℂfld evalSub1 ℚ ) ‘ 𝑋 ) ‘ 𝐴 ) ) = ( 3 ( .g ‘ ( mulGrp ‘ ℂfld ) ) 𝐴 ) )
77 cnfldexp ⊢ ( ( 𝐴 ∈ ℂ ∧ 3 ∈ ℕ0 ) → ( 3 ( .g ‘ ( mulGrp ‘ ℂfld ) ) 𝐴 ) = ( 𝐴 ↑ 3 ) )
78 33 53 77 syl2anc ⊢ ( ⊤ → ( 3 ( .g ‘ ( mulGrp ‘ ℂfld ) ) 𝐴 ) = ( 𝐴 ↑ 3 ) )
79 70 76 78 3eqtrd ⊢ ( ⊤ → ( ( ( ℂfld evalSub1 ℚ ) ‘ ( 3 ↑ 𝑋 ) ) ‘ 𝐴 ) = ( 𝐴 ↑ 3 ) )
80 9 oveq1i ⊢ ( 𝐴 ↑ 3 ) = ( ( 2 ↑𝑐 ( 1 / 3 ) ) ↑ 3 )
81 3nn ⊢ 3 ∈ ℕ
82 cxproot ⊢ ( ( 2 ∈ ℂ ∧ 3 ∈ ℕ ) → ( ( 2 ↑𝑐 ( 1 / 3 ) ) ↑ 3 ) = 2 )
83 26 81 82 mp2an ⊢ ( ( 2 ↑𝑐 ( 1 / 3 ) ) ↑ 3 ) = 2
84 80 83 eqtri ⊢ ( 𝐴 ↑ 3 ) = 2
85 79 84 eqtrdi ⊢ ( ⊤ → ( ( ( ℂfld evalSub1 ℚ ) ‘ ( 3 ↑ 𝑋 ) ) ‘ 𝐴 ) = 2 )
86 11 4 1 14 5 41 42 66 33 evls1scafv ⊢ ( ⊤ → ( ( ( ℂfld evalSub1 ℚ ) ‘ ( 𝐾 ‘ 2 ) ) ‘ 𝐴 ) = 2 )
87 85 86 oveq12d ⊢ ( ⊤ → ( ( ( ( ℂfld evalSub1 ℚ ) ‘ ( 3 ↑ 𝑋 ) ) ‘ 𝐴 ) − ( ( ( ℂfld evalSub1 ℚ ) ‘ ( 𝐾 ‘ 2 ) ) ‘ 𝐴 ) ) = ( 2 − 2 ) )
88 26 subidi ⊢ ( 2 − 2 ) = 0
89 87 88 eqtrdi ⊢ ( ⊤ → ( ( ( ( ℂfld evalSub1 ℚ ) ‘ ( 3 ↑ 𝑋 ) ) ‘ 𝐴 ) − ( ( ( ℂfld evalSub1 ℚ ) ‘ ( 𝐾 ‘ 2 ) ) ‘ 𝐴 ) ) = 0 )
90 38 68 89 3eqtrd ⊢ ( ⊤ → ( ( ( ℂfld evalSub1 ℚ ) ‘ 𝐹 ) ‘ 𝐴 ) = 0 )
91 1 qrng0 ⊢ 0 = ( 0g ‘ 𝑄 )
92 eqid ⊢ ( eval1 ‘ 𝑄 ) = ( eval1 ‘ 𝑄 )
93 fldsdrgfld ⊢ ( ( ℂfld ∈ Field ∧ ℚ ∈ ( SubDRing ‘ ℂfld ) ) → ( ℂfld ↾s ℚ ) ∈ Field )
94 18 24 93 mp2an ⊢ ( ℂfld ↾s ℚ ) ∈ Field
95 1 94 eqeltri ⊢ 𝑄 ∈ Field
96 95 a1i ⊢ ( ⊤ → 𝑄 ∈ Field )
97 49 ringgrpd ⊢ ( ⊤ → 𝑃 ∈ Grp )
98 39 2 grpsubcl ⊢ ( ( 𝑃 ∈ Grp ∧ ( 3 ↑ 𝑋 ) ∈ ( Base ‘ 𝑃 ) ∧ ( 𝐾 ‘ 2 ) ∈ ( Base ‘ 𝑃 ) ) → ( ( 3 ↑ 𝑋 ) − ( 𝐾 ‘ 2 ) ) ∈ ( Base ‘ 𝑃 ) )
99 97 56 67 98 syl3anc ⊢ ( ⊤ → ( ( 3 ↑ 𝑋 ) − ( 𝐾 ‘ 2 ) ) ∈ ( Base ‘ 𝑃 ) )
100 8 99 eqeltrid ⊢ ( ⊤ → 𝐹 ∈ ( Base ‘ 𝑃 ) )
101 96 fldcrngd ⊢ ( ⊤ → 𝑄 ∈ CRing )
102 92 4 39 101 62 100 evl1fvf ⊢ ( ⊤ → ( ( eval1 ‘ 𝑄 ) ‘ 𝐹 ) : ℚ ⟶ ℚ )
103 102 ffnd ⊢ ( ⊤ → ( ( eval1 ‘ 𝑄 ) ‘ 𝐹 ) Fn ℚ )
104 fniniseg2 ⊢ ( ( ( eval1 ‘ 𝑄 ) ‘ 𝐹 ) Fn ℚ → ( ◡ ( ( eval1 ‘ 𝑄 ) ‘ 𝐹 ) “ { 0 } ) = { 𝑥 ∈ ℚ ∣ ( ( ( eval1 ‘ 𝑄 ) ‘ 𝐹 ) ‘ 𝑥 ) = 0 } )
105 103 104 syl ⊢ ( ⊤ → ( ◡ ( ( eval1 ‘ 𝑄 ) ‘ 𝐹 ) “ { 0 } ) = { 𝑥 ∈ ℚ ∣ ( ( ( eval1 ‘ 𝑄 ) ‘ 𝐹 ) ‘ 𝑥 ) = 0 } )
106 cnfldmul ⊢ · = ( .r ‘ ℂfld )
107 1 106 ressmulr ⊢ ( ℚ ∈ ( SubRing ‘ ℂfld ) → · = ( .r ‘ 𝑄 ) )
108 21 107 ax-mp ⊢ · = ( .r ‘ 𝑄 )
109 cnfldadd ⊢ + = ( +g ‘ ℂfld )
110 1 109 ressplusg ⊢ ( ℚ ∈ ( SubRing ‘ ℂfld ) → + = ( +g ‘ 𝑄 ) )
111 21 110 ax-mp ⊢ + = ( +g ‘ 𝑄 )
112 eqid ⊢ ( .g ‘ ( mulGrp ‘ 𝑄 ) ) = ( .g ‘ ( mulGrp ‘ 𝑄 ) )
113 eqid ⊢ ( coe1 ‘ 𝐹 ) = ( coe1 ‘ 𝐹 )
114 8 fveq2i ⊢ ( coe1 ‘ 𝐹 ) = ( coe1 ‘ ( ( 3 ↑ 𝑋 ) − ( 𝐾 ‘ 2 ) ) )
115 114 a1i ⊢ ( ⊤ → ( coe1 ‘ 𝐹 ) = ( coe1 ‘ ( ( 3 ↑ 𝑋 ) − ( 𝐾 ‘ 2 ) ) ) )
116 8 fveq2i ⊢ ( 𝐷 ‘ 𝐹 ) = ( 𝐷 ‘ ( ( 3 ↑ 𝑋 ) − ( 𝐾 ‘ 2 ) ) )
117 116 a1i ⊢ ( ⊤ → ( 𝐷 ‘ 𝐹 ) = ( 𝐷 ‘ ( ( 3 ↑ 𝑋 ) − ( 𝐾 ‘ 2 ) ) ) )
118 3pos ⊢ 0 < 3
119 118 a1i ⊢ ( ⊤ → 0 < 3 )
120 2ne0 ⊢ 2 ≠ 0
121 120 a1i ⊢ ( ⊤ → 2 ≠ 0 )
122 7 4 62 5 91 deg1scl ⊢ ( ( 𝑄 ∈ Ring ∧ 2 ∈ ℚ ∧ 2 ≠ 0 ) → ( 𝐷 ‘ ( 𝐾 ‘ 2 ) ) = 0 )
123 47 66 121 122 syl3anc ⊢ ( ⊤ → ( 𝐷 ‘ ( 𝐾 ‘ 2 ) ) = 0 )
124 drngnzr ⊢ ( 𝑄 ∈ DivRing → 𝑄 ∈ NzRing )
125 45 124 mp1i ⊢ ( ⊤ → 𝑄 ∈ NzRing )
126 7 4 6 43 3 deg1pw ⊢ ( ( 𝑄 ∈ NzRing ∧ 3 ∈ ℕ0 ) → ( 𝐷 ‘ ( 3 ↑ 𝑋 ) ) = 3 )
127 125 53 126 syl2anc ⊢ ( ⊤ → ( 𝐷 ‘ ( 3 ↑ 𝑋 ) ) = 3 )
128 119 123 127 3brtr4d ⊢ ( ⊤ → ( 𝐷 ‘ ( 𝐾 ‘ 2 ) ) < ( 𝐷 ‘ ( 3 ↑ 𝑋 ) ) )
129 4 7 47 39 2 56 67 128 deg1sub ⊢ ( ⊤ → ( 𝐷 ‘ ( ( 3 ↑ 𝑋 ) − ( 𝐾 ‘ 2 ) ) ) = ( 𝐷 ‘ ( 3 ↑ 𝑋 ) ) )
130 117 129 127 3eqtrd ⊢ ( ⊤ → ( 𝐷 ‘ 𝐹 ) = 3 )
131 115 130 fveq12d ⊢ ( ⊤ → ( ( coe1 ‘ 𝐹 ) ‘ ( 𝐷 ‘ 𝐹 ) ) = ( ( coe1 ‘ ( ( 3 ↑ 𝑋 ) − ( 𝐾 ‘ 2 ) ) ) ‘ 3 ) )
132 eqid ⊢ ( -g ‘ 𝑄 ) = ( -g ‘ 𝑄 )
133 4 39 2 132 coe1subfv ⊢ ( ( ( 𝑄 ∈ Ring ∧ ( 3 ↑ 𝑋 ) ∈ ( Base ‘ 𝑃 ) ∧ ( 𝐾 ‘ 2 ) ∈ ( Base ‘ 𝑃 ) ) ∧ 3 ∈ ℕ0 ) → ( ( coe1 ‘ ( ( 3 ↑ 𝑋 ) − ( 𝐾 ‘ 2 ) ) ) ‘ 3 ) = ( ( ( coe1 ‘ ( 3 ↑ 𝑋 ) ) ‘ 3 ) ( -g ‘ 𝑄 ) ( ( coe1 ‘ ( 𝐾 ‘ 2 ) ) ‘ 3 ) ) )
134 47 56 67 53 133 syl31anc ⊢ ( ⊤ → ( ( coe1 ‘ ( ( 3 ↑ 𝑋 ) − ( 𝐾 ‘ 2 ) ) ) ‘ 3 ) = ( ( ( coe1 ‘ ( 3 ↑ 𝑋 ) ) ‘ 3 ) ( -g ‘ 𝑄 ) ( ( coe1 ‘ ( 𝐾 ‘ 2 ) ) ‘ 3 ) ) )
135 subrgsubg ⊢ ( ℚ ∈ ( SubRing ‘ ℂfld ) → ℚ ∈ ( SubGrp ‘ ℂfld ) )
136 21 135 mp1i ⊢ ( ⊤ → ℚ ∈ ( SubGrp ‘ ℂfld ) )
137 eqid ⊢ ( coe1 ‘ ( 3 ↑ 𝑋 ) ) = ( coe1 ‘ ( 3 ↑ 𝑋 ) )
138 137 39 4 62 coe1fvalcl ⊢ ( ( ( 3 ↑ 𝑋 ) ∈ ( Base ‘ 𝑃 ) ∧ 3 ∈ ℕ0 ) → ( ( coe1 ‘ ( 3 ↑ 𝑋 ) ) ‘ 3 ) ∈ ℚ )
139 56 53 138 syl2anc ⊢ ( ⊤ → ( ( coe1 ‘ ( 3 ↑ 𝑋 ) ) ‘ 3 ) ∈ ℚ )
140 eqid ⊢ ( coe1 ‘ ( 𝐾 ‘ 2 ) ) = ( coe1 ‘ ( 𝐾 ‘ 2 ) )
141 140 39 4 62 coe1fvalcl ⊢ ( ( ( 𝐾 ‘ 2 ) ∈ ( Base ‘ 𝑃 ) ∧ 3 ∈ ℕ0 ) → ( ( coe1 ‘ ( 𝐾 ‘ 2 ) ) ‘ 3 ) ∈ ℚ )
142 67 53 141 syl2anc ⊢ ( ⊤ → ( ( coe1 ‘ ( 𝐾 ‘ 2 ) ) ‘ 3 ) ∈ ℚ )
143 40 1 132 subgsub ⊢ ( ( ℚ ∈ ( SubGrp ‘ ℂfld ) ∧ ( ( coe1 ‘ ( 3 ↑ 𝑋 ) ) ‘ 3 ) ∈ ℚ ∧ ( ( coe1 ‘ ( 𝐾 ‘ 2 ) ) ‘ 3 ) ∈ ℚ ) → ( ( ( coe1 ‘ ( 3 ↑ 𝑋 ) ) ‘ 3 ) − ( ( coe1 ‘ ( 𝐾 ‘ 2 ) ) ‘ 3 ) ) = ( ( ( coe1 ‘ ( 3 ↑ 𝑋 ) ) ‘ 3 ) ( -g ‘ 𝑄 ) ( ( coe1 ‘ ( 𝐾 ‘ 2 ) ) ‘ 3 ) ) )
144 136 139 142 143 syl3anc ⊢ ( ⊤ → ( ( ( coe1 ‘ ( 3 ↑ 𝑋 ) ) ‘ 3 ) − ( ( coe1 ‘ ( 𝐾 ‘ 2 ) ) ‘ 3 ) ) = ( ( ( coe1 ‘ ( 3 ↑ 𝑋 ) ) ‘ 3 ) ( -g ‘ 𝑄 ) ( ( coe1 ‘ ( 𝐾 ‘ 2 ) ) ‘ 3 ) ) )
145 iftrue ⊢ ( 𝑖 = 3 → if ( 𝑖 = 3 , 1 , 0 ) = 1 )
146 1 qrng1 ⊢ 1 = ( 1r ‘ 𝑄 )
147 4 6 3 47 53 91 146 coe1mon ⊢ ( ⊤ → ( coe1 ‘ ( 3 ↑ 𝑋 ) ) = ( 𝑖 ∈ ℕ0 ↦ if ( 𝑖 = 3 , 1 , 0 ) ) )
148 1cnd ⊢ ( ⊤ → 1 ∈ ℂ )
149 145 147 53 148 fvmptd4 ⊢ ( ⊤ → ( ( coe1 ‘ ( 3 ↑ 𝑋 ) ) ‘ 3 ) = 1 )
150 28 neii ⊢ ¬ 3 = 0
151 eqeq1 ⊢ ( 𝑖 = 3 → ( 𝑖 = 0 ↔ 3 = 0 ) )
152 150 151 mtbiri ⊢ ( 𝑖 = 3 → ¬ 𝑖 = 0 )
153 152 iffalsed ⊢ ( 𝑖 = 3 → if ( 𝑖 = 0 , 2 , 0 ) = 0 )
154 4 5 62 91 coe1scl ⊢ ( ( 𝑄 ∈ Ring ∧ 2 ∈ ℚ ) → ( coe1 ‘ ( 𝐾 ‘ 2 ) ) = ( 𝑖 ∈ ℕ0 ↦ if ( 𝑖 = 0 , 2 , 0 ) ) )
155 47 66 154 syl2anc ⊢ ( ⊤ → ( coe1 ‘ ( 𝐾 ‘ 2 ) ) = ( 𝑖 ∈ ℕ0 ↦ if ( 𝑖 = 0 , 2 , 0 ) ) )
156 0nn0 ⊢ 0 ∈ ℕ0
157 156 a1i ⊢ ( ⊤ → 0 ∈ ℕ0 )
158 153 155 53 157 fvmptd4 ⊢ ( ⊤ → ( ( coe1 ‘ ( 𝐾 ‘ 2 ) ) ‘ 3 ) = 0 )
159 149 158 oveq12d ⊢ ( ⊤ → ( ( ( coe1 ‘ ( 3 ↑ 𝑋 ) ) ‘ 3 ) − ( ( coe1 ‘ ( 𝐾 ‘ 2 ) ) ‘ 3 ) ) = ( 1 − 0 ) )
160 1m0e1 ⊢ ( 1 − 0 ) = 1
161 159 160 eqtrdi ⊢ ( ⊤ → ( ( ( coe1 ‘ ( 3 ↑ 𝑋 ) ) ‘ 3 ) − ( ( coe1 ‘ ( 𝐾 ‘ 2 ) ) ‘ 3 ) ) = 1 )
162 144 161 eqtr3d ⊢ ( ⊤ → ( ( ( coe1 ‘ ( 3 ↑ 𝑋 ) ) ‘ 3 ) ( -g ‘ 𝑄 ) ( ( coe1 ‘ ( 𝐾 ‘ 2 ) ) ‘ 3 ) ) = 1 )
163 131 134 162 3eqtrd ⊢ ( ⊤ → ( ( coe1 ‘ 𝐹 ) ‘ ( 𝐷 ‘ 𝐹 ) ) = 1 )
164 130 fveq2d ⊢ ( ⊤ → ( ( coe1 ‘ 𝐹 ) ‘ ( 𝐷 ‘ 𝐹 ) ) = ( ( coe1 ‘ 𝐹 ) ‘ 3 ) )
165 163 164 eqtr3d ⊢ ( ⊤ → 1 = ( ( coe1 ‘ 𝐹 ) ‘ 3 ) )
166 165 mptru ⊢ 1 = ( ( coe1 ‘ 𝐹 ) ‘ 3 )
167 115 fveq1d ⊢ ( ⊤ → ( ( coe1 ‘ 𝐹 ) ‘ 2 ) = ( ( coe1 ‘ ( ( 3 ↑ 𝑋 ) − ( 𝐾 ‘ 2 ) ) ) ‘ 2 ) )
168 2nn0 ⊢ 2 ∈ ℕ0
169 168 a1i ⊢ ( ⊤ → 2 ∈ ℕ0 )
170 4 39 2 132 coe1subfv ⊢ ( ( ( 𝑄 ∈ Ring ∧ ( 3 ↑ 𝑋 ) ∈ ( Base ‘ 𝑃 ) ∧ ( 𝐾 ‘ 2 ) ∈ ( Base ‘ 𝑃 ) ) ∧ 2 ∈ ℕ0 ) → ( ( coe1 ‘ ( ( 3 ↑ 𝑋 ) − ( 𝐾 ‘ 2 ) ) ) ‘ 2 ) = ( ( ( coe1 ‘ ( 3 ↑ 𝑋 ) ) ‘ 2 ) ( -g ‘ 𝑄 ) ( ( coe1 ‘ ( 𝐾 ‘ 2 ) ) ‘ 2 ) ) )
171 47 56 67 169 170 syl31anc ⊢ ( ⊤ → ( ( coe1 ‘ ( ( 3 ↑ 𝑋 ) − ( 𝐾 ‘ 2 ) ) ) ‘ 2 ) = ( ( ( coe1 ‘ ( 3 ↑ 𝑋 ) ) ‘ 2 ) ( -g ‘ 𝑄 ) ( ( coe1 ‘ ( 𝐾 ‘ 2 ) ) ‘ 2 ) ) )
172 2re ⊢ 2 ∈ ℝ
173 2lt3 ⊢ 2 < 3
174 172 173 ltneii ⊢ 2 ≠ 3
175 neeq1 ⊢ ( 𝑖 = 2 → ( 𝑖 ≠ 3 ↔ 2 ≠ 3 ) )
176 174 175 mpbiri ⊢ ( 𝑖 = 2 → 𝑖 ≠ 3 )
177 176 adantl ⊢ ( ( ⊤ ∧ 𝑖 = 2 ) → 𝑖 ≠ 3 )
178 177 neneqd ⊢ ( ( ⊤ ∧ 𝑖 = 2 ) → ¬ 𝑖 = 3 )
179 178 iffalsed ⊢ ( ( ⊤ ∧ 𝑖 = 2 ) → if ( 𝑖 = 3 , 1 , 0 ) = 0 )
180 147 179 169 157 fvmptd ⊢ ( ⊤ → ( ( coe1 ‘ ( 3 ↑ 𝑋 ) ) ‘ 2 ) = 0 )
181 neeq1 ⊢ ( 𝑖 = 2 → ( 𝑖 ≠ 0 ↔ 2 ≠ 0 ) )
182 120 181 mpbiri ⊢ ( 𝑖 = 2 → 𝑖 ≠ 0 )
183 182 neneqd ⊢ ( 𝑖 = 2 → ¬ 𝑖 = 0 )
184 183 adantl ⊢ ( ( ⊤ ∧ 𝑖 = 2 ) → ¬ 𝑖 = 0 )
185 184 iffalsed ⊢ ( ( ⊤ ∧ 𝑖 = 2 ) → if ( 𝑖 = 0 , 2 , 0 ) = 0 )
186 155 185 169 157 fvmptd ⊢ ( ⊤ → ( ( coe1 ‘ ( 𝐾 ‘ 2 ) ) ‘ 2 ) = 0 )
187 180 186 oveq12d ⊢ ( ⊤ → ( ( ( coe1 ‘ ( 3 ↑ 𝑋 ) ) ‘ 2 ) ( -g ‘ 𝑄 ) ( ( coe1 ‘ ( 𝐾 ‘ 2 ) ) ‘ 2 ) ) = ( 0 ( -g ‘ 𝑄 ) 0 ) )
188 171 187 eqtrd ⊢ ( ⊤ → ( ( coe1 ‘ ( ( 3 ↑ 𝑋 ) − ( 𝐾 ‘ 2 ) ) ) ‘ 2 ) = ( 0 ( -g ‘ 𝑄 ) 0 ) )
189 158 142 eqeltrrd ⊢ ( ⊤ → 0 ∈ ℚ )
190 40 1 132 subgsub ⊢ ( ( ℚ ∈ ( SubGrp ‘ ℂfld ) ∧ 0 ∈ ℚ ∧ 0 ∈ ℚ ) → ( 0 − 0 ) = ( 0 ( -g ‘ 𝑄 ) 0 ) )
191 136 189 189 190 syl3anc ⊢ ( ⊤ → ( 0 − 0 ) = ( 0 ( -g ‘ 𝑄 ) 0 ) )
192 0m0e0 ⊢ ( 0 − 0 ) = 0
193 191 192 eqtr3di ⊢ ( ⊤ → ( 0 ( -g ‘ 𝑄 ) 0 ) = 0 )
194 167 188 193 3eqtrrd ⊢ ( ⊤ → 0 = ( ( coe1 ‘ 𝐹 ) ‘ 2 ) )
195 194 mptru ⊢ 0 = ( ( coe1 ‘ 𝐹 ) ‘ 2 )
196 115 fveq1d ⊢ ( ⊤ → ( ( coe1 ‘ 𝐹 ) ‘ 1 ) = ( ( coe1 ‘ ( ( 3 ↑ 𝑋 ) − ( 𝐾 ‘ 2 ) ) ) ‘ 1 ) )
197 1nn0 ⊢ 1 ∈ ℕ0
198 197 a1i ⊢ ( ⊤ → 1 ∈ ℕ0 )
199 4 39 2 132 coe1subfv ⊢ ( ( ( 𝑄 ∈ Ring ∧ ( 3 ↑ 𝑋 ) ∈ ( Base ‘ 𝑃 ) ∧ ( 𝐾 ‘ 2 ) ∈ ( Base ‘ 𝑃 ) ) ∧ 1 ∈ ℕ0 ) → ( ( coe1 ‘ ( ( 3 ↑ 𝑋 ) − ( 𝐾 ‘ 2 ) ) ) ‘ 1 ) = ( ( ( coe1 ‘ ( 3 ↑ 𝑋 ) ) ‘ 1 ) ( -g ‘ 𝑄 ) ( ( coe1 ‘ ( 𝐾 ‘ 2 ) ) ‘ 1 ) ) )
200 47 56 67 198 199 syl31anc ⊢ ( ⊤ → ( ( coe1 ‘ ( ( 3 ↑ 𝑋 ) − ( 𝐾 ‘ 2 ) ) ) ‘ 1 ) = ( ( ( coe1 ‘ ( 3 ↑ 𝑋 ) ) ‘ 1 ) ( -g ‘ 𝑄 ) ( ( coe1 ‘ ( 𝐾 ‘ 2 ) ) ‘ 1 ) ) )
201 1re ⊢ 1 ∈ ℝ
202 1lt3 ⊢ 1 < 3
203 201 202 ltneii ⊢ 1 ≠ 3
204 neeq1 ⊢ ( 𝑖 = 1 → ( 𝑖 ≠ 3 ↔ 1 ≠ 3 ) )
205 203 204 mpbiri ⊢ ( 𝑖 = 1 → 𝑖 ≠ 3 )
206 205 neneqd ⊢ ( 𝑖 = 1 → ¬ 𝑖 = 3 )
207 206 adantl ⊢ ( ( ⊤ ∧ 𝑖 = 1 ) → ¬ 𝑖 = 3 )
208 207 iffalsed ⊢ ( ( ⊤ ∧ 𝑖 = 1 ) → if ( 𝑖 = 3 , 1 , 0 ) = 0 )
209 147 208 198 157 fvmptd ⊢ ( ⊤ → ( ( coe1 ‘ ( 3 ↑ 𝑋 ) ) ‘ 1 ) = 0 )
210 ax-1ne0 ⊢ 1 ≠ 0
211 neeq1 ⊢ ( 𝑖 = 1 → ( 𝑖 ≠ 0 ↔ 1 ≠ 0 ) )
212 210 211 mpbiri ⊢ ( 𝑖 = 1 → 𝑖 ≠ 0 )
213 212 neneqd ⊢ ( 𝑖 = 1 → ¬ 𝑖 = 0 )
214 213 adantl ⊢ ( ( ⊤ ∧ 𝑖 = 1 ) → ¬ 𝑖 = 0 )
215 214 iffalsed ⊢ ( ( ⊤ ∧ 𝑖 = 1 ) → if ( 𝑖 = 0 , 2 , 0 ) = 0 )
216 155 215 198 157 fvmptd ⊢ ( ⊤ → ( ( coe1 ‘ ( 𝐾 ‘ 2 ) ) ‘ 1 ) = 0 )
217 209 216 oveq12d ⊢ ( ⊤ → ( ( ( coe1 ‘ ( 3 ↑ 𝑋 ) ) ‘ 1 ) ( -g ‘ 𝑄 ) ( ( coe1 ‘ ( 𝐾 ‘ 2 ) ) ‘ 1 ) ) = ( 0 ( -g ‘ 𝑄 ) 0 ) )
218 200 217 eqtrd ⊢ ( ⊤ → ( ( coe1 ‘ ( ( 3 ↑ 𝑋 ) − ( 𝐾 ‘ 2 ) ) ) ‘ 1 ) = ( 0 ( -g ‘ 𝑄 ) 0 ) )
219 196 218 193 3eqtrrd ⊢ ( ⊤ → 0 = ( ( coe1 ‘ 𝐹 ) ‘ 1 ) )
220 219 mptru ⊢ 0 = ( ( coe1 ‘ 𝐹 ) ‘ 1 )
221 115 fveq1d ⊢ ( ⊤ → ( ( coe1 ‘ 𝐹 ) ‘ 0 ) = ( ( coe1 ‘ ( ( 3 ↑ 𝑋 ) − ( 𝐾 ‘ 2 ) ) ) ‘ 0 ) )
222 4 39 2 132 coe1subfv ⊢ ( ( ( 𝑄 ∈ Ring ∧ ( 3 ↑ 𝑋 ) ∈ ( Base ‘ 𝑃 ) ∧ ( 𝐾 ‘ 2 ) ∈ ( Base ‘ 𝑃 ) ) ∧ 0 ∈ ℕ0 ) → ( ( coe1 ‘ ( ( 3 ↑ 𝑋 ) − ( 𝐾 ‘ 2 ) ) ) ‘ 0 ) = ( ( ( coe1 ‘ ( 3 ↑ 𝑋 ) ) ‘ 0 ) ( -g ‘ 𝑄 ) ( ( coe1 ‘ ( 𝐾 ‘ 2 ) ) ‘ 0 ) ) )
223 47 56 67 157 222 syl31anc ⊢ ( ⊤ → ( ( coe1 ‘ ( ( 3 ↑ 𝑋 ) − ( 𝐾 ‘ 2 ) ) ) ‘ 0 ) = ( ( ( coe1 ‘ ( 3 ↑ 𝑋 ) ) ‘ 0 ) ( -g ‘ 𝑄 ) ( ( coe1 ‘ ( 𝐾 ‘ 2 ) ) ‘ 0 ) ) )
224 28 necomi ⊢ 0 ≠ 3
225 neeq1 ⊢ ( 𝑖 = 0 → ( 𝑖 ≠ 3 ↔ 0 ≠ 3 ) )
226 224 225 mpbiri ⊢ ( 𝑖 = 0 → 𝑖 ≠ 3 )
227 226 neneqd ⊢ ( 𝑖 = 0 → ¬ 𝑖 = 3 )
228 227 adantl ⊢ ( ( ⊤ ∧ 𝑖 = 0 ) → ¬ 𝑖 = 3 )
229 228 iffalsed ⊢ ( ( ⊤ ∧ 𝑖 = 0 ) → if ( 𝑖 = 3 , 1 , 0 ) = 0 )
230 147 229 157 157 fvmptd ⊢ ( ⊤ → ( ( coe1 ‘ ( 3 ↑ 𝑋 ) ) ‘ 0 ) = 0 )
231 simpr ⊢ ( ( ⊤ ∧ 𝑖 = 0 ) → 𝑖 = 0 )
232 231 iftrued ⊢ ( ( ⊤ ∧ 𝑖 = 0 ) → if ( 𝑖 = 0 , 2 , 0 ) = 2 )
233 155 232 157 169 fvmptd ⊢ ( ⊤ → ( ( coe1 ‘ ( 𝐾 ‘ 2 ) ) ‘ 0 ) = 2 )
234 230 233 oveq12d ⊢ ( ⊤ → ( ( ( coe1 ‘ ( 3 ↑ 𝑋 ) ) ‘ 0 ) ( -g ‘ 𝑄 ) ( ( coe1 ‘ ( 𝐾 ‘ 2 ) ) ‘ 0 ) ) = ( 0 ( -g ‘ 𝑄 ) 2 ) )
235 223 234 eqtrd ⊢ ( ⊤ → ( ( coe1 ‘ ( ( 3 ↑ 𝑋 ) − ( 𝐾 ‘ 2 ) ) ) ‘ 0 ) = ( 0 ( -g ‘ 𝑄 ) 2 ) )
236 df-neg ⊢ - 2 = ( 0 − 2 )
237 40 1 132 subgsub ⊢ ( ( ℚ ∈ ( SubGrp ‘ ℂfld ) ∧ 0 ∈ ℚ ∧ 2 ∈ ℚ ) → ( 0 − 2 ) = ( 0 ( -g ‘ 𝑄 ) 2 ) )
238 136 189 66 237 syl3anc ⊢ ( ⊤ → ( 0 − 2 ) = ( 0 ( -g ‘ 𝑄 ) 2 ) )
239 236 238 eqtr2id ⊢ ( ⊤ → ( 0 ( -g ‘ 𝑄 ) 2 ) = - 2 )
240 221 235 239 3eqtrrd ⊢ ( ⊤ → - 2 = ( ( coe1 ‘ 𝐹 ) ‘ 0 ) )
241 240 mptru ⊢ - 2 = ( ( coe1 ‘ 𝐹 ) ‘ 0 )
242 95 a1i ⊢ ( 𝑥 ∈ ℚ → 𝑄 ∈ Field )
243 242 fldcrngd ⊢ ( 𝑥 ∈ ℚ → 𝑄 ∈ CRing )
244 100 mptru ⊢ 𝐹 ∈ ( Base ‘ 𝑃 )
245 244 a1i ⊢ ( 𝑥 ∈ ℚ → 𝐹 ∈ ( Base ‘ 𝑃 ) )
246 130 mptru ⊢ ( 𝐷 ‘ 𝐹 ) = 3
247 246 a1i ⊢ ( 𝑥 ∈ ℚ → ( 𝐷 ‘ 𝐹 ) = 3 )
248 id ⊢ ( 𝑥 ∈ ℚ → 𝑥 ∈ ℚ )
249 4 92 62 39 108 111 112 113 7 166 195 220 241 243 245 247 248 evl1deg3 ⊢ ( 𝑥 ∈ ℚ → ( ( ( eval1 ‘ 𝑄 ) ‘ 𝐹 ) ‘ 𝑥 ) = ( ( ( 1 · ( 3 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) 𝑥 ) ) + ( 0 · ( 2 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) 𝑥 ) ) ) + ( ( 0 · 𝑥 ) + - 2 ) ) )
250 qsscn ⊢ ℚ ⊆ ℂ
251 eqid ⊢ ( ( mulGrp ‘ ℂfld ) ↾s ℚ ) = ( ( mulGrp ‘ ℂfld ) ↾s ℚ )
252 eqid ⊢ ( mulGrp ‘ ℂfld ) = ( mulGrp ‘ ℂfld )
253 252 14 mgpbas ⊢ ℂ = ( Base ‘ ( mulGrp ‘ ℂfld ) )
254 251 253 ressbas2 ⊢ ( ℚ ⊆ ℂ → ℚ = ( Base ‘ ( ( mulGrp ‘ ℂfld ) ↾s ℚ ) ) )
255 250 254 ax-mp ⊢ ℚ = ( Base ‘ ( ( mulGrp ‘ ℂfld ) ↾s ℚ ) )
256 1 252 mgpress ⊢ ( ( ℂfld ∈ DivRing ∧ ℚ ∈ ( SubRing ‘ ℂfld ) ) → ( ( mulGrp ‘ ℂfld ) ↾s ℚ ) = ( mulGrp ‘ 𝑄 ) )
257 15 21 256 mp2an ⊢ ( ( mulGrp ‘ ℂfld ) ↾s ℚ ) = ( mulGrp ‘ 𝑄 )
258 257 fveq2i ⊢ ( Base ‘ ( ( mulGrp ‘ ℂfld ) ↾s ℚ ) ) = ( Base ‘ ( mulGrp ‘ 𝑄 ) )
259 255 258 eqtri ⊢ ℚ = ( Base ‘ ( mulGrp ‘ 𝑄 ) )
260 eqid ⊢ ( mulGrp ‘ 𝑄 ) = ( mulGrp ‘ 𝑄 )
261 260 ringmgp ⊢ ( 𝑄 ∈ Ring → ( mulGrp ‘ 𝑄 ) ∈ Mnd )
262 57 261 mp1i ⊢ ( 𝑥 ∈ ℚ → ( mulGrp ‘ 𝑄 ) ∈ Mnd )
263 52 a1i ⊢ ( 𝑥 ∈ ℚ → 3 ∈ ℕ0 )
264 259 112 262 263 248 mulgnn0cld ⊢ ( 𝑥 ∈ ℚ → ( 3 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) 𝑥 ) ∈ ℚ )
265 250 264 sselid ⊢ ( 𝑥 ∈ ℚ → ( 3 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) 𝑥 ) ∈ ℂ )
266 265 mullidd ⊢ ( 𝑥 ∈ ℚ → ( 1 · ( 3 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) 𝑥 ) ) = ( 3 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) 𝑥 ) )
267 257 eqcomi ⊢ ( mulGrp ‘ 𝑄 ) = ( ( mulGrp ‘ ℂfld ) ↾s ℚ )
268 250 253 sseqtri ⊢ ℚ ⊆ ( Base ‘ ( mulGrp ‘ ℂfld ) )
269 268 a1i ⊢ ( 𝑥 ∈ ℚ → ℚ ⊆ ( Base ‘ ( mulGrp ‘ ℂfld ) ) )
270 81 a1i ⊢ ( 𝑥 ∈ ℚ → 3 ∈ ℕ )
271 267 269 248 270 ressmulgnnd ⊢ ( 𝑥 ∈ ℚ → ( 3 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) 𝑥 ) = ( 3 ( .g ‘ ( mulGrp ‘ ℂfld ) ) 𝑥 ) )
272 qcn ⊢ ( 𝑥 ∈ ℚ → 𝑥 ∈ ℂ )
273 cnfldexp ⊢ ( ( 𝑥 ∈ ℂ ∧ 3 ∈ ℕ0 ) → ( 3 ( .g ‘ ( mulGrp ‘ ℂfld ) ) 𝑥 ) = ( 𝑥 ↑ 3 ) )
274 272 263 273 syl2anc ⊢ ( 𝑥 ∈ ℚ → ( 3 ( .g ‘ ( mulGrp ‘ ℂfld ) ) 𝑥 ) = ( 𝑥 ↑ 3 ) )
275 266 271 274 3eqtrd ⊢ ( 𝑥 ∈ ℚ → ( 1 · ( 3 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) 𝑥 ) ) = ( 𝑥 ↑ 3 ) )
276 168 a1i ⊢ ( 𝑥 ∈ ℚ → 2 ∈ ℕ0 )
277 259 112 262 276 248 mulgnn0cld ⊢ ( 𝑥 ∈ ℚ → ( 2 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) 𝑥 ) ∈ ℚ )
278 250 277 sselid ⊢ ( 𝑥 ∈ ℚ → ( 2 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) 𝑥 ) ∈ ℂ )
279 278 mul02d ⊢ ( 𝑥 ∈ ℚ → ( 0 · ( 2 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) 𝑥 ) ) = 0 )
280 275 279 oveq12d ⊢ ( 𝑥 ∈ ℚ → ( ( 1 · ( 3 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) 𝑥 ) ) + ( 0 · ( 2 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) 𝑥 ) ) ) = ( ( 𝑥 ↑ 3 ) + 0 ) )
281 272 263 expcld ⊢ ( 𝑥 ∈ ℚ → ( 𝑥 ↑ 3 ) ∈ ℂ )
282 281 addridd ⊢ ( 𝑥 ∈ ℚ → ( ( 𝑥 ↑ 3 ) + 0 ) = ( 𝑥 ↑ 3 ) )
283 280 282 eqtrd ⊢ ( 𝑥 ∈ ℚ → ( ( 1 · ( 3 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) 𝑥 ) ) + ( 0 · ( 2 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) 𝑥 ) ) ) = ( 𝑥 ↑ 3 ) )
284 272 mul02d ⊢ ( 𝑥 ∈ ℚ → ( 0 · 𝑥 ) = 0 )
285 284 oveq1d ⊢ ( 𝑥 ∈ ℚ → ( ( 0 · 𝑥 ) + - 2 ) = ( 0 + - 2 ) )
286 26 a1i ⊢ ( 𝑥 ∈ ℚ → 2 ∈ ℂ )
287 286 negcld ⊢ ( 𝑥 ∈ ℚ → - 2 ∈ ℂ )
288 287 addlidd ⊢ ( 𝑥 ∈ ℚ → ( 0 + - 2 ) = - 2 )
289 285 288 eqtrd ⊢ ( 𝑥 ∈ ℚ → ( ( 0 · 𝑥 ) + - 2 ) = - 2 )
290 283 289 oveq12d ⊢ ( 𝑥 ∈ ℚ → ( ( ( 1 · ( 3 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) 𝑥 ) ) + ( 0 · ( 2 ( .g ‘ ( mulGrp ‘ 𝑄 ) ) 𝑥 ) ) ) + ( ( 0 · 𝑥 ) + - 2 ) ) = ( ( 𝑥 ↑ 3 ) + - 2 ) )
291 281 286 negsubd ⊢ ( 𝑥 ∈ ℚ → ( ( 𝑥 ↑ 3 ) + - 2 ) = ( ( 𝑥 ↑ 3 ) − 2 ) )
292 249 290 291 3eqtrd ⊢ ( 𝑥 ∈ ℚ → ( ( ( eval1 ‘ 𝑄 ) ‘ 𝐹 ) ‘ 𝑥 ) = ( ( 𝑥 ↑ 3 ) − 2 ) )
293 2prm ⊢ 2 ∈ ℙ
294 3z ⊢ 3 ∈ ℤ
295 3re ⊢ 3 ∈ ℝ
296 172 295 173 ltleii ⊢ 2 ≤ 3
297 64 eluz1i ⊢ ( 3 ∈ ( ℤ≥ ‘ 2 ) ↔ ( 3 ∈ ℤ ∧ 2 ≤ 3 ) )
298 294 296 297 mpbir2an ⊢ 3 ∈ ( ℤ≥ ‘ 2 )
299 rtprmirr ⊢ ( ( 2 ∈ ℙ ∧ 3 ∈ ( ℤ≥ ‘ 2 ) ) → ( 2 ↑𝑐 ( 1 / 3 ) ) ∈ ( ℝ ∖ ℚ ) )
300 293 298 299 mp2an ⊢ ( 2 ↑𝑐 ( 1 / 3 ) ) ∈ ( ℝ ∖ ℚ )
301 eldifn ⊢ ( ( 2 ↑𝑐 ( 1 / 3 ) ) ∈ ( ℝ ∖ ℚ ) → ¬ ( 2 ↑𝑐 ( 1 / 3 ) ) ∈ ℚ )
302 300 301 ax-mp ⊢ ¬ ( 2 ↑𝑐 ( 1 / 3 ) ) ∈ ℚ
303 nelne2 ⊢ ( ( 𝑥 ∈ ℚ ∧ ¬ ( 2 ↑𝑐 ( 1 / 3 ) ) ∈ ℚ ) → 𝑥 ≠ ( 2 ↑𝑐 ( 1 / 3 ) ) )
304 302 303 mpan2 ⊢ ( 𝑥 ∈ ℚ → 𝑥 ≠ ( 2 ↑𝑐 ( 1 / 3 ) ) )
305 qre ⊢ ( 𝑥 ∈ ℚ → 𝑥 ∈ ℝ )
306 305 adantr ⊢ ( ( 𝑥 ∈ ℚ ∧ ( ( 𝑥 ↑ 3 ) − 2 ) = 0 ) → 𝑥 ∈ ℝ )
307 2pos ⊢ 0 < 2
308 281 286 subeq0ad ⊢ ( 𝑥 ∈ ℚ → ( ( ( 𝑥 ↑ 3 ) − 2 ) = 0 ↔ ( 𝑥 ↑ 3 ) = 2 ) )
309 308 biimpa ⊢ ( ( 𝑥 ∈ ℚ ∧ ( ( 𝑥 ↑ 3 ) − 2 ) = 0 ) → ( 𝑥 ↑ 3 ) = 2 )
310 307 309 breqtrrid ⊢ ( ( 𝑥 ∈ ℚ ∧ ( ( 𝑥 ↑ 3 ) − 2 ) = 0 ) → 0 < ( 𝑥 ↑ 3 ) )
311 81 a1i ⊢ ( ( 𝑥 ∈ ℚ ∧ ( ( 𝑥 ↑ 3 ) − 2 ) = 0 ) → 3 ∈ ℕ )
312 n2dvds3 ⊢ ¬ 2 ∥ 3
313 312 a1i ⊢ ( ( 𝑥 ∈ ℚ ∧ ( ( 𝑥 ↑ 3 ) − 2 ) = 0 ) → ¬ 2 ∥ 3 )
314 306 311 313 expgt0b ⊢ ( ( 𝑥 ∈ ℚ ∧ ( ( 𝑥 ↑ 3 ) − 2 ) = 0 ) → ( 0 < 𝑥 ↔ 0 < ( 𝑥 ↑ 3 ) ) )
315 310 314 mpbird ⊢ ( ( 𝑥 ∈ ℚ ∧ ( ( 𝑥 ↑ 3 ) − 2 ) = 0 ) → 0 < 𝑥 )
316 306 315 elrpd ⊢ ( ( 𝑥 ∈ ℚ ∧ ( ( 𝑥 ↑ 3 ) − 2 ) = 0 ) → 𝑥 ∈ ℝ+ )
317 295 a1i ⊢ ( ( 𝑥 ∈ ℚ ∧ ( ( 𝑥 ↑ 3 ) − 2 ) = 0 ) → 3 ∈ ℝ )
318 29 a1i ⊢ ( ( 𝑥 ∈ ℚ ∧ ( ( 𝑥 ↑ 3 ) − 2 ) = 0 ) → ( 1 / 3 ) ∈ ℂ )
319 316 317 318 cxpmuld ⊢ ( ( 𝑥 ∈ ℚ ∧ ( ( 𝑥 ↑ 3 ) − 2 ) = 0 ) → ( 𝑥 ↑𝑐 ( 3 · ( 1 / 3 ) ) ) = ( ( 𝑥 ↑𝑐 3 ) ↑𝑐 ( 1 / 3 ) ) )
320 27 a1i ⊢ ( 𝑥 ∈ ℚ → 3 ∈ ℂ )
321 28 a1i ⊢ ( 𝑥 ∈ ℚ → 3 ≠ 0 )
322 320 321 recidd ⊢ ( 𝑥 ∈ ℚ → ( 3 · ( 1 / 3 ) ) = 1 )
323 322 oveq2d ⊢ ( 𝑥 ∈ ℚ → ( 𝑥 ↑𝑐 ( 3 · ( 1 / 3 ) ) ) = ( 𝑥 ↑𝑐 1 ) )
324 272 cxp1d ⊢ ( 𝑥 ∈ ℚ → ( 𝑥 ↑𝑐 1 ) = 𝑥 )
325 323 324 eqtrd ⊢ ( 𝑥 ∈ ℚ → ( 𝑥 ↑𝑐 ( 3 · ( 1 / 3 ) ) ) = 𝑥 )
326 325 adantr ⊢ ( ( 𝑥 ∈ ℚ ∧ ( ( 𝑥 ↑ 3 ) − 2 ) = 0 ) → ( 𝑥 ↑𝑐 ( 3 · ( 1 / 3 ) ) ) = 𝑥 )
327 cxpexp ⊢ ( ( 𝑥 ∈ ℂ ∧ 3 ∈ ℕ0 ) → ( 𝑥 ↑𝑐 3 ) = ( 𝑥 ↑ 3 ) )
328 272 263 327 syl2anc ⊢ ( 𝑥 ∈ ℚ → ( 𝑥 ↑𝑐 3 ) = ( 𝑥 ↑ 3 ) )
329 328 oveq1d ⊢ ( 𝑥 ∈ ℚ → ( ( 𝑥 ↑𝑐 3 ) ↑𝑐 ( 1 / 3 ) ) = ( ( 𝑥 ↑ 3 ) ↑𝑐 ( 1 / 3 ) ) )
330 329 adantr ⊢ ( ( 𝑥 ∈ ℚ ∧ ( ( 𝑥 ↑ 3 ) − 2 ) = 0 ) → ( ( 𝑥 ↑𝑐 3 ) ↑𝑐 ( 1 / 3 ) ) = ( ( 𝑥 ↑ 3 ) ↑𝑐 ( 1 / 3 ) ) )
331 319 326 330 3eqtr3rd ⊢ ( ( 𝑥 ∈ ℚ ∧ ( ( 𝑥 ↑ 3 ) − 2 ) = 0 ) → ( ( 𝑥 ↑ 3 ) ↑𝑐 ( 1 / 3 ) ) = 𝑥 )
332 309 oveq1d ⊢ ( ( 𝑥 ∈ ℚ ∧ ( ( 𝑥 ↑ 3 ) − 2 ) = 0 ) → ( ( 𝑥 ↑ 3 ) ↑𝑐 ( 1 / 3 ) ) = ( 2 ↑𝑐 ( 1 / 3 ) ) )
333 331 332 eqtr3d ⊢ ( ( 𝑥 ∈ ℚ ∧ ( ( 𝑥 ↑ 3 ) − 2 ) = 0 ) → 𝑥 = ( 2 ↑𝑐 ( 1 / 3 ) ) )
334 304 333 mteqand ⊢ ( 𝑥 ∈ ℚ → ( ( 𝑥 ↑ 3 ) − 2 ) ≠ 0 )
335 292 334 eqnetrd ⊢ ( 𝑥 ∈ ℚ → ( ( ( eval1 ‘ 𝑄 ) ‘ 𝐹 ) ‘ 𝑥 ) ≠ 0 )
336 335 neneqd ⊢ ( 𝑥 ∈ ℚ → ¬ ( ( ( eval1 ‘ 𝑄 ) ‘ 𝐹 ) ‘ 𝑥 ) = 0 )
337 336 rgen ⊢ ∀ 𝑥 ∈ ℚ ¬ ( ( ( eval1 ‘ 𝑄 ) ‘ 𝐹 ) ‘ 𝑥 ) = 0
338 337 a1i ⊢ ( ⊤ → ∀ 𝑥 ∈ ℚ ¬ ( ( ( eval1 ‘ 𝑄 ) ‘ 𝐹 ) ‘ 𝑥 ) = 0 )
339 rabeq0 ⊢ ( { 𝑥 ∈ ℚ ∣ ( ( ( eval1 ‘ 𝑄 ) ‘ 𝐹 ) ‘ 𝑥 ) = 0 } = ∅ ↔ ∀ 𝑥 ∈ ℚ ¬ ( ( ( eval1 ‘ 𝑄 ) ‘ 𝐹 ) ‘ 𝑥 ) = 0 )
340 338 339 sylibr ⊢ ( ⊤ → { 𝑥 ∈ ℚ ∣ ( ( ( eval1 ‘ 𝑄 ) ‘ 𝐹 ) ‘ 𝑥 ) = 0 } = ∅ )
341 105 340 eqtrd ⊢ ( ⊤ → ( ◡ ( ( eval1 ‘ 𝑄 ) ‘ 𝐹 ) “ { 0 } ) = ∅ )
342 91 92 7 4 39 96 100 341 130 ply1dg3rt0irred ⊢ ( ⊤ → 𝐹 ∈ ( Irred ‘ 𝑃 ) )
343 eqid ⊢ ( Irred ‘ 𝑃 ) = ( Irred ‘ 𝑃 )
344 343 35 irredn0 ⊢ ( ( 𝑃 ∈ Ring ∧ 𝐹 ∈ ( Irred ‘ 𝑃 ) ) → 𝐹 ≠ ( 0g ‘ 𝑃 ) )
345 49 342 344 syl2anc ⊢ ( ⊤ → 𝐹 ≠ ( 0g ‘ 𝑃 ) )
346 1 fveq2i ⊢ ( deg1 ‘ 𝑄 ) = ( deg1 ‘ ( ℂfld ↾s ℚ ) )
347 7 346 eqtri ⊢ 𝐷 = ( deg1 ‘ ( ℂfld ↾s ℚ ) )
348 eqid ⊢ ( Monic1p ‘ ( ℂfld ↾s ℚ ) ) = ( Monic1p ‘ ( ℂfld ↾s ℚ ) )
349 eqid ⊢ ( ℂfld ↾s ℚ ) = ( ℂfld ↾s ℚ )
350 349 qrng1 ⊢ 1 = ( 1r ‘ ( ℂfld ↾s ℚ ) )
351 13 39 35 347 348 350 ismon1p ⊢ ( 𝐹 ∈ ( Monic1p ‘ ( ℂfld ↾s ℚ ) ) ↔ ( 𝐹 ∈ ( Base ‘ 𝑃 ) ∧ 𝐹 ≠ ( 0g ‘ 𝑃 ) ∧ ( ( coe1 ‘ 𝐹 ) ‘ ( 𝐷 ‘ 𝐹 ) ) = 1 ) )
352 100 345 163 351 syl3anbrc ⊢ ( ⊤ → 𝐹 ∈ ( Monic1p ‘ ( ℂfld ↾s ℚ ) ) )
353 11 13 14 19 25 33 34 10 35 90 342 352 irredminply ⊢ ( ⊤ → 𝐹 = ( 𝑀 ‘ 𝐴 ) )
354 353 130 jca ⊢ ( ⊤ → ( 𝐹 = ( 𝑀 ‘ 𝐴 ) ∧ ( 𝐷 ‘ 𝐹 ) = 3 ) )
355 354 mptru ⊢ ( 𝐹 = ( 𝑀 ‘ 𝐴 ) ∧ ( 𝐷 ‘ 𝐹 ) = 3 )