Metamath Proof Explorer

Theorem psrbagev1

Description: A bag of multipliers provides the conditions for a valid sum. (Contributed by Stefan O'Rear, 9-Mar-2015) (Revised by AV, 18-Jul-2019) (Revised by AV, 11-Apr-2024) Remove a sethood hypothesis. (Revised by SN, 7-Aug-2024)

Ref Expression
Hypotheses psrbagev1.d ⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
psrbagev1.c ⊢ 𝐶 = ( Base ‘ 𝑇 )
psrbagev1.x ⊢ · = ( .g ‘ 𝑇 )
psrbagev1.z ⊢ 0 = ( 0g ‘ 𝑇 )
psrbagev1.t ⊢ ( 𝜑 → 𝑇 ∈ CMnd )
psrbagev1.b ⊢ ( 𝜑 → 𝐵 ∈ 𝐷 )
psrbagev1.g ⊢ ( 𝜑 → 𝐺 : 𝐼 ⟶ 𝐶 )
Assertion psrbagev1 ( 𝜑 → ( ( 𝐵 ∘f · 𝐺 ) : 𝐼 ⟶ 𝐶 ∧ ( 𝐵 ∘f · 𝐺 ) finSupp 0 ) )

Proof

Step Hyp Ref Expression
1 psrbagev1.d ⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
2 psrbagev1.c ⊢ 𝐶 = ( Base ‘ 𝑇 )
3 psrbagev1.x ⊢ · = ( .g ‘ 𝑇 )
4 psrbagev1.z ⊢ 0 = ( 0g ‘ 𝑇 )
5 psrbagev1.t ⊢ ( 𝜑 → 𝑇 ∈ CMnd )
6 psrbagev1.b ⊢ ( 𝜑 → 𝐵 ∈ 𝐷 )
7 psrbagev1.g ⊢ ( 𝜑 → 𝐺 : 𝐼 ⟶ 𝐶 )
8 5 cmnmndd ⊢ ( 𝜑 → 𝑇 ∈ Mnd )
9 2 3 mulgnn0cl ⊢ ( ( 𝑇 ∈ Mnd ∧ 𝑦 ∈ ℕ0 ∧ 𝑧 ∈ 𝐶 ) → ( 𝑦 · 𝑧 ) ∈ 𝐶 )
10 9 3expb ⊢ ( ( 𝑇 ∈ Mnd ∧ ( 𝑦 ∈ ℕ0 ∧ 𝑧 ∈ 𝐶 ) ) → ( 𝑦 · 𝑧 ) ∈ 𝐶 )
11 8 10 sylan ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ℕ0 ∧ 𝑧 ∈ 𝐶 ) ) → ( 𝑦 · 𝑧 ) ∈ 𝐶 )
12 1 psrbagf ⊢ ( 𝐵 ∈ 𝐷 → 𝐵 : 𝐼 ⟶ ℕ0 )
13 6 12 syl ⊢ ( 𝜑 → 𝐵 : 𝐼 ⟶ ℕ0 )
14 13 ffnd ⊢ ( 𝜑 → 𝐵 Fn 𝐼 )
15 6 14 fndmexd ⊢ ( 𝜑 → 𝐼 ∈ V )
16 inidm ⊢ ( 𝐼 ∩ 𝐼 ) = 𝐼
17 11 13 7 15 15 16 off ⊢ ( 𝜑 → ( 𝐵 ∘f · 𝐺 ) : 𝐼 ⟶ 𝐶 )
18 ovexd ⊢ ( 𝜑 → ( 𝐵 ∘f · 𝐺 ) ∈ V )
19 7 ffnd ⊢ ( 𝜑 → 𝐺 Fn 𝐼 )
20 14 19 15 15 offun ⊢ ( 𝜑 → Fun ( 𝐵 ∘f · 𝐺 ) )
21 4 fvexi ⊢ 0 ∈ V
22 21 a1i ⊢ ( 𝜑 → 0 ∈ V )
23 1 psrbagfsupp ⊢ ( 𝐵 ∈ 𝐷 → 𝐵 finSupp 0 )
24 6 23 syl ⊢ ( 𝜑 → 𝐵 finSupp 0 )
25 24 fsuppimpd ⊢ ( 𝜑 → ( 𝐵 supp 0 ) ∈ Fin )
26 ssidd ⊢ ( 𝜑 → ( 𝐵 supp 0 ) ⊆ ( 𝐵 supp 0 ) )
27 2 4 3 mulg0 ⊢ ( 𝑧 ∈ 𝐶 → ( 0 · 𝑧 ) = 0 )
28 27 adantl ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐶 ) → ( 0 · 𝑧 ) = 0 )
29 c0ex ⊢ 0 ∈ V
30 29 a1i ⊢ ( 𝜑 → 0 ∈ V )
31 26 28 13 7 15 30 suppssof1 ⊢ ( 𝜑 → ( ( 𝐵 ∘f · 𝐺 ) supp 0 ) ⊆ ( 𝐵 supp 0 ) )
32 suppssfifsupp ⊢ ( ( ( ( 𝐵 ∘f · 𝐺 ) ∈ V ∧ Fun ( 𝐵 ∘f · 𝐺 ) ∧ 0 ∈ V ) ∧ ( ( 𝐵 supp 0 ) ∈ Fin ∧ ( ( 𝐵 ∘f · 𝐺 ) supp 0 ) ⊆ ( 𝐵 supp 0 ) ) ) → ( 𝐵 ∘f · 𝐺 ) finSupp 0 )
33 18 20 22 25 31 32 syl32anc ⊢ ( 𝜑 → ( 𝐵 ∘f · 𝐺 ) finSupp 0 )
34 17 33 jca ⊢ ( 𝜑 → ( ( 𝐵 ∘f · 𝐺 ) : 𝐼 ⟶ 𝐶 ∧ ( 𝐵 ∘f · 𝐺 ) finSupp 0 ) )