Metamath Proof Explorer

Theorem gsummptrev

Description: Revert ordering in a group sum. See also gsumwrev . (Contributed by Thierry Arnoux, 15-Feb-2026)

Ref Expression
Hypotheses gsummptrev.1 ⊢ 𝐵 = ( Base ‘ 𝑀 )
gsummptrev.2 ⊢ ( 𝜑 → 𝑀 ∈ CMnd )
gsummptrev.3 ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
gsummptrev.4 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → 𝑋 ∈ 𝐵 )
gsummptrev.5 ⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑘 = ( 𝑁 − 𝑙 ) ) → 𝑋 = 𝑌 )
Assertion gsummptrev ( 𝜑 → ( 𝑀 Σg ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ 𝑋 ) ) = ( 𝑀 Σg ( 𝑙 ∈ ( 0 ... 𝑁 ) ↦ 𝑌 ) ) )

Proof

Step Hyp Ref Expression
1 gsummptrev.1 ⊢ 𝐵 = ( Base ‘ 𝑀 )
2 gsummptrev.2 ⊢ ( 𝜑 → 𝑀 ∈ CMnd )
3 gsummptrev.3 ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
4 gsummptrev.4 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → 𝑋 ∈ 𝐵 )
5 gsummptrev.5 ⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑘 = ( 𝑁 − 𝑙 ) ) → 𝑋 = 𝑌 )
6 nfcv ⊢ Ⅎ 𝑘 𝑌
7 eqid ⊢ ( 0g ‘ 𝑀 ) = ( 0g ‘ 𝑀 )
8 fzfid ⊢ ( 𝜑 → ( 0 ... 𝑁 ) ∈ Fin )
9 ssidd ⊢ ( 𝜑 → 𝐵 ⊆ 𝐵 )
10 fznn0sub2 ⊢ ( 𝑙 ∈ ( 0 ... 𝑁 ) → ( 𝑁 − 𝑙 ) ∈ ( 0 ... 𝑁 ) )
11 10 adantl ⊢ ( ( 𝜑 ∧ 𝑙 ∈ ( 0 ... 𝑁 ) ) → ( 𝑁 − 𝑙 ) ∈ ( 0 ... 𝑁 ) )
12 fznn0sub2 ⊢ ( 𝑘 ∈ ( 0 ... 𝑁 ) → ( 𝑁 − 𝑘 ) ∈ ( 0 ... 𝑁 ) )
13 12 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( 𝑁 − 𝑘 ) ∈ ( 0 ... 𝑁 ) )
14 elfznn0 ⊢ ( 𝑘 ∈ ( 0 ... 𝑁 ) → 𝑘 ∈ ℕ0 )
15 14 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑙 ∈ ( 0 ... 𝑁 ) ) → 𝑘 ∈ ℕ0 )
16 15 nn0cnd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑙 ∈ ( 0 ... 𝑁 ) ) → 𝑘 ∈ ℂ )
17 elfznn0 ⊢ ( 𝑙 ∈ ( 0 ... 𝑁 ) → 𝑙 ∈ ℕ0 )
18 17 adantl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑙 ∈ ( 0 ... 𝑁 ) ) → 𝑙 ∈ ℕ0 )
19 18 nn0cnd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑙 ∈ ( 0 ... 𝑁 ) ) → 𝑙 ∈ ℂ )
20 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑙 ∈ ( 0 ... 𝑁 ) ) → 𝑁 ∈ ℕ0 )
21 20 nn0cnd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑙 ∈ ( 0 ... 𝑁 ) ) → 𝑁 ∈ ℂ )
22 16 19 21 subexsub ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑙 ∈ ( 0 ... 𝑁 ) ) → ( 𝑘 = ( 𝑁 − 𝑙 ) ↔ 𝑙 = ( 𝑁 − 𝑘 ) ) )
23 13 22 reu6dv ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ∃! 𝑙 ∈ ( 0 ... 𝑁 ) 𝑘 = ( 𝑁 − 𝑙 ) )
24 6 1 7 5 2 8 9 4 11 23 gsummptf1od ⊢ ( 𝜑 → ( 𝑀 Σg ( 𝑘 ∈ ( 0 ... 𝑁 ) ↦ 𝑋 ) ) = ( 𝑀 Σg ( 𝑙 ∈ ( 0 ... 𝑁 ) ↦ 𝑌 ) ) )