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

Metamath Proof Explorer

Theorem gsummptfidminv

Description: Inverse of a group sum expressed as mapping with a finite domain. (Contributed by AV, 23-Jul-2019)

Ref Expression
Hypotheses gsuminv.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
gsuminv.z ⊢ 0 = ( 0g ‘ 𝐺 )
gsuminv.p ⊢ 𝐼 = ( invg ‘ 𝐺 )
gsuminv.g ⊢ ( 𝜑 → 𝐺 ∈ Abel )
gsummptfidminv.a ⊢ ( 𝜑 → 𝐴 ∈ Fin )
gsummptfidminv.c ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ 𝐵 )
gsummptfidminv.f ⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐶 )
Assertion gsummptfidminv ( 𝜑 → ( 𝐺 Σ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 gsummptfidminv.a ⊢ ( 𝜑 → 𝐴 ∈ Fin )
6 gsummptfidminv.c ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ 𝐵 )
7 gsummptfidminv.f ⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐶 )
8 6 7 fmptd ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
9 2 fvexi ⊢ 0 ∈ V
10 9 a1i ⊢ ( 𝜑 → 0 ∈ V )
11 7 5 6 10 fsuppmptdm ⊢ ( 𝜑 → 𝐹 finSupp 0 )
12 1 2 3 4 5 8 11 gsuminv ⊢ ( 𝜑 → ( 𝐺 Σg ( 𝐼 ∘ 𝐹 ) ) = ( 𝐼 ‘ ( 𝐺 Σg 𝐹 ) ) )