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