Theorem mgpsumunsn

Description: Extract a summand/factor from the group sum for the multiplicative group of a unital ring. (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 ‘ 𝑅 ) )
	mgpsumunsn.x	⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝑅 ) )
	mgpsumunsn.e	⊢ ( 𝑘 = 𝐼 → 𝐴 = 𝑋 )
Assertion	mgpsumunsn	⊢ ( 𝜑 → ( 𝑀 Σ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		mgpsumunsn.x	⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝑅 ) )
8		mgpsumunsn.e	⊢ ( 𝑘 = 𝐼 → 𝐴 = 𝑋 )
9		difsnid	⊢ ( 𝐼 ∈ 𝑁 → ( ( 𝑁 ∖ { 𝐼 } ) ∪ { 𝐼 } ) = 𝑁 )
10	5 9	syl	⊢ ( 𝜑 → ( ( 𝑁 ∖ { 𝐼 } ) ∪ { 𝐼 } ) = 𝑁 )
11	10	eqcomd	⊢ ( 𝜑 → 𝑁 = ( ( 𝑁 ∖ { 𝐼 } ) ∪ { 𝐼 } ) )
12	11	mpteq1d	⊢ ( 𝜑 → ( 𝑘 ∈ 𝑁 ↦ 𝐴 ) = ( 𝑘 ∈ ( ( 𝑁 ∖ { 𝐼 } ) ∪ { 𝐼 } ) ↦ 𝐴 ) )
13	12	oveq2d	⊢ ( 𝜑 → ( 𝑀 Σg ( 𝑘 ∈ 𝑁 ↦ 𝐴 ) ) = ( 𝑀 Σg ( 𝑘 ∈ ( ( 𝑁 ∖ { 𝐼 } ) ∪ { 𝐼 } ) ↦ 𝐴 ) ) )
14		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
15	1 14	mgpbas	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑀 )
16	1 2	mgpplusg	⊢ · = ( +g ‘ 𝑀 )
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		neldifsnd	⊢ ( 𝜑 → ¬ 𝐼 ∈ ( 𝑁 ∖ { 𝐼 } ) )
24	15 16 18 20 22 5 23 7 8	gsumunsn	⊢ ( 𝜑 → ( 𝑀 Σg ( 𝑘 ∈ ( ( 𝑁 ∖ { 𝐼 } ) ∪ { 𝐼 } ) ↦ 𝐴 ) ) = ( ( 𝑀 Σg ( 𝑘 ∈ ( 𝑁 ∖ { 𝐼 } ) ↦ 𝐴 ) ) · 𝑋 ) )
25	13 24	eqtrd	⊢ ( 𝜑 → ( 𝑀 Σg ( 𝑘 ∈ 𝑁 ↦ 𝐴 ) ) = ( ( 𝑀 Σg ( 𝑘 ∈ ( 𝑁 ∖ { 𝐼 } ) ↦ 𝐴 ) ) · 𝑋 ) )