Metamath Proof Explorer

Theorem mgpsumn

Description: If the group sum for the multiplicative group of a unital ring contains a summand/factor that is the one of the ring, this summand/ factor can be removed from the group sum. (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 ) )
mgpsumn.n 
|- .1. = ( 1r ` R )
mgpsumn.1 
|- ( k = I -> A = .1. )
Assertion mgpsumn 
|- ( ph -> ( M gsum ( k e. N |-> A ) ) = ( M gsum ( k e. ( N \ { I } ) |-> A ) ) )

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