Theorem gsummptun

Description: Group sum of a disjoint union, whereas sums are expressed as mappings. (Contributed by Thierry Arnoux, 28-Mar-2018) (Proof shortened by AV, 11-Dec-2019)

	Ref	Expression
Hypotheses	gsummptun.b	|- B = ( Base ` W )
	gsummptun.p	|- .+ = ( +g ` W )
	gsummptun.w	|- ( ph -> W e. CMnd )
	gsummptun.a	|- ( ph -> ( A u. C ) e. Fin )
	gsummptun.d	|- ( ph -> ( A i^i C ) = (/) )
	gsummptun.1	|- ( ( ph /\ x e. ( A u. C ) ) -> D e. B )
Assertion	gsummptun	|- ( ph -> ( W gsum ( x e. ( A u. C ) |-> D ) ) = ( ( W gsum ( x e. A |-> D ) ) .+ ( W gsum ( x e. C |-> D ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		gsummptun.b	|- B = ( Base ` W )
2		gsummptun.p	|- .+ = ( +g ` W )
3		gsummptun.w	|- ( ph -> W e. CMnd )
4		gsummptun.a	|- ( ph -> ( A u. C ) e. Fin )
5		gsummptun.d	|- ( ph -> ( A i^i C ) = (/) )
6		gsummptun.1	|- ( ( ph /\ x e. ( A u. C ) ) -> D e. B )
7		eqidd	|- ( ph -> ( A u. C ) = ( A u. C ) )
8	1 2 3 4 6 5 7	gsummptfidmsplit	|- ( ph -> ( W gsum ( x e. ( A u. C ) |-> D ) ) = ( ( W gsum ( x e. A |-> D ) ) .+ ( W gsum ( x e. C |-> D ) ) ) )