Theorem gsumdifsndf

Description: Extract a summand from a finitely supported group sum. (Contributed by AV, 4-Sep-2019)

	Ref	Expression
Hypotheses	gsumdifsndf.k	⊢ Ⅎ 𝑘 𝑌
	gsumdifsndf.n	⊢ Ⅎ 𝑘 𝜑
	gsumdifsndf.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
	gsumdifsndf.p	⊢ + = ( +g ‘ 𝐺 )
	gsumdifsndf.g	⊢ ( 𝜑 → 𝐺 ∈ CMnd )
	gsumdifsndf.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑊 )
	gsumdifsndf.f	⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) finSupp ( 0g ‘ 𝐺 ) )
	gsumdifsndf.e	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝑋 ∈ 𝐵 )
	gsumdifsndf.m	⊢ ( 𝜑 → 𝑀 ∈ 𝐴 )
	gsumdifsndf.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
	gsumdifsndf.s	⊢ ( ( 𝜑 ∧ 𝑘 = 𝑀 ) → 𝑋 = 𝑌 )
Assertion	gsumdifsndf	⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) ) = ( ( 𝐺 Σg ( 𝑘 ∈ ( 𝐴 ∖ { 𝑀 } ) ↦ 𝑋 ) ) + 𝑌 ) )

Proof

Step	Hyp	Ref	Expression
1		gsumdifsndf.k	⊢ Ⅎ 𝑘 𝑌
2		gsumdifsndf.n	⊢ Ⅎ 𝑘 𝜑
3		gsumdifsndf.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
4		gsumdifsndf.p	⊢ + = ( +g ‘ 𝐺 )
5		gsumdifsndf.g	⊢ ( 𝜑 → 𝐺 ∈ CMnd )
6		gsumdifsndf.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑊 )
7		gsumdifsndf.f	⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) finSupp ( 0g ‘ 𝐺 ) )
8		gsumdifsndf.e	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝑋 ∈ 𝐵 )
9		gsumdifsndf.m	⊢ ( 𝜑 → 𝑀 ∈ 𝐴 )
10		gsumdifsndf.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
11		gsumdifsndf.s	⊢ ( ( 𝜑 ∧ 𝑘 = 𝑀 ) → 𝑋 = 𝑌 )
12		eqid	⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
13	9	snssd	⊢ ( 𝜑 → { 𝑀 } ⊆ 𝐴 )
14		difin2	⊢ ( { 𝑀 } ⊆ 𝐴 → ( { 𝑀 } ∖ { 𝑀 } ) = ( ( 𝐴 ∖ { 𝑀 } ) ∩ { 𝑀 } ) )
15	13 14	syl	⊢ ( 𝜑 → ( { 𝑀 } ∖ { 𝑀 } ) = ( ( 𝐴 ∖ { 𝑀 } ) ∩ { 𝑀 } ) )
16		difid	⊢ ( { 𝑀 } ∖ { 𝑀 } ) = ∅
17	15 16	eqtr3di	⊢ ( 𝜑 → ( ( 𝐴 ∖ { 𝑀 } ) ∩ { 𝑀 } ) = ∅ )
18		difsnid	⊢ ( 𝑀 ∈ 𝐴 → ( ( 𝐴 ∖ { 𝑀 } ) ∪ { 𝑀 } ) = 𝐴 )
19	9 18	syl	⊢ ( 𝜑 → ( ( 𝐴 ∖ { 𝑀 } ) ∪ { 𝑀 } ) = 𝐴 )
20	19	eqcomd	⊢ ( 𝜑 → 𝐴 = ( ( 𝐴 ∖ { 𝑀 } ) ∪ { 𝑀 } ) )
21	2 3 12 4 5 6 8 7 17 20	gsumsplit2f	⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) ) = ( ( 𝐺 Σg ( 𝑘 ∈ ( 𝐴 ∖ { 𝑀 } ) ↦ 𝑋 ) ) + ( 𝐺 Σg ( 𝑘 ∈ { 𝑀 } ↦ 𝑋 ) ) ) )
22		cmnmnd	⊢ ( 𝐺 ∈ CMnd → 𝐺 ∈ Mnd )
23	5 22	syl	⊢ ( 𝜑 → 𝐺 ∈ Mnd )
24	3 23 9 10 11 2 1	gsumsnfd	⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑘 ∈ { 𝑀 } ↦ 𝑋 ) ) = 𝑌 )
25	24	oveq2d	⊢ ( 𝜑 → ( ( 𝐺 Σg ( 𝑘 ∈ ( 𝐴 ∖ { 𝑀 } ) ↦ 𝑋 ) ) + ( 𝐺 Σg ( 𝑘 ∈ { 𝑀 } ↦ 𝑋 ) ) ) = ( ( 𝐺 Σg ( 𝑘 ∈ ( 𝐴 ∖ { 𝑀 } ) ↦ 𝑋 ) ) + 𝑌 ) )
26	21 25	eqtrd	⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) ) = ( ( 𝐺 Σg ( 𝑘 ∈ ( 𝐴 ∖ { 𝑀 } ) ↦ 𝑋 ) ) + 𝑌 ) )