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 𝐺 = ( mulGrp ‘ 𝑅 )
gsummgp0.0 0 = ( 0g𝑅 )
gsummgp0.r ( 𝜑𝑅 ∈ CRing )
gsummgp0.n ( 𝜑𝑁 ∈ Fin )
gsummgp0.a ( ( 𝜑𝑛𝑁 ) → 𝐴 ∈ ( Base ‘ 𝑅 ) )
gsummgp0.e ( ( 𝜑𝑛 = 𝑖 ) → 𝐴 = 𝐵 )
gsummgp0.b ( 𝜑 → ∃ 𝑖𝑁 𝐵 = 0 )
Assertion gsummgp0 ( 𝜑 → ( 𝐺 Σg ( 𝑛𝑁𝐴 ) ) = 0 )

Proof

Step Hyp Ref Expression
1 gsummgp0.g 𝐺 = ( mulGrp ‘ 𝑅 )
2 gsummgp0.0 0 = ( 0g𝑅 )
3 gsummgp0.r ( 𝜑𝑅 ∈ CRing )
4 gsummgp0.n ( 𝜑𝑁 ∈ Fin )
5 gsummgp0.a ( ( 𝜑𝑛𝑁 ) → 𝐴 ∈ ( Base ‘ 𝑅 ) )
6 gsummgp0.e ( ( 𝜑𝑛 = 𝑖 ) → 𝐴 = 𝐵 )
7 gsummgp0.b ( 𝜑 → ∃ 𝑖𝑁 𝐵 = 0 )
8 difsnid ( 𝑖𝑁 → ( ( 𝑁 ∖ { 𝑖 } ) ∪ { 𝑖 } ) = 𝑁 )
9 8 eqcomd ( 𝑖𝑁𝑁 = ( ( 𝑁 ∖ { 𝑖 } ) ∪ { 𝑖 } ) )
10 9 ad2antrl ( ( 𝜑 ∧ ( 𝑖𝑁𝐵 = 0 ) ) → 𝑁 = ( ( 𝑁 ∖ { 𝑖 } ) ∪ { 𝑖 } ) )
11 10 mpteq1d ( ( 𝜑 ∧ ( 𝑖𝑁𝐵 = 0 ) ) → ( 𝑛𝑁𝐴 ) = ( 𝑛 ∈ ( ( 𝑁 ∖ { 𝑖 } ) ∪ { 𝑖 } ) ↦ 𝐴 ) )
12 11 oveq2d ( ( 𝜑 ∧ ( 𝑖𝑁𝐵 = 0 ) ) → ( 𝐺 Σg ( 𝑛𝑁𝐴 ) ) = ( 𝐺 Σg ( 𝑛 ∈ ( ( 𝑁 ∖ { 𝑖 } ) ∪ { 𝑖 } ) ↦ 𝐴 ) ) )
13 eqid ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
14 1 13 mgpbas ( Base ‘ 𝑅 ) = ( Base ‘ 𝐺 )
15 eqid ( .r𝑅 ) = ( .r𝑅 )
16 1 15 mgpplusg ( .r𝑅 ) = ( +g𝐺 )
17 1 crngmgp ( 𝑅 ∈ CRing → 𝐺 ∈ CMnd )
18 3 17 syl ( 𝜑𝐺 ∈ CMnd )
19 18 adantr ( ( 𝜑 ∧ ( 𝑖𝑁𝐵 = 0 ) ) → 𝐺 ∈ CMnd )
20 diffi ( 𝑁 ∈ Fin → ( 𝑁 ∖ { 𝑖 } ) ∈ Fin )
21 4 20 syl ( 𝜑 → ( 𝑁 ∖ { 𝑖 } ) ∈ Fin )
22 21 adantr ( ( 𝜑 ∧ ( 𝑖𝑁𝐵 = 0 ) ) → ( 𝑁 ∖ { 𝑖 } ) ∈ Fin )
23 simpl ( ( 𝜑 ∧ ( 𝑖𝑁𝐵 = 0 ) ) → 𝜑 )
24 eldifi ( 𝑛 ∈ ( 𝑁 ∖ { 𝑖 } ) → 𝑛𝑁 )
25 23 24 5 syl2an ( ( ( 𝜑 ∧ ( 𝑖𝑁𝐵 = 0 ) ) ∧ 𝑛 ∈ ( 𝑁 ∖ { 𝑖 } ) ) → 𝐴 ∈ ( Base ‘ 𝑅 ) )
26 simprl ( ( 𝜑 ∧ ( 𝑖𝑁𝐵 = 0 ) ) → 𝑖𝑁 )
27 neldifsnd ( ( 𝜑 ∧ ( 𝑖𝑁𝐵 = 0 ) ) → ¬ 𝑖 ∈ ( 𝑁 ∖ { 𝑖 } ) )
28 crngring ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
29 3 28 syl ( 𝜑𝑅 ∈ Ring )
30 ringmnd ( 𝑅 ∈ Ring → 𝑅 ∈ Mnd )
31 13 2 mndidcl ( 𝑅 ∈ Mnd → 0 ∈ ( Base ‘ 𝑅 ) )
32 29 30 31 3syl ( 𝜑0 ∈ ( Base ‘ 𝑅 ) )
33 32 adantr ( ( 𝜑 ∧ ( 𝑖𝑁𝐵 = 0 ) ) → 0 ∈ ( Base ‘ 𝑅 ) )
34 eleq1 ( 𝐵 = 0 → ( 𝐵 ∈ ( Base ‘ 𝑅 ) ↔ 0 ∈ ( Base ‘ 𝑅 ) ) )
35 34 ad2antll ( ( 𝜑 ∧ ( 𝑖𝑁𝐵 = 0 ) ) → ( 𝐵 ∈ ( Base ‘ 𝑅 ) ↔ 0 ∈ ( Base ‘ 𝑅 ) ) )
36 33 35 mpbird ( ( 𝜑 ∧ ( 𝑖𝑁𝐵 = 0 ) ) → 𝐵 ∈ ( Base ‘ 𝑅 ) )
37 6 adantlr ( ( ( 𝜑 ∧ ( 𝑖𝑁𝐵 = 0 ) ) ∧ 𝑛 = 𝑖 ) → 𝐴 = 𝐵 )
38 14 16 19 22 25 26 27 36 37 gsumunsnd ( ( 𝜑 ∧ ( 𝑖𝑁𝐵 = 0 ) ) → ( 𝐺 Σg ( 𝑛 ∈ ( ( 𝑁 ∖ { 𝑖 } ) ∪ { 𝑖 } ) ↦ 𝐴 ) ) = ( ( 𝐺 Σg ( 𝑛 ∈ ( 𝑁 ∖ { 𝑖 } ) ↦ 𝐴 ) ) ( .r𝑅 ) 𝐵 ) )
39 oveq2 ( 𝐵 = 0 → ( ( 𝐺 Σg ( 𝑛 ∈ ( 𝑁 ∖ { 𝑖 } ) ↦ 𝐴 ) ) ( .r𝑅 ) 𝐵 ) = ( ( 𝐺 Σg ( 𝑛 ∈ ( 𝑁 ∖ { 𝑖 } ) ↦ 𝐴 ) ) ( .r𝑅 ) 0 ) )
40 39 ad2antll ( ( 𝜑 ∧ ( 𝑖𝑁𝐵 = 0 ) ) → ( ( 𝐺 Σg ( 𝑛 ∈ ( 𝑁 ∖ { 𝑖 } ) ↦ 𝐴 ) ) ( .r𝑅 ) 𝐵 ) = ( ( 𝐺 Σg ( 𝑛 ∈ ( 𝑁 ∖ { 𝑖 } ) ↦ 𝐴 ) ) ( .r𝑅 ) 0 ) )
41 24 5 sylan2 ( ( 𝜑𝑛 ∈ ( 𝑁 ∖ { 𝑖 } ) ) → 𝐴 ∈ ( Base ‘ 𝑅 ) )
42 41 ralrimiva ( 𝜑 → ∀ 𝑛 ∈ ( 𝑁 ∖ { 𝑖 } ) 𝐴 ∈ ( Base ‘ 𝑅 ) )
43 14 18 21 42 gsummptcl ( 𝜑 → ( 𝐺 Σg ( 𝑛 ∈ ( 𝑁 ∖ { 𝑖 } ) ↦ 𝐴 ) ) ∈ ( Base ‘ 𝑅 ) )
44 43 adantr ( ( 𝜑 ∧ ( 𝑖𝑁𝐵 = 0 ) ) → ( 𝐺 Σg ( 𝑛 ∈ ( 𝑁 ∖ { 𝑖 } ) ↦ 𝐴 ) ) ∈ ( Base ‘ 𝑅 ) )
45 13 15 2 ringrz ( ( 𝑅 ∈ Ring ∧ ( 𝐺 Σg ( 𝑛 ∈ ( 𝑁 ∖ { 𝑖 } ) ↦ 𝐴 ) ) ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝐺 Σg ( 𝑛 ∈ ( 𝑁 ∖ { 𝑖 } ) ↦ 𝐴 ) ) ( .r𝑅 ) 0 ) = 0 )
46 29 44 45 syl2an2r ( ( 𝜑 ∧ ( 𝑖𝑁𝐵 = 0 ) ) → ( ( 𝐺 Σg ( 𝑛 ∈ ( 𝑁 ∖ { 𝑖 } ) ↦ 𝐴 ) ) ( .r𝑅 ) 0 ) = 0 )
47 40 46 eqtrd ( ( 𝜑 ∧ ( 𝑖𝑁𝐵 = 0 ) ) → ( ( 𝐺 Σg ( 𝑛 ∈ ( 𝑁 ∖ { 𝑖 } ) ↦ 𝐴 ) ) ( .r𝑅 ) 𝐵 ) = 0 )
48 12 38 47 3eqtrd ( ( 𝜑 ∧ ( 𝑖𝑁𝐵 = 0 ) ) → ( 𝐺 Σg ( 𝑛𝑁𝐴 ) ) = 0 )
49 7 48 rexlimddv ( 𝜑 → ( 𝐺 Σg ( 𝑛𝑁𝐴 ) ) = 0 )