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 ⊢ 𝐺 = ( 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 )