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 𝐹 ) = 𝐴 ) |
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 𝐹 ) = 𝐴 ) |