Theorem gsummptfidmsplit

Description: Split a group sum expressed as mapping with a finite domain into two parts. (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	⊢ ( 𝜑 → 𝐴 = ( 𝐶 ∪ 𝐷 ) )
Assertion	gsummptfidmsplit	⊢ ( 𝜑 → ( 𝐺 Σ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		eqid	⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
9		eqid	⊢ ( 𝑘 ∈ 𝐴 ↦ 𝑌 ) = ( 𝑘 ∈ 𝐴 ↦ 𝑌 )
10		fvexd	⊢ ( 𝜑 → ( 0g ‘ 𝐺 ) ∈ V )
11	9 4 5 10	fsuppmptdm	⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 ↦ 𝑌 ) finSupp ( 0g ‘ 𝐺 ) )
12	1 8 2 3 4 5 11 6 7	gsumsplit2	⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑘 ∈ 𝐴 ↦ 𝑌 ) ) = ( ( 𝐺 Σg ( 𝑘 ∈ 𝐶 ↦ 𝑌 ) ) + ( 𝐺 Σg ( 𝑘 ∈ 𝐷 ↦ 𝑌 ) ) ) )