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 gsumsnf
Description: Group sum of a singleton, 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
gsumsnf.c ⊢ Ⅎ 𝑘 𝐶
gsumsnf.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
gsumsnf.s ⊢ ( 𝑘 = 𝑀 → 𝐴 = 𝐶 )
Assertion
gsumsnf ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑀 ∈ 𝑉 ∧ 𝐶 ∈ 𝐵 ) → ( 𝐺 Σg 𝑘 ∈ { 𝑀 } ↦ 𝐴 ) ) = 𝐶 )
Proof
Step
Hyp
Ref
Expression
1
gsumsnf.c ⊢ Ⅎ 𝑘 𝐶
2
gsumsnf.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
3
gsumsnf.s ⊢ ( 𝑘 = 𝑀 → 𝐴 = 𝐶 )
4
simp1 ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑀 ∈ 𝑉 ∧ 𝐶 ∈ 𝐵 ) → 𝐺 ∈ Mnd )
5
simp2 ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑀 ∈ 𝑉 ∧ 𝐶 ∈ 𝐵 ) → 𝑀 ∈ 𝑉 )
6
simp3 ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑀 ∈ 𝑉 ∧ 𝐶 ∈ 𝐵 ) → 𝐶 ∈ 𝐵 )
7
3
adantl ⊢ ( ( ( 𝐺 ∈ Mnd ∧ 𝑀 ∈ 𝑉 ∧ 𝐶 ∈ 𝐵 ) ∧ 𝑘 = 𝑀 ) → 𝐴 = 𝐶 )
8
nfv ⊢ Ⅎ 𝑘 𝐺 ∈ Mnd
9
nfv ⊢ Ⅎ 𝑘 𝑀 ∈ 𝑉
10
1
nfel1 ⊢ Ⅎ 𝑘 𝐶 ∈ 𝐵
11
8 9 10
nf3an ⊢ Ⅎ 𝑘 ( 𝐺 ∈ Mnd ∧ 𝑀 ∈ 𝑉 ∧ 𝐶 ∈ 𝐵 )
12
2 4 5 6 7 11 1
gsumsnfd ⊢ ( ( 𝐺 ∈ Mnd ∧ 𝑀 ∈ 𝑉 ∧ 𝐶 ∈ 𝐵 ) → ( 𝐺 Σg 𝑘 ∈ { 𝑀 } ↦ 𝐴 ) ) = 𝐶 )