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	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	gsummoncoe1fzo.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
	gsummoncoe1fzo.x	⊢ 𝑋 = ( var1 ‘ 𝑅 )
	gsummoncoe1fzo.e	⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑃 ) )
	gsummoncoe1fzo.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
	gsummoncoe1fzo.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
	gsummoncoe1fzo.m	⊢ ∗ = ( ·𝑠 ‘ 𝑃 )
	gsummoncoe1fzo.1	⊢ 0 = ( 0g ‘ 𝑅 )
	gsummoncoe1fzo.a	⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 0 ..^ 𝑁 ) 𝐴 ∈ 𝐾 )
	gsummoncoe1fzo.l	⊢ ( 𝜑 → 𝐿 ∈ ( 0 ..^ 𝑁 ) )
	gsummoncoe1fzo.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
	gsummoncoe1fzo.2	⊢ ( 𝑘 = 𝐿 → 𝐴 = 𝐶 )
Assertion	gsummoncoe1fzo	⊢ ( 𝜑 → ( ( coe1 ‘ ( 𝑃 Σg ( 𝑘 ∈ ( 0 ..^ 𝑁 ) ↦ ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) ) ‘ 𝐿 ) = 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		gsummoncoe1fzo.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2		gsummoncoe1fzo.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
3		gsummoncoe1fzo.x	⊢ 𝑋 = ( var1 ‘ 𝑅 )
4		gsummoncoe1fzo.e	⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑃 ) )
5		gsummoncoe1fzo.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
6		gsummoncoe1fzo.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
7		gsummoncoe1fzo.m	⊢ ∗ = ( ·𝑠 ‘ 𝑃 )
8		gsummoncoe1fzo.1	⊢ 0 = ( 0g ‘ 𝑅 )
9		gsummoncoe1fzo.a	⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 0 ..^ 𝑁 ) 𝐴 ∈ 𝐾 )
10		gsummoncoe1fzo.l	⊢ ( 𝜑 → 𝐿 ∈ ( 0 ..^ 𝑁 ) )
11		gsummoncoe1fzo.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
12		gsummoncoe1fzo.2	⊢ ( 𝑘 = 𝐿 → 𝐴 = 𝐶 )
13		eqid	⊢ ( 0g ‘ 𝑃 ) = ( 0g ‘ 𝑃 )
14	1	ply1ring	⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ Ring )
15	5 14	syl	⊢ ( 𝜑 → 𝑃 ∈ Ring )
16	15	ringcmnd	⊢ ( 𝜑 → 𝑃 ∈ CMnd )
17		nn0ex	⊢ ℕ0 ∈ V
18	17	a1i	⊢ ( 𝜑 → ℕ0 ∈ V )
19		simpr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℕ0 ∖ ( 0 ..^ 𝑁 ) ) ) → 𝑘 ∈ ( ℕ0 ∖ ( 0 ..^ 𝑁 ) ) )
20	19	eldifbd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℕ0 ∖ ( 0 ..^ 𝑁 ) ) ) → ¬ 𝑘 ∈ ( 0 ..^ 𝑁 ) )
21	20	iffalsed	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℕ0 ∖ ( 0 ..^ 𝑁 ) ) ) → if ( 𝑘 ∈ ( 0 ..^ 𝑁 ) , 𝐴 , 0 ) = 0 )
22	21	oveq1d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℕ0 ∖ ( 0 ..^ 𝑁 ) ) ) → ( if ( 𝑘 ∈ ( 0 ..^ 𝑁 ) , 𝐴 , 0 ) ∗ ( 𝑘 ↑ 𝑋 ) ) = ( 0 ∗ ( 𝑘 ↑ 𝑋 ) ) )
23	5	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℕ0 ∖ ( 0 ..^ 𝑁 ) ) ) → 𝑅 ∈ Ring )
24	19	eldifad	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℕ0 ∖ ( 0 ..^ 𝑁 ) ) ) → 𝑘 ∈ ℕ0 )
25		eqid	⊢ ( mulGrp ‘ 𝑃 ) = ( mulGrp ‘ 𝑃 )
26	25 2	mgpbas	⊢ 𝐵 = ( Base ‘ ( mulGrp ‘ 𝑃 ) )
27	25	ringmgp	⊢ ( 𝑃 ∈ Ring → ( mulGrp ‘ 𝑃 ) ∈ Mnd )
28	15 27	syl	⊢ ( 𝜑 → ( mulGrp ‘ 𝑃 ) ∈ Mnd )
29	28	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( mulGrp ‘ 𝑃 ) ∈ Mnd )
30		simpr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 𝑘 ∈ ℕ0 )
31	3 1 2	vr1cl	⊢ ( 𝑅 ∈ Ring → 𝑋 ∈ 𝐵 )
32	5 31	syl	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
33	32	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 𝑋 ∈ 𝐵 )
34	26 4 29 30 33	mulgnn0cld	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝑘 ↑ 𝑋 ) ∈ 𝐵 )
35	24 34	syldan	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℕ0 ∖ ( 0 ..^ 𝑁 ) ) ) → ( 𝑘 ↑ 𝑋 ) ∈ 𝐵 )
36	1 2 7 8	ply10s0	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑘 ↑ 𝑋 ) ∈ 𝐵 ) → ( 0 ∗ ( 𝑘 ↑ 𝑋 ) ) = ( 0g ‘ 𝑃 ) )
37	23 35 36	syl2anc	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℕ0 ∖ ( 0 ..^ 𝑁 ) ) ) → ( 0 ∗ ( 𝑘 ↑ 𝑋 ) ) = ( 0g ‘ 𝑃 ) )
38	22 37	eqtrd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℕ0 ∖ ( 0 ..^ 𝑁 ) ) ) → ( if ( 𝑘 ∈ ( 0 ..^ 𝑁 ) , 𝐴 , 0 ) ∗ ( 𝑘 ↑ 𝑋 ) ) = ( 0g ‘ 𝑃 ) )
39		fzofi	⊢ ( 0 ..^ 𝑁 ) ∈ Fin
40	39	a1i	⊢ ( 𝜑 → ( 0 ..^ 𝑁 ) ∈ Fin )
41	1	ply1lmod	⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ LMod )
42	5 41	syl	⊢ ( 𝜑 → 𝑃 ∈ LMod )
43	42	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 𝑃 ∈ LMod )
44	9	r19.21bi	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → 𝐴 ∈ 𝐾 )
45	44	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → 𝐴 ∈ 𝐾 )
46	6 8	ring0cl	⊢ ( 𝑅 ∈ Ring → 0 ∈ 𝐾 )
47	5 46	syl	⊢ ( 𝜑 → 0 ∈ 𝐾 )
48	47	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) ∧ ¬ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → 0 ∈ 𝐾 )
49	45 48	ifclda	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → if ( 𝑘 ∈ ( 0 ..^ 𝑁 ) , 𝐴 , 0 ) ∈ 𝐾 )
50	1	ply1sca	⊢ ( 𝑅 ∈ Ring → 𝑅 = ( Scalar ‘ 𝑃 ) )
51	5 50	syl	⊢ ( 𝜑 → 𝑅 = ( Scalar ‘ 𝑃 ) )
52	51	fveq2d	⊢ ( 𝜑 → ( Base ‘ 𝑅 ) = ( Base ‘ ( Scalar ‘ 𝑃 ) ) )
53	6 52	eqtrid	⊢ ( 𝜑 → 𝐾 = ( Base ‘ ( Scalar ‘ 𝑃 ) ) )
54	53	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 𝐾 = ( Base ‘ ( Scalar ‘ 𝑃 ) ) )
55	49 54	eleqtrd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → if ( 𝑘 ∈ ( 0 ..^ 𝑁 ) , 𝐴 , 0 ) ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) )
56		eqid	⊢ ( Scalar ‘ 𝑃 ) = ( Scalar ‘ 𝑃 )
57		eqid	⊢ ( Base ‘ ( Scalar ‘ 𝑃 ) ) = ( Base ‘ ( Scalar ‘ 𝑃 ) )
58	2 56 7 57	lmodvscl	⊢ ( ( 𝑃 ∈ LMod ∧ if ( 𝑘 ∈ ( 0 ..^ 𝑁 ) , 𝐴 , 0 ) ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∧ ( 𝑘 ↑ 𝑋 ) ∈ 𝐵 ) → ( if ( 𝑘 ∈ ( 0 ..^ 𝑁 ) , 𝐴 , 0 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ∈ 𝐵 )
59	43 55 34 58	syl3anc	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( if ( 𝑘 ∈ ( 0 ..^ 𝑁 ) , 𝐴 , 0 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ∈ 𝐵 )
60		fzo0ssnn0	⊢ ( 0 ..^ 𝑁 ) ⊆ ℕ0
61	60	a1i	⊢ ( 𝜑 → ( 0 ..^ 𝑁 ) ⊆ ℕ0 )
62	2 13 16 18 38 40 59 61	gsummptres2	⊢ ( 𝜑 → ( 𝑃 Σg ( 𝑘 ∈ ℕ0 ↦ ( if ( 𝑘 ∈ ( 0 ..^ 𝑁 ) , 𝐴 , 0 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) = ( 𝑃 Σg ( 𝑘 ∈ ( 0 ..^ 𝑁 ) ↦ ( if ( 𝑘 ∈ ( 0 ..^ 𝑁 ) , 𝐴 , 0 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) )
63		simpr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → 𝑘 ∈ ( 0 ..^ 𝑁 ) )
64	63	iftrued	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → if ( 𝑘 ∈ ( 0 ..^ 𝑁 ) , 𝐴 , 0 ) = 𝐴 )
65	64	oveq1d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ..^ 𝑁 ) ) → ( if ( 𝑘 ∈ ( 0 ..^ 𝑁 ) , 𝐴 , 0 ) ∗ ( 𝑘 ↑ 𝑋 ) ) = ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) )
66	65	mpteq2dva	⊢ ( 𝜑 → ( 𝑘 ∈ ( 0 ..^ 𝑁 ) ↦ ( if ( 𝑘 ∈ ( 0 ..^ 𝑁 ) , 𝐴 , 0 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ) = ( 𝑘 ∈ ( 0 ..^ 𝑁 ) ↦ ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) ) )
67	66	oveq2d	⊢ ( 𝜑 → ( 𝑃 Σg ( 𝑘 ∈ ( 0 ..^ 𝑁 ) ↦ ( if ( 𝑘 ∈ ( 0 ..^ 𝑁 ) , 𝐴 , 0 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) = ( 𝑃 Σg ( 𝑘 ∈ ( 0 ..^ 𝑁 ) ↦ ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) )
68	62 67	eqtrd	⊢ ( 𝜑 → ( 𝑃 Σg ( 𝑘 ∈ ℕ0 ↦ ( if ( 𝑘 ∈ ( 0 ..^ 𝑁 ) , 𝐴 , 0 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) = ( 𝑃 Σg ( 𝑘 ∈ ( 0 ..^ 𝑁 ) ↦ ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) )
69	68	fveq2d	⊢ ( 𝜑 → ( coe1 ‘ ( 𝑃 Σg ( 𝑘 ∈ ℕ0 ↦ ( if ( 𝑘 ∈ ( 0 ..^ 𝑁 ) , 𝐴 , 0 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) ) = ( coe1 ‘ ( 𝑃 Σg ( 𝑘 ∈ ( 0 ..^ 𝑁 ) ↦ ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) ) )
70	69	fveq1d	⊢ ( 𝜑 → ( ( coe1 ‘ ( 𝑃 Σg ( 𝑘 ∈ ℕ0 ↦ ( if ( 𝑘 ∈ ( 0 ..^ 𝑁 ) , 𝐴 , 0 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) ) ‘ 𝐿 ) = ( ( coe1 ‘ ( 𝑃 Σg ( 𝑘 ∈ ( 0 ..^ 𝑁 ) ↦ ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) ) ‘ 𝐿 ) )
71	49	ralrimiva	⊢ ( 𝜑 → ∀ 𝑘 ∈ ℕ0 if ( 𝑘 ∈ ( 0 ..^ 𝑁 ) , 𝐴 , 0 ) ∈ 𝐾 )
72		eqid	⊢ ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 ∈ ( 0 ..^ 𝑁 ) , 𝐴 , 0 ) ) = ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 ∈ ( 0 ..^ 𝑁 ) , 𝐴 , 0 ) )
73	72 18 40 44 47	mptiffisupp	⊢ ( 𝜑 → ( 𝑘 ∈ ℕ0 ↦ if ( 𝑘 ∈ ( 0 ..^ 𝑁 ) , 𝐴 , 0 ) ) finSupp 0 )
74	60 10	sselid	⊢ ( 𝜑 → 𝐿 ∈ ℕ0 )
75	1 2 3 4 5 6 7 8 71 73 74	gsummoncoe1	⊢ ( 𝜑 → ( ( coe1 ‘ ( 𝑃 Σg ( 𝑘 ∈ ℕ0 ↦ ( if ( 𝑘 ∈ ( 0 ..^ 𝑁 ) , 𝐴 , 0 ) ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) ) ‘ 𝐿 ) = ⦋ 𝐿 / 𝑘 ⦌ if ( 𝑘 ∈ ( 0 ..^ 𝑁 ) , 𝐴 , 0 ) )
76	70 75	eqtr3d	⊢ ( 𝜑 → ( ( coe1 ‘ ( 𝑃 Σg ( 𝑘 ∈ ( 0 ..^ 𝑁 ) ↦ ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) ) ‘ 𝐿 ) = ⦋ 𝐿 / 𝑘 ⦌ if ( 𝑘 ∈ ( 0 ..^ 𝑁 ) , 𝐴 , 0 ) )
77		eleq1	⊢ ( 𝑘 = 𝐿 → ( 𝑘 ∈ ( 0 ..^ 𝑁 ) ↔ 𝐿 ∈ ( 0 ..^ 𝑁 ) ) )
78	77 12	ifbieq1d	⊢ ( 𝑘 = 𝐿 → if ( 𝑘 ∈ ( 0 ..^ 𝑁 ) , 𝐴 , 0 ) = if ( 𝐿 ∈ ( 0 ..^ 𝑁 ) , 𝐶 , 0 ) )
79	78	adantl	⊢ ( ( 𝜑 ∧ 𝑘 = 𝐿 ) → if ( 𝑘 ∈ ( 0 ..^ 𝑁 ) , 𝐴 , 0 ) = if ( 𝐿 ∈ ( 0 ..^ 𝑁 ) , 𝐶 , 0 ) )
80	10 79	csbied	⊢ ( 𝜑 → ⦋ 𝐿 / 𝑘 ⦌ if ( 𝑘 ∈ ( 0 ..^ 𝑁 ) , 𝐴 , 0 ) = if ( 𝐿 ∈ ( 0 ..^ 𝑁 ) , 𝐶 , 0 ) )
81	10	iftrued	⊢ ( 𝜑 → if ( 𝐿 ∈ ( 0 ..^ 𝑁 ) , 𝐶 , 0 ) = 𝐶 )
82	76 80 81	3eqtrd	⊢ ( 𝜑 → ( ( coe1 ‘ ( 𝑃 Σg ( 𝑘 ∈ ( 0 ..^ 𝑁 ) ↦ ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) ) ‘ 𝐿 ) = 𝐶 )