Theorem cos9thpiminplylem6 33983

Description: Evaluation of the polynomial ((𝑋↑3) + ((-3 · 𝑋) + 1)). (Contributed by Thierry Arnoux, 14-Nov-2025.)

Hypotheses

Ref	Expression
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

Ref	Expression
cos9thpiminplylem6	⊢ (𝜑 → (((ℂfld evalSub1 ℚ)‘𝐹)‘𝑌) = ((𝑌↑3) + ((-3 · 𝑌) + 1)))

Proof of Theorem cos9thpiminplylem6

Step	Hyp	Ref	Expression
1		cos9thpiminply.f	. . . 4 ⊢ 𝐹 = ((3 ↑ 𝑋) + (((𝐾‘-3) · 𝑋) + (𝐾‘1)))
2	1	fveq2i 6834	. . 3 ⊢ ((ℂfld evalSub1 ℚ)‘𝐹) = ((ℂfld evalSub1 ℚ)‘((3 ↑ 𝑋) + (((𝐾‘-3) · 𝑋) + (𝐾‘1))))
3	2	fveq1i 6832	. 2 ⊢ (((ℂfld evalSub1 ℚ)‘𝐹)‘𝑌) = (((ℂfld evalSub1 ℚ)‘((3 ↑ 𝑋) + (((𝐾‘-3) · 𝑋) + (𝐾‘1))))‘𝑌)
4		eqid 2741	. . . 4 ⊢ (ℂfld evalSub1 ℚ) = (ℂfld evalSub1 ℚ)
5		cnfldbas 21355	. . . 4 ⊢ ℂ = (Base‘ℂfld)
6		cos9thpiminply.p	. . . 4 ⊢ 𝑃 = (Poly1‘𝑄)
7		cos9thpiminply.q	. . . 4 ⊢ 𝑄 = (ℂfld ↾s ℚ)
8		eqid 2741	. . . 4 ⊢ (Base‘𝑃) = (Base‘𝑃)
9		cos9thpiminply.4	. . . 4 ⊢ + = (+g‘𝑃)
10		cnfldadd 21357	. . . 4 ⊢ + = (+g‘ℂfld)
11		cncrng 21372	. . . . 5 ⊢ ℂfld ∈ CRing
12	11	a1i 11	. . . 4 ⊢ (𝜑 → ℂfld ∈ CRing)
13		qsubdrg 21398	. . . . . 6 ⊢ (ℚ ∈ (SubRing‘ℂfld) ∧ (ℂfld ↾s ℚ) ∈ DivRing)
14	13	simpli 485	. . . . 5 ⊢ ℚ ∈ (SubRing‘ℂfld)
15	14	a1i 11	. . . 4 ⊢ (𝜑 → ℚ ∈ (SubRing‘ℂfld))
16		eqid 2741	. . . . . 6 ⊢ (mulGrp‘𝑃) = (mulGrp‘𝑃)
17	16, 8	mgpbas 20121	. . . . 5 ⊢ (Base‘𝑃) = (Base‘(mulGrp‘𝑃))
18		cos9thpiminply.6	. . . . 5 ⊢ ↑ = (.g‘(mulGrp‘𝑃))
19	7	qdrng 27605	. . . . . . . . 9 ⊢ 𝑄 ∈ DivRing
20	19	a1i 11	. . . . . . . 8 ⊢ (𝜑 → 𝑄 ∈ DivRing)
21	20	drngringd 20713	. . . . . . 7 ⊢ (𝜑 → 𝑄 ∈ Ring)
22	6	ply1ring 22236	. . . . . . 7 ⊢ (𝑄 ∈ Ring → 𝑃 ∈ Ring)
23	21, 22	syl 17	. . . . . 6 ⊢ (𝜑 → 𝑃 ∈ Ring)
24	16	ringmgp 20215	. . . . . 6 ⊢ (𝑃 ∈ Ring → (mulGrp‘𝑃) ∈ Mnd)
25	23, 24	syl 17	. . . . 5 ⊢ (𝜑 → (mulGrp‘𝑃) ∈ Mnd)
26		3nn0 12450	. . . . . 6 ⊢ 3 ∈ ℕ0
27	26	a1i 11	. . . . 5 ⊢ (𝜑 → 3 ∈ ℕ0)
28		cos9thpiminply.x	. . . . . . 7 ⊢ 𝑋 = (var1‘𝑄)
29	28, 6, 8	vr1cl 22206	. . . . . 6 ⊢ (𝑄 ∈ Ring → 𝑋 ∈ (Base‘𝑃))
30	21, 29	syl 17	. . . . 5 ⊢ (𝜑 → 𝑋 ∈ (Base‘𝑃))
31	17, 18, 25, 27, 30	mulgnn0cld 19066	. . . 4 ⊢ (𝜑 → (3 ↑ 𝑋) ∈ (Base‘𝑃))
32	23	ringgrpd 20218	. . . . 5 ⊢ (𝜑 → 𝑃 ∈ Grp)
33		cos9thpiminply.5	. . . . . 6 ⊢ · = (.r‘𝑃)
34		cos9thpiminply.k	. . . . . . . 8 ⊢ 𝐾 = (algSc‘𝑃)
35	6	ply1sca 22241	. . . . . . . . 9 ⊢ (𝑄 ∈ DivRing → 𝑄 = (Scalar‘𝑃))
36	19, 35	ax-mp 5	. . . . . . . 8 ⊢ 𝑄 = (Scalar‘𝑃)
37	6	ply1lmod 22240	. . . . . . . . 9 ⊢ (𝑄 ∈ Ring → 𝑃 ∈ LMod)
38	21, 37	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝑃 ∈ LMod)
39	7	qrngbas 27604	. . . . . . . 8 ⊢ ℚ = (Base‘𝑄)
40	34, 36, 23, 38, 39, 8	asclf 21860	. . . . . . 7 ⊢ (𝜑 → 𝐾:ℚ⟶(Base‘𝑃))
41	27	nn0zd 12544	. . . . . . . . 9 ⊢ (𝜑 → 3 ∈ ℤ)
42		zq 12899	. . . . . . . . 9 ⊢ (3 ∈ ℤ → 3 ∈ ℚ)
43	41, 42	syl 17	. . . . . . . 8 ⊢ (𝜑 → 3 ∈ ℚ)
44		qnegcl 12911	. . . . . . . 8 ⊢ (3 ∈ ℚ → -3 ∈ ℚ)
45	43, 44	syl 17	. . . . . . 7 ⊢ (𝜑 → -3 ∈ ℚ)
46	40, 45	ffvelcdmd 7030	. . . . . 6 ⊢ (𝜑 → (𝐾‘-3) ∈ (Base‘𝑃))
47	8, 33, 23, 46, 30	ringcld 20236	. . . . 5 ⊢ (𝜑 → ((𝐾‘-3) · 𝑋) ∈ (Base‘𝑃))
48		1zzd 12553	. . . . . . 7 ⊢ (𝜑 → 1 ∈ ℤ)
49		zq 12899	. . . . . . 7 ⊢ (1 ∈ ℤ → 1 ∈ ℚ)
50	48, 49	syl 17	. . . . . 6 ⊢ (𝜑 → 1 ∈ ℚ)
51	40, 50	ffvelcdmd 7030	. . . . 5 ⊢ (𝜑 → (𝐾‘1) ∈ (Base‘𝑃))
52	8, 9, 32, 47, 51	grpcld 18918	. . . 4 ⊢ (𝜑 → (((𝐾‘-3) · 𝑋) + (𝐾‘1)) ∈ (Base‘𝑃))
53		cos9thpiminplylem6.1	. . . 4 ⊢ (𝜑 → 𝑌 ∈ ℂ)
54	4, 5, 6, 7, 8, 9, 10, 12, 15, 31, 52, 53	evls1addd 22361	. . 3 ⊢ (𝜑 → (((ℂfld evalSub1 ℚ)‘((3 ↑ 𝑋) + (((𝐾‘-3) · 𝑋) + (𝐾‘1))))‘𝑌) = ((((ℂfld evalSub1 ℚ)‘(3 ↑ 𝑋))‘𝑌) + (((ℂfld evalSub1 ℚ)‘(((𝐾‘-3) · 𝑋) + (𝐾‘1)))‘𝑌)))
55		eqid 2741	. . . . . 6 ⊢ (.g‘(mulGrp‘ℂfld)) = (.g‘(mulGrp‘ℂfld))
56	4, 5, 6, 7, 8, 12, 15, 18, 55, 27, 30, 53	evls1expd 22357	. . . . 5 ⊢ (𝜑 → (((ℂfld evalSub1 ℚ)‘(3 ↑ 𝑋))‘𝑌) = (3(.g‘(mulGrp‘ℂfld))(((ℂfld evalSub1 ℚ)‘𝑋)‘𝑌)))
57	4, 28, 7, 5, 12, 15	evls1var 22328	. . . . . . . 8 ⊢ (𝜑 → ((ℂfld evalSub1 ℚ)‘𝑋) = ( I ↾ ℂ))
58	57	fveq1d 6833	. . . . . . 7 ⊢ (𝜑 → (((ℂfld evalSub1 ℚ)‘𝑋)‘𝑌) = (( I ↾ ℂ)‘𝑌))
59		fvresi 7121	. . . . . . . 8 ⊢ (𝑌 ∈ ℂ → (( I ↾ ℂ)‘𝑌) = 𝑌)
60	53, 59	syl 17	. . . . . . 7 ⊢ (𝜑 → (( I ↾ ℂ)‘𝑌) = 𝑌)
61	58, 60	eqtrd 2776	. . . . . 6 ⊢ (𝜑 → (((ℂfld evalSub1 ℚ)‘𝑋)‘𝑌) = 𝑌)
62	61	oveq2d 7376	. . . . 5 ⊢ (𝜑 → (3(.g‘(mulGrp‘ℂfld))(((ℂfld evalSub1 ℚ)‘𝑋)‘𝑌)) = (3(.g‘(mulGrp‘ℂfld))𝑌))
63		cnfldexp 21384	. . . . . 6 ⊢ ((𝑌 ∈ ℂ ∧ 3 ∈ ℕ0) → (3(.g‘(mulGrp‘ℂfld))𝑌) = (𝑌↑3))
64	53, 26, 63	sylancl 593	. . . . 5 ⊢ (𝜑 → (3(.g‘(mulGrp‘ℂfld))𝑌) = (𝑌↑3))
65	56, 62, 64	3eqtrd 2780	. . . 4 ⊢ (𝜑 → (((ℂfld evalSub1 ℚ)‘(3 ↑ 𝑋))‘𝑌) = (𝑌↑3))
66	4, 5, 6, 7, 8, 9, 10, 12, 15, 47, 51, 53	evls1addd 22361	. . . . 5 ⊢ (𝜑 → (((ℂfld evalSub1 ℚ)‘(((𝐾‘-3) · 𝑋) + (𝐾‘1)))‘𝑌) = ((((ℂfld evalSub1 ℚ)‘((𝐾‘-3) · 𝑋))‘𝑌) + (((ℂfld evalSub1 ℚ)‘(𝐾‘1))‘𝑌)))
67		cnfldmul 21359	. . . . . . . 8 ⊢ · = (.r‘ℂfld)
68	4, 5, 6, 7, 8, 33, 67, 12, 15, 46, 30, 53	evls1muld 22362	. . . . . . 7 ⊢ (𝜑 → (((ℂfld evalSub1 ℚ)‘((𝐾‘-3) · 𝑋))‘𝑌) = ((((ℂfld evalSub1 ℚ)‘(𝐾‘-3))‘𝑌) · (((ℂfld evalSub1 ℚ)‘𝑋)‘𝑌)))
69	4, 6, 7, 5, 34, 12, 15, 45, 53	evls1scafv 22356	. . . . . . . 8 ⊢ (𝜑 → (((ℂfld evalSub1 ℚ)‘(𝐾‘-3))‘𝑌) = -3)
70	69, 61	oveq12d 7378	. . . . . . 7 ⊢ (𝜑 → ((((ℂfld evalSub1 ℚ)‘(𝐾‘-3))‘𝑌) · (((ℂfld evalSub1 ℚ)‘𝑋)‘𝑌)) = (-3 · 𝑌))
71	68, 70	eqtrd 2776	. . . . . 6 ⊢ (𝜑 → (((ℂfld evalSub1 ℚ)‘((𝐾‘-3) · 𝑋))‘𝑌) = (-3 · 𝑌))
72	4, 6, 7, 5, 34, 12, 15, 50, 53	evls1scafv 22356	. . . . . 6 ⊢ (𝜑 → (((ℂfld evalSub1 ℚ)‘(𝐾‘1))‘𝑌) = 1)
73	71, 72	oveq12d 7378	. . . . 5 ⊢ (𝜑 → ((((ℂfld evalSub1 ℚ)‘((𝐾‘-3) · 𝑋))‘𝑌) + (((ℂfld evalSub1 ℚ)‘(𝐾‘1))‘𝑌)) = ((-3 · 𝑌) + 1))
74	66, 73	eqtrd 2776	. . . 4 ⊢ (𝜑 → (((ℂfld evalSub1 ℚ)‘(((𝐾‘-3) · 𝑋) + (𝐾‘1)))‘𝑌) = ((-3 · 𝑌) + 1))
75	65, 74	oveq12d 7378	. . 3 ⊢ (𝜑 → ((((ℂfld evalSub1 ℚ)‘(3 ↑ 𝑋))‘𝑌) + (((ℂfld evalSub1 ℚ)‘(((𝐾‘-3) · 𝑋) + (𝐾‘1)))‘𝑌)) = ((𝑌↑3) + ((-3 · 𝑌) + 1)))
76	54, 75	eqtrd 2776	. 2 ⊢ (𝜑 → (((ℂfld evalSub1 ℚ)‘((3 ↑ 𝑋) + (((𝐾‘-3) · 𝑋) + (𝐾‘1))))‘𝑌) = ((𝑌↑3) + ((-3 · 𝑌) + 1)))
77	3, 76	eqtrid 2788	1 ⊢ (𝜑 → (((ℂfld evalSub1 ℚ)‘𝐹)‘𝑌) = ((𝑌↑3) + ((-3 · 𝑌) + 1)))

Syntax hints:   → wi 4   = wceq 1548   ∈ wcel 2121   I cid 5515   ↾ cres 5623  ‘cfv 6489  (class class class)co 7360  ℂcc 11031  1c1 11034  ici 11035   + caddc 11036   · cmul 11038  -cneg 11373   / cdiv 11802  2c2 12231  3c3 12232  ℕ₀cn0 12432  ℤcz 12519  ℚcq 12893  ↑cexp 14018  expce 16021  πcpi 16026  Basecbs 17174   ↾_s cress 17195  +_gcplusg 17215  ._rcmulr 17216  Scalarcsca 17218  Mndcmnd 18697  ._gcmg 19038  mulGrpcmgp 20116  Ringcrg 20209  CRingccrg 20210  SubRingcsubrg 20545  DivRingcdr 20705  LModclmod 20854  ℂ_fldccnfld 21351  algSccascl 21831  var₁cv1 22165  Poly₁cpl1 22166   evalSub₁ ces1 22303  deg₁cdg1 26041  ↑_𝑐ccxp 26541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-10 2154  ax-11 2170  ax-12 2191  ax-ext 2713  ax-rep 5202  ax-sep 5221  ax-nul 5231  ax-pow 5297  ax-pr 5365  ax-un 7682  ax-cnex 11089  ax-resscn 11090  ax-1cn 11091  ax-icn 11092  ax-addcl 11093  ax-addrcl 11094  ax-mulcl 11095  ax-mulrcl 11096  ax-mulcom 11097  ax-addass 11098  ax-mulass 11099  ax-distr 11100  ax-i2m1 11101  ax-1ne0 11102  ax-1rid 11103  ax-rnegex 11104  ax-rrecex 11105  ax-cnre 11106  ax-pre-lttri 11107  ax-pre-lttrn 11108  ax-pre-ltadd 11109  ax-pre-mulgt0 11110  ax-addf 11112  ax-mulf 11113

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-3or 1094  df-3an 1095  df-tru 1551  df-fal 1561  df-ex 1788  df-nf 1792  df-sb 2075  df-mo 2545  df-eu 2575  df-clab 2720  df-cleq 2733  df-clel 2816  df-nfc 2890  df-ne 2937  df-nel 3041  df-ral 3056  df-rex 3066  df-rmo 3346  df-reu 3347  df-rab 3394  df-v 3435  df-sbc 3726  df-csb 3834  df-dif 3888  df-un 3890  df-in 3892  df-ss 3902  df-pss 3905  df-nul 4265  df-if 4458  df-pw 4534  df-sn 4559  df-pr 4561  df-tp 4563  df-op 4565  df-uni 4842  df-int 4881  df-iun 4926  df-iin 4927  df-br 5076  df-opab 5138  df-mpt 5157  df-tr 5183  df-id 5516  df-eprel 5521  df-po 5529  df-so 5530  df-fr 5574  df-se 5575  df-we 5576  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-pred 6256  df-ord 6317  df-on 6318  df-lim 6319  df-suc 6320  df-iota 6445  df-fun 6491  df-fn 6492  df-f 6493  df-f1 6494  df-fo 6495  df-f1o 6496  df-fv 6497  df-isom 6498  df-riota 7317  df-ov 7363  df-oprab 7364  df-mpo 7365  df-of 7624  df-ofr 7625  df-om 7811  df-1st 7935  df-2nd 7936  df-supp 8105  df-tpos 8170  df-frecs 8225  df-wrecs 8256  df-recs 8305  df-rdg 8343  df-1o 8399  df-2o 8400  df-er 8637  df-map 8769  df-pm 8770  df-ixp 8840  df-en 8888  df-dom 8889  df-sdom 8890  df-fin 8891  df-fsupp 9269  df-sup 9349  df-oi 9419  df-card 9858  df-pnf 11176  df-mnf 11177  df-xr 11178  df-ltxr 11179  df-le 11180  df-sub 11374  df-neg 11375  df-div 11803  df-nn 12170  df-2 12239  df-3 12240  df-4 12241  df-5 12242  df-6 12243  df-7 12244  df-8 12245  df-9 12246  df-n0 12433  df-z 12520  df-dec 12640  df-uz 12784  df-q 12894  df-fz 13457  df-fzo 13604  df-seq 13959  df-exp 14019  df-hash 14288  df-struct 17112  df-sets 17129  df-slot 17147  df-ndx 17159  df-base 17175  df-ress 17196  df-plusg 17228  df-mulr 17229  df-starv 17230  df-sca 17231  df-vsca 17232  df-ip 17233  df-tset 17234  df-ple 17235  df-ds 17237  df-unif 17238  df-hom 17239  df-cco 17240  df-0g 17399  df-gsum 17400  df-prds 17405  df-pws 17407  df-mre 17543  df-mrc 17544  df-acs 17546  df-mgm 18603  df-sgrp 18682  df-mnd 18698  df-mhm 18746  df-submnd 18747  df-grp 18907  df-minusg 18908  df-sbg 18909  df-mulg 19039  df-subg 19094  df-ghm 19183  df-cntz 19287  df-cmn 19752  df-abl 19753  df-mgp 20117  df-rng 20129  df-ur 20158  df-srg 20163  df-ring 20211  df-cring 20212  df-oppr 20312  df-dvdsr 20332  df-unit 20333  df-invr 20363  df-dvr 20376  df-rhm 20447  df-subrng 20522  df-subrg 20546  df-drng 20707  df-lmod 20856  df-lss 20926  df-lsp 20966  df-cnfld 21352  df-assa 21832  df-asp 21833  df-ascl 21834  df-psr 21888  df-mvr 21889  df-mpl 21890  df-opsr 21892  df-evls 22054  df-evl 22055  df-psr1 22169  df-vr1 22170  df-ply1 22171  df-coe1 22172  df-evls1 22305  df-evl1 22306

This theorem is referenced by:  cos9thpiminply  33984