This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem gsumunsnd

Description: Append an element to a finite group sum. (Contributed by Mario Carneiro, 19-Dec-2014) (Revised by AV, 2-Jan-2019) (Proof shortened by AV, 11-Dec-2019)

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

Proof

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