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 ‘ 𝐺 )
	tsms0.1	⊢ ( 𝜑 → 𝐺 ∈ CMnd )
	tsms0.2	⊢ ( 𝜑 → 𝐺 ∈ TopSp )
	tsms0.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
Assertion	tsms0	⊢ ( 𝜑 → 0 ∈ ( 𝐺 tsums ( 𝑥 ∈ 𝐴 ↦ 0 ) ) )

Proof

Step	Hyp	Ref	Expression
1		tsms0.z	⊢ 0 = ( 0g ‘ 𝐺 )
2		tsms0.1	⊢ ( 𝜑 → 𝐺 ∈ CMnd )
3		tsms0.2	⊢ ( 𝜑 → 𝐺 ∈ TopSp )
4		tsms0.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
5		cmnmnd	⊢ ( 𝐺 ∈ CMnd → 𝐺 ∈ Mnd )
6	2 5	syl	⊢ ( 𝜑 → 𝐺 ∈ Mnd )
7	1	gsumz	⊢ ( ( 𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑉 ) → ( 𝐺 Σg ( 𝑥 ∈ 𝐴 ↦ 0 ) ) = 0 )
8	6 4 7	syl2anc	⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑥 ∈ 𝐴 ↦ 0 ) ) = 0 )
9		eqid	⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
10	9 1	mndidcl	⊢ ( 𝐺 ∈ Mnd → 0 ∈ ( Base ‘ 𝐺 ) )
11	6 10	syl	⊢ ( 𝜑 → 0 ∈ ( Base ‘ 𝐺 ) )
12	11	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 0 ∈ ( Base ‘ 𝐺 ) )
13	12	fmpttd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 0 ) : 𝐴 ⟶ ( Base ‘ 𝐺 ) )
14		fconstmpt	⊢ ( 𝐴 × { 0 } ) = ( 𝑥 ∈ 𝐴 ↦ 0 )
15	1	fvexi	⊢ 0 ∈ V
16	15	a1i	⊢ ( 𝜑 → 0 ∈ V )
17	4 16	fczfsuppd	⊢ ( 𝜑 → ( 𝐴 × { 0 } ) finSupp 0 )
18	14 17	eqbrtrrid	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 0 ) finSupp 0 )
19	9 1 2 3 4 13 18	tsmsid	⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑥 ∈ 𝐴 ↦ 0 ) ) ∈ ( 𝐺 tsums ( 𝑥 ∈ 𝐴 ↦ 0 ) ) )
20	8 19	eqeltrrd	⊢ ( 𝜑 → 0 ∈ ( 𝐺 tsums ( 𝑥 ∈ 𝐴 ↦ 0 ) ) )