Theorem gsummptres2

Description: Extend a finite group sum by padding outside with zeroes. (Contributed by Thierry Arnoux, 22-Jun-2024)

	Ref	Expression
Hypotheses	gsummptres2.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
	gsummptres2.z	⊢ 0 = ( 0g ‘ 𝐺 )
	gsummptres2.g	⊢ ( 𝜑 → 𝐺 ∈ CMnd )
	gsummptres2.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	gsummptres2.0	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑆 ) ) → 𝑌 = 0 )
	gsummptres2.1	⊢ ( 𝜑 → 𝑆 ∈ Fin )
	gsummptres2.y	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑌 ∈ 𝐵 )
	gsummptres2.2	⊢ ( 𝜑 → 𝑆 ⊆ 𝐴 )
Assertion	gsummptres2	⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑥 ∈ 𝐴 ↦ 𝑌 ) ) = ( 𝐺 Σg ( 𝑥 ∈ 𝑆 ↦ 𝑌 ) ) )

Proof

Step	Hyp	Ref	Expression
1		gsummptres2.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		gsummptres2.z	⊢ 0 = ( 0g ‘ 𝐺 )
3		gsummptres2.g	⊢ ( 𝜑 → 𝐺 ∈ CMnd )
4		gsummptres2.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
5		gsummptres2.0	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∖ 𝑆 ) ) → 𝑌 = 0 )
6		gsummptres2.1	⊢ ( 𝜑 → 𝑆 ∈ Fin )
7		gsummptres2.y	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑌 ∈ 𝐵 )
8		gsummptres2.2	⊢ ( 𝜑 → 𝑆 ⊆ 𝐴 )
9		eqid	⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
10	4	mptexd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝑌 ) ∈ V )
11		funmpt	⊢ Fun ( 𝑥 ∈ 𝐴 ↦ 𝑌 )
12	11	a1i	⊢ ( 𝜑 → Fun ( 𝑥 ∈ 𝐴 ↦ 𝑌 ) )
13	2	fvexi	⊢ 0 ∈ V
14	13	a1i	⊢ ( 𝜑 → 0 ∈ V )
15	5 4	suppss2	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝑌 ) supp 0 ) ⊆ 𝑆 )
16		suppssfifsupp	⊢ ( ( ( ( 𝑥 ∈ 𝐴 ↦ 𝑌 ) ∈ V ∧ Fun ( 𝑥 ∈ 𝐴 ↦ 𝑌 ) ∧ 0 ∈ V ) ∧ ( 𝑆 ∈ Fin ∧ ( ( 𝑥 ∈ 𝐴 ↦ 𝑌 ) supp 0 ) ⊆ 𝑆 ) ) → ( 𝑥 ∈ 𝐴 ↦ 𝑌 ) finSupp 0 )
17	10 12 14 6 15 16	syl32anc	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝑌 ) finSupp 0 )
18		disjdif	⊢ ( 𝑆 ∩ ( 𝐴 ∖ 𝑆 ) ) = ∅
19	18	a1i	⊢ ( 𝜑 → ( 𝑆 ∩ ( 𝐴 ∖ 𝑆 ) ) = ∅ )
20		undif	⊢ ( 𝑆 ⊆ 𝐴 ↔ ( 𝑆 ∪ ( 𝐴 ∖ 𝑆 ) ) = 𝐴 )
21	8 20	sylib	⊢ ( 𝜑 → ( 𝑆 ∪ ( 𝐴 ∖ 𝑆 ) ) = 𝐴 )
22	21	eqcomd	⊢ ( 𝜑 → 𝐴 = ( 𝑆 ∪ ( 𝐴 ∖ 𝑆 ) ) )
23	1 2 9 3 4 7 17 19 22	gsumsplit2	⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑥 ∈ 𝐴 ↦ 𝑌 ) ) = ( ( 𝐺 Σg ( 𝑥 ∈ 𝑆 ↦ 𝑌 ) ) ( +g ‘ 𝐺 ) ( 𝐺 Σg ( 𝑥 ∈ ( 𝐴 ∖ 𝑆 ) ↦ 𝑌 ) ) ) )
24	5	mpteq2dva	⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 ∖ 𝑆 ) ↦ 𝑌 ) = ( 𝑥 ∈ ( 𝐴 ∖ 𝑆 ) ↦ 0 ) )
25	24	oveq2d	⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑥 ∈ ( 𝐴 ∖ 𝑆 ) ↦ 𝑌 ) ) = ( 𝐺 Σg ( 𝑥 ∈ ( 𝐴 ∖ 𝑆 ) ↦ 0 ) ) )
26	3	cmnmndd	⊢ ( 𝜑 → 𝐺 ∈ Mnd )
27		difexg	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∖ 𝑆 ) ∈ V )
28	4 27	syl	⊢ ( 𝜑 → ( 𝐴 ∖ 𝑆 ) ∈ V )
29	2	gsumz	⊢ ( ( 𝐺 ∈ Mnd ∧ ( 𝐴 ∖ 𝑆 ) ∈ V ) → ( 𝐺 Σg ( 𝑥 ∈ ( 𝐴 ∖ 𝑆 ) ↦ 0 ) ) = 0 )
30	26 28 29	syl2anc	⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑥 ∈ ( 𝐴 ∖ 𝑆 ) ↦ 0 ) ) = 0 )
31	25 30	eqtrd	⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑥 ∈ ( 𝐴 ∖ 𝑆 ) ↦ 𝑌 ) ) = 0 )
32	31	oveq2d	⊢ ( 𝜑 → ( ( 𝐺 Σg ( 𝑥 ∈ 𝑆 ↦ 𝑌 ) ) ( +g ‘ 𝐺 ) ( 𝐺 Σg ( 𝑥 ∈ ( 𝐴 ∖ 𝑆 ) ↦ 𝑌 ) ) ) = ( ( 𝐺 Σg ( 𝑥 ∈ 𝑆 ↦ 𝑌 ) ) ( +g ‘ 𝐺 ) 0 ) )
33	7	ralrimiva	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 𝑌 ∈ 𝐵 )
34		ssralv	⊢ ( 𝑆 ⊆ 𝐴 → ( ∀ 𝑥 ∈ 𝐴 𝑌 ∈ 𝐵 → ∀ 𝑥 ∈ 𝑆 𝑌 ∈ 𝐵 ) )
35	8 33 34	sylc	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑆 𝑌 ∈ 𝐵 )
36	1 3 6 35	gsummptcl	⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑥 ∈ 𝑆 ↦ 𝑌 ) ) ∈ 𝐵 )
37	1 9 2	mndrid	⊢ ( ( 𝐺 ∈ Mnd ∧ ( 𝐺 Σg ( 𝑥 ∈ 𝑆 ↦ 𝑌 ) ) ∈ 𝐵 ) → ( ( 𝐺 Σg ( 𝑥 ∈ 𝑆 ↦ 𝑌 ) ) ( +g ‘ 𝐺 ) 0 ) = ( 𝐺 Σg ( 𝑥 ∈ 𝑆 ↦ 𝑌 ) ) )
38	26 36 37	syl2anc	⊢ ( 𝜑 → ( ( 𝐺 Σg ( 𝑥 ∈ 𝑆 ↦ 𝑌 ) ) ( +g ‘ 𝐺 ) 0 ) = ( 𝐺 Σg ( 𝑥 ∈ 𝑆 ↦ 𝑌 ) ) )
39	23 32 38	3eqtrd	⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑥 ∈ 𝐴 ↦ 𝑌 ) ) = ( 𝐺 Σg ( 𝑥 ∈ 𝑆 ↦ 𝑌 ) ) )