This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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. )