Database
BASIC ALGEBRAIC STRUCTURES
Groups
Abelian groups
Group sum operation
gsumf1o
Metamath Proof Explorer
Description: Re-index a finite group sum using a bijection. (Contributed by Mario
Carneiro , 15-Dec-2014) (Revised by Mario Carneiro , 24-Apr-2016)
(Revised by AV , 3-Jun-2019)
Ref
Expression
Hypotheses
gsumcl.b
⊢ 𝐵 = ( Base ‘ 𝐺 )
gsumcl.z
⊢ 0 = ( 0g ‘ 𝐺 )
gsumcl.g
⊢ ( 𝜑 → 𝐺 ∈ CMnd )
gsumcl.a
⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
gsumcl.f
⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
gsumcl.w
⊢ ( 𝜑 → 𝐹 finSupp 0 )
gsumf1o.h
⊢ ( 𝜑 → 𝐻 : 𝐶 –1-1 -onto → 𝐴 )
Assertion
gsumf1o
⊢ ( 𝜑 → ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg ( 𝐹 ∘ 𝐻 ) ) )
Proof
Step
Hyp
Ref
Expression
1
gsumcl.b
⊢ 𝐵 = ( Base ‘ 𝐺 )
2
gsumcl.z
⊢ 0 = ( 0g ‘ 𝐺 )
3
gsumcl.g
⊢ ( 𝜑 → 𝐺 ∈ CMnd )
4
gsumcl.a
⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
5
gsumcl.f
⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
6
gsumcl.w
⊢ ( 𝜑 → 𝐹 finSupp 0 )
7
gsumf1o.h
⊢ ( 𝜑 → 𝐻 : 𝐶 –1-1 -onto → 𝐴 )
8
eqid
⊢ ( Cntz ‘ 𝐺 ) = ( Cntz ‘ 𝐺 )
9
cmnmnd
⊢ ( 𝐺 ∈ CMnd → 𝐺 ∈ Mnd )
10
3 9
syl
⊢ ( 𝜑 → 𝐺 ∈ Mnd )
11
1 8 3 5
cntzcmnf
⊢ ( 𝜑 → ran 𝐹 ⊆ ( ( Cntz ‘ 𝐺 ) ‘ ran 𝐹 ) )
12
1 2 8 10 4 5 11 6 7
gsumzf1o
⊢ ( 𝜑 → ( 𝐺 Σg 𝐹 ) = ( 𝐺 Σg ( 𝐹 ∘ 𝐻 ) ) )