Theorem mplgsum

Description: Finite commutative sums of polynomials are taken componentwise. (Contributed by Thierry Arnoux, 16-Mar-2026)

	Ref	Expression
Hypotheses	mplgsum.p	⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
	mplgsum.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
	mplgsum.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
	mplgsum.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
	mplgsum.d	⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 }
	mplgsum.a	⊢ ( 𝜑 → 𝐴 ∈ Fin )
	mplgsum.f	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
Assertion	mplgsum	⊢ ( 𝜑 → ( 𝑃 Σg 𝐹 ) = ( 𝑦 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑘 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		mplgsum.p	⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
2		mplgsum.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
3		mplgsum.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
4		mplgsum.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
5		mplgsum.d	⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 }
6		mplgsum.a	⊢ ( 𝜑 → 𝐴 ∈ Fin )
7		mplgsum.f	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
8		eqid	⊢ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) = ( Base ‘ ( 𝐼 mPwSer 𝑅 ) )
9		eqid	⊢ ( +g ‘ ( 𝐼 mPwSer 𝑅 ) ) = ( +g ‘ ( 𝐼 mPwSer 𝑅 ) )
10		eqid	⊢ ( 𝐼 mPwSer 𝑅 ) = ( 𝐼 mPwSer 𝑅 )
11	1 10 2	mplval2	⊢ 𝑃 = ( ( 𝐼 mPwSer 𝑅 ) ↾s 𝐵 )
12		ovexd	⊢ ( 𝜑 → ( 𝐼 mPwSer 𝑅 ) ∈ V )
13	1 10 2 8	mplbasss	⊢ 𝐵 ⊆ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) )
14	13	a1i	⊢ ( 𝜑 → 𝐵 ⊆ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) )
15	3	ringgrpd	⊢ ( 𝜑 → 𝑅 ∈ Grp )
16	5	psrbasfsupp	⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
17		eqid	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
18		eqid	⊢ ( 0g ‘ ( 𝐼 mPwSer 𝑅 ) ) = ( 0g ‘ ( 𝐼 mPwSer 𝑅 ) )
19	10 4 15 16 17 18	psr0	⊢ ( 𝜑 → ( 0g ‘ ( 𝐼 mPwSer 𝑅 ) ) = ( 𝐷 × { ( 0g ‘ 𝑅 ) } ) )
20		eqid	⊢ ( 0g ‘ 𝑃 ) = ( 0g ‘ 𝑃 )
21	1 16 17 20 4 15	mpl0	⊢ ( 𝜑 → ( 0g ‘ 𝑃 ) = ( 𝐷 × { ( 0g ‘ 𝑅 ) } ) )
22	19 21	eqtr4d	⊢ ( 𝜑 → ( 0g ‘ ( 𝐼 mPwSer 𝑅 ) ) = ( 0g ‘ 𝑃 ) )
23	1	mplgrp	⊢ ( ( 𝐼 ∈ 𝑉 ∧ 𝑅 ∈ Grp ) → 𝑃 ∈ Grp )
24	4 15 23	syl2anc	⊢ ( 𝜑 → 𝑃 ∈ Grp )
25	2 20	grpidcl	⊢ ( 𝑃 ∈ Grp → ( 0g ‘ 𝑃 ) ∈ 𝐵 )
26	24 25	syl	⊢ ( 𝜑 → ( 0g ‘ 𝑃 ) ∈ 𝐵 )
27	22 26	eqeltrd	⊢ ( 𝜑 → ( 0g ‘ ( 𝐼 mPwSer 𝑅 ) ) ∈ 𝐵 )
28	10 4 15	psrgrp	⊢ ( 𝜑 → ( 𝐼 mPwSer 𝑅 ) ∈ Grp )
29	28	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ) → ( 𝐼 mPwSer 𝑅 ) ∈ Grp )
30		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ) → 𝑥 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) )
31	8 9 18 29 30	grplidd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ) → ( ( 0g ‘ ( 𝐼 mPwSer 𝑅 ) ) ( +g ‘ ( 𝐼 mPwSer 𝑅 ) ) 𝑥 ) = 𝑥 )
32	8 9 18 29 30	grpridd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ) → ( 𝑥 ( +g ‘ ( 𝐼 mPwSer 𝑅 ) ) ( 0g ‘ ( 𝐼 mPwSer 𝑅 ) ) ) = 𝑥 )
33	31 32	jca	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ) → ( ( ( 0g ‘ ( 𝐼 mPwSer 𝑅 ) ) ( +g ‘ ( 𝐼 mPwSer 𝑅 ) ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( +g ‘ ( 𝐼 mPwSer 𝑅 ) ) ( 0g ‘ ( 𝐼 mPwSer 𝑅 ) ) ) = 𝑥 ) )
34	8 9 11 12 6 14 7 27 33	gsumress	⊢ ( 𝜑 → ( ( 𝐼 mPwSer 𝑅 ) Σg 𝐹 ) = ( 𝑃 Σg 𝐹 ) )
35	7 14	fssd	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) )
36	10 8 3 4 5 6 35	psrgsum	⊢ ( 𝜑 → ( ( 𝐼 mPwSer 𝑅 ) Σg 𝐹 ) = ( 𝑦 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑘 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) ) ) ) )
37	34 36	eqtr3d	⊢ ( 𝜑 → ( 𝑃 Σg 𝐹 ) = ( 𝑦 ∈ 𝐷 ↦ ( 𝑅 Σg ( 𝑘 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) ) ) ) )