gsumdifsnd

Description: Extract a summand from a finitely supported group sum. (Contributed by AV, 21-Apr-2019) (Revised by AV, 28-Jul-2019)

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

Proof

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

Metamath Proof Explorer

Theorem gsumdifsnd

Proof