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	$$⊢O={\mathrm{e}}^{\frac{\mathrm{i}2\mathrm{\pi }}{3}}$$
	cos9thpiminplylem4.2	$$⊢Z=O^{\frac{1}{3}}$$
	cos9thpiminplylem5.3	$$⊢A=Z+\left(\frac{1}{Z}\right)$$
	cos9thpiminply.q	$$⊢Q={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}$$
	cos9thpiminply.4	$$⊢\underset{\dot{}}{+}={+}_P$$
	cos9thpiminply.5	$$⊢\underset{\dot{}}{·}={\cdot }_P$$
	cos9thpiminply.6	$$⊢\underset{\dot{}}{\times }={\cdot }_{{\mathrm{mulGrp}}_P}$$
	cos9thpiminply.p	$$⊢P={\mathrm{Poly}}_1\left(Q\right)$$
	cos9thpiminply.k	$$⊢K=\mathrm{algSc}\left(P\right)$$
	cos9thpiminply.x	$$⊢X={\mathrm{var}}_1\left(Q\right)$$
	cos9thpiminply.d	$$⊢D={\mathrm{deg}}_1\left(Q\right)$$
	cos9thpiminply.f	$$⊢F=\left(3\underset{\dot{}}{\times }X\right)\underset{\dot{}}{+}\left(\left(K\left(-3\right)\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}K\left(1\right)\right)$$
	cos9thpiminplylem6.1	$$⊢\phi \to Y\in ℂ$$
Assertion	cos9thpiminplylem6	$$⊢\phi \to \left({ℂ}_{\mathrm{fld}}{\mathrm{evalSub}}_1\mathbb{Q}\right)\left(F\right)\left(Y\right)=Y^3+-3Y+1$$

Proof

Step	Hyp	Ref	Expression
1		cos9thpiminplylem3.1	$$⊢O={\mathrm{e}}^{\frac{\mathrm{i}2\mathrm{\pi }}{3}}$$
2		cos9thpiminplylem4.2	$$⊢Z=O^{\frac{1}{3}}$$
3		cos9thpiminplylem5.3	$$⊢A=Z+\left(\frac{1}{Z}\right)$$
4		cos9thpiminply.q	$$⊢Q={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}$$
5		cos9thpiminply.4	$$⊢\underset{\dot{}}{+}={+}_P$$
6		cos9thpiminply.5	$$⊢\underset{\dot{}}{·}={\cdot }_P$$
7		cos9thpiminply.6	$$⊢\underset{\dot{}}{\times }={\cdot }_{{\mathrm{mulGrp}}_P}$$
8		cos9thpiminply.p	$$⊢P={\mathrm{Poly}}_1\left(Q\right)$$
9		cos9thpiminply.k	$$⊢K=\mathrm{algSc}\left(P\right)$$
10		cos9thpiminply.x	$$⊢X={\mathrm{var}}_1\left(Q\right)$$
11		cos9thpiminply.d	$$⊢D={\mathrm{deg}}_1\left(Q\right)$$
12		cos9thpiminply.f	$$⊢F=\left(3\underset{\dot{}}{\times }X\right)\underset{\dot{}}{+}\left(\left(K\left(-3\right)\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}K\left(1\right)\right)$$
13		cos9thpiminplylem6.1	$$⊢\phi \to Y\in ℂ$$
14	12	fveq2i	$$⊢\left({ℂ}_{\mathrm{fld}}{\mathrm{evalSub}}_1\mathbb{Q}\right)\left(F\right)=\left({ℂ}_{\mathrm{fld}}{\mathrm{evalSub}}_1\mathbb{Q}\right)\left(\left(3\underset{\dot{}}{\times }X\right)\underset{\dot{}}{+}\left(\left(K\left(-3\right)\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}K\left(1\right)\right)\right)$$
15	14	fveq1i	$$⊢\left({ℂ}_{\mathrm{fld}}{\mathrm{evalSub}}_1\mathbb{Q}\right)\left(F\right)\left(Y\right)=\left({ℂ}_{\mathrm{fld}}{\mathrm{evalSub}}_1\mathbb{Q}\right)\left(\left(3\underset{\dot{}}{\times }X\right)\underset{\dot{}}{+}\left(\left(K\left(-3\right)\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}K\left(1\right)\right)\right)\left(Y\right)$$
16		eqid	$$⊢{ℂ}_{\mathrm{fld}}{\mathrm{evalSub}}_1\mathbb{Q}={ℂ}_{\mathrm{fld}}{\mathrm{evalSub}}_1\mathbb{Q}$$
17		cnfldbas	$$⊢ℂ={\mathrm{Base}}_{{ℂ}_{\mathrm{fld}}}$$
18		eqid	$$⊢{\mathrm{Base}}_P={\mathrm{Base}}_P$$
19		cnfldadd	$$⊢+={+}_{{ℂ}_{\mathrm{fld}}}$$
20		cncrng	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{CRing}$$
21	20	a1i	$$⊢\phi \to {ℂ}_{\mathrm{fld}}\in \mathrm{CRing}$$
22		qsubdrg	$$⊢\left(\mathbb{Q}\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)\wedge {ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}\mathbb{Q}\in \mathrm{DivRing}\right)$$
23	22	simpli	$$⊢\mathbb{Q}\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)$$
24	23	a1i	$$⊢\phi \to \mathbb{Q}\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)$$
25		eqid	$$⊢{\mathrm{mulGrp}}_P={\mathrm{mulGrp}}_P$$
26	25 18	mgpbas	$$⊢{\mathrm{Base}}_P={\mathrm{Base}}_{{\mathrm{mulGrp}}_P}$$
27	4	qdrng	$$⊢Q\in \mathrm{DivRing}$$
28	27	a1i	$$⊢\phi \to Q\in \mathrm{DivRing}$$
29	28	drngringd	$$⊢\phi \to Q\in \mathrm{Ring}$$
30	8	ply1ring	$$⊢Q\in \mathrm{Ring}\to P\in \mathrm{Ring}$$
31	29 30	syl	$$⊢\phi \to P\in \mathrm{Ring}$$
32	25	ringmgp	$$⊢P\in \mathrm{Ring}\to {\mathrm{mulGrp}}_P\in \mathrm{Mnd}$$
33	31 32	syl	$$⊢\phi \to {\mathrm{mulGrp}}_P\in \mathrm{Mnd}$$
34		3nn0	$$⊢3\in {\mathbb{N}}_0$$
35	34	a1i	$$⊢\phi \to 3\in {\mathbb{N}}_0$$
36	10 8 18	vr1cl	$$⊢Q\in \mathrm{Ring}\to X\in {\mathrm{Base}}_P$$
37	29 36	syl	$$⊢\phi \to X\in {\mathrm{Base}}_P$$
38	26 7 33 35 37	mulgnn0cld	$$⊢\phi \to 3\underset{\dot{}}{\times }X\in {\mathrm{Base}}_P$$
39	31	ringgrpd	$$⊢\phi \to P\in \mathrm{Grp}$$
40	8	ply1sca	$$⊢Q\in \mathrm{DivRing}\to Q=\mathrm{Scalar}\left(P\right)$$
41	27 40	ax-mp	$$⊢Q=\mathrm{Scalar}\left(P\right)$$
42	8	ply1lmod	$$⊢Q\in \mathrm{Ring}\to P\in \mathrm{LMod}$$
43	29 42	syl	$$⊢\phi \to P\in \mathrm{LMod}$$
44	4	qrngbas	$$⊢\mathbb{Q}={\mathrm{Base}}_Q$$
45	9 41 31 43 44 18	asclf	$$⊢\phi \to K:\mathbb{Q}⟶{\mathrm{Base}}_P$$
46	35	nn0zd	$$⊢\phi \to 3\in \mathbb{Z}$$
47		zq	$$⊢3\in \mathbb{Z}\to 3\in \mathbb{Q}$$
48	46 47	syl	$$⊢\phi \to 3\in \mathbb{Q}$$
49		qnegcl	$$⊢3\in \mathbb{Q}\to -3\in \mathbb{Q}$$
50	48 49	syl	$$⊢\phi \to -3\in \mathbb{Q}$$
51	45 50	ffvelcdmd	$$⊢\phi \to K\left(-3\right)\in {\mathrm{Base}}_P$$
52	18 6 31 51 37	ringcld	$$⊢\phi \to K\left(-3\right)\underset{\dot{}}{·}X\in {\mathrm{Base}}_P$$
53		1zzd	$$⊢\phi \to 1\in \mathbb{Z}$$
54		zq	$$⊢1\in \mathbb{Z}\to 1\in \mathbb{Q}$$
55	53 54	syl	$$⊢\phi \to 1\in \mathbb{Q}$$
56	45 55	ffvelcdmd	$$⊢\phi \to K\left(1\right)\in {\mathrm{Base}}_P$$
57	18 5 39 52 56	grpcld	$$⊢\phi \to \left(K\left(-3\right)\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}K\left(1\right)\in {\mathrm{Base}}_P$$
58	16 17 8 4 18 5 19 21 24 38 57 13	evls1addd	$$⊢\phi \to \left({ℂ}_{\mathrm{fld}}{\mathrm{evalSub}}_1\mathbb{Q}\right)\left(\left(3\underset{\dot{}}{\times }X\right)\underset{\dot{}}{+}\left(\left(K\left(-3\right)\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}K\left(1\right)\right)\right)\left(Y\right)=\left({ℂ}_{\mathrm{fld}}{\mathrm{evalSub}}_1\mathbb{Q}\right)\left(3\underset{\dot{}}{\times }X\right)\left(Y\right)+\left({ℂ}_{\mathrm{fld}}{\mathrm{evalSub}}_1\mathbb{Q}\right)\left(\left(K\left(-3\right)\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}K\left(1\right)\right)\left(Y\right)$$
59		eqid	$$⊢{\cdot }_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}={\cdot }_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}$$
60	16 17 8 4 18 21 24 7 59 35 37 13	evls1expd	$$⊢\phi \to \left({ℂ}_{\mathrm{fld}}{\mathrm{evalSub}}_1\mathbb{Q}\right)\left(3\underset{\dot{}}{\times }X\right)\left(Y\right)=3{\cdot }_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}\left({ℂ}_{\mathrm{fld}}{\mathrm{evalSub}}_1\mathbb{Q}\right)\left(X\right)\left(Y\right)$$
61	16 10 4 17 21 24	evls1var	$$⊢\phi \to \left({ℂ}_{\mathrm{fld}}{\mathrm{evalSub}}_1\mathbb{Q}\right)\left(X\right)={\mathrm{I}\upharpoonright }_{ℂ}$$
62	61	fveq1d	$$⊢\phi \to \left({ℂ}_{\mathrm{fld}}{\mathrm{evalSub}}_1\mathbb{Q}\right)\left(X\right)\left(Y\right)=\left({\mathrm{I}\upharpoonright }_{ℂ}\right)\left(Y\right)$$
63		fvresi	$$⊢Y\in ℂ\to \left({\mathrm{I}\upharpoonright }_{ℂ}\right)\left(Y\right)=Y$$
64	13 63	syl	$$⊢\phi \to \left({\mathrm{I}\upharpoonright }_{ℂ}\right)\left(Y\right)=Y$$
65	62 64	eqtrd	$$⊢\phi \to \left({ℂ}_{\mathrm{fld}}{\mathrm{evalSub}}_1\mathbb{Q}\right)\left(X\right)\left(Y\right)=Y$$
66	65	oveq2d	$$⊢\phi \to 3{\cdot }_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}\left({ℂ}_{\mathrm{fld}}{\mathrm{evalSub}}_1\mathbb{Q}\right)\left(X\right)\left(Y\right)=3{\cdot }_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}Y$$
67		cnfldexp	$$⊢\left(Y\in ℂ\wedge 3\in {\mathbb{N}}_0\right)\to 3{\cdot }_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}Y=Y^3$$
68	13 34 67	sylancl	$$⊢\phi \to 3{\cdot }_{{\mathrm{mulGrp}}_{{ℂ}_{\mathrm{fld}}}}Y=Y^3$$
69	60 66 68	3eqtrd	$$⊢\phi \to \left({ℂ}_{\mathrm{fld}}{\mathrm{evalSub}}_1\mathbb{Q}\right)\left(3\underset{\dot{}}{\times }X\right)\left(Y\right)=Y^3$$
70	16 17 8 4 18 5 19 21 24 52 56 13	evls1addd	$$⊢\phi \to \left({ℂ}_{\mathrm{fld}}{\mathrm{evalSub}}_1\mathbb{Q}\right)\left(\left(K\left(-3\right)\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}K\left(1\right)\right)\left(Y\right)=\left({ℂ}_{\mathrm{fld}}{\mathrm{evalSub}}_1\mathbb{Q}\right)\left(K\left(-3\right)\underset{\dot{}}{·}X\right)\left(Y\right)+\left({ℂ}_{\mathrm{fld}}{\mathrm{evalSub}}_1\mathbb{Q}\right)\left(K\left(1\right)\right)\left(Y\right)$$
71		cnfldmul	$$⊢\times ={\cdot }_{{ℂ}_{\mathrm{fld}}}$$
72	16 17 8 4 18 6 71 21 24 51 37 13	evls1muld	$$⊢\phi \to \left({ℂ}_{\mathrm{fld}}{\mathrm{evalSub}}_1\mathbb{Q}\right)\left(K\left(-3\right)\underset{\dot{}}{·}X\right)\left(Y\right)=\left({ℂ}_{\mathrm{fld}}{\mathrm{evalSub}}_1\mathbb{Q}\right)\left(K\left(-3\right)\right)\left(Y\right)\left({ℂ}_{\mathrm{fld}}{\mathrm{evalSub}}_1\mathbb{Q}\right)\left(X\right)\left(Y\right)$$
73	16 8 4 17 9 21 24 50 13	evls1scafv	$$⊢\phi \to \left({ℂ}_{\mathrm{fld}}{\mathrm{evalSub}}_1\mathbb{Q}\right)\left(K\left(-3\right)\right)\left(Y\right)=-3$$
74	73 65	oveq12d	$$⊢\phi \to \left({ℂ}_{\mathrm{fld}}{\mathrm{evalSub}}_1\mathbb{Q}\right)\left(K\left(-3\right)\right)\left(Y\right)\left({ℂ}_{\mathrm{fld}}{\mathrm{evalSub}}_1\mathbb{Q}\right)\left(X\right)\left(Y\right)=-3Y$$
75	72 74	eqtrd	$$⊢\phi \to \left({ℂ}_{\mathrm{fld}}{\mathrm{evalSub}}_1\mathbb{Q}\right)\left(K\left(-3\right)\underset{\dot{}}{·}X\right)\left(Y\right)=-3Y$$
76	16 8 4 17 9 21 24 55 13	evls1scafv	$$⊢\phi \to \left({ℂ}_{\mathrm{fld}}{\mathrm{evalSub}}_1\mathbb{Q}\right)\left(K\left(1\right)\right)\left(Y\right)=1$$
77	75 76	oveq12d	$$⊢\phi \to \left({ℂ}_{\mathrm{fld}}{\mathrm{evalSub}}_1\mathbb{Q}\right)\left(K\left(-3\right)\underset{\dot{}}{·}X\right)\left(Y\right)+\left({ℂ}_{\mathrm{fld}}{\mathrm{evalSub}}_1\mathbb{Q}\right)\left(K\left(1\right)\right)\left(Y\right)=-3Y+1$$
78	70 77	eqtrd	$$⊢\phi \to \left({ℂ}_{\mathrm{fld}}{\mathrm{evalSub}}_1\mathbb{Q}\right)\left(\left(K\left(-3\right)\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}K\left(1\right)\right)\left(Y\right)=-3Y+1$$
79	69 78	oveq12d	$$⊢\phi \to \left({ℂ}_{\mathrm{fld}}{\mathrm{evalSub}}_1\mathbb{Q}\right)\left(3\underset{\dot{}}{\times }X\right)\left(Y\right)+\left({ℂ}_{\mathrm{fld}}{\mathrm{evalSub}}_1\mathbb{Q}\right)\left(\left(K\left(-3\right)\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}K\left(1\right)\right)\left(Y\right)=Y^3+-3Y+1$$
80	58 79	eqtrd	$$⊢\phi \to \left({ℂ}_{\mathrm{fld}}{\mathrm{evalSub}}_1\mathbb{Q}\right)\left(\left(3\underset{\dot{}}{\times }X\right)\underset{\dot{}}{+}\left(\left(K\left(-3\right)\underset{\dot{}}{·}X\right)\underset{\dot{}}{+}K\left(1\right)\right)\right)\left(Y\right)=Y^3+-3Y+1$$
81	15 80	eqtrid	$$⊢\phi \to \left({ℂ}_{\mathrm{fld}}{\mathrm{evalSub}}_1\mathbb{Q}\right)\left(F\right)\left(Y\right)=Y^3+-3Y+1$$