Metamath Proof Explorer

Theorem mgpsumunsn

Description: Extract a summand/factor from the group sum for the multiplicative group of a unital ring. (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 ) )
mgpsumunsn.x 
|- ( ph -> X e. ( Base ` R ) )
mgpsumunsn.e 
|- ( k = I -> A = X )
Assertion mgpsumunsn 
|- ( ph -> ( M gsum ( k e. N |-> A ) ) = ( ( M gsum ( k e. ( N \ { I } ) |-> A ) ) .x. X ) )

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 mgpsumunsn.x 
 |-  ( ph -> X e. ( Base ` R ) )
8 mgpsumunsn.e 
 |-  ( k = I -> A = X )
9 difsnid 
 |-  ( I e. N -> ( ( N \ { I } ) u. { I } ) = N )
10 5 9 syl 
 |-  ( ph -> ( ( N \ { I } ) u. { I } ) = N )
11 10 eqcomd 
 |-  ( ph -> N = ( ( N \ { I } ) u. { I } ) )
12 11 mpteq1d 
 |-  ( ph -> ( k e. N |-> A ) = ( k e. ( ( N \ { I } ) u. { I } ) |-> A ) )
13 12 oveq2d 
 |-  ( ph -> ( M gsum ( k e. N |-> A ) ) = ( M gsum ( k e. ( ( N \ { I } ) u. { I } ) |-> A ) ) )
14 eqid 
 |-  ( Base ` R ) = ( Base ` R )
15 1 14 mgpbas 
 |-  ( Base ` R ) = ( Base ` M )
16 1 2 mgpplusg 
 |-  .x. = ( +g ` 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 neldifsnd 
 |-  ( ph -> -. I e. ( N \ { I } ) )
24 15 16 18 20 22 5 23 7 8 gsumunsn 
 |-  ( ph -> ( M gsum ( k e. ( ( N \ { I } ) u. { I } ) |-> A ) ) = ( ( M gsum ( k e. ( N \ { I } ) |-> A ) ) .x. X ) )
25 13 24 eqtrd 
 |-  ( ph -> ( M gsum ( k e. N |-> A ) ) = ( ( M gsum ( k e. ( N \ { I } ) |-> A ) ) .x. X ) )