Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  gsummptcl Structured version   Visualization version   GIF version

Theorem gsummptcl 18189
 Description: Closure of a finite group sum over a finite set as map. (Contributed by AV, 29-Dec-2018.)
Hypotheses
Ref Expression
gsummptcl.b 𝐵 = (Base‘𝐺)
gsummptcl.g (𝜑𝐺 ∈ CMnd)
gsummptcl.n (𝜑𝑁 ∈ Fin)
gsummptcl.e (𝜑 → ∀𝑖𝑁 𝑋𝐵)
Assertion
Ref Expression
gsummptcl (𝜑 → (𝐺 Σg (𝑖𝑁𝑋)) ∈ 𝐵)
Distinct variable groups:   𝐵,𝑖   𝑖,𝑁
Allowed substitution hints:   𝜑(𝑖)   𝐺(𝑖)   𝑋(𝑖)

Proof of Theorem gsummptcl
StepHypRef Expression
1 gsummptcl.b . 2 𝐵 = (Base‘𝐺)
2 eqid 2610 . 2 (0g𝐺) = (0g𝐺)
3 gsummptcl.g . 2 (𝜑𝐺 ∈ CMnd)
4 gsummptcl.n . 2 (𝜑𝑁 ∈ Fin)
5 gsummptcl.e . . 3 (𝜑 → ∀𝑖𝑁 𝑋𝐵)
6 eqid 2610 . . . 4 (𝑖𝑁𝑋) = (𝑖𝑁𝑋)
76fmpt 6289 . . 3 (∀𝑖𝑁 𝑋𝐵 ↔ (𝑖𝑁𝑋):𝑁𝐵)
85, 7sylib 207 . 2 (𝜑 → (𝑖𝑁𝑋):𝑁𝐵)
96fnmpt 5933 . . . 4 (∀𝑖𝑁 𝑋𝐵 → (𝑖𝑁𝑋) Fn 𝑁)
105, 9syl 17 . . 3 (𝜑 → (𝑖𝑁𝑋) Fn 𝑁)
11 fvex 6113 . . . 4 (0g𝐺) ∈ V
1211a1i 11 . . 3 (𝜑 → (0g𝐺) ∈ V)
1310, 4, 12fndmfifsupp 8171 . 2 (𝜑 → (𝑖𝑁𝑋) finSupp (0g𝐺))
141, 2, 3, 4, 8, 13gsumcl 18139 1 (𝜑 → (𝐺 Σg (𝑖𝑁𝑋)) ∈ 𝐵)