This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem gsuminv

Description: Inverse of a group sum. (Contributed by Mario Carneiro, 15-Dec-2014) (Revised by Mario Carneiro, 4-May-2015) (Revised by AV, 6-Jun-2019)

Ref Expression
Hypotheses gsuminv.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
gsuminv.z ⊢ 0 = ( 0g ‘ 𝐺 )
gsuminv.p ⊢ 𝐼 = ( invg ‘ 𝐺 )
gsuminv.g ⊢ ( 𝜑 → 𝐺 ∈ Abel )
gsuminv.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
gsuminv.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
gsuminv.n ⊢ ( 𝜑 → 𝐹 finSupp 0 )
Assertion gsuminv ( 𝜑 → ( 𝐺 Σg ( 𝐼 ∘ 𝐹 ) ) = ( 𝐼 ‘ ( 𝐺 Σg 𝐹 ) ) )

Proof

Step Hyp Ref Expression
1 gsuminv.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 gsuminv.z ⊢ 0 = ( 0g ‘ 𝐺 )
3 gsuminv.p ⊢ 𝐼 = ( invg ‘ 𝐺 )
4 gsuminv.g ⊢ ( 𝜑 → 𝐺 ∈ Abel )
5 gsuminv.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
6 gsuminv.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
7 gsuminv.n ⊢ ( 𝜑 → 𝐹 finSupp 0 )
8 ablcmn ⊢ ( 𝐺 ∈ Abel → 𝐺 ∈ CMnd )
9 4 8 syl ⊢ ( 𝜑 → 𝐺 ∈ CMnd )
10 cmnmnd ⊢ ( 𝐺 ∈ CMnd → 𝐺 ∈ Mnd )
11 9 10 syl ⊢ ( 𝜑 → 𝐺 ∈ Mnd )
12 1 3 invghm ⊢ ( 𝐺 ∈ Abel ↔ 𝐼 ∈ ( 𝐺 GrpHom 𝐺 ) )
13 4 12 sylib ⊢ ( 𝜑 → 𝐼 ∈ ( 𝐺 GrpHom 𝐺 ) )
14 ghmmhm ⊢ ( 𝐼 ∈ ( 𝐺 GrpHom 𝐺 ) → 𝐼 ∈ ( 𝐺 MndHom 𝐺 ) )
15 13 14 syl ⊢ ( 𝜑 → 𝐼 ∈ ( 𝐺 MndHom 𝐺 ) )
16 1 2 9 11 5 15 6 7 gsummhm ⊢ ( 𝜑 → ( 𝐺 Σg ( 𝐼 ∘ 𝐹 ) ) = ( 𝐼 ‘ ( 𝐺 Σg 𝐹 ) ) )