This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ( 𝑘 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑦 ) ) ) ) )