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

Metamath Proof Explorer

Theorem psrbagev2

Description: Closure of a sum using a bag of multipliers. (Contributed by Stefan O'Rear, 9-Mar-2015) (Proof shortened by AV, 18-Jul-2019) (Revised by AV, 11-Apr-2024) Remove a sethood hypothesis. (Revised by SN, 7-Aug-2024)

		Ref	Expression
	Hypotheses	psrbagev2.d	$⊢ D = \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\}$
		psrbagev2.c	$⊢ C = {Base}_{T}$
		psrbagev2.x	$⊢ \underset{˙}{\cdot} = \cdot_{T}$
		psrbagev2.t	$⊢ φ \to T \in CMnd$
		psrbagev2.b	$⊢ φ \to B \in D$
		psrbagev2.g	$⊢ φ \to G : I ⟶ C$
	Assertion	psrbagev2	$⊢ φ \to \sum_{T} (B {\underset{˙}{\cdot}}_{f} G) \in C$

Proof

Step	Hyp	Ref	Expression
1		psrbagev2.d	$⊢ D = \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\}$
2		psrbagev2.c	$⊢ C = {Base}_{T}$
3		psrbagev2.x	$⊢ \underset{˙}{\cdot} = \cdot_{T}$
4		psrbagev2.t	$⊢ φ \to T \in CMnd$
5		psrbagev2.b	$⊢ φ \to B \in D$
6		psrbagev2.g	$⊢ φ \to G : I ⟶ C$
7		eqid	$⊢ 0_{T} = 0_{T}$
8		ovexd	$⊢ φ \to B {\underset{˙}{\cdot}}_{f} G \in V$
9	1 2 3 7 4 5 6	psrbagev1	$⊢ φ \to ((B {\underset{˙}{\cdot}}_{f} G) : I ⟶ C \land {finSupp}_{0_{T}} ((B {\underset{˙}{\cdot}}_{f} G)))$
10	9	simpld	$⊢ φ \to (B {\underset{˙}{\cdot}}_{f} G) : I ⟶ C$
11	10	ffnd	$⊢ φ \to (B {\underset{˙}{\cdot}}_{f} G) Fn I$
12	8 11	fndmexd	$⊢ φ \to I \in V$
13	9	simprd	$⊢ φ \to {finSupp}_{0_{T}} ((B {\underset{˙}{\cdot}}_{f} G))$
14	2 7 4 12 10 13	gsumcl	$⊢ φ \to \sum_{T} (B {\underset{˙}{\cdot}}_{f} G) \in C$