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 )