Theorem gsummoncoe1fzo

Description: A coefficient of the polynomial represented as a sum of scaled monomials is the coefficient of the corresponding scaled monomial. (Contributed by Thierry Arnoux, 20-Feb-2025)

	Ref	Expression
Hypotheses	gsummoncoe1fzo.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
	gsummoncoe1fzo.b	$$⊢B={\mathrm{Base}}_P$$
	gsummoncoe1fzo.x	$$⊢X={\mathrm{var}}_1\left(R\right)$$
	gsummoncoe1fzo.e	$$⊢\underset{\dot{}}{\times }={\cdot }_{{\mathrm{mulGrp}}_P}$$
	gsummoncoe1fzo.r	$$⊢\phi \to R\in \mathrm{Ring}$$
	gsummoncoe1fzo.k	$$⊢K={\mathrm{Base}}_R$$
	gsummoncoe1fzo.m	$$⊢\underset{\dot{}}{\ast }={\cdot }_P$$
	gsummoncoe1fzo.1	$$⊢\underset{\dot{}}{0}=0_R$$
	gsummoncoe1fzo.a	$$⊢\phi \to \forall k\in \left(0..^N\right)A\in K$$
	gsummoncoe1fzo.l	$$⊢\phi \to L\in \left(0..^N\right)$$
	gsummoncoe1fzo.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
	gsummoncoe1fzo.2	$$⊢k=L\to A=C$$
Assertion	gsummoncoe1fzo	$$⊢\phi \to {\mathrm{coe}}_1\left(\underset{k\in \left(0..^N\right)}{{\sum }_P}\left(A\underset{\dot{}}{\ast }\left(k\underset{\dot{}}{\times }X\right)\right)\right)\left(L\right)=C$$

Proof

Step	Hyp	Ref	Expression
1		gsummoncoe1fzo.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
2		gsummoncoe1fzo.b	$$⊢B={\mathrm{Base}}_P$$
3		gsummoncoe1fzo.x	$$⊢X={\mathrm{var}}_1\left(R\right)$$
4		gsummoncoe1fzo.e	$$⊢\underset{\dot{}}{\times }={\cdot }_{{\mathrm{mulGrp}}_P}$$
5		gsummoncoe1fzo.r	$$⊢\phi \to R\in \mathrm{Ring}$$
6		gsummoncoe1fzo.k	$$⊢K={\mathrm{Base}}_R$$
7		gsummoncoe1fzo.m	$$⊢\underset{\dot{}}{\ast }={\cdot }_P$$
8		gsummoncoe1fzo.1	$$⊢\underset{\dot{}}{0}=0_R$$
9		gsummoncoe1fzo.a	$$⊢\phi \to \forall k\in \left(0..^N\right)A\in K$$
10		gsummoncoe1fzo.l	$$⊢\phi \to L\in \left(0..^N\right)$$
11		gsummoncoe1fzo.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
12		gsummoncoe1fzo.2	$$⊢k=L\to A=C$$
13		eqid	$$⊢0_P=0_P$$
14	1	ply1ring	$$⊢R\in \mathrm{Ring}\to P\in \mathrm{Ring}$$
15	5 14	syl	$$⊢\phi \to P\in \mathrm{Ring}$$
16	15	ringcmnd	$$⊢\phi \to P\in \mathrm{CMnd}$$
17		nn0ex	$$⊢{\mathbb{N}}_0\in \mathrm{V}$$
18	17	a1i	$$⊢\phi \to {\mathbb{N}}_0\in \mathrm{V}$$
19		simpr	$$⊢\left(\phi \wedge k\in \left({\mathbb{N}}_0\setminus \left(0..^N\right)\right)\right)\to k\in \left({\mathbb{N}}_0\setminus \left(0..^N\right)\right)$$
20	19	eldifbd	$$⊢\left(\phi \wedge k\in \left({\mathbb{N}}_0\setminus \left(0..^N\right)\right)\right)\to \neg k\in \left(0..^N\right)$$
21	20	iffalsed	$$⊢\left(\phi \wedge k\in \left({\mathbb{N}}_0\setminus \left(0..^N\right)\right)\right)\to if\left(k\in \left(0..^N\right),A,\underset{\dot{}}{0}\right)=\underset{\dot{}}{0}$$
22	21	oveq1d	$$⊢\left(\phi \wedge k\in \left({\mathbb{N}}_0\setminus \left(0..^N\right)\right)\right)\to if\left(k\in \left(0..^N\right),A,\underset{\dot{}}{0}\right)\underset{\dot{}}{\ast }\left(k\underset{\dot{}}{\times }X\right)=\underset{\dot{}}{0}\underset{\dot{}}{\ast }\left(k\underset{\dot{}}{\times }X\right)$$
23	5	adantr	$$⊢\left(\phi \wedge k\in \left({\mathbb{N}}_0\setminus \left(0..^N\right)\right)\right)\to R\in \mathrm{Ring}$$
24	19	eldifad	$$⊢\left(\phi \wedge k\in \left({\mathbb{N}}_0\setminus \left(0..^N\right)\right)\right)\to k\in {\mathbb{N}}_0$$
25		eqid	$$⊢{\mathrm{mulGrp}}_P={\mathrm{mulGrp}}_P$$
26	25 2	mgpbas	$$⊢B={\mathrm{Base}}_{{\mathrm{mulGrp}}_P}$$
27	25	ringmgp	$$⊢P\in \mathrm{Ring}\to {\mathrm{mulGrp}}_P\in \mathrm{Mnd}$$
28	15 27	syl	$$⊢\phi \to {\mathrm{mulGrp}}_P\in \mathrm{Mnd}$$
29	28	adantr	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to {\mathrm{mulGrp}}_P\in \mathrm{Mnd}$$
30		simpr	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to k\in {\mathbb{N}}_0$$
31	3 1 2	vr1cl	$$⊢R\in \mathrm{Ring}\to X\in B$$
32	5 31	syl	$$⊢\phi \to X\in B$$
33	32	adantr	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to X\in B$$
34	26 4 29 30 33	mulgnn0cld	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to k\underset{\dot{}}{\times }X\in B$$
35	24 34	syldan	$$⊢\left(\phi \wedge k\in \left({\mathbb{N}}_0\setminus \left(0..^N\right)\right)\right)\to k\underset{\dot{}}{\times }X\in B$$
36	1 2 7 8	ply10s0	$$⊢\left(R\in \mathrm{Ring}\wedge k\underset{\dot{}}{\times }X\in B\right)\to \underset{\dot{}}{0}\underset{\dot{}}{\ast }\left(k\underset{\dot{}}{\times }X\right)=0_P$$
37	23 35 36	syl2anc	$$⊢\left(\phi \wedge k\in \left({\mathbb{N}}_0\setminus \left(0..^N\right)\right)\right)\to \underset{\dot{}}{0}\underset{\dot{}}{\ast }\left(k\underset{\dot{}}{\times }X\right)=0_P$$
38	22 37	eqtrd	$$⊢\left(\phi \wedge k\in \left({\mathbb{N}}_0\setminus \left(0..^N\right)\right)\right)\to if\left(k\in \left(0..^N\right),A,\underset{\dot{}}{0}\right)\underset{\dot{}}{\ast }\left(k\underset{\dot{}}{\times }X\right)=0_P$$
39		fzofi	$$⊢\left(0..^N\right)\in \mathrm{Fin}$$
40	39	a1i	$$⊢\phi \to \left(0..^N\right)\in \mathrm{Fin}$$
41	1	ply1lmod	$$⊢R\in \mathrm{Ring}\to P\in \mathrm{LMod}$$
42	5 41	syl	$$⊢\phi \to P\in \mathrm{LMod}$$
43	42	adantr	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to P\in \mathrm{LMod}$$
44	9	r19.21bi	$$⊢\left(\phi \wedge k\in \left(0..^N\right)\right)\to A\in K$$
45	44	adantlr	$$⊢\left(\left(\phi \wedge k\in {\mathbb{N}}_0\right)\wedge k\in \left(0..^N\right)\right)\to A\in K$$
46	6 8	ring0cl	$$⊢R\in \mathrm{Ring}\to \underset{\dot{}}{0}\in K$$
47	5 46	syl	$$⊢\phi \to \underset{\dot{}}{0}\in K$$
48	47	ad2antrr	$$⊢\left(\left(\phi \wedge k\in {\mathbb{N}}_0\right)\wedge \neg k\in \left(0..^N\right)\right)\to \underset{\dot{}}{0}\in K$$
49	45 48	ifclda	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to if\left(k\in \left(0..^N\right),A,\underset{\dot{}}{0}\right)\in K$$
50	1	ply1sca	$$⊢R\in \mathrm{Ring}\to R=\mathrm{Scalar}\left(P\right)$$
51	5 50	syl	$$⊢\phi \to R=\mathrm{Scalar}\left(P\right)$$
52	51	fveq2d	$$⊢\phi \to {\mathrm{Base}}_R={\mathrm{Base}}_{\mathrm{Scalar}\left(P\right)}$$
53	6 52	eqtrid	$$⊢\phi \to K={\mathrm{Base}}_{\mathrm{Scalar}\left(P\right)}$$
54	53	adantr	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to K={\mathrm{Base}}_{\mathrm{Scalar}\left(P\right)}$$
55	49 54	eleqtrd	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to if\left(k\in \left(0..^N\right),A,\underset{\dot{}}{0}\right)\in {\mathrm{Base}}_{\mathrm{Scalar}\left(P\right)}$$
56		eqid	$$⊢\mathrm{Scalar}\left(P\right)=\mathrm{Scalar}\left(P\right)$$
57		eqid	$$⊢{\mathrm{Base}}_{\mathrm{Scalar}\left(P\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left(P\right)}$$
58	2 56 7 57	lmodvscl	$$⊢\left(P\in \mathrm{LMod}\wedge if\left(k\in \left(0..^N\right),A,\underset{\dot{}}{0}\right)\in {\mathrm{Base}}_{\mathrm{Scalar}\left(P\right)}\wedge k\underset{\dot{}}{\times }X\in B\right)\to if\left(k\in \left(0..^N\right),A,\underset{\dot{}}{0}\right)\underset{\dot{}}{\ast }\left(k\underset{\dot{}}{\times }X\right)\in B$$
59	43 55 34 58	syl3anc	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to if\left(k\in \left(0..^N\right),A,\underset{\dot{}}{0}\right)\underset{\dot{}}{\ast }\left(k\underset{\dot{}}{\times }X\right)\in B$$
60		fzo0ssnn0	$$⊢\left(0..^N\right)\subseteq {\mathbb{N}}_0$$
61	60	a1i	$$⊢\phi \to \left(0..^N\right)\subseteq {\mathbb{N}}_0$$
62	2 13 16 18 38 40 59 61	gsummptres2	$$⊢\phi \to \underset{k\in {\mathbb{N}}_0}{{\sum }_P}\left(if\left(k\in \left(0..^N\right),A,\underset{\dot{}}{0}\right)\underset{\dot{}}{\ast }\left(k\underset{\dot{}}{\times }X\right)\right)=\underset{k\in \left(0..^N\right)}{{\sum }_P}\left(if\left(k\in \left(0..^N\right),A,\underset{\dot{}}{0}\right)\underset{\dot{}}{\ast }\left(k\underset{\dot{}}{\times }X\right)\right)$$
63		simpr	$$⊢\left(\phi \wedge k\in \left(0..^N\right)\right)\to k\in \left(0..^N\right)$$
64	63	iftrued	$$⊢\left(\phi \wedge k\in \left(0..^N\right)\right)\to if\left(k\in \left(0..^N\right),A,\underset{\dot{}}{0}\right)=A$$
65	64	oveq1d	$$⊢\left(\phi \wedge k\in \left(0..^N\right)\right)\to if\left(k\in \left(0..^N\right),A,\underset{\dot{}}{0}\right)\underset{\dot{}}{\ast }\left(k\underset{\dot{}}{\times }X\right)=A\underset{\dot{}}{\ast }\left(k\underset{\dot{}}{\times }X\right)$$
66	65	mpteq2dva	$$⊢\phi \to \left(k\in \left(0..^N\right)⟼if\left(k\in \left(0..^N\right),A,\underset{\dot{}}{0}\right)\underset{\dot{}}{\ast }\left(k\underset{\dot{}}{\times }X\right)\right)=\left(k\in \left(0..^N\right)⟼A\underset{\dot{}}{\ast }\left(k\underset{\dot{}}{\times }X\right)\right)$$
67	66	oveq2d	$$⊢\phi \to \underset{k\in \left(0..^N\right)}{{\sum }_P}\left(if\left(k\in \left(0..^N\right),A,\underset{\dot{}}{0}\right)\underset{\dot{}}{\ast }\left(k\underset{\dot{}}{\times }X\right)\right)=\underset{k\in \left(0..^N\right)}{{\sum }_P}\left(A\underset{\dot{}}{\ast }\left(k\underset{\dot{}}{\times }X\right)\right)$$
68	62 67	eqtrd	$$⊢\phi \to \underset{k\in {\mathbb{N}}_0}{{\sum }_P}\left(if\left(k\in \left(0..^N\right),A,\underset{\dot{}}{0}\right)\underset{\dot{}}{\ast }\left(k\underset{\dot{}}{\times }X\right)\right)=\underset{k\in \left(0..^N\right)}{{\sum }_P}\left(A\underset{\dot{}}{\ast }\left(k\underset{\dot{}}{\times }X\right)\right)$$
69	68	fveq2d	$$⊢\phi \to {\mathrm{coe}}_1\left(\underset{k\in {\mathbb{N}}_0}{{\sum }_P}\left(if\left(k\in \left(0..^N\right),A,\underset{\dot{}}{0}\right)\underset{\dot{}}{\ast }\left(k\underset{\dot{}}{\times }X\right)\right)\right)={\mathrm{coe}}_1\left(\underset{k\in \left(0..^N\right)}{{\sum }_P}\left(A\underset{\dot{}}{\ast }\left(k\underset{\dot{}}{\times }X\right)\right)\right)$$
70	69	fveq1d	$$⊢\phi \to {\mathrm{coe}}_1\left(\underset{k\in {\mathbb{N}}_0}{{\sum }_P}\left(if\left(k\in \left(0..^N\right),A,\underset{\dot{}}{0}\right)\underset{\dot{}}{\ast }\left(k\underset{\dot{}}{\times }X\right)\right)\right)\left(L\right)={\mathrm{coe}}_1\left(\underset{k\in \left(0..^N\right)}{{\sum }_P}\left(A\underset{\dot{}}{\ast }\left(k\underset{\dot{}}{\times }X\right)\right)\right)\left(L\right)$$
71	49	ralrimiva	$$⊢\phi \to \forall k\in {\mathbb{N}}_{0}if\left(k\in \left(0..^N\right),A,\underset{\dot{}}{0}\right)\in K$$
72		eqid	$$⊢\left(k\in {\mathbb{N}}_0⟼if\left(k\in \left(0..^N\right),A,\underset{\dot{}}{0}\right)\right)=\left(k\in {\mathbb{N}}_0⟼if\left(k\in \left(0..^N\right),A,\underset{\dot{}}{0}\right)\right)$$
73	72 18 40 44 47	mptiffisupp	$$⊢\phi \to {finSupp}_{\underset{\dot{}}{0}}\left(\left(k\in {\mathbb{N}}_0⟼if\left(k\in \left(0..^N\right),A,\underset{\dot{}}{0}\right)\right)\right)$$
74	60 10	sselid	$$⊢\phi \to L\in {\mathbb{N}}_0$$
75	1 2 3 4 5 6 7 8 71 73 74	gsummoncoe1	$$⊢\phi \to {\mathrm{coe}}_1\left(\underset{k\in {\mathbb{N}}_0}{{\sum }_P}\left(if\left(k\in \left(0..^N\right),A,\underset{\dot{}}{0}\right)\underset{\dot{}}{\ast }\left(k\underset{\dot{}}{\times }X\right)\right)\right)\left(L\right)=⦋L/k⦌if\left(k\in \left(0..^N\right),A,\underset{\dot{}}{0}\right)$$
76	70 75	eqtr3d	$$⊢\phi \to {\mathrm{coe}}_1\left(\underset{k\in \left(0..^N\right)}{{\sum }_P}\left(A\underset{\dot{}}{\ast }\left(k\underset{\dot{}}{\times }X\right)\right)\right)\left(L\right)=⦋L/k⦌if\left(k\in \left(0..^N\right),A,\underset{\dot{}}{0}\right)$$
77		eleq1	$$⊢k=L\to \left(k\in \left(0..^N\right)\leftrightarrow L\in \left(0..^N\right)\right)$$
78	77 12	ifbieq1d	$$⊢k=L\to if\left(k\in \left(0..^N\right),A,\underset{\dot{}}{0}\right)=if\left(L\in \left(0..^N\right),C,\underset{\dot{}}{0}\right)$$
79	78	adantl	$$⊢\left(\phi \wedge k=L\right)\to if\left(k\in \left(0..^N\right),A,\underset{\dot{}}{0}\right)=if\left(L\in \left(0..^N\right),C,\underset{\dot{}}{0}\right)$$
80	10 79	csbied	$$⊢\phi \to ⦋L/k⦌if\left(k\in \left(0..^N\right),A,\underset{\dot{}}{0}\right)=if\left(L\in \left(0..^N\right),C,\underset{\dot{}}{0}\right)$$
81	10	iftrued	$$⊢\phi \to if\left(L\in \left(0..^N\right),C,\underset{\dot{}}{0}\right)=C$$
82	76 80 81	3eqtrd	$$⊢\phi \to {\mathrm{coe}}_1\left(\underset{k\in \left(0..^N\right)}{{\sum }_P}\left(A\underset{\dot{}}{\ast }\left(k\underset{\dot{}}{\times }X\right)\right)\right)\left(L\right)=C$$