Metamath Proof Explorer


Theorem gsummptif1n0

Description: If only one summand in a finite group sum is not zero, the whole sum equals this summand. (Contributed by AV, 17-Feb-2019) (Proof shortened by AV, 11-Oct-2019)

Ref Expression
Hypotheses gsummpt1n0.0 0 = ( 0g𝐺 )
gsummpt1n0.g ( 𝜑𝐺 ∈ Mnd )
gsummpt1n0.i ( 𝜑𝐼𝑊 )
gsummpt1n0.x ( 𝜑𝑋𝐼 )
gsummpt1n0.f 𝐹 = ( 𝑛𝐼 ↦ if ( 𝑛 = 𝑋 , 𝐴 , 0 ) )
gsummptif1n0.a ( 𝜑𝐴 ∈ ( Base ‘ 𝐺 ) )
Assertion gsummptif1n0 ( 𝜑 → ( 𝐺 Σg 𝐹 ) = 𝐴 )

Proof

Step Hyp Ref Expression
1 gsummpt1n0.0 0 = ( 0g𝐺 )
2 gsummpt1n0.g ( 𝜑𝐺 ∈ Mnd )
3 gsummpt1n0.i ( 𝜑𝐼𝑊 )
4 gsummpt1n0.x ( 𝜑𝑋𝐼 )
5 gsummpt1n0.f 𝐹 = ( 𝑛𝐼 ↦ if ( 𝑛 = 𝑋 , 𝐴 , 0 ) )
6 gsummptif1n0.a ( 𝜑𝐴 ∈ ( Base ‘ 𝐺 ) )
7 6 ralrimivw ( 𝜑 → ∀ 𝑛𝐼 𝐴 ∈ ( Base ‘ 𝐺 ) )
8 1 2 3 4 5 7 gsummpt1n0 ( 𝜑 → ( 𝐺 Σg 𝐹 ) = 𝑋 / 𝑛 𝐴 )
9 csbconstg ( 𝑋𝐼 𝑋 / 𝑛 𝐴 = 𝐴 )
10 4 9 syl ( 𝜑 𝑋 / 𝑛 𝐴 = 𝐴 )
11 8 10 eqtrd ( 𝜑 → ( 𝐺 Σg 𝐹 ) = 𝐴 )