Theorem gsummptfidmsub

Description: The difference of two group sums expressed as mappings with finite domain. (Contributed by AV, 7-Nov-2019)

	Ref	Expression
Hypotheses	gsummptfidmsub.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
	gsummptfidmsub.s	⊢ − = ( -g ‘ 𝐺 )
	gsummptfidmsub.g	⊢ ( 𝜑 → 𝐺 ∈ Abel )
	gsummptfidmsub.a	⊢ ( 𝜑 → 𝐴 ∈ Fin )
	gsummptfidmsub.c	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ 𝐵 )
	gsummptfidmsub.d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐷 ∈ 𝐵 )
	gsummptfidmsub.f	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐶 )
	gsummptfidmsub.h	⊢ 𝐻 = ( 𝑥 ∈ 𝐴 ↦ 𝐷 )
Assertion	gsummptfidmsub	⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑥 ∈ 𝐴 ↦ ( 𝐶 − 𝐷 ) ) ) = ( ( 𝐺 Σg 𝐹 ) − ( 𝐺 Σg 𝐻 ) ) )

Proof

Step	Hyp	Ref	Expression
1		gsummptfidmsub.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		gsummptfidmsub.s	⊢ − = ( -g ‘ 𝐺 )
3		gsummptfidmsub.g	⊢ ( 𝜑 → 𝐺 ∈ Abel )
4		gsummptfidmsub.a	⊢ ( 𝜑 → 𝐴 ∈ Fin )
5		gsummptfidmsub.c	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ 𝐵 )
6		gsummptfidmsub.d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐷 ∈ 𝐵 )
7		gsummptfidmsub.f	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐶 )
8		gsummptfidmsub.h	⊢ 𝐻 = ( 𝑥 ∈ 𝐴 ↦ 𝐷 )
9		eqid	⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
10	7	a1i	⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) )
11	8	a1i	⊢ ( 𝜑 → 𝐻 = ( 𝑥 ∈ 𝐴 ↦ 𝐷 ) )
12		fvexd	⊢ ( 𝜑 → ( 0g ‘ 𝐺 ) ∈ V )
13	7 4 5 12	fsuppmptdm	⊢ ( 𝜑 → 𝐹 finSupp ( 0g ‘ 𝐺 ) )
14	8 4 6 12	fsuppmptdm	⊢ ( 𝜑 → 𝐻 finSupp ( 0g ‘ 𝐺 ) )
15	1 9 2 3 4 5 6 10 11 13 14	gsummptfssub	⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑥 ∈ 𝐴 ↦ ( 𝐶 − 𝐷 ) ) ) = ( ( 𝐺 Σg 𝐹 ) − ( 𝐺 Σg 𝐻 ) ) )