Metamath Proof Explorer


Theorem gsumreidx

Description: Re-index a finite group sum using a bijection. Corresponds to the first equation in Lang p. 5 with M = 1 . (Contributed by AV, 26-Dec-2023)

Ref Expression
Hypotheses gsumreidx.b 𝐵 = ( Base ‘ 𝐺 )
gsumreidx.z 0 = ( 0g𝐺 )
gsumreidx.g ( 𝜑𝐺 ∈ CMnd )
gsumreidx.f ( 𝜑𝐹 : ( 𝑀 ... 𝑁 ) ⟶ 𝐵 )
gsumreidx.h ( 𝜑𝐻 : ( 𝑀 ... 𝑁 ) –1-1-onto→ ( 𝑀 ... 𝑁 ) )
Assertion gsumreidx ( 𝜑 → ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg ( 𝐹𝐻 ) ) )

Proof

Step Hyp Ref Expression
1 gsumreidx.b 𝐵 = ( Base ‘ 𝐺 )
2 gsumreidx.z 0 = ( 0g𝐺 )
3 gsumreidx.g ( 𝜑𝐺 ∈ CMnd )
4 gsumreidx.f ( 𝜑𝐹 : ( 𝑀 ... 𝑁 ) ⟶ 𝐵 )
5 gsumreidx.h ( 𝜑𝐻 : ( 𝑀 ... 𝑁 ) –1-1-onto→ ( 𝑀 ... 𝑁 ) )
6 ovexd ( 𝜑 → ( 𝑀 ... 𝑁 ) ∈ V )
7 fzfid ( 𝜑 → ( 𝑀 ... 𝑁 ) ∈ Fin )
8 2 fvexi 0 ∈ V
9 8 a1i ( 𝜑0 ∈ V )
10 4 7 9 fdmfifsupp ( 𝜑𝐹 finSupp 0 )
11 1 2 3 6 4 10 5 gsumf1o ( 𝜑 → ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg ( 𝐹𝐻 ) ) )