Theorem gsumunsnf

Description: Append an element to a finite group sum, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Mario Carneiro, 19-Dec-2014) (Revised by Thierry Arnoux, 28-Mar-2018) (Proof shortened by AV, 11-Dec-2019)

	Ref	Expression
Hypotheses	gsumunsnf.0	⊢ Ⅎ 𝑘 𝑌
	gsumunsnf.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
	gsumunsnf.p	⊢ + = ( +g ‘ 𝐺 )
	gsumunsnf.g	⊢ ( 𝜑 → 𝐺 ∈ CMnd )
	gsumunsnf.a	⊢ ( 𝜑 → 𝐴 ∈ Fin )
	gsumunsnf.f	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝑋 ∈ 𝐵 )
	gsumunsnf.m	⊢ ( 𝜑 → 𝑀 ∈ 𝑉 )
	gsumunsnf.d	⊢ ( 𝜑 → ¬ 𝑀 ∈ 𝐴 )
	gsumunsnf.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
	gsumunsnf.s	⊢ ( 𝑘 = 𝑀 → 𝑋 = 𝑌 )
Assertion	gsumunsnf	⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑘 ∈ ( 𝐴 ∪ { 𝑀 } ) ↦ 𝑋 ) ) = ( ( 𝐺 Σg ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) ) + 𝑌 ) )

Proof

Step	Hyp	Ref	Expression
1		gsumunsnf.0	⊢ Ⅎ 𝑘 𝑌
2		gsumunsnf.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
3		gsumunsnf.p	⊢ + = ( +g ‘ 𝐺 )
4		gsumunsnf.g	⊢ ( 𝜑 → 𝐺 ∈ CMnd )
5		gsumunsnf.a	⊢ ( 𝜑 → 𝐴 ∈ Fin )
6		gsumunsnf.f	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝑋 ∈ 𝐵 )
7		gsumunsnf.m	⊢ ( 𝜑 → 𝑀 ∈ 𝑉 )
8		gsumunsnf.d	⊢ ( 𝜑 → ¬ 𝑀 ∈ 𝐴 )
9		gsumunsnf.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
10		gsumunsnf.s	⊢ ( 𝑘 = 𝑀 → 𝑋 = 𝑌 )
11	10	adantl	⊢ ( ( 𝜑 ∧ 𝑘 = 𝑀 ) → 𝑋 = 𝑌 )
12	2 3 4 5 6 7 8 9 11 1	gsumunsnfd	⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑘 ∈ ( 𝐴 ∪ { 𝑀 } ) ↦ 𝑋 ) ) = ( ( 𝐺 Σg ( 𝑘 ∈ 𝐴 ↦ 𝑋 ) ) + 𝑌 ) )