Theorem mgpsumz

Description: If the group sum for the multiplicative group of a unital ring contains a summand/factor that is the zero of the ring, the group sum itself is zero. (Contributed by AV, 29-Dec-2018)

	Ref	Expression
Hypotheses	mgpsumunsn.m	⊢ 𝑀 = ( mulGrp ‘ 𝑅 )
	mgpsumunsn.t	⊢ · = ( .r ‘ 𝑅 )
	mgpsumunsn.r	⊢ ( 𝜑 → 𝑅 ∈ CRing )
	mgpsumunsn.n	⊢ ( 𝜑 → 𝑁 ∈ Fin )
	mgpsumunsn.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑁 )
	mgpsumunsn.a	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑁 ) → 𝐴 ∈ ( Base ‘ 𝑅 ) )
	mgpsumz.z	⊢ 0 = ( 0g ‘ 𝑅 )
	mgpsumz.0	⊢ ( 𝑘 = 𝐼 → 𝐴 = 0 )
Assertion	mgpsumz	⊢ ( 𝜑 → ( 𝑀 Σg ( 𝑘 ∈ 𝑁 ↦ 𝐴 ) ) = 0 )

Proof

Step	Hyp	Ref	Expression
1		mgpsumunsn.m	⊢ 𝑀 = ( mulGrp ‘ 𝑅 )
2		mgpsumunsn.t	⊢ · = ( .r ‘ 𝑅 )
3		mgpsumunsn.r	⊢ ( 𝜑 → 𝑅 ∈ CRing )
4		mgpsumunsn.n	⊢ ( 𝜑 → 𝑁 ∈ Fin )
5		mgpsumunsn.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑁 )
6		mgpsumunsn.a	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑁 ) → 𝐴 ∈ ( Base ‘ 𝑅 ) )
7		mgpsumz.z	⊢ 0 = ( 0g ‘ 𝑅 )
8		mgpsumz.0	⊢ ( 𝑘 = 𝐼 → 𝐴 = 0 )
9		crngring	⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
10		ringmnd	⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Mnd )
11	9 10	syl	⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Mnd )
12	3 11	syl	⊢ ( 𝜑 → 𝑅 ∈ Mnd )
13		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
14	13 7	mndidcl	⊢ ( 𝑅 ∈ Mnd → 0 ∈ ( Base ‘ 𝑅 ) )
15	12 14	syl	⊢ ( 𝜑 → 0 ∈ ( Base ‘ 𝑅 ) )
16	1 2 3 4 5 6 15 8	mgpsumunsn	⊢ ( 𝜑 → ( 𝑀 Σg ( 𝑘 ∈ 𝑁 ↦ 𝐴 ) ) = ( ( 𝑀 Σg ( 𝑘 ∈ ( 𝑁 ∖ { 𝐼 } ) ↦ 𝐴 ) ) · 0 ) )
17	3 9	syl	⊢ ( 𝜑 → 𝑅 ∈ Ring )
18	1 13	mgpbas	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑀 )
19	1	crngmgp	⊢ ( 𝑅 ∈ CRing → 𝑀 ∈ CMnd )
20	3 19	syl	⊢ ( 𝜑 → 𝑀 ∈ CMnd )
21		diffi	⊢ ( 𝑁 ∈ Fin → ( 𝑁 ∖ { 𝐼 } ) ∈ Fin )
22	4 21	syl	⊢ ( 𝜑 → ( 𝑁 ∖ { 𝐼 } ) ∈ Fin )
23		eldifi	⊢ ( 𝑘 ∈ ( 𝑁 ∖ { 𝐼 } ) → 𝑘 ∈ 𝑁 )
24	23 6	sylan2	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑁 ∖ { 𝐼 } ) ) → 𝐴 ∈ ( Base ‘ 𝑅 ) )
25	24	ralrimiva	⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 𝑁 ∖ { 𝐼 } ) 𝐴 ∈ ( Base ‘ 𝑅 ) )
26	18 20 22 25	gsummptcl	⊢ ( 𝜑 → ( 𝑀 Σg ( 𝑘 ∈ ( 𝑁 ∖ { 𝐼 } ) ↦ 𝐴 ) ) ∈ ( Base ‘ 𝑅 ) )
27	13 2 7	ringrz	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑀 Σg ( 𝑘 ∈ ( 𝑁 ∖ { 𝐼 } ) ↦ 𝐴 ) ) ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝑀 Σg ( 𝑘 ∈ ( 𝑁 ∖ { 𝐼 } ) ↦ 𝐴 ) ) · 0 ) = 0 )
28	17 26 27	syl2anc	⊢ ( 𝜑 → ( ( 𝑀 Σg ( 𝑘 ∈ ( 𝑁 ∖ { 𝐼 } ) ↦ 𝐴 ) ) · 0 ) = 0 )
29	16 28	eqtrd	⊢ ( 𝜑 → ( 𝑀 Σg ( 𝑘 ∈ 𝑁 ↦ 𝐴 ) ) = 0 )