Theorem gsumply1eq

Description: Two univariate polynomials given as (finitely supported) sum of scaled monomials are equal iff the corresponding coefficients are equal. (Contributed by AV, 21-Nov-2019)

	Ref	Expression
Hypotheses	gsumply1eq.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
	gsumply1eq.x	$$⊢X={\mathrm{var}}_1\left(R\right)$$
	gsumply1eq.e	$$⊢\underset{\dot{}}{\times }={\cdot }_{{\mathrm{mulGrp}}_P}$$
	gsumply1eq.r	$$⊢\phi \to R\in \mathrm{Ring}$$
	gsumply1eq.k	$$⊢K={\mathrm{Base}}_R$$
	gsumply1eq.m	$$⊢\underset{\dot{}}{\ast }={\cdot }_P$$
	gsumply1eq.0	$$⊢\underset{\dot{}}{0}=0_R$$
	gsumply1eq.a	$$⊢\phi \to \forall k\in {\mathbb{N}}_{0}A\in K$$
	gsumply1eq.f1	$$⊢\phi \to {finSupp}_{\underset{\dot{}}{0}}\left(\left(k\in {\mathbb{N}}_0⟼A\right)\right)$$
	gsumply1eq.b	$$⊢\phi \to \forall k\in {\mathbb{N}}_{0}B\in K$$
	gsumply1eq.f2	$$⊢\phi \to {finSupp}_{\underset{\dot{}}{0}}\left(\left(k\in {\mathbb{N}}_0⟼B\right)\right)$$
	gsumply1eq.o	$$⊢\phi \to O=\underset{k\in {\mathbb{N}}_0}{{\sum }_P}\left(A\underset{\dot{}}{\ast }\left(k\underset{\dot{}}{\times }X\right)\right)$$
	gsumply1eq.q	$$⊢\phi \to Q=\underset{k\in {\mathbb{N}}_0}{{\sum }_P}\left(B\underset{\dot{}}{\ast }\left(k\underset{\dot{}}{\times }X\right)\right)$$
Assertion	gsumply1eq	$$⊢\phi \to \left(O=Q\leftrightarrow \forall k\in {\mathbb{N}}_{0}A=B\right)$$

Proof

Step	Hyp	Ref	Expression
1		gsumply1eq.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
2		gsumply1eq.x	$$⊢X={\mathrm{var}}_1\left(R\right)$$
3		gsumply1eq.e	$$⊢\underset{\dot{}}{\times }={\cdot }_{{\mathrm{mulGrp}}_P}$$
4		gsumply1eq.r	$$⊢\phi \to R\in \mathrm{Ring}$$
5		gsumply1eq.k	$$⊢K={\mathrm{Base}}_R$$
6		gsumply1eq.m	$$⊢\underset{\dot{}}{\ast }={\cdot }_P$$
7		gsumply1eq.0	$$⊢\underset{\dot{}}{0}=0_R$$
8		gsumply1eq.a	$$⊢\phi \to \forall k\in {\mathbb{N}}_{0}A\in K$$
9		gsumply1eq.f1	$$⊢\phi \to {finSupp}_{\underset{\dot{}}{0}}\left(\left(k\in {\mathbb{N}}_0⟼A\right)\right)$$
10		gsumply1eq.b	$$⊢\phi \to \forall k\in {\mathbb{N}}_{0}B\in K$$
11		gsumply1eq.f2	$$⊢\phi \to {finSupp}_{\underset{\dot{}}{0}}\left(\left(k\in {\mathbb{N}}_0⟼B\right)\right)$$
12		gsumply1eq.o	$$⊢\phi \to O=\underset{k\in {\mathbb{N}}_0}{{\sum }_P}\left(A\underset{\dot{}}{\ast }\left(k\underset{\dot{}}{\times }X\right)\right)$$
13		gsumply1eq.q	$$⊢\phi \to Q=\underset{k\in {\mathbb{N}}_0}{{\sum }_P}\left(B\underset{\dot{}}{\ast }\left(k\underset{\dot{}}{\times }X\right)\right)$$
14		eqid	$$⊢{\mathrm{Base}}_P={\mathrm{Base}}_P$$
15	1 14 2 3 4 5 6 7 8 9	gsumsmonply1	$$⊢\phi \to \underset{k\in {\mathbb{N}}_0}{{\sum }_P}\left(A\underset{\dot{}}{\ast }\left(k\underset{\dot{}}{\times }X\right)\right)\in {\mathrm{Base}}_P$$
16	12 15	eqeltrd	$$⊢\phi \to O\in {\mathrm{Base}}_P$$
17	1 14 2 3 4 5 6 7 10 11	gsumsmonply1	$$⊢\phi \to \underset{k\in {\mathbb{N}}_0}{{\sum }_P}\left(B\underset{\dot{}}{\ast }\left(k\underset{\dot{}}{\times }X\right)\right)\in {\mathrm{Base}}_P$$
18	13 17	eqeltrd	$$⊢\phi \to Q\in {\mathrm{Base}}_P$$
19		eqid	$$⊢{\mathrm{coe}}_1\left(O\right)={\mathrm{coe}}_1\left(O\right)$$
20		eqid	$$⊢{\mathrm{coe}}_1\left(Q\right)={\mathrm{coe}}_1\left(Q\right)$$
21	1 14 19 20	ply1coe1eq	$$⊢\left(R\in \mathrm{Ring}\wedge O\in {\mathrm{Base}}_P\wedge Q\in {\mathrm{Base}}_P\right)\to \left(\forall k\in {\mathbb{N}}_0{\mathrm{coe}}_1\left(O\right)\left(k\right)={\mathrm{coe}}_1\left(Q\right)\left(k\right)\leftrightarrow O=Q\right)$$
22	21	bicomd	$$⊢\left(R\in \mathrm{Ring}\wedge O\in {\mathrm{Base}}_P\wedge Q\in {\mathrm{Base}}_P\right)\to \left(O=Q\leftrightarrow \forall k\in {\mathbb{N}}_0{\mathrm{coe}}_1\left(O\right)\left(k\right)={\mathrm{coe}}_1\left(Q\right)\left(k\right)\right)$$
23	4 16 18 22	syl3anc	$$⊢\phi \to \left(O=Q\leftrightarrow \forall k\in {\mathbb{N}}_0{\mathrm{coe}}_1\left(O\right)\left(k\right)={\mathrm{coe}}_1\left(Q\right)\left(k\right)\right)$$
24	12	adantr	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to O=\underset{k\in {\mathbb{N}}_0}{{\sum }_P}\left(A\underset{\dot{}}{\ast }\left(k\underset{\dot{}}{\times }X\right)\right)$$
25		nfcv	$$⊢\underset{\_}{Ⅎ}l\left(A\underset{\dot{}}{\ast }\left(k\underset{\dot{}}{\times }X\right)\right)$$
26		nfcsb1v	$$⊢\underset{\_}{Ⅎ}k⦋l/k⦌A$$
27		nfcv	$$⊢\underset{\_}{Ⅎ}k\underset{\dot{}}{\ast }$$
28		nfcv	$$⊢\underset{\_}{Ⅎ}k\left(l\underset{\dot{}}{\times }X\right)$$
29	26 27 28	nfov	$$⊢\underset{\_}{Ⅎ}k\left(⦋l/k⦌A\underset{\dot{}}{\ast }\left(l\underset{\dot{}}{\times }X\right)\right)$$
30		csbeq1a	$$⊢k=l\to A=⦋l/k⦌A$$
31		oveq1	$$⊢k=l\to k\underset{\dot{}}{\times }X=l\underset{\dot{}}{\times }X$$
32	30 31	oveq12d	$$⊢k=l\to A\underset{\dot{}}{\ast }\left(k\underset{\dot{}}{\times }X\right)=⦋l/k⦌A\underset{\dot{}}{\ast }\left(l\underset{\dot{}}{\times }X\right)$$
33	25 29 32	cbvmpt	$$⊢\left(k\in {\mathbb{N}}_0⟼A\underset{\dot{}}{\ast }\left(k\underset{\dot{}}{\times }X\right)\right)=\left(l\in {\mathbb{N}}_0⟼⦋l/k⦌A\underset{\dot{}}{\ast }\left(l\underset{\dot{}}{\times }X\right)\right)$$
34	33	oveq2i	$$⊢\underset{k\in {\mathbb{N}}_0}{{\sum }_P}\left(A\underset{\dot{}}{\ast }\left(k\underset{\dot{}}{\times }X\right)\right)=\underset{l\in {\mathbb{N}}_0}{{\sum }_P}\left(⦋l/k⦌A\underset{\dot{}}{\ast }\left(l\underset{\dot{}}{\times }X\right)\right)$$
35	24 34	eqtrdi	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to O=\underset{l\in {\mathbb{N}}_0}{{\sum }_P}\left(⦋l/k⦌A\underset{\dot{}}{\ast }\left(l\underset{\dot{}}{\times }X\right)\right)$$
36	35	fveq2d	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to {\mathrm{coe}}_1\left(O\right)={\mathrm{coe}}_1\left(\underset{l\in {\mathbb{N}}_0}{{\sum }_P}\left(⦋l/k⦌A\underset{\dot{}}{\ast }\left(l\underset{\dot{}}{\times }X\right)\right)\right)$$
37	36	fveq1d	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to {\mathrm{coe}}_1\left(O\right)\left(k\right)={\mathrm{coe}}_1\left(\underset{l\in {\mathbb{N}}_0}{{\sum }_P}\left(⦋l/k⦌A\underset{\dot{}}{\ast }\left(l\underset{\dot{}}{\times }X\right)\right)\right)\left(k\right)$$
38	4	adantr	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to R\in \mathrm{Ring}$$
39		nfv	$$⊢ℲlA\in K$$
40	26	nfel1	$$⊢Ⅎk⦋l/k⦌A\in K$$
41	30	eleq1d	$$⊢k=l\to \left(A\in K\leftrightarrow ⦋l/k⦌A\in K\right)$$
42	39 40 41	cbvralw	$$⊢\forall k\in {\mathbb{N}}_{0}A\in K\leftrightarrow \forall l\in {\mathbb{N}}_0⦋l/k⦌A\in K$$
43	8 42	sylib	$$⊢\phi \to \forall l\in {\mathbb{N}}_0⦋l/k⦌A\in K$$
44	43	adantr	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to \forall l\in {\mathbb{N}}_0⦋l/k⦌A\in K$$
45		nfcv	$$⊢\underset{\_}{Ⅎ}lA$$
46	45 26 30	cbvmpt	$$⊢\left(k\in {\mathbb{N}}_0⟼A\right)=\left(l\in {\mathbb{N}}_0⟼⦋l/k⦌A\right)$$
47	46 9	eqbrtrrid	$$⊢\phi \to {finSupp}_{\underset{\dot{}}{0}}\left(\left(l\in {\mathbb{N}}_0⟼⦋l/k⦌A\right)\right)$$
48	47	adantr	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to {finSupp}_{\underset{\dot{}}{0}}\left(\left(l\in {\mathbb{N}}_0⟼⦋l/k⦌A\right)\right)$$
49		simpr	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to k\in {\mathbb{N}}_0$$
50	1 14 2 3 38 5 6 7 44 48 49	gsummoncoe1	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to {\mathrm{coe}}_1\left(\underset{l\in {\mathbb{N}}_0}{{\sum }_P}\left(⦋l/k⦌A\underset{\dot{}}{\ast }\left(l\underset{\dot{}}{\times }X\right)\right)\right)\left(k\right)=⦋k/l⦌⦋l/k⦌A$$
51		csbcow	$$⊢⦋k/l⦌⦋l/k⦌A=⦋k/k⦌A$$
52		csbid	$$⊢⦋k/k⦌A=A$$
53	51 52	eqtri	$$⊢⦋k/l⦌⦋l/k⦌A=A$$
54	50 53	eqtrdi	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to {\mathrm{coe}}_1\left(\underset{l\in {\mathbb{N}}_0}{{\sum }_P}\left(⦋l/k⦌A\underset{\dot{}}{\ast }\left(l\underset{\dot{}}{\times }X\right)\right)\right)\left(k\right)=A$$
55	37 54	eqtrd	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to {\mathrm{coe}}_1\left(O\right)\left(k\right)=A$$
56	13	adantr	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to Q=\underset{k\in {\mathbb{N}}_0}{{\sum }_P}\left(B\underset{\dot{}}{\ast }\left(k\underset{\dot{}}{\times }X\right)\right)$$
57		nfcv	$$⊢\underset{\_}{Ⅎ}l\left(B\underset{\dot{}}{\ast }\left(k\underset{\dot{}}{\times }X\right)\right)$$
58		nfcsb1v	$$⊢\underset{\_}{Ⅎ}k⦋l/k⦌B$$
59	58 27 28	nfov	$$⊢\underset{\_}{Ⅎ}k\left(⦋l/k⦌B\underset{\dot{}}{\ast }\left(l\underset{\dot{}}{\times }X\right)\right)$$
60		csbeq1a	$$⊢k=l\to B=⦋l/k⦌B$$
61	60 31	oveq12d	$$⊢k=l\to B\underset{\dot{}}{\ast }\left(k\underset{\dot{}}{\times }X\right)=⦋l/k⦌B\underset{\dot{}}{\ast }\left(l\underset{\dot{}}{\times }X\right)$$
62	57 59 61	cbvmpt	$$⊢\left(k\in {\mathbb{N}}_0⟼B\underset{\dot{}}{\ast }\left(k\underset{\dot{}}{\times }X\right)\right)=\left(l\in {\mathbb{N}}_0⟼⦋l/k⦌B\underset{\dot{}}{\ast }\left(l\underset{\dot{}}{\times }X\right)\right)$$
63	62	a1i	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to \left(k\in {\mathbb{N}}_0⟼B\underset{\dot{}}{\ast }\left(k\underset{\dot{}}{\times }X\right)\right)=\left(l\in {\mathbb{N}}_0⟼⦋l/k⦌B\underset{\dot{}}{\ast }\left(l\underset{\dot{}}{\times }X\right)\right)$$
64	63	oveq2d	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to \underset{k\in {\mathbb{N}}_0}{{\sum }_P}\left(B\underset{\dot{}}{\ast }\left(k\underset{\dot{}}{\times }X\right)\right)=\underset{l\in {\mathbb{N}}_0}{{\sum }_P}\left(⦋l/k⦌B\underset{\dot{}}{\ast }\left(l\underset{\dot{}}{\times }X\right)\right)$$
65	56 64	eqtrd	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to Q=\underset{l\in {\mathbb{N}}_0}{{\sum }_P}\left(⦋l/k⦌B\underset{\dot{}}{\ast }\left(l\underset{\dot{}}{\times }X\right)\right)$$
66	65	fveq2d	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to {\mathrm{coe}}_1\left(Q\right)={\mathrm{coe}}_1\left(\underset{l\in {\mathbb{N}}_0}{{\sum }_P}\left(⦋l/k⦌B\underset{\dot{}}{\ast }\left(l\underset{\dot{}}{\times }X\right)\right)\right)$$
67	66	fveq1d	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to {\mathrm{coe}}_1\left(Q\right)\left(k\right)={\mathrm{coe}}_1\left(\underset{l\in {\mathbb{N}}_0}{{\sum }_P}\left(⦋l/k⦌B\underset{\dot{}}{\ast }\left(l\underset{\dot{}}{\times }X\right)\right)\right)\left(k\right)$$
68		nfv	$$⊢ℲlB\in K$$
69	58	nfel1	$$⊢Ⅎk⦋l/k⦌B\in K$$
70	60	eleq1d	$$⊢k=l\to \left(B\in K\leftrightarrow ⦋l/k⦌B\in K\right)$$
71	68 69 70	cbvralw	$$⊢\forall k\in {\mathbb{N}}_{0}B\in K\leftrightarrow \forall l\in {\mathbb{N}}_0⦋l/k⦌B\in K$$
72	10 71	sylib	$$⊢\phi \to \forall l\in {\mathbb{N}}_0⦋l/k⦌B\in K$$
73	72	adantr	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to \forall l\in {\mathbb{N}}_0⦋l/k⦌B\in K$$
74		nfcv	$$⊢\underset{\_}{Ⅎ}lB$$
75	74 58 60	cbvmpt	$$⊢\left(k\in {\mathbb{N}}_0⟼B\right)=\left(l\in {\mathbb{N}}_0⟼⦋l/k⦌B\right)$$
76	75 11	eqbrtrrid	$$⊢\phi \to {finSupp}_{\underset{\dot{}}{0}}\left(\left(l\in {\mathbb{N}}_0⟼⦋l/k⦌B\right)\right)$$
77	76	adantr	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to {finSupp}_{\underset{\dot{}}{0}}\left(\left(l\in {\mathbb{N}}_0⟼⦋l/k⦌B\right)\right)$$
78	1 14 2 3 38 5 6 7 73 77 49	gsummoncoe1	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to {\mathrm{coe}}_1\left(\underset{l\in {\mathbb{N}}_0}{{\sum }_P}\left(⦋l/k⦌B\underset{\dot{}}{\ast }\left(l\underset{\dot{}}{\times }X\right)\right)\right)\left(k\right)=⦋k/l⦌⦋l/k⦌B$$
79		csbcow	$$⊢⦋k/l⦌⦋l/k⦌B=⦋k/k⦌B$$
80		csbid	$$⊢⦋k/k⦌B=B$$
81	79 80	eqtri	$$⊢⦋k/l⦌⦋l/k⦌B=B$$
82	78 81	eqtrdi	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to {\mathrm{coe}}_1\left(\underset{l\in {\mathbb{N}}_0}{{\sum }_P}\left(⦋l/k⦌B\underset{\dot{}}{\ast }\left(l\underset{\dot{}}{\times }X\right)\right)\right)\left(k\right)=B$$
83	67 82	eqtrd	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to {\mathrm{coe}}_1\left(Q\right)\left(k\right)=B$$
84	55 83	eqeq12d	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to \left({\mathrm{coe}}_1\left(O\right)\left(k\right)={\mathrm{coe}}_1\left(Q\right)\left(k\right)\leftrightarrow A=B\right)$$
85	84	ralbidva	$$⊢\phi \to \left(\forall k\in {\mathbb{N}}_0{\mathrm{coe}}_1\left(O\right)\left(k\right)={\mathrm{coe}}_1\left(Q\right)\left(k\right)\leftrightarrow \forall k\in {\mathbb{N}}_{0}A=B\right)$$
86	23 85	bitrd	$$⊢\phi \to \left(O=Q\leftrightarrow \forall k\in {\mathbb{N}}_{0}A=B\right)$$