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	$⊢ D = \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\}$
	psrbagev1.c	$⊢ C = {Base}_{T}$
	psrbagev1.x	$⊢ \underset{˙}{\cdot} = \cdot_{T}$
	psrbagev1.z	$⊢ \underset{˙}{0} = 0_{T}$
	psrbagev1.t	$⊢ φ \to T \in CMnd$
	psrbagev1.b	$⊢ φ \to B \in D$
	psrbagev1.g	$⊢ φ \to G : I ⟶ C$
Assertion	psrbagev1	$⊢ φ \to ((B {\underset{˙}{\cdot}}_{f} G) : I ⟶ C \land {finSupp}_{\underset{˙}{0}} ((B {\underset{˙}{\cdot}}_{f} G)))$

Proof

Step	Hyp	Ref	Expression
1		psrbagev1.d	$⊢ D = \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\}$
2		psrbagev1.c	$⊢ C = {Base}_{T}$
3		psrbagev1.x	$⊢ \underset{˙}{\cdot} = \cdot_{T}$
4		psrbagev1.z	$⊢ \underset{˙}{0} = 0_{T}$
5		psrbagev1.t	$⊢ φ \to T \in CMnd$
6		psrbagev1.b	$⊢ φ \to B \in D$
7		psrbagev1.g	$⊢ φ \to G : I ⟶ C$
8	5	cmnmndd	$⊢ φ \to T \in Mnd$
9	2 3	mulgnn0cl	$⊢ (T \in Mnd \land y \in ℕ_{0} \land z \in C) \to y \underset{˙}{\cdot} z \in C$
10	9	3expb	$⊢ (T \in Mnd \land (y \in ℕ_{0} \land z \in C)) \to y \underset{˙}{\cdot} z \in C$
11	8 10	sylan	$⊢ (φ \land (y \in ℕ_{0} \land z \in C)) \to y \underset{˙}{\cdot} z \in C$
12	1	psrbagf	$⊢ B \in D \to B : I ⟶ ℕ_{0}$
13	6 12	syl	$⊢ φ \to B : I ⟶ ℕ_{0}$
14	13	ffnd	$⊢ φ \to B Fn I$
15	6 14	fndmexd	$⊢ φ \to I \in V$
16		inidm	$⊢ I \cap I = I$
17	11 13 7 15 15 16	off	$⊢ φ \to (B {\underset{˙}{\cdot}}_{f} G) : I ⟶ C$
18		ovexd	$⊢ φ \to B {\underset{˙}{\cdot}}_{f} G \in V$
19	7	ffnd	$⊢ φ \to G Fn I$
20	14 19 15 15	offun	$⊢ φ \to Fun (B {\underset{˙}{\cdot}}_{f} G)$
21	4	fvexi	$⊢ \underset{˙}{0} \in V$
22	21	a1i	$⊢ φ \to \underset{˙}{0} \in V$
23	1	psrbagfsupp	$⊢ B \in D \to {finSupp}_{0} (B)$
24	6 23	syl	$⊢ φ \to {finSupp}_{0} (B)$
25	24	fsuppimpd	$⊢ φ \to B supp 0 \in Fin$
26		ssidd	$⊢ φ \to B supp 0 \subseteq B supp 0$
27	2 4 3	mulg0	$⊢ z \in C \to 0 \underset{˙}{\cdot} z = \underset{˙}{0}$
28	27	adantl	$⊢ (φ \land z \in C) \to 0 \underset{˙}{\cdot} z = \underset{˙}{0}$
29		c0ex	$⊢ 0 \in V$
30	29	a1i	$⊢ φ \to 0 \in V$
31	26 28 13 7 15 30	suppssof1	$⊢ φ \to (B {\underset{˙}{\cdot}}_{f} G) supp \underset{˙}{0} \subseteq B supp 0$
32		suppssfifsupp	$⊢ ((B {\underset{˙}{\cdot}}_{f} G \in V \land Fun (B {\underset{˙}{\cdot}}_{f} G) \land \underset{˙}{0} \in V) \land (B supp 0 \in Fin \land (B {\underset{˙}{\cdot}}_{f} G) supp \underset{˙}{0} \subseteq B supp 0)) \to {finSupp}_{\underset{˙}{0}} ((B {\underset{˙}{\cdot}}_{f} G))$
33	18 20 22 25 31 32	syl32anc	$⊢ φ \to {finSupp}_{\underset{˙}{0}} ((B {\underset{˙}{\cdot}}_{f} G))$
34	17 33	jca	$⊢ φ \to ((B {\underset{˙}{\cdot}}_{f} G) : I ⟶ C \land {finSupp}_{\underset{˙}{0}} ((B {\underset{˙}{\cdot}}_{f} G)))$

Metamath Proof Explorer

Theorem psrbagev1

Proof