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	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	gsumply1eq.x	⊢ 𝑋 = ( var1 ‘ 𝑅 )
	gsumply1eq.e	⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑃 ) )
	gsumply1eq.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
	gsumply1eq.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
	gsumply1eq.m	⊢ ∗ = ( ·𝑠 ‘ 𝑃 )
	gsumply1eq.0	⊢ 0 = ( 0g ‘ 𝑅 )
	gsumply1eq.a	⊢ ( 𝜑 → ∀ 𝑘 ∈ ℕ0 𝐴 ∈ 𝐾 )
	gsumply1eq.f1	⊢ ( 𝜑 → ( 𝑘 ∈ ℕ0 ↦ 𝐴 ) finSupp 0 )
	gsumply1eq.b	⊢ ( 𝜑 → ∀ 𝑘 ∈ ℕ0 𝐵 ∈ 𝐾 )
	gsumply1eq.f2	⊢ ( 𝜑 → ( 𝑘 ∈ ℕ0 ↦ 𝐵 ) finSupp 0 )
	gsumply1eq.o	⊢ ( 𝜑 → 𝑂 = ( 𝑃 Σg ( 𝑘 ∈ ℕ0 ↦ ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) )
	gsumply1eq.q	⊢ ( 𝜑 → 𝑄 = ( 𝑃 Σg ( 𝑘 ∈ ℕ0 ↦ ( 𝐵 ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) )
Assertion	gsumply1eq	⊢ ( 𝜑 → ( 𝑂 = 𝑄 ↔ ∀ 𝑘 ∈ ℕ0 𝐴 = 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		gsumply1eq.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2		gsumply1eq.x	⊢ 𝑋 = ( var1 ‘ 𝑅 )
3		gsumply1eq.e	⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑃 ) )
4		gsumply1eq.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
5		gsumply1eq.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
6		gsumply1eq.m	⊢ ∗ = ( ·𝑠 ‘ 𝑃 )
7		gsumply1eq.0	⊢ 0 = ( 0g ‘ 𝑅 )
8		gsumply1eq.a	⊢ ( 𝜑 → ∀ 𝑘 ∈ ℕ0 𝐴 ∈ 𝐾 )
9		gsumply1eq.f1	⊢ ( 𝜑 → ( 𝑘 ∈ ℕ0 ↦ 𝐴 ) finSupp 0 )
10		gsumply1eq.b	⊢ ( 𝜑 → ∀ 𝑘 ∈ ℕ0 𝐵 ∈ 𝐾 )
11		gsumply1eq.f2	⊢ ( 𝜑 → ( 𝑘 ∈ ℕ0 ↦ 𝐵 ) finSupp 0 )
12		gsumply1eq.o	⊢ ( 𝜑 → 𝑂 = ( 𝑃 Σg ( 𝑘 ∈ ℕ0 ↦ ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) )
13		gsumply1eq.q	⊢ ( 𝜑 → 𝑄 = ( 𝑃 Σg ( 𝑘 ∈ ℕ0 ↦ ( 𝐵 ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) )
14		eqid	⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
15	1 14 2 3 4 5 6 7 8 9	gsumsmonply1	⊢ ( 𝜑 → ( 𝑃 Σg ( 𝑘 ∈ ℕ0 ↦ ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) ∈ ( Base ‘ 𝑃 ) )
16	12 15	eqeltrd	⊢ ( 𝜑 → 𝑂 ∈ ( Base ‘ 𝑃 ) )
17	1 14 2 3 4 5 6 7 10 11	gsumsmonply1	⊢ ( 𝜑 → ( 𝑃 Σg ( 𝑘 ∈ ℕ0 ↦ ( 𝐵 ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) ∈ ( Base ‘ 𝑃 ) )
18	13 17	eqeltrd	⊢ ( 𝜑 → 𝑄 ∈ ( Base ‘ 𝑃 ) )
19		eqid	⊢ ( coe1 ‘ 𝑂 ) = ( coe1 ‘ 𝑂 )
20		eqid	⊢ ( coe1 ‘ 𝑄 ) = ( coe1 ‘ 𝑄 )
21	1 14 19 20	ply1coe1eq	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑂 ∈ ( Base ‘ 𝑃 ) ∧ 𝑄 ∈ ( Base ‘ 𝑃 ) ) → ( ∀ 𝑘 ∈ ℕ0 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) = ( ( coe1 ‘ 𝑄 ) ‘ 𝑘 ) ↔ 𝑂 = 𝑄 ) )
22	21	bicomd	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑂 ∈ ( Base ‘ 𝑃 ) ∧ 𝑄 ∈ ( Base ‘ 𝑃 ) ) → ( 𝑂 = 𝑄 ↔ ∀ 𝑘 ∈ ℕ0 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) = ( ( coe1 ‘ 𝑄 ) ‘ 𝑘 ) ) )
23	4 16 18 22	syl3anc	⊢ ( 𝜑 → ( 𝑂 = 𝑄 ↔ ∀ 𝑘 ∈ ℕ0 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) = ( ( coe1 ‘ 𝑄 ) ‘ 𝑘 ) ) )
24	12	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 𝑂 = ( 𝑃 Σg ( 𝑘 ∈ ℕ0 ↦ ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) )
25		nfcv	⊢ Ⅎ 𝑙 ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) )
26		nfcsb1v	⊢ Ⅎ 𝑘 ⦋ 𝑙 / 𝑘 ⦌ 𝐴
27		nfcv	⊢ Ⅎ 𝑘 ∗
28		nfcv	⊢ Ⅎ 𝑘 ( 𝑙 ↑ 𝑋 )
29	26 27 28	nfov	⊢ Ⅎ 𝑘 ( ⦋ 𝑙 / 𝑘 ⦌ 𝐴 ∗ ( 𝑙 ↑ 𝑋 ) )
30		csbeq1a	⊢ ( 𝑘 = 𝑙 → 𝐴 = ⦋ 𝑙 / 𝑘 ⦌ 𝐴 )
31		oveq1	⊢ ( 𝑘 = 𝑙 → ( 𝑘 ↑ 𝑋 ) = ( 𝑙 ↑ 𝑋 ) )
32	30 31	oveq12d	⊢ ( 𝑘 = 𝑙 → ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) = ( ⦋ 𝑙 / 𝑘 ⦌ 𝐴 ∗ ( 𝑙 ↑ 𝑋 ) ) )
33	25 29 32	cbvmpt	⊢ ( 𝑘 ∈ ℕ0 ↦ ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) ) = ( 𝑙 ∈ ℕ0 ↦ ( ⦋ 𝑙 / 𝑘 ⦌ 𝐴 ∗ ( 𝑙 ↑ 𝑋 ) ) )
34	33	oveq2i	⊢ ( 𝑃 Σg ( 𝑘 ∈ ℕ0 ↦ ( 𝐴 ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) = ( 𝑃 Σg ( 𝑙 ∈ ℕ0 ↦ ( ⦋ 𝑙 / 𝑘 ⦌ 𝐴 ∗ ( 𝑙 ↑ 𝑋 ) ) ) )
35	24 34	eqtrdi	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 𝑂 = ( 𝑃 Σg ( 𝑙 ∈ ℕ0 ↦ ( ⦋ 𝑙 / 𝑘 ⦌ 𝐴 ∗ ( 𝑙 ↑ 𝑋 ) ) ) ) )
36	35	fveq2d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( coe1 ‘ 𝑂 ) = ( coe1 ‘ ( 𝑃 Σg ( 𝑙 ∈ ℕ0 ↦ ( ⦋ 𝑙 / 𝑘 ⦌ 𝐴 ∗ ( 𝑙 ↑ 𝑋 ) ) ) ) ) )
37	36	fveq1d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) = ( ( coe1 ‘ ( 𝑃 Σg ( 𝑙 ∈ ℕ0 ↦ ( ⦋ 𝑙 / 𝑘 ⦌ 𝐴 ∗ ( 𝑙 ↑ 𝑋 ) ) ) ) ) ‘ 𝑘 ) )
38	4	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 𝑅 ∈ Ring )
39		nfv	⊢ Ⅎ 𝑙 𝐴 ∈ 𝐾
40	26	nfel1	⊢ Ⅎ 𝑘 ⦋ 𝑙 / 𝑘 ⦌ 𝐴 ∈ 𝐾
41	30	eleq1d	⊢ ( 𝑘 = 𝑙 → ( 𝐴 ∈ 𝐾 ↔ ⦋ 𝑙 / 𝑘 ⦌ 𝐴 ∈ 𝐾 ) )
42	39 40 41	cbvralw	⊢ ( ∀ 𝑘 ∈ ℕ0 𝐴 ∈ 𝐾 ↔ ∀ 𝑙 ∈ ℕ0 ⦋ 𝑙 / 𝑘 ⦌ 𝐴 ∈ 𝐾 )
43	8 42	sylib	⊢ ( 𝜑 → ∀ 𝑙 ∈ ℕ0 ⦋ 𝑙 / 𝑘 ⦌ 𝐴 ∈ 𝐾 )
44	43	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ∀ 𝑙 ∈ ℕ0 ⦋ 𝑙 / 𝑘 ⦌ 𝐴 ∈ 𝐾 )
45		nfcv	⊢ Ⅎ 𝑙 𝐴
46	45 26 30	cbvmpt	⊢ ( 𝑘 ∈ ℕ0 ↦ 𝐴 ) = ( 𝑙 ∈ ℕ0 ↦ ⦋ 𝑙 / 𝑘 ⦌ 𝐴 )
47	46 9	eqbrtrrid	⊢ ( 𝜑 → ( 𝑙 ∈ ℕ0 ↦ ⦋ 𝑙 / 𝑘 ⦌ 𝐴 ) finSupp 0 )
48	47	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝑙 ∈ ℕ0 ↦ ⦋ 𝑙 / 𝑘 ⦌ 𝐴 ) finSupp 0 )
49		simpr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 𝑘 ∈ ℕ0 )
50	1 14 2 3 38 5 6 7 44 48 49	gsummoncoe1	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( coe1 ‘ ( 𝑃 Σg ( 𝑙 ∈ ℕ0 ↦ ( ⦋ 𝑙 / 𝑘 ⦌ 𝐴 ∗ ( 𝑙 ↑ 𝑋 ) ) ) ) ) ‘ 𝑘 ) = ⦋ 𝑘 / 𝑙 ⦌ ⦋ 𝑙 / 𝑘 ⦌ 𝐴 )
51		csbcow	⊢ ⦋ 𝑘 / 𝑙 ⦌ ⦋ 𝑙 / 𝑘 ⦌ 𝐴 = ⦋ 𝑘 / 𝑘 ⦌ 𝐴
52		csbid	⊢ ⦋ 𝑘 / 𝑘 ⦌ 𝐴 = 𝐴
53	51 52	eqtri	⊢ ⦋ 𝑘 / 𝑙 ⦌ ⦋ 𝑙 / 𝑘 ⦌ 𝐴 = 𝐴
54	50 53	eqtrdi	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( coe1 ‘ ( 𝑃 Σg ( 𝑙 ∈ ℕ0 ↦ ( ⦋ 𝑙 / 𝑘 ⦌ 𝐴 ∗ ( 𝑙 ↑ 𝑋 ) ) ) ) ) ‘ 𝑘 ) = 𝐴 )
55	37 54	eqtrd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) = 𝐴 )
56	13	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 𝑄 = ( 𝑃 Σg ( 𝑘 ∈ ℕ0 ↦ ( 𝐵 ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) )
57		nfcv	⊢ Ⅎ 𝑙 ( 𝐵 ∗ ( 𝑘 ↑ 𝑋 ) )
58		nfcsb1v	⊢ Ⅎ 𝑘 ⦋ 𝑙 / 𝑘 ⦌ 𝐵
59	58 27 28	nfov	⊢ Ⅎ 𝑘 ( ⦋ 𝑙 / 𝑘 ⦌ 𝐵 ∗ ( 𝑙 ↑ 𝑋 ) )
60		csbeq1a	⊢ ( 𝑘 = 𝑙 → 𝐵 = ⦋ 𝑙 / 𝑘 ⦌ 𝐵 )
61	60 31	oveq12d	⊢ ( 𝑘 = 𝑙 → ( 𝐵 ∗ ( 𝑘 ↑ 𝑋 ) ) = ( ⦋ 𝑙 / 𝑘 ⦌ 𝐵 ∗ ( 𝑙 ↑ 𝑋 ) ) )
62	57 59 61	cbvmpt	⊢ ( 𝑘 ∈ ℕ0 ↦ ( 𝐵 ∗ ( 𝑘 ↑ 𝑋 ) ) ) = ( 𝑙 ∈ ℕ0 ↦ ( ⦋ 𝑙 / 𝑘 ⦌ 𝐵 ∗ ( 𝑙 ↑ 𝑋 ) ) )
63	62	a1i	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝑘 ∈ ℕ0 ↦ ( 𝐵 ∗ ( 𝑘 ↑ 𝑋 ) ) ) = ( 𝑙 ∈ ℕ0 ↦ ( ⦋ 𝑙 / 𝑘 ⦌ 𝐵 ∗ ( 𝑙 ↑ 𝑋 ) ) ) )
64	63	oveq2d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝑃 Σg ( 𝑘 ∈ ℕ0 ↦ ( 𝐵 ∗ ( 𝑘 ↑ 𝑋 ) ) ) ) = ( 𝑃 Σg ( 𝑙 ∈ ℕ0 ↦ ( ⦋ 𝑙 / 𝑘 ⦌ 𝐵 ∗ ( 𝑙 ↑ 𝑋 ) ) ) ) )
65	56 64	eqtrd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → 𝑄 = ( 𝑃 Σg ( 𝑙 ∈ ℕ0 ↦ ( ⦋ 𝑙 / 𝑘 ⦌ 𝐵 ∗ ( 𝑙 ↑ 𝑋 ) ) ) ) )
66	65	fveq2d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( coe1 ‘ 𝑄 ) = ( coe1 ‘ ( 𝑃 Σg ( 𝑙 ∈ ℕ0 ↦ ( ⦋ 𝑙 / 𝑘 ⦌ 𝐵 ∗ ( 𝑙 ↑ 𝑋 ) ) ) ) ) )
67	66	fveq1d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( coe1 ‘ 𝑄 ) ‘ 𝑘 ) = ( ( coe1 ‘ ( 𝑃 Σg ( 𝑙 ∈ ℕ0 ↦ ( ⦋ 𝑙 / 𝑘 ⦌ 𝐵 ∗ ( 𝑙 ↑ 𝑋 ) ) ) ) ) ‘ 𝑘 ) )
68		nfv	⊢ Ⅎ 𝑙 𝐵 ∈ 𝐾
69	58	nfel1	⊢ Ⅎ 𝑘 ⦋ 𝑙 / 𝑘 ⦌ 𝐵 ∈ 𝐾
70	60	eleq1d	⊢ ( 𝑘 = 𝑙 → ( 𝐵 ∈ 𝐾 ↔ ⦋ 𝑙 / 𝑘 ⦌ 𝐵 ∈ 𝐾 ) )
71	68 69 70	cbvralw	⊢ ( ∀ 𝑘 ∈ ℕ0 𝐵 ∈ 𝐾 ↔ ∀ 𝑙 ∈ ℕ0 ⦋ 𝑙 / 𝑘 ⦌ 𝐵 ∈ 𝐾 )
72	10 71	sylib	⊢ ( 𝜑 → ∀ 𝑙 ∈ ℕ0 ⦋ 𝑙 / 𝑘 ⦌ 𝐵 ∈ 𝐾 )
73	72	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ∀ 𝑙 ∈ ℕ0 ⦋ 𝑙 / 𝑘 ⦌ 𝐵 ∈ 𝐾 )
74		nfcv	⊢ Ⅎ 𝑙 𝐵
75	74 58 60	cbvmpt	⊢ ( 𝑘 ∈ ℕ0 ↦ 𝐵 ) = ( 𝑙 ∈ ℕ0 ↦ ⦋ 𝑙 / 𝑘 ⦌ 𝐵 )
76	75 11	eqbrtrrid	⊢ ( 𝜑 → ( 𝑙 ∈ ℕ0 ↦ ⦋ 𝑙 / 𝑘 ⦌ 𝐵 ) finSupp 0 )
77	76	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝑙 ∈ ℕ0 ↦ ⦋ 𝑙 / 𝑘 ⦌ 𝐵 ) finSupp 0 )
78	1 14 2 3 38 5 6 7 73 77 49	gsummoncoe1	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( coe1 ‘ ( 𝑃 Σg ( 𝑙 ∈ ℕ0 ↦ ( ⦋ 𝑙 / 𝑘 ⦌ 𝐵 ∗ ( 𝑙 ↑ 𝑋 ) ) ) ) ) ‘ 𝑘 ) = ⦋ 𝑘 / 𝑙 ⦌ ⦋ 𝑙 / 𝑘 ⦌ 𝐵 )
79		csbcow	⊢ ⦋ 𝑘 / 𝑙 ⦌ ⦋ 𝑙 / 𝑘 ⦌ 𝐵 = ⦋ 𝑘 / 𝑘 ⦌ 𝐵
80		csbid	⊢ ⦋ 𝑘 / 𝑘 ⦌ 𝐵 = 𝐵
81	79 80	eqtri	⊢ ⦋ 𝑘 / 𝑙 ⦌ ⦋ 𝑙 / 𝑘 ⦌ 𝐵 = 𝐵
82	78 81	eqtrdi	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( coe1 ‘ ( 𝑃 Σg ( 𝑙 ∈ ℕ0 ↦ ( ⦋ 𝑙 / 𝑘 ⦌ 𝐵 ∗ ( 𝑙 ↑ 𝑋 ) ) ) ) ) ‘ 𝑘 ) = 𝐵 )
83	67 82	eqtrd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( coe1 ‘ 𝑄 ) ‘ 𝑘 ) = 𝐵 )
84	55 83	eqeq12d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) = ( ( coe1 ‘ 𝑄 ) ‘ 𝑘 ) ↔ 𝐴 = 𝐵 ) )
85	84	ralbidva	⊢ ( 𝜑 → ( ∀ 𝑘 ∈ ℕ0 ( ( coe1 ‘ 𝑂 ) ‘ 𝑘 ) = ( ( coe1 ‘ 𝑄 ) ‘ 𝑘 ) ↔ ∀ 𝑘 ∈ ℕ0 𝐴 = 𝐵 ) )
86	23 85	bitrd	⊢ ( 𝜑 → ( 𝑂 = 𝑄 ↔ ∀ 𝑘 ∈ ℕ0 𝐴 = 𝐵 ) )