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 = ( 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 ) ) )
	cos9thpiminplylem6.1	\|- ( ph -> Y e. CC )
Assertion	cos9thpiminplylem6	\|- ( ph -> ( ( ( CCfld evalSub1 QQ ) ` F ) ` Y ) = ( ( Y ^ 3 ) + ( ( -u 3 x. Y ) + 1 ) ) )

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		cos9thpiminplylem6.1	\|- ( ph -> Y e. CC )
14	12	fveq2i	\|- ( ( CCfld evalSub1 QQ ) ` F ) = ( ( CCfld evalSub1 QQ ) ` ( ( 3 .^ X ) .+ ( ( ( K ` -u 3 ) .x. X ) .+ ( K ` 1 ) ) ) )
15	14	fveq1i	\|- ( ( ( CCfld evalSub1 QQ ) ` F ) ` Y ) = ( ( ( CCfld evalSub1 QQ ) ` ( ( 3 .^ X ) .+ ( ( ( K ` -u 3 ) .x. X ) .+ ( K ` 1 ) ) ) ) ` Y )
16		eqid	\|- ( CCfld evalSub1 QQ ) = ( CCfld evalSub1 QQ )
17		cnfldbas	\|- CC = ( Base ` CCfld )
18		eqid	\|- ( Base ` P ) = ( Base ` P )
19		cnfldadd	\|- + = ( +g ` CCfld )
20		cncrng	\|- CCfld e. CRing
21	20	a1i	\|- ( ph -> CCfld e. CRing )
22		qsubdrg	\|- ( QQ e. ( SubRing ` CCfld ) /\ ( CCfld \|`s QQ ) e. DivRing )
23	22	simpli	\|- QQ e. ( SubRing ` CCfld )
24	23	a1i	\|- ( ph -> QQ e. ( SubRing ` CCfld ) )
25		eqid	\|- ( mulGrp ` P ) = ( mulGrp ` P )
26	25 18	mgpbas	\|- ( Base ` P ) = ( Base ` ( mulGrp ` P ) )
27	4	qdrng	\|- Q e. DivRing
28	27	a1i	\|- ( ph -> Q e. DivRing )
29	28	drngringd	\|- ( ph -> Q e. Ring )
30	8	ply1ring	\|- ( Q e. Ring -> P e. Ring )
31	29 30	syl	\|- ( ph -> P e. Ring )
32	25	ringmgp	\|- ( P e. Ring -> ( mulGrp ` P ) e. Mnd )
33	31 32	syl	\|- ( ph -> ( mulGrp ` P ) e. Mnd )
34		3nn0	\|- 3 e. NN0
35	34	a1i	\|- ( ph -> 3 e. NN0 )
36	10 8 18	vr1cl	\|- ( Q e. Ring -> X e. ( Base ` P ) )
37	29 36	syl	\|- ( ph -> X e. ( Base ` P ) )
38	26 7 33 35 37	mulgnn0cld	\|- ( ph -> ( 3 .^ X ) e. ( Base ` P ) )
39	31	ringgrpd	\|- ( ph -> P e. Grp )
40	8	ply1sca	\|- ( Q e. DivRing -> Q = ( Scalar ` P ) )
41	27 40	ax-mp	\|- Q = ( Scalar ` P )
42	8	ply1lmod	\|- ( Q e. Ring -> P e. LMod )
43	29 42	syl	\|- ( ph -> P e. LMod )
44	4	qrngbas	\|- QQ = ( Base ` Q )
45	9 41 31 43 44 18	asclf	\|- ( ph -> K : QQ --> ( Base ` P ) )
46	35	nn0zd	\|- ( ph -> 3 e. ZZ )
47		zq	\|- ( 3 e. ZZ -> 3 e. QQ )
48	46 47	syl	\|- ( ph -> 3 e. QQ )
49		qnegcl	\|- ( 3 e. QQ -> -u 3 e. QQ )
50	48 49	syl	\|- ( ph -> -u 3 e. QQ )
51	45 50	ffvelcdmd	\|- ( ph -> ( K ` -u 3 ) e. ( Base ` P ) )
52	18 6 31 51 37	ringcld	\|- ( ph -> ( ( K ` -u 3 ) .x. X ) e. ( Base ` P ) )
53		1zzd	\|- ( ph -> 1 e. ZZ )
54		zq	\|- ( 1 e. ZZ -> 1 e. QQ )
55	53 54	syl	\|- ( ph -> 1 e. QQ )
56	45 55	ffvelcdmd	\|- ( ph -> ( K ` 1 ) e. ( Base ` P ) )
57	18 5 39 52 56	grpcld	\|- ( ph -> ( ( ( K ` -u 3 ) .x. X ) .+ ( K ` 1 ) ) e. ( Base ` P ) )
58	16 17 8 4 18 5 19 21 24 38 57 13	evls1addd	\|- ( ph -> ( ( ( CCfld evalSub1 QQ ) ` ( ( 3 .^ X ) .+ ( ( ( K ` -u 3 ) .x. X ) .+ ( K ` 1 ) ) ) ) ` Y ) = ( ( ( ( CCfld evalSub1 QQ ) ` ( 3 .^ X ) ) ` Y ) + ( ( ( CCfld evalSub1 QQ ) ` ( ( ( K ` -u 3 ) .x. X ) .+ ( K ` 1 ) ) ) ` Y ) ) )
59		eqid	\|- ( .g ` ( mulGrp ` CCfld ) ) = ( .g ` ( mulGrp ` CCfld ) )
60	16 17 8 4 18 21 24 7 59 35 37 13	evls1expd	\|- ( ph -> ( ( ( CCfld evalSub1 QQ ) ` ( 3 .^ X ) ) ` Y ) = ( 3 ( .g ` ( mulGrp ` CCfld ) ) ( ( ( CCfld evalSub1 QQ ) ` X ) ` Y ) ) )
61	16 10 4 17 21 24	evls1var	\|- ( ph -> ( ( CCfld evalSub1 QQ ) ` X ) = ( _I \|` CC ) )
62	61	fveq1d	\|- ( ph -> ( ( ( CCfld evalSub1 QQ ) ` X ) ` Y ) = ( ( _I \|` CC ) ` Y ) )
63		fvresi	\|- ( Y e. CC -> ( ( _I \|` CC ) ` Y ) = Y )
64	13 63	syl	\|- ( ph -> ( ( _I \|` CC ) ` Y ) = Y )
65	62 64	eqtrd	\|- ( ph -> ( ( ( CCfld evalSub1 QQ ) ` X ) ` Y ) = Y )
66	65	oveq2d	\|- ( ph -> ( 3 ( .g ` ( mulGrp ` CCfld ) ) ( ( ( CCfld evalSub1 QQ ) ` X ) ` Y ) ) = ( 3 ( .g ` ( mulGrp ` CCfld ) ) Y ) )
67		cnfldexp	\|- ( ( Y e. CC /\ 3 e. NN0 ) -> ( 3 ( .g ` ( mulGrp ` CCfld ) ) Y ) = ( Y ^ 3 ) )
68	13 34 67	sylancl	\|- ( ph -> ( 3 ( .g ` ( mulGrp ` CCfld ) ) Y ) = ( Y ^ 3 ) )
69	60 66 68	3eqtrd	\|- ( ph -> ( ( ( CCfld evalSub1 QQ ) ` ( 3 .^ X ) ) ` Y ) = ( Y ^ 3 ) )
70	16 17 8 4 18 5 19 21 24 52 56 13	evls1addd	\|- ( ph -> ( ( ( CCfld evalSub1 QQ ) ` ( ( ( K ` -u 3 ) .x. X ) .+ ( K ` 1 ) ) ) ` Y ) = ( ( ( ( CCfld evalSub1 QQ ) ` ( ( K ` -u 3 ) .x. X ) ) ` Y ) + ( ( ( CCfld evalSub1 QQ ) ` ( K ` 1 ) ) ` Y ) ) )
71		cnfldmul	\|- x. = ( .r ` CCfld )
72	16 17 8 4 18 6 71 21 24 51 37 13	evls1muld	\|- ( ph -> ( ( ( CCfld evalSub1 QQ ) ` ( ( K ` -u 3 ) .x. X ) ) ` Y ) = ( ( ( ( CCfld evalSub1 QQ ) ` ( K ` -u 3 ) ) ` Y ) x. ( ( ( CCfld evalSub1 QQ ) ` X ) ` Y ) ) )
73	16 8 4 17 9 21 24 50 13	evls1scafv	\|- ( ph -> ( ( ( CCfld evalSub1 QQ ) ` ( K ` -u 3 ) ) ` Y ) = -u 3 )
74	73 65	oveq12d	\|- ( ph -> ( ( ( ( CCfld evalSub1 QQ ) ` ( K ` -u 3 ) ) ` Y ) x. ( ( ( CCfld evalSub1 QQ ) ` X ) ` Y ) ) = ( -u 3 x. Y ) )
75	72 74	eqtrd	\|- ( ph -> ( ( ( CCfld evalSub1 QQ ) ` ( ( K ` -u 3 ) .x. X ) ) ` Y ) = ( -u 3 x. Y ) )
76	16 8 4 17 9 21 24 55 13	evls1scafv	\|- ( ph -> ( ( ( CCfld evalSub1 QQ ) ` ( K ` 1 ) ) ` Y ) = 1 )
77	75 76	oveq12d	\|- ( ph -> ( ( ( ( CCfld evalSub1 QQ ) ` ( ( K ` -u 3 ) .x. X ) ) ` Y ) + ( ( ( CCfld evalSub1 QQ ) ` ( K ` 1 ) ) ` Y ) ) = ( ( -u 3 x. Y ) + 1 ) )
78	70 77	eqtrd	\|- ( ph -> ( ( ( CCfld evalSub1 QQ ) ` ( ( ( K ` -u 3 ) .x. X ) .+ ( K ` 1 ) ) ) ` Y ) = ( ( -u 3 x. Y ) + 1 ) )
79	69 78	oveq12d	\|- ( ph -> ( ( ( ( CCfld evalSub1 QQ ) ` ( 3 .^ X ) ) ` Y ) + ( ( ( CCfld evalSub1 QQ ) ` ( ( ( K ` -u 3 ) .x. X ) .+ ( K ` 1 ) ) ) ` Y ) ) = ( ( Y ^ 3 ) + ( ( -u 3 x. Y ) + 1 ) ) )
80	58 79	eqtrd	\|- ( ph -> ( ( ( CCfld evalSub1 QQ ) ` ( ( 3 .^ X ) .+ ( ( ( K ` -u 3 ) .x. X ) .+ ( K ` 1 ) ) ) ) ` Y ) = ( ( Y ^ 3 ) + ( ( -u 3 x. Y ) + 1 ) ) )
81	15 80	eqtrid	\|- ( ph -> ( ( ( CCfld evalSub1 QQ ) ` F ) ` Y ) = ( ( Y ^ 3 ) + ( ( -u 3 x. Y ) + 1 ) ) )

Metamath Proof Explorer

Theorem cos9thpiminplylem6

Proof