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 ) )