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	⊢ ( 𝜑 → 𝑁 ∈ ℕ₀ )
	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	⊢ ( 𝜑 → 𝑁 ∈ ℕ₀ )
4		gsummptrev.4	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → 𝑋 ∈ 𝐵 )
5		gsummptrev.5	⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑘 = ( 𝑁 − 𝑙 ) ) → 𝑋 = 𝑌 )
6		nfcv	⊢ Ⅎ 𝑘 𝑌
7		eqid	⊢ ( 0_g ‘ 𝑀 ) = ( 0_g ‘ 𝑀 )
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 ... 𝑁 ) → 𝑘 ∈ ℕ₀ )
15	14	ad2antlr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑙 ∈ ( 0 ... 𝑁 ) ) → 𝑘 ∈ ℕ₀ )
16	15	nn0cnd	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑙 ∈ ( 0 ... 𝑁 ) ) → 𝑘 ∈ ℂ )
17		elfznn0	⊢ ( 𝑙 ∈ ( 0 ... 𝑁 ) → 𝑙 ∈ ℕ₀ )
18	17	adantl	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑙 ∈ ( 0 ... 𝑁 ) ) → 𝑙 ∈ ℕ₀ )
19	18	nn0cnd	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) ∧ 𝑙 ∈ ( 0 ... 𝑁 ) ) → 𝑙 ∈ ℂ )
20	3	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 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 ... 𝑁 ) ↦ 𝑌 ) ) )

Metamath Proof Explorer

Theorem gsummptrev

Proof