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		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
12	11 7	mndidcl	⊢ ( 𝑅 ∈ Mnd → 0 ∈ ( Base ‘ 𝑅 ) )
13	3 9 10 12	4syl	⊢ ( 𝜑 → 0 ∈ ( Base ‘ 𝑅 ) )
14	1 2 3 4 5 6 13 8	mgpsumunsn	⊢ ( 𝜑 → ( 𝑀 Σg ( 𝑘 ∈ 𝑁 ↦ 𝐴 ) ) = ( ( 𝑀 Σg ( 𝑘 ∈ ( 𝑁 ∖ { 𝐼 } ) ↦ 𝐴 ) ) · 0 ) )
15	3 9	syl	⊢ ( 𝜑 → 𝑅 ∈ Ring )
16	1 11	mgpbas	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑀 )
17	1	crngmgp	⊢ ( 𝑅 ∈ CRing → 𝑀 ∈ CMnd )
18	3 17	syl	⊢ ( 𝜑 → 𝑀 ∈ CMnd )
19		diffi	⊢ ( 𝑁 ∈ Fin → ( 𝑁 ∖ { 𝐼 } ) ∈ Fin )
20	4 19	syl	⊢ ( 𝜑 → ( 𝑁 ∖ { 𝐼 } ) ∈ Fin )
21		eldifi	⊢ ( 𝑘 ∈ ( 𝑁 ∖ { 𝐼 } ) → 𝑘 ∈ 𝑁 )
22	21 6	sylan2	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑁 ∖ { 𝐼 } ) ) → 𝐴 ∈ ( Base ‘ 𝑅 ) )
23	22	ralrimiva	⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 𝑁 ∖ { 𝐼 } ) 𝐴 ∈ ( Base ‘ 𝑅 ) )
24	16 18 20 23	gsummptcl	⊢ ( 𝜑 → ( 𝑀 Σg ( 𝑘 ∈ ( 𝑁 ∖ { 𝐼 } ) ↦ 𝐴 ) ) ∈ ( Base ‘ 𝑅 ) )
25	11 2 7	ringrz	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑀 Σg ( 𝑘 ∈ ( 𝑁 ∖ { 𝐼 } ) ↦ 𝐴 ) ) ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝑀 Σg ( 𝑘 ∈ ( 𝑁 ∖ { 𝐼 } ) ↦ 𝐴 ) ) · 0 ) = 0 )
26	15 24 25	syl2anc	⊢ ( 𝜑 → ( ( 𝑀 Σg ( 𝑘 ∈ ( 𝑁 ∖ { 𝐼 } ) ↦ 𝐴 ) ) · 0 ) = 0 )
27	14 26	eqtrd	⊢ ( 𝜑 → ( 𝑀 Σg ( 𝑘 ∈ 𝑁 ↦ 𝐴 ) ) = 0 )