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

Metamath Proof Explorer

Theorem gsumunsn

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

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

Proof

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