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={\mathrm{Base}}_W$$
	gsummptun.p	$$⊢\underset{\dot{}}{+}={+}_W$$
	gsummptun.w	$$⊢\phi \to W\in \mathrm{CMnd}$$
	gsummptun.a	$$⊢\phi \to A\cup C\in \mathrm{Fin}$$
	gsummptun.d	$$⊢\phi \to A\cap C=\varnothing$$
	gsummptun.1	$$⊢\left(\phi \wedge x\in \left(A\cup C\right)\right)\to D\in B$$
Assertion	gsummptun	$$⊢\phi \to \underset{x\in A\cup C}{{\sum }_W}D=\left(\underset{x\in A}{{\sum }_W},D\right)\underset{\dot{}}{+}\left(\underset{x\in C}{{\sum }_W},D\right)$$

Proof

Step	Hyp	Ref	Expression
1		gsummptun.b	$$⊢B={\mathrm{Base}}_W$$
2		gsummptun.p	$$⊢\underset{\dot{}}{+}={+}_W$$
3		gsummptun.w	$$⊢\phi \to W\in \mathrm{CMnd}$$
4		gsummptun.a	$$⊢\phi \to A\cup C\in \mathrm{Fin}$$
5		gsummptun.d	$$⊢\phi \to A\cap C=\varnothing$$
6		gsummptun.1	$$⊢\left(\phi \wedge x\in \left(A\cup C\right)\right)\to D\in B$$
7		eqidd	$$⊢\phi \to A\cup C=A\cup C$$
8	1 2 3 4 6 5 7	gsummptfidmsplit	$$⊢\phi \to \underset{x\in A\cup C}{{\sum }_W}D=\left(\underset{x\in A}{{\sum }_W},D\right)\underset{\dot{}}{+}\left(\underset{x\in C}{{\sum }_W},D\right)$$