This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) ) )