Theorem mgpsumn

Description: If the group sum for the multiplicative group of a unital ring contains a summand/factor that is the one of the ring, this summand/ factor can be removed from the group sum. (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 ‘ 𝑅 ) )
	mgpsumn.n	⊢ 1 = ( 1r ‘ 𝑅 )
	mgpsumn.1	⊢ ( 𝑘 = 𝐼 → 𝐴 = 1 )
Assertion	mgpsumn	⊢ ( 𝜑 → ( 𝑀 Σg ( 𝑘 ∈ 𝑁 ↦ 𝐴 ) ) = ( 𝑀 Σg ( 𝑘 ∈ ( 𝑁 ∖ { 𝐼 } ) ↦ 𝐴 ) ) )

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