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

Metamath Proof Explorer

Theorem gsumsnfd

Description: Group sum of a singleton, deduction form, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Mario Carneiro, 19-Dec-2014) (Revised by Thierry Arnoux, 28-Mar-2018) (Revised by AV, 11-Dec-2019)

Ref Expression
Hypotheses gsumsnd.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
gsumsnd.g ⊢ ( 𝜑 → 𝐺 ∈ Mnd )
gsumsnd.m ⊢ ( 𝜑 → 𝑀 ∈ 𝑉 )
gsumsnd.c ⊢ ( 𝜑 → 𝐶 ∈ 𝐵 )
gsumsnd.s ⊢ ( ( 𝜑 ∧ 𝑘 = 𝑀 ) → 𝐴 = 𝐶 )
gsumsnfd.p ⊢ Ⅎ 𝑘 𝜑
gsumsnfd.c ⊢ Ⅎ 𝑘 𝐶
Assertion gsumsnfd ( 𝜑 → ( 𝐺 Σg ( 𝑘 ∈ { 𝑀 } ↦ 𝐴 ) ) = 𝐶 )

Proof

Step Hyp Ref Expression
1 gsumsnd.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 gsumsnd.g ⊢ ( 𝜑 → 𝐺 ∈ Mnd )
3 gsumsnd.m ⊢ ( 𝜑 → 𝑀 ∈ 𝑉 )
4 gsumsnd.c ⊢ ( 𝜑 → 𝐶 ∈ 𝐵 )
5 gsumsnd.s ⊢ ( ( 𝜑 ∧ 𝑘 = 𝑀 ) → 𝐴 = 𝐶 )
6 gsumsnfd.p ⊢ Ⅎ 𝑘 𝜑
7 gsumsnfd.c ⊢ Ⅎ 𝑘 𝐶
8 elsni ⊢ ( 𝑘 ∈ { 𝑀 } → 𝑘 = 𝑀 )
9 8 5 sylan2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ { 𝑀 } ) → 𝐴 = 𝐶 )
10 6 9 mpteq2da ⊢ ( 𝜑 → ( 𝑘 ∈ { 𝑀 } ↦ 𝐴 ) = ( 𝑘 ∈ { 𝑀 } ↦ 𝐶 ) )
11 10 oveq2d ⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑘 ∈ { 𝑀 } ↦ 𝐴 ) ) = ( 𝐺 Σg ( 𝑘 ∈ { 𝑀 } ↦ 𝐶 ) ) )
12 snfi ⊢ { 𝑀 } ∈ Fin
13 12 a1i ⊢ ( 𝜑 → { 𝑀 } ∈ Fin )
14 eqid ⊢ ( .g ‘ 𝐺 ) = ( .g ‘ 𝐺 )
15 7 1 14 gsumconstf ⊢ ( ( 𝐺 ∈ Mnd ∧ { 𝑀 } ∈ Fin ∧ 𝐶 ∈ 𝐵 ) → ( 𝐺 Σg ( 𝑘 ∈ { 𝑀 } ↦ 𝐶 ) ) = ( ( ♯ ‘ { 𝑀 } ) ( .g ‘ 𝐺 ) 𝐶 ) )
16 2 13 4 15 syl3anc ⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑘 ∈ { 𝑀 } ↦ 𝐶 ) ) = ( ( ♯ ‘ { 𝑀 } ) ( .g ‘ 𝐺 ) 𝐶 ) )
17 11 16 eqtrd ⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑘 ∈ { 𝑀 } ↦ 𝐴 ) ) = ( ( ♯ ‘ { 𝑀 } ) ( .g ‘ 𝐺 ) 𝐶 ) )
18 hashsng ⊢ ( 𝑀 ∈ 𝑉 → ( ♯ ‘ { 𝑀 } ) = 1 )
19 3 18 syl ⊢ ( 𝜑 → ( ♯ ‘ { 𝑀 } ) = 1 )
20 19 oveq1d ⊢ ( 𝜑 → ( ( ♯ ‘ { 𝑀 } ) ( .g ‘ 𝐺 ) 𝐶 ) = ( 1 ( .g ‘ 𝐺 ) 𝐶 ) )
21 1 14 mulg1 ⊢ ( 𝐶 ∈ 𝐵 → ( 1 ( .g ‘ 𝐺 ) 𝐶 ) = 𝐶 )
22 4 21 syl ⊢ ( 𝜑 → ( 1 ( .g ‘ 𝐺 ) 𝐶 ) = 𝐶 )
23 17 20 22 3eqtrd ⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑘 ∈ { 𝑀 } ↦ 𝐴 ) ) = 𝐶 )