Metamath Proof Explorer


Theorem gsummgp0

Description: If one factor in a finite group sum of the multiplicative group of a commutative ring is 0, the whole "sum" (i.e. product) is 0. (Contributed by AV, 3-Jan-2019)

Ref Expression
Hypotheses gsummgp0.g
|- G = ( mulGrp ` R )
gsummgp0.0
|- .0. = ( 0g ` R )
gsummgp0.r
|- ( ph -> R e. CRing )
gsummgp0.n
|- ( ph -> N e. Fin )
gsummgp0.a
|- ( ( ph /\ n e. N ) -> A e. ( Base ` R ) )
gsummgp0.e
|- ( ( ph /\ n = i ) -> A = B )
gsummgp0.b
|- ( ph -> E. i e. N B = .0. )
Assertion gsummgp0
|- ( ph -> ( G gsum ( n e. N |-> A ) ) = .0. )

Proof

Step Hyp Ref Expression
1 gsummgp0.g
 |-  G = ( mulGrp ` R )
2 gsummgp0.0
 |-  .0. = ( 0g ` R )
3 gsummgp0.r
 |-  ( ph -> R e. CRing )
4 gsummgp0.n
 |-  ( ph -> N e. Fin )
5 gsummgp0.a
 |-  ( ( ph /\ n e. N ) -> A e. ( Base ` R ) )
6 gsummgp0.e
 |-  ( ( ph /\ n = i ) -> A = B )
7 gsummgp0.b
 |-  ( ph -> E. i e. N B = .0. )
8 difsnid
 |-  ( i e. N -> ( ( N \ { i } ) u. { i } ) = N )
9 8 eqcomd
 |-  ( i e. N -> N = ( ( N \ { i } ) u. { i } ) )
10 9 ad2antrl
 |-  ( ( ph /\ ( i e. N /\ B = .0. ) ) -> N = ( ( N \ { i } ) u. { i } ) )
11 10 mpteq1d
 |-  ( ( ph /\ ( i e. N /\ B = .0. ) ) -> ( n e. N |-> A ) = ( n e. ( ( N \ { i } ) u. { i } ) |-> A ) )
12 11 oveq2d
 |-  ( ( ph /\ ( i e. N /\ B = .0. ) ) -> ( G gsum ( n e. N |-> A ) ) = ( G gsum ( n e. ( ( N \ { i } ) u. { i } ) |-> A ) ) )
13 eqid
 |-  ( Base ` R ) = ( Base ` R )
14 1 13 mgpbas
 |-  ( Base ` R ) = ( Base ` G )
15 eqid
 |-  ( .r ` R ) = ( .r ` R )
16 1 15 mgpplusg
 |-  ( .r ` R ) = ( +g ` G )
17 1 crngmgp
 |-  ( R e. CRing -> G e. CMnd )
18 3 17 syl
 |-  ( ph -> G e. CMnd )
19 18 adantr
 |-  ( ( ph /\ ( i e. N /\ B = .0. ) ) -> G e. CMnd )
20 diffi
 |-  ( N e. Fin -> ( N \ { i } ) e. Fin )
21 4 20 syl
 |-  ( ph -> ( N \ { i } ) e. Fin )
22 21 adantr
 |-  ( ( ph /\ ( i e. N /\ B = .0. ) ) -> ( N \ { i } ) e. Fin )
23 simpl
 |-  ( ( ph /\ ( i e. N /\ B = .0. ) ) -> ph )
24 eldifi
 |-  ( n e. ( N \ { i } ) -> n e. N )
25 23 24 5 syl2an
 |-  ( ( ( ph /\ ( i e. N /\ B = .0. ) ) /\ n e. ( N \ { i } ) ) -> A e. ( Base ` R ) )
26 simprl
 |-  ( ( ph /\ ( i e. N /\ B = .0. ) ) -> i e. N )
27 neldifsnd
 |-  ( ( ph /\ ( i e. N /\ B = .0. ) ) -> -. i e. ( N \ { i } ) )
28 crngring
 |-  ( R e. CRing -> R e. Ring )
29 3 28 syl
 |-  ( ph -> R e. Ring )
30 ringmnd
 |-  ( R e. Ring -> R e. Mnd )
31 13 2 mndidcl
 |-  ( R e. Mnd -> .0. e. ( Base ` R ) )
32 29 30 31 3syl
 |-  ( ph -> .0. e. ( Base ` R ) )
33 32 adantr
 |-  ( ( ph /\ ( i e. N /\ B = .0. ) ) -> .0. e. ( Base ` R ) )
34 eleq1
 |-  ( B = .0. -> ( B e. ( Base ` R ) <-> .0. e. ( Base ` R ) ) )
35 34 ad2antll
 |-  ( ( ph /\ ( i e. N /\ B = .0. ) ) -> ( B e. ( Base ` R ) <-> .0. e. ( Base ` R ) ) )
36 33 35 mpbird
 |-  ( ( ph /\ ( i e. N /\ B = .0. ) ) -> B e. ( Base ` R ) )
37 6 adantlr
 |-  ( ( ( ph /\ ( i e. N /\ B = .0. ) ) /\ n = i ) -> A = B )
38 14 16 19 22 25 26 27 36 37 gsumunsnd
 |-  ( ( ph /\ ( i e. N /\ B = .0. ) ) -> ( G gsum ( n e. ( ( N \ { i } ) u. { i } ) |-> A ) ) = ( ( G gsum ( n e. ( N \ { i } ) |-> A ) ) ( .r ` R ) B ) )
39 oveq2
 |-  ( B = .0. -> ( ( G gsum ( n e. ( N \ { i } ) |-> A ) ) ( .r ` R ) B ) = ( ( G gsum ( n e. ( N \ { i } ) |-> A ) ) ( .r ` R ) .0. ) )
40 39 ad2antll
 |-  ( ( ph /\ ( i e. N /\ B = .0. ) ) -> ( ( G gsum ( n e. ( N \ { i } ) |-> A ) ) ( .r ` R ) B ) = ( ( G gsum ( n e. ( N \ { i } ) |-> A ) ) ( .r ` R ) .0. ) )
41 24 5 sylan2
 |-  ( ( ph /\ n e. ( N \ { i } ) ) -> A e. ( Base ` R ) )
42 41 ralrimiva
 |-  ( ph -> A. n e. ( N \ { i } ) A e. ( Base ` R ) )
43 14 18 21 42 gsummptcl
 |-  ( ph -> ( G gsum ( n e. ( N \ { i } ) |-> A ) ) e. ( Base ` R ) )
44 43 adantr
 |-  ( ( ph /\ ( i e. N /\ B = .0. ) ) -> ( G gsum ( n e. ( N \ { i } ) |-> A ) ) e. ( Base ` R ) )
45 13 15 2 ringrz
 |-  ( ( R e. Ring /\ ( G gsum ( n e. ( N \ { i } ) |-> A ) ) e. ( Base ` R ) ) -> ( ( G gsum ( n e. ( N \ { i } ) |-> A ) ) ( .r ` R ) .0. ) = .0. )
46 29 44 45 syl2an2r
 |-  ( ( ph /\ ( i e. N /\ B = .0. ) ) -> ( ( G gsum ( n e. ( N \ { i } ) |-> A ) ) ( .r ` R ) .0. ) = .0. )
47 40 46 eqtrd
 |-  ( ( ph /\ ( i e. N /\ B = .0. ) ) -> ( ( G gsum ( n e. ( N \ { i } ) |-> A ) ) ( .r ` R ) B ) = .0. )
48 12 38 47 3eqtrd
 |-  ( ( ph /\ ( i e. N /\ B = .0. ) ) -> ( G gsum ( n e. N |-> A ) ) = .0. )
49 7 48 rexlimddv
 |-  ( ph -> ( G gsum ( n e. N |-> A ) ) = .0. )