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 = {Poly}_{1} (R)$
	gsummoncoe1fzo.b	$⊢ B = {Base}_{P}$
	gsummoncoe1fzo.x	$⊢ X = {var}_{1} (R)$
	gsummoncoe1fzo.e	$⊢ \underset{˙}{\times} = \cdot_{{mulGrp}_{P}}$
	gsummoncoe1fzo.r	$⊢ φ \to R \in Ring$
	gsummoncoe1fzo.k	$⊢ K = {Base}_{R}$
	gsummoncoe1fzo.m	$⊢ \underset{˙}{*} = \cdot_{P}$
	gsummoncoe1fzo.1	$⊢ \underset{˙}{0} = 0_{R}$
	gsummoncoe1fzo.a	$⊢ φ \to \forall k \in (0 ..^N) A \in K$
	gsummoncoe1fzo.l	$⊢ φ \to L \in (0 ..^N)$
	gsummoncoe1fzo.n	$⊢ φ \to N \in ℕ_{0}$
	gsummoncoe1fzo.2	$⊢ k = L \to A = C$
Assertion	gsummoncoe1fzo	$⊢ φ \to {coe}_{1} (\underset{k \in (0 ..^N)}{\sum_{P}} (A \underset{˙}{*} (k \underset{˙}{\times} X))) (L) = C$

Proof

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

Metamath Proof Explorer

Theorem gsummoncoe1fzo

Proof