Theorem gsummptfidmsplitres

Description: Split a group sum expressed as mapping with a finite domain into two parts using restrictions. (Contributed by AV, 23-Jul-2019)

	Ref	Expression
Hypotheses	gsummptfidmsplit.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
	gsummptfidmsplit.p	⊢ + = ( +g ‘ 𝐺 )
	gsummptfidmsplit.g	⊢ ( 𝜑 → 𝐺 ∈ CMnd )
	gsummptfidmsplit.a	⊢ ( 𝜑 → 𝐴 ∈ Fin )
	gsummptfidmsplit.y	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝑌 ∈ 𝐵 )
	gsummptfidmsplit.i	⊢ ( 𝜑 → ( 𝐶 ∩ 𝐷 ) = ∅ )
	gsummptfidmsplit.u	⊢ ( 𝜑 → 𝐴 = ( 𝐶 ∪ 𝐷 ) )
	gsummptfidmsplitres.f	⊢ 𝐹 = ( 𝑘 ∈ 𝐴 ↦ 𝑌 )
Assertion	gsummptfidmsplitres	⊢ ( 𝜑 → ( 𝐺 Σg 𝐹 ) = ( ( 𝐺 Σg ( 𝐹 ↾ 𝐶 ) ) + ( 𝐺 Σg ( 𝐹 ↾ 𝐷 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		gsummptfidmsplit.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		gsummptfidmsplit.p	⊢ + = ( +g ‘ 𝐺 )
3		gsummptfidmsplit.g	⊢ ( 𝜑 → 𝐺 ∈ CMnd )
4		gsummptfidmsplit.a	⊢ ( 𝜑 → 𝐴 ∈ Fin )
5		gsummptfidmsplit.y	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝑌 ∈ 𝐵 )
6		gsummptfidmsplit.i	⊢ ( 𝜑 → ( 𝐶 ∩ 𝐷 ) = ∅ )
7		gsummptfidmsplit.u	⊢ ( 𝜑 → 𝐴 = ( 𝐶 ∪ 𝐷 ) )
8		gsummptfidmsplitres.f	⊢ 𝐹 = ( 𝑘 ∈ 𝐴 ↦ 𝑌 )
9		eqid	⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
10	5 8	fmptd	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
11		fvexd	⊢ ( 𝜑 → ( 0g ‘ 𝐺 ) ∈ V )
12	8 4 5 11	fsuppmptdm	⊢ ( 𝜑 → 𝐹 finSupp ( 0g ‘ 𝐺 ) )
13	1 9 2 3 4 10 12 6 7	gsumsplit	⊢ ( 𝜑 → ( 𝐺 Σg 𝐹 ) = ( ( 𝐺 Σg ( 𝐹 ↾ 𝐶 ) ) + ( 𝐺 Σg ( 𝐹 ↾ 𝐷 ) ) ) )