Metamath Proof Explorer

Theorem mgpsumz

Description: If the group sum for the multiplicative group of a unital ring contains a summand/factor that is the zero of the ring, the group sum itself is zero. (Contributed by AV, 29-Dec-2018)

Ref Expression
Hypotheses mgpsumunsn.m 
|- M = ( mulGrp ` R )
mgpsumunsn.t 
|- .x. = ( .r ` R )
mgpsumunsn.r 
|- ( ph -> R e. CRing )
mgpsumunsn.n 
|- ( ph -> N e. Fin )
mgpsumunsn.i 
|- ( ph -> I e. N )
mgpsumunsn.a 
|- ( ( ph /\ k e. N ) -> A e. ( Base ` R ) )
mgpsumz.z 
|- .0. = ( 0g ` R )
mgpsumz.0 
|- ( k = I -> A = .0. )
Assertion mgpsumz 
|- ( ph -> ( M gsum ( k e. N |-> A ) ) = .0. )

Proof

Step Hyp Ref Expression
1 mgpsumunsn.m 
 |-  M = ( mulGrp ` R )
2 mgpsumunsn.t 
 |-  .x. = ( .r ` R )
3 mgpsumunsn.r 
 |-  ( ph -> R e. CRing )
4 mgpsumunsn.n 
 |-  ( ph -> N e. Fin )
5 mgpsumunsn.i 
 |-  ( ph -> I e. N )
6 mgpsumunsn.a 
 |-  ( ( ph /\ k e. N ) -> A e. ( Base ` R ) )
7 mgpsumz.z 
 |-  .0. = ( 0g ` R )
8 mgpsumz.0 
 |-  ( k = I -> A = .0. )
9 crngring 
 |-  ( R e. CRing -> R e. Ring )
10 ringmnd 
 |-  ( R e. Ring -> R e. Mnd )
11 eqid 
 |-  ( Base ` R ) = ( Base ` R )
12 11 7 mndidcl 
 |-  ( R e. Mnd -> .0. e. ( Base ` R ) )
13 3 9 10 12 4syl 
 |-  ( ph -> .0. e. ( Base ` R ) )
14 1 2 3 4 5 6 13 8 mgpsumunsn 
 |-  ( ph -> ( M gsum ( k e. N |-> A ) ) = ( ( M gsum ( k e. ( N \ { I } ) |-> A ) ) .x. .0. ) )
15 3 9 syl 
 |-  ( ph -> R e. Ring )
16 1 11 mgpbas 
 |-  ( Base ` R ) = ( Base ` M )
17 1 crngmgp 
 |-  ( R e. CRing -> M e. CMnd )
18 3 17 syl 
 |-  ( ph -> M e. CMnd )
19 diffi 
 |-  ( N e. Fin -> ( N \ { I } ) e. Fin )
20 4 19 syl 
 |-  ( ph -> ( N \ { I } ) e. Fin )
21 eldifi 
 |-  ( k e. ( N \ { I } ) -> k e. N )
22 21 6 sylan2 
 |-  ( ( ph /\ k e. ( N \ { I } ) ) -> A e. ( Base ` R ) )
23 22 ralrimiva 
 |-  ( ph -> A. k e. ( N \ { I } ) A e. ( Base ` R ) )
24 16 18 20 23 gsummptcl 
 |-  ( ph -> ( M gsum ( k e. ( N \ { I } ) |-> A ) ) e. ( Base ` R ) )
25 11 2 7 ringrz 
 |-  ( ( R e. Ring /\ ( M gsum ( k e. ( N \ { I } ) |-> A ) ) e. ( Base ` R ) ) -> ( ( M gsum ( k e. ( N \ { I } ) |-> A ) ) .x. .0. ) = .0. )
26 15 24 25 syl2anc 
 |-  ( ph -> ( ( M gsum ( k e. ( N \ { I } ) |-> A ) ) .x. .0. ) = .0. )
27 14 26 eqtrd 
 |-  ( ph -> ( M gsum ( k e. N |-> A ) ) = .0. )