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 9 10 syl 
 |-  ( R e. CRing -> R e. Mnd )
12 3 11 syl 
 |-  ( ph -> R e. Mnd )
13 eqid 
 |-  ( Base ` R ) = ( Base ` R )
14 13 7 mndidcl 
 |-  ( R e. Mnd -> .0. e. ( Base ` R ) )
15 12 14 syl 
 |-  ( ph -> .0. e. ( Base ` R ) )
16 1 2 3 4 5 6 15 8 mgpsumunsn 
 |-  ( ph -> ( M gsum ( k e. N |-> A ) ) = ( ( M gsum ( k e. ( N \ { I } ) |-> A ) ) .x. .0. ) )
17 3 9 syl 
 |-  ( ph -> R e. Ring )
18 1 13 mgpbas 
 |-  ( Base ` R ) = ( Base ` M )
19 1 crngmgp 
 |-  ( R e. CRing -> M e. CMnd )
20 3 19 syl 
 |-  ( ph -> M e. CMnd )
21 diffi 
 |-  ( N e. Fin -> ( N \ { I } ) e. Fin )
22 4 21 syl 
 |-  ( ph -> ( N \ { I } ) e. Fin )
23 eldifi 
 |-  ( k e. ( N \ { I } ) -> k e. N )
24 23 6 sylan2 
 |-  ( ( ph /\ k e. ( N \ { I } ) ) -> A e. ( Base ` R ) )
25 24 ralrimiva 
 |-  ( ph -> A. k e. ( N \ { I } ) A e. ( Base ` R ) )
26 18 20 22 25 gsummptcl 
 |-  ( ph -> ( M gsum ( k e. ( N \ { I } ) |-> A ) ) e. ( Base ` R ) )
27 13 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. )
28 17 26 27 syl2anc 
 |-  ( ph -> ( ( M gsum ( k e. ( N \ { I } ) |-> A ) ) .x. .0. ) = .0. )
29 16 28 eqtrd 
 |-  ( ph -> ( M gsum ( k e. N |-> A ) ) = .0. )