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 ( 𝐹 ∘ 𝐻 ) ) ) |
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 ( 𝐹 ∘ 𝐻 ) ) ) |