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