Theorem ply1gsumz

Description: If a polynomial given as a sum of scaled monomials by factors A is the zero polynomial, then all factors A are zero. (Contributed by Thierry Arnoux, 20-Feb-2025)

	Ref	Expression
Hypotheses	ply1gsumz.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	ply1gsumz.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	ply1gsumz.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
	ply1gsumz.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
	ply1gsumz.f	⊢ 𝐹 = ( 𝑛 ∈ ( 0 ..^ 𝑁 ) ↦ ( 𝑛 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) )
	ply1gsumz.1	⊢ 0 = ( 0g ‘ 𝑅 )
	ply1gsumz.z	⊢ 𝑍 = ( 0g ‘ 𝑃 )
	ply1gsumz.a	⊢ ( 𝜑 → 𝐴 : ( 0 ..^ 𝑁 ) ⟶ 𝐵 )
	ply1gsumz.s	⊢ ( 𝜑 → ( 𝑃 Σg ( 𝐴 ∘f ( ·𝑠 ‘ 𝑃 ) 𝐹 ) ) = 𝑍 )
Assertion	ply1gsumz	⊢ ( 𝜑 → 𝐴 = ( ( 0 ..^ 𝑁 ) × { 0 } ) )

Proof

Step	Hyp	Ref	Expression
1		ply1gsumz.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2		ply1gsumz.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
3		ply1gsumz.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
4		ply1gsumz.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
5		ply1gsumz.f	⊢ 𝐹 = ( 𝑛 ∈ ( 0 ..^ 𝑁 ) ↦ ( 𝑛 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) )
6		ply1gsumz.1	⊢ 0 = ( 0g ‘ 𝑅 )
7		ply1gsumz.z	⊢ 𝑍 = ( 0g ‘ 𝑃 )
8		ply1gsumz.a	⊢ ( 𝜑 → 𝐴 : ( 0 ..^ 𝑁 ) ⟶ 𝐵 )
9		ply1gsumz.s	⊢ ( 𝜑 → ( 𝑃 Σg ( 𝐴 ∘f ( ·𝑠 ‘ 𝑃 ) 𝐹 ) ) = 𝑍 )
10	8	ffnd	⊢ ( 𝜑 → 𝐴 Fn ( 0 ..^ 𝑁 ) )
11	1	ply1ring	⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ Ring )
12		eqid	⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
13	12 7	ring0cl	⊢ ( 𝑃 ∈ Ring → 𝑍 ∈ ( Base ‘ 𝑃 ) )
14	4 11 13	3syl	⊢ ( 𝜑 → 𝑍 ∈ ( Base ‘ 𝑃 ) )
15		eqid	⊢ ( coe1 ‘ 𝑍 ) = ( coe1 ‘ 𝑍 )
16	15 12 1 2	coe1f	⊢ ( 𝑍 ∈ ( Base ‘ 𝑃 ) → ( coe1 ‘ 𝑍 ) : ℕ0 ⟶ 𝐵 )
17	14 16	syl	⊢ ( 𝜑 → ( coe1 ‘ 𝑍 ) : ℕ0 ⟶ 𝐵 )
18	17	ffnd	⊢ ( 𝜑 → ( coe1 ‘ 𝑍 ) Fn ℕ0 )
19		fzo0ssnn0	⊢ ( 0 ..^ 𝑁 ) ⊆ ℕ0
20	19	a1i	⊢ ( 𝜑 → ( 0 ..^ 𝑁 ) ⊆ ℕ0 )
21	18 20	fnssresd	⊢ ( 𝜑 → ( ( coe1 ‘ 𝑍 ) ↾ ( 0 ..^ 𝑁 ) ) Fn ( 0 ..^ 𝑁 ) )
22		simpr	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝑗 ∈ ( 0 ..^ 𝑁 ) )
23	22	fvresd	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( ( coe1 ‘ 𝑍 ) ↾ ( 0 ..^ 𝑁 ) ) ‘ 𝑗 ) = ( ( coe1 ‘ 𝑍 ) ‘ 𝑗 ) )
24		elfzonn0	⊢ ( 𝑗 ∈ ( 0 ..^ 𝑁 ) → 𝑗 ∈ ℕ0 )
25	9 14	eqeltrd	⊢ ( 𝜑 → ( 𝑃 Σg ( 𝐴 ∘f ( ·𝑠 ‘ 𝑃 ) 𝐹 ) ) ∈ ( Base ‘ 𝑃 ) )
26		eqid	⊢ ( coe1 ‘ ( 𝑃 Σg ( 𝐴 ∘f ( ·𝑠 ‘ 𝑃 ) 𝐹 ) ) ) = ( coe1 ‘ ( 𝑃 Σg ( 𝐴 ∘f ( ·𝑠 ‘ 𝑃 ) 𝐹 ) ) )
27	1 12 26 15	ply1coe1eq	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑃 Σg ( 𝐴 ∘f ( ·𝑠 ‘ 𝑃 ) 𝐹 ) ) ∈ ( Base ‘ 𝑃 ) ∧ 𝑍 ∈ ( Base ‘ 𝑃 ) ) → ( ∀ 𝑗 ∈ ℕ0 ( ( coe1 ‘ ( 𝑃 Σg ( 𝐴 ∘f ( ·𝑠 ‘ 𝑃 ) 𝐹 ) ) ) ‘ 𝑗 ) = ( ( coe1 ‘ 𝑍 ) ‘ 𝑗 ) ↔ ( 𝑃 Σg ( 𝐴 ∘f ( ·𝑠 ‘ 𝑃 ) 𝐹 ) ) = 𝑍 ) )
28	27	biimpar	⊢ ( ( ( 𝑅 ∈ Ring ∧ ( 𝑃 Σg ( 𝐴 ∘f ( ·𝑠 ‘ 𝑃 ) 𝐹 ) ) ∈ ( Base ‘ 𝑃 ) ∧ 𝑍 ∈ ( Base ‘ 𝑃 ) ) ∧ ( 𝑃 Σg ( 𝐴 ∘f ( ·𝑠 ‘ 𝑃 ) 𝐹 ) ) = 𝑍 ) → ∀ 𝑗 ∈ ℕ0 ( ( coe1 ‘ ( 𝑃 Σg ( 𝐴 ∘f ( ·𝑠 ‘ 𝑃 ) 𝐹 ) ) ) ‘ 𝑗 ) = ( ( coe1 ‘ 𝑍 ) ‘ 𝑗 ) )
29	4 25 14 9 28	syl31anc	⊢ ( 𝜑 → ∀ 𝑗 ∈ ℕ0 ( ( coe1 ‘ ( 𝑃 Σg ( 𝐴 ∘f ( ·𝑠 ‘ 𝑃 ) 𝐹 ) ) ) ‘ 𝑗 ) = ( ( coe1 ‘ 𝑍 ) ‘ 𝑗 ) )
30	29	r19.21bi	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ0 ) → ( ( coe1 ‘ ( 𝑃 Σg ( 𝐴 ∘f ( ·𝑠 ‘ 𝑃 ) 𝐹 ) ) ) ‘ 𝑗 ) = ( ( coe1 ‘ 𝑍 ) ‘ 𝑗 ) )
31	24 30	sylan2	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( coe1 ‘ ( 𝑃 Σg ( 𝐴 ∘f ( ·𝑠 ‘ 𝑃 ) 𝐹 ) ) ) ‘ 𝑗 ) = ( ( coe1 ‘ 𝑍 ) ‘ 𝑗 ) )
32	10	adantr	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝐴 Fn ( 0 ..^ 𝑁 ) )
33		nfv	⊢ Ⅎ 𝑛 𝜑
34		ovexd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑛 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ∈ V )
35	33 34 5	fnmptd	⊢ ( 𝜑 → 𝐹 Fn ( 0 ..^ 𝑁 ) )
36	35	adantr	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝐹 Fn ( 0 ..^ 𝑁 ) )
37		ovexd	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 0 ..^ 𝑁 ) ∈ V )
38		inidm	⊢ ( ( 0 ..^ 𝑁 ) ∩ ( 0 ..^ 𝑁 ) ) = ( 0 ..^ 𝑁 )
39		eqidd	⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐴 ‘ 𝑖 ) = ( 𝐴 ‘ 𝑖 ) )
40		oveq1	⊢ ( 𝑛 = 𝑖 → ( 𝑛 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) = ( 𝑖 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) )
41		simpr	⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) → 𝑖 ∈ ( 0 ..^ 𝑁 ) )
42		ovexd	⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑖 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ∈ V )
43	5 40 41 42	fvmptd3	⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐹 ‘ 𝑖 ) = ( 𝑖 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) )
44	32 36 37 37 38 39 43	offval	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐴 ∘f ( ·𝑠 ‘ 𝑃 ) 𝐹 ) = ( 𝑖 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝐴 ‘ 𝑖 ) ( ·𝑠 ‘ 𝑃 ) ( 𝑖 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) )
45	44	oveq2d	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑃 Σg ( 𝐴 ∘f ( ·𝑠 ‘ 𝑃 ) 𝐹 ) ) = ( 𝑃 Σg ( 𝑖 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝐴 ‘ 𝑖 ) ( ·𝑠 ‘ 𝑃 ) ( 𝑖 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) ) )
46	45	fveq2d	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( coe1 ‘ ( 𝑃 Σg ( 𝐴 ∘f ( ·𝑠 ‘ 𝑃 ) 𝐹 ) ) ) = ( coe1 ‘ ( 𝑃 Σg ( 𝑖 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝐴 ‘ 𝑖 ) ( ·𝑠 ‘ 𝑃 ) ( 𝑖 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) ) ) )
47	46	fveq1d	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( coe1 ‘ ( 𝑃 Σg ( 𝐴 ∘f ( ·𝑠 ‘ 𝑃 ) 𝐹 ) ) ) ‘ 𝑗 ) = ( ( coe1 ‘ ( 𝑃 Σg ( 𝑖 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝐴 ‘ 𝑖 ) ( ·𝑠 ‘ 𝑃 ) ( 𝑖 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) ) ) ‘ 𝑗 ) )
48		eqid	⊢ ( var1 ‘ 𝑅 ) = ( var1 ‘ 𝑅 )
49		eqid	⊢ ( .g ‘ ( mulGrp ‘ 𝑃 ) ) = ( .g ‘ ( mulGrp ‘ 𝑃 ) )
50	4	adantr	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝑅 ∈ Ring )
51		eqid	⊢ ( ·𝑠 ‘ 𝑃 ) = ( ·𝑠 ‘ 𝑃 )
52	8	adantr	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝐴 : ( 0 ..^ 𝑁 ) ⟶ 𝐵 )
53	52	ffvelcdmda	⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑖 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐴 ‘ 𝑖 ) ∈ 𝐵 )
54	53	ralrimiva	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) ( 𝐴 ‘ 𝑖 ) ∈ 𝐵 )
55	3	adantr	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → 𝑁 ∈ ℕ0 )
56		fveq2	⊢ ( 𝑖 = 𝑗 → ( 𝐴 ‘ 𝑖 ) = ( 𝐴 ‘ 𝑗 ) )
57	1 12 48 49 50 2 51 6 54 22 55 56	gsummoncoe1fzo	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( coe1 ‘ ( 𝑃 Σg ( 𝑖 ∈ ( 0 ..^ 𝑁 ) ↦ ( ( 𝐴 ‘ 𝑖 ) ( ·𝑠 ‘ 𝑃 ) ( 𝑖 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) ) ) ‘ 𝑗 ) = ( 𝐴 ‘ 𝑗 ) )
58	47 57	eqtrd	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( ( coe1 ‘ ( 𝑃 Σg ( 𝐴 ∘f ( ·𝑠 ‘ 𝑃 ) 𝐹 ) ) ) ‘ 𝑗 ) = ( 𝐴 ‘ 𝑗 ) )
59	23 31 58	3eqtr2rd	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐴 ‘ 𝑗 ) = ( ( ( coe1 ‘ 𝑍 ) ↾ ( 0 ..^ 𝑁 ) ) ‘ 𝑗 ) )
60	10 21 59	eqfnfvd	⊢ ( 𝜑 → 𝐴 = ( ( coe1 ‘ 𝑍 ) ↾ ( 0 ..^ 𝑁 ) ) )
61	1 7 6	coe1z	⊢ ( 𝑅 ∈ Ring → ( coe1 ‘ 𝑍 ) = ( ℕ0 × { 0 } ) )
62	4 61	syl	⊢ ( 𝜑 → ( coe1 ‘ 𝑍 ) = ( ℕ0 × { 0 } ) )
63	62	reseq1d	⊢ ( 𝜑 → ( ( coe1 ‘ 𝑍 ) ↾ ( 0 ..^ 𝑁 ) ) = ( ( ℕ0 × { 0 } ) ↾ ( 0 ..^ 𝑁 ) ) )
64	60 63	eqtrd	⊢ ( 𝜑 → 𝐴 = ( ( ℕ0 × { 0 } ) ↾ ( 0 ..^ 𝑁 ) ) )
65		xpssres	⊢ ( ( 0 ..^ 𝑁 ) ⊆ ℕ0 → ( ( ℕ0 × { 0 } ) ↾ ( 0 ..^ 𝑁 ) ) = ( ( 0 ..^ 𝑁 ) × { 0 } ) )
66	19 65	ax-mp	⊢ ( ( ℕ0 × { 0 } ) ↾ ( 0 ..^ 𝑁 ) ) = ( ( 0 ..^ 𝑁 ) × { 0 } )
67	64 66	eqtrdi	⊢ ( 𝜑 → 𝐴 = ( ( 0 ..^ 𝑁 ) × { 0 } ) )