Theorem tsms0

Description: The sum of zero is zero. (Contributed by Mario Carneiro, 18-Sep-2015) (Proof shortened by AV, 24-Jul-2019)

	Ref	Expression
Hypotheses	tsms0.z	$$⊢\underset{\dot{}}{0}=0_G$$
	tsms0.1	$$⊢\phi \to G\in \mathrm{CMnd}$$
	tsms0.2	$$⊢\phi \to G\in \mathrm{TopSp}$$
	tsms0.a	$$⊢\phi \to A\in V$$
Assertion	tsms0	$$⊢\phi \to \underset{\dot{}}{0}\in \left(G\mathrm{tsums}\left(x\in A⟼\underset{\dot{}}{0}\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		tsms0.z	$$⊢\underset{\dot{}}{0}=0_G$$
2		tsms0.1	$$⊢\phi \to G\in \mathrm{CMnd}$$
3		tsms0.2	$$⊢\phi \to G\in \mathrm{TopSp}$$
4		tsms0.a	$$⊢\phi \to A\in V$$
5		cmnmnd	$$⊢G\in \mathrm{CMnd}\to G\in \mathrm{Mnd}$$
6	2 5	syl	$$⊢\phi \to G\in \mathrm{Mnd}$$
7	1	gsumz	$$⊢\left(G\in \mathrm{Mnd}\wedge A\in V\right)\to \underset{x\in A}{{\sum }_G}\underset{\dot{}}{0}=\underset{\dot{}}{0}$$
8	6 4 7	syl2anc	$$⊢\phi \to \underset{x\in A}{{\sum }_G}\underset{\dot{}}{0}=\underset{\dot{}}{0}$$
9		eqid	$$⊢{\mathrm{Base}}_G={\mathrm{Base}}_G$$
10	9 1	mndidcl	$$⊢G\in \mathrm{Mnd}\to \underset{\dot{}}{0}\in {\mathrm{Base}}_G$$
11	6 10	syl	$$⊢\phi \to \underset{\dot{}}{0}\in {\mathrm{Base}}_G$$
12	11	adantr	$$⊢\left(\phi \wedge x\in A\right)\to \underset{\dot{}}{0}\in {\mathrm{Base}}_G$$
13	12	fmpttd	$$⊢\phi \to \left(x\in A⟼\underset{\dot{}}{0}\right):A⟶{\mathrm{Base}}_G$$
14		fconstmpt	$$⊢A\times \left\{\underset{\dot{}}{0}\right\}=\left(x\in A⟼\underset{\dot{}}{0}\right)$$
15	1	fvexi	$$⊢\underset{\dot{}}{0}\in \mathrm{V}$$
16	15	a1i	$$⊢\phi \to \underset{\dot{}}{0}\in \mathrm{V}$$
17	4 16	fczfsuppd	$$⊢\phi \to {finSupp}_{\underset{\dot{}}{0}}\left(\left(A\times \left\{\underset{\dot{}}{0}\right\}\right)\right)$$
18	14 17	eqbrtrrid	$$⊢\phi \to {finSupp}_{\underset{\dot{}}{0}}\left(\left(x\in A⟼\underset{\dot{}}{0}\right)\right)$$
19	9 1 2 3 4 13 18	tsmsid	$$⊢\phi \to \underset{x\in A}{{\sum }_G}\underset{\dot{}}{0}\in \left(G\mathrm{tsums}\left(x\in A⟼\underset{\dot{}}{0}\right)\right)$$
20	8 19	eqeltrrd	$$⊢\phi \to \underset{\dot{}}{0}\in \left(G\mathrm{tsums}\left(x\in A⟼\underset{\dot{}}{0}\right)\right)$$