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 ⊢ B = Base G
gsuminv.z ⊢ 0 ˙ = 0 G
gsuminv.p ⊢ I = inv g ⁡ G
gsuminv.g ⊢ φ → G ∈ Abel
gsummptfidminv.a ⊢ φ → A ∈ Fin
gsummptfidminv.c ⊢ φ ∧ x ∈ A → C ∈ B
gsummptfidminv.f ⊢ F = x ∈ A ⟼ C
Assertion gsummptfidminv ⊢ φ → ∑ G I ∘ F = I ⁡ ∑ G F

Proof

Step Hyp Ref Expression
1 gsuminv.b ⊢ B = Base G
2 gsuminv.z ⊢ 0 ˙ = 0 G
3 gsuminv.p ⊢ I = inv g ⁡ G
4 gsuminv.g ⊢ φ → G ∈ Abel
5 gsummptfidminv.a ⊢ φ → A ∈ Fin
6 gsummptfidminv.c ⊢ φ ∧ x ∈ A → C ∈ B
7 gsummptfidminv.f ⊢ F = x ∈ A ⟼ C
8 6 7 fmptd ⊢ φ → F : A ⟶ B
9 2 fvexi ⊢ 0 ˙ ∈ V
10 9 a1i ⊢ φ → 0 ˙ ∈ V
11 7 5 6 10 fsuppmptdm ⊢ φ → finSupp 0 ˙⁡ F
12 1 2 3 4 5 8 11 gsuminv ⊢ φ → ∑ G I ∘ F = I ⁡ ∑ G F