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 ⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
psrbagev2.c ⊢ 𝐶 = ( Base ‘ 𝑇 )
psrbagev2.x ⊢ · = ( .g ‘ 𝑇 )
psrbagev2.t ⊢ ( 𝜑 → 𝑇 ∈ CMnd )
psrbagev2.b ⊢ ( 𝜑 → 𝐵 ∈ 𝐷 )
psrbagev2.g ⊢ ( 𝜑 → 𝐺 : 𝐼 ⟶ 𝐶 )
Assertion psrbagev2 ( 𝜑 → ( 𝑇 Σg ( 𝐵 ∘f · 𝐺 ) ) ∈ 𝐶 )

Proof

Step Hyp Ref Expression
1 psrbagev2.d ⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
2 psrbagev2.c ⊢ 𝐶 = ( Base ‘ 𝑇 )
3 psrbagev2.x ⊢ · = ( .g ‘ 𝑇 )
4 psrbagev2.t ⊢ ( 𝜑 → 𝑇 ∈ CMnd )
5 psrbagev2.b ⊢ ( 𝜑 → 𝐵 ∈ 𝐷 )
6 psrbagev2.g ⊢ ( 𝜑 → 𝐺 : 𝐼 ⟶ 𝐶 )
7 eqid ⊢ ( 0g ‘ 𝑇 ) = ( 0g ‘ 𝑇 )
8 ovexd ⊢ ( 𝜑 → ( 𝐵 ∘f · 𝐺 ) ∈ V )
9 1 2 3 7 4 5 6 psrbagev1 ⊢ ( 𝜑 → ( ( 𝐵 ∘f · 𝐺 ) : 𝐼 ⟶ 𝐶 ∧ ( 𝐵 ∘f · 𝐺 ) finSupp ( 0g ‘ 𝑇 ) ) )
10 9 simpld ⊢ ( 𝜑 → ( 𝐵 ∘f · 𝐺 ) : 𝐼 ⟶ 𝐶 )
11 10 ffnd ⊢ ( 𝜑 → ( 𝐵 ∘f · 𝐺 ) Fn 𝐼 )
12 8 11 fndmexd ⊢ ( 𝜑 → 𝐼 ∈ V )
13 9 simprd ⊢ ( 𝜑 → ( 𝐵 ∘f · 𝐺 ) finSupp ( 0g ‘ 𝑇 ) )
14 2 7 4 12 10 13 gsumcl ⊢ ( 𝜑 → ( 𝑇 Σg ( 𝐵 ∘f · 𝐺 ) ) ∈ 𝐶 )