Metamath Proof Explorer

Theorem cos9thpiminplylem6

Description: Evaluation of the polynomial ( ( X ^ 3 ) + ( ( -u 3 x. X ) + 1 ) ) . (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 ) ) )
cos9thpiminplylem6.1 ⊢ ( 𝜑 → 𝑌 ∈ ℂ )
Assertion cos9thpiminplylem6 ( 𝜑 → ( ( ( ℂfld evalSub1 ℚ ) ‘ 𝐹 ) ‘ 𝑌 ) = ( ( 𝑌 ↑ 3 ) + ( ( - 3 · 𝑌 ) + 1 ) ) )

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 cos9thpiminplylem6.1 ⊢ ( 𝜑 → 𝑌 ∈ ℂ )
14 12 fveq2i ⊢ ( ( ℂfld evalSub1 ℚ ) ‘ 𝐹 ) = ( ( ℂfld evalSub1 ℚ ) ‘ ( ( 3 ↑ 𝑋 ) + ( ( ( 𝐾 ‘ - 3 ) · 𝑋 ) + ( 𝐾 ‘ 1 ) ) ) )
15 14 fveq1i ⊢ ( ( ( ℂfld evalSub1 ℚ ) ‘ 𝐹 ) ‘ 𝑌 ) = ( ( ( ℂfld evalSub1 ℚ ) ‘ ( ( 3 ↑ 𝑋 ) + ( ( ( 𝐾 ‘ - 3 ) · 𝑋 ) + ( 𝐾 ‘ 1 ) ) ) ) ‘ 𝑌 )
16 eqid ⊢ ( ℂfld evalSub1 ℚ ) = ( ℂfld evalSub1 ℚ )
17 cnfldbas ⊢ ℂ = ( Base ‘ ℂfld )
18 eqid ⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
19 cnfldadd ⊢ + = ( +g ‘ ℂfld )
20 cncrng ⊢ ℂfld ∈ CRing
21 20 a1i ⊢ ( 𝜑 → ℂfld ∈ CRing )
22 qsubdrg ⊢ ( ℚ ∈ ( SubRing ‘ ℂfld ) ∧ ( ℂfld ↾s ℚ ) ∈ DivRing )
23 22 simpli ⊢ ℚ ∈ ( SubRing ‘ ℂfld )
24 23 a1i ⊢ ( 𝜑 → ℚ ∈ ( SubRing ‘ ℂfld ) )
25 eqid ⊢ ( mulGrp ‘ 𝑃 ) = ( mulGrp ‘ 𝑃 )
26 25 18 mgpbas ⊢ ( Base ‘ 𝑃 ) = ( Base ‘ ( mulGrp ‘ 𝑃 ) )
27 4 qdrng ⊢ 𝑄 ∈ DivRing
28 27 a1i ⊢ ( 𝜑 → 𝑄 ∈ DivRing )
29 28 drngringd ⊢ ( 𝜑 → 𝑄 ∈ Ring )
30 8 ply1ring ⊢ ( 𝑄 ∈ Ring → 𝑃 ∈ Ring )
31 29 30 syl ⊢ ( 𝜑 → 𝑃 ∈ Ring )
32 25 ringmgp ⊢ ( 𝑃 ∈ Ring → ( mulGrp ‘ 𝑃 ) ∈ Mnd )
33 31 32 syl ⊢ ( 𝜑 → ( mulGrp ‘ 𝑃 ) ∈ Mnd )
34 3nn0 ⊢ 3 ∈ ℕ0
35 34 a1i ⊢ ( 𝜑 → 3 ∈ ℕ0 )
36 10 8 18 vr1cl ⊢ ( 𝑄 ∈ Ring → 𝑋 ∈ ( Base ‘ 𝑃 ) )
37 29 36 syl ⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝑃 ) )
38 26 7 33 35 37 mulgnn0cld ⊢ ( 𝜑 → ( 3 ↑ 𝑋 ) ∈ ( Base ‘ 𝑃 ) )
39 31 ringgrpd ⊢ ( 𝜑 → 𝑃 ∈ Grp )
40 8 ply1sca ⊢ ( 𝑄 ∈ DivRing → 𝑄 = ( Scalar ‘ 𝑃 ) )
41 27 40 ax-mp ⊢ 𝑄 = ( Scalar ‘ 𝑃 )
42 8 ply1lmod ⊢ ( 𝑄 ∈ Ring → 𝑃 ∈ LMod )
43 29 42 syl ⊢ ( 𝜑 → 𝑃 ∈ LMod )
44 4 qrngbas ⊢ ℚ = ( Base ‘ 𝑄 )
45 9 41 31 43 44 18 asclf ⊢ ( 𝜑 → 𝐾 : ℚ ⟶ ( Base ‘ 𝑃 ) )
46 35 nn0zd ⊢ ( 𝜑 → 3 ∈ ℤ )
47 zq ⊢ ( 3 ∈ ℤ → 3 ∈ ℚ )
48 46 47 syl ⊢ ( 𝜑 → 3 ∈ ℚ )
49 qnegcl ⊢ ( 3 ∈ ℚ → - 3 ∈ ℚ )
50 48 49 syl ⊢ ( 𝜑 → - 3 ∈ ℚ )
51 45 50 ffvelcdmd ⊢ ( 𝜑 → ( 𝐾 ‘ - 3 ) ∈ ( Base ‘ 𝑃 ) )
52 18 6 31 51 37 ringcld ⊢ ( 𝜑 → ( ( 𝐾 ‘ - 3 ) · 𝑋 ) ∈ ( Base ‘ 𝑃 ) )
53 1zzd ⊢ ( 𝜑 → 1 ∈ ℤ )
54 zq ⊢ ( 1 ∈ ℤ → 1 ∈ ℚ )
55 53 54 syl ⊢ ( 𝜑 → 1 ∈ ℚ )
56 45 55 ffvelcdmd ⊢ ( 𝜑 → ( 𝐾 ‘ 1 ) ∈ ( Base ‘ 𝑃 ) )
57 18 5 39 52 56 grpcld ⊢ ( 𝜑 → ( ( ( 𝐾 ‘ - 3 ) · 𝑋 ) + ( 𝐾 ‘ 1 ) ) ∈ ( Base ‘ 𝑃 ) )
58 16 17 8 4 18 5 19 21 24 38 57 13 evls1addd ⊢ ( 𝜑 → ( ( ( ℂfld evalSub1 ℚ ) ‘ ( ( 3 ↑ 𝑋 ) + ( ( ( 𝐾 ‘ - 3 ) · 𝑋 ) + ( 𝐾 ‘ 1 ) ) ) ) ‘ 𝑌 ) = ( ( ( ( ℂfld evalSub1 ℚ ) ‘ ( 3 ↑ 𝑋 ) ) ‘ 𝑌 ) + ( ( ( ℂfld evalSub1 ℚ ) ‘ ( ( ( 𝐾 ‘ - 3 ) · 𝑋 ) + ( 𝐾 ‘ 1 ) ) ) ‘ 𝑌 ) ) )
59 eqid ⊢ ( .g ‘ ( mulGrp ‘ ℂfld ) ) = ( .g ‘ ( mulGrp ‘ ℂfld ) )
60 16 17 8 4 18 21 24 7 59 35 37 13 evls1expd ⊢ ( 𝜑 → ( ( ( ℂfld evalSub1 ℚ ) ‘ ( 3 ↑ 𝑋 ) ) ‘ 𝑌 ) = ( 3 ( .g ‘ ( mulGrp ‘ ℂfld ) ) ( ( ( ℂfld evalSub1 ℚ ) ‘ 𝑋 ) ‘ 𝑌 ) ) )
61 16 10 4 17 21 24 evls1var ⊢ ( 𝜑 → ( ( ℂfld evalSub1 ℚ ) ‘ 𝑋 ) = ( I ↾ ℂ ) )
62 61 fveq1d ⊢ ( 𝜑 → ( ( ( ℂfld evalSub1 ℚ ) ‘ 𝑋 ) ‘ 𝑌 ) = ( ( I ↾ ℂ ) ‘ 𝑌 ) )
63 fvresi ⊢ ( 𝑌 ∈ ℂ → ( ( I ↾ ℂ ) ‘ 𝑌 ) = 𝑌 )
64 13 63 syl ⊢ ( 𝜑 → ( ( I ↾ ℂ ) ‘ 𝑌 ) = 𝑌 )
65 62 64 eqtrd ⊢ ( 𝜑 → ( ( ( ℂfld evalSub1 ℚ ) ‘ 𝑋 ) ‘ 𝑌 ) = 𝑌 )
66 65 oveq2d ⊢ ( 𝜑 → ( 3 ( .g ‘ ( mulGrp ‘ ℂfld ) ) ( ( ( ℂfld evalSub1 ℚ ) ‘ 𝑋 ) ‘ 𝑌 ) ) = ( 3 ( .g ‘ ( mulGrp ‘ ℂfld ) ) 𝑌 ) )
67 cnfldexp ⊢ ( ( 𝑌 ∈ ℂ ∧ 3 ∈ ℕ0 ) → ( 3 ( .g ‘ ( mulGrp ‘ ℂfld ) ) 𝑌 ) = ( 𝑌 ↑ 3 ) )
68 13 34 67 sylancl ⊢ ( 𝜑 → ( 3 ( .g ‘ ( mulGrp ‘ ℂfld ) ) 𝑌 ) = ( 𝑌 ↑ 3 ) )
69 60 66 68 3eqtrd ⊢ ( 𝜑 → ( ( ( ℂfld evalSub1 ℚ ) ‘ ( 3 ↑ 𝑋 ) ) ‘ 𝑌 ) = ( 𝑌 ↑ 3 ) )
70 16 17 8 4 18 5 19 21 24 52 56 13 evls1addd ⊢ ( 𝜑 → ( ( ( ℂfld evalSub1 ℚ ) ‘ ( ( ( 𝐾 ‘ - 3 ) · 𝑋 ) + ( 𝐾 ‘ 1 ) ) ) ‘ 𝑌 ) = ( ( ( ( ℂfld evalSub1 ℚ ) ‘ ( ( 𝐾 ‘ - 3 ) · 𝑋 ) ) ‘ 𝑌 ) + ( ( ( ℂfld evalSub1 ℚ ) ‘ ( 𝐾 ‘ 1 ) ) ‘ 𝑌 ) ) )
71 cnfldmul ⊢ · = ( .r ‘ ℂfld )
72 16 17 8 4 18 6 71 21 24 51 37 13 evls1muld ⊢ ( 𝜑 → ( ( ( ℂfld evalSub1 ℚ ) ‘ ( ( 𝐾 ‘ - 3 ) · 𝑋 ) ) ‘ 𝑌 ) = ( ( ( ( ℂfld evalSub1 ℚ ) ‘ ( 𝐾 ‘ - 3 ) ) ‘ 𝑌 ) · ( ( ( ℂfld evalSub1 ℚ ) ‘ 𝑋 ) ‘ 𝑌 ) ) )
73 16 8 4 17 9 21 24 50 13 evls1scafv ⊢ ( 𝜑 → ( ( ( ℂfld evalSub1 ℚ ) ‘ ( 𝐾 ‘ - 3 ) ) ‘ 𝑌 ) = - 3 )
74 73 65 oveq12d ⊢ ( 𝜑 → ( ( ( ( ℂfld evalSub1 ℚ ) ‘ ( 𝐾 ‘ - 3 ) ) ‘ 𝑌 ) · ( ( ( ℂfld evalSub1 ℚ ) ‘ 𝑋 ) ‘ 𝑌 ) ) = ( - 3 · 𝑌 ) )
75 72 74 eqtrd ⊢ ( 𝜑 → ( ( ( ℂfld evalSub1 ℚ ) ‘ ( ( 𝐾 ‘ - 3 ) · 𝑋 ) ) ‘ 𝑌 ) = ( - 3 · 𝑌 ) )
76 16 8 4 17 9 21 24 55 13 evls1scafv ⊢ ( 𝜑 → ( ( ( ℂfld evalSub1 ℚ ) ‘ ( 𝐾 ‘ 1 ) ) ‘ 𝑌 ) = 1 )
77 75 76 oveq12d ⊢ ( 𝜑 → ( ( ( ( ℂfld evalSub1 ℚ ) ‘ ( ( 𝐾 ‘ - 3 ) · 𝑋 ) ) ‘ 𝑌 ) + ( ( ( ℂfld evalSub1 ℚ ) ‘ ( 𝐾 ‘ 1 ) ) ‘ 𝑌 ) ) = ( ( - 3 · 𝑌 ) + 1 ) )
78 70 77 eqtrd ⊢ ( 𝜑 → ( ( ( ℂfld evalSub1 ℚ ) ‘ ( ( ( 𝐾 ‘ - 3 ) · 𝑋 ) + ( 𝐾 ‘ 1 ) ) ) ‘ 𝑌 ) = ( ( - 3 · 𝑌 ) + 1 ) )
79 69 78 oveq12d ⊢ ( 𝜑 → ( ( ( ( ℂfld evalSub1 ℚ ) ‘ ( 3 ↑ 𝑋 ) ) ‘ 𝑌 ) + ( ( ( ℂfld evalSub1 ℚ ) ‘ ( ( ( 𝐾 ‘ - 3 ) · 𝑋 ) + ( 𝐾 ‘ 1 ) ) ) ‘ 𝑌 ) ) = ( ( 𝑌 ↑ 3 ) + ( ( - 3 · 𝑌 ) + 1 ) ) )
80 58 79 eqtrd ⊢ ( 𝜑 → ( ( ( ℂfld evalSub1 ℚ ) ‘ ( ( 3 ↑ 𝑋 ) + ( ( ( 𝐾 ‘ - 3 ) · 𝑋 ) + ( 𝐾 ‘ 1 ) ) ) ) ‘ 𝑌 ) = ( ( 𝑌 ↑ 3 ) + ( ( - 3 · 𝑌 ) + 1 ) ) )
81 15 80 eqtrid ⊢ ( 𝜑 → ( ( ( ℂfld evalSub1 ℚ ) ‘ 𝐹 ) ‘ 𝑌 ) = ( ( 𝑌 ↑ 3 ) + ( ( - 3 · 𝑌 ) + 1 ) ) )