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{˙}{0} = 0_{G}$
	tsms0.1	$⊢ φ \to G \in CMnd$
	tsms0.2	$⊢ φ \to G \in TopSp$
	tsms0.a	$⊢ φ \to A \in V$
Assertion	tsms0	$⊢ φ \to \underset{˙}{0} \in (G tsums (x \in A ⟼ \underset{˙}{0}))$

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

Metamath Proof Explorer