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