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	|- .0. = ( 0g ` G )
	tsms0.1	|- ( ph -> G e. CMnd )
	tsms0.2	|- ( ph -> G e. TopSp )
	tsms0.a	|- ( ph -> A e. V )
Assertion	tsms0	|- ( ph -> .0. e. ( G tsums ( x e. A |-> .0. ) ) )

Proof

Step	Hyp	Ref	Expression
1		tsms0.z	|- .0. = ( 0g ` G )
2		tsms0.1	|- ( ph -> G e. CMnd )
3		tsms0.2	|- ( ph -> G e. TopSp )
4		tsms0.a	|- ( ph -> A e. V )
5		cmnmnd	|- ( G e. CMnd -> G e. Mnd )
6	2 5	syl	|- ( ph -> G e. Mnd )
7	1	gsumz	|- ( ( G e. Mnd /\ A e. V ) -> ( G gsum ( x e. A |-> .0. ) ) = .0. )
8	6 4 7	syl2anc	|- ( ph -> ( G gsum ( x e. A |-> .0. ) ) = .0. )
9		eqid	|- ( Base ` G ) = ( Base ` G )
10	9 1	mndidcl	|- ( G e. Mnd -> .0. e. ( Base ` G ) )
11	6 10	syl	|- ( ph -> .0. e. ( Base ` G ) )
12	11	adantr	|- ( ( ph /\ x e. A ) -> .0. e. ( Base ` G ) )
13	12	fmpttd	|- ( ph -> ( x e. A |-> .0. ) : A --> ( Base ` G ) )
14		fconstmpt	|- ( A X. { .0. } ) = ( x e. A |-> .0. )
15	1	fvexi	|- .0. e. _V
16	15	a1i	|- ( ph -> .0. e. _V )
17	4 16	fczfsuppd	|- ( ph -> ( A X. { .0. } ) finSupp .0. )
18	14 17	eqbrtrrid	|- ( ph -> ( x e. A |-> .0. ) finSupp .0. )
19	9 1 2 3 4 13 18	tsmsid	|- ( ph -> ( G gsum ( x e. A |-> .0. ) ) e. ( G tsums ( x e. A |-> .0. ) ) )
20	8 19	eqeltrrd	|- ( ph -> .0. e. ( G tsums ( x e. A |-> .0. ) ) )