This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database BASIC ALGEBRAIC STRUCTURES Groups Abelian groups Group sum operation 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 𝑘 ∈ 𝐴 ↦ 𝑋 ) ) + 𝑌 ) )