Theorem psrbagev2OLD

Description: Obsolete version of psrbagev2 as of 7-Aug-2024. (Contributed by Stefan O'Rear, 9-Mar-2015) (Proof shortened by AV, 18-Jul-2019) (Revised by AV, 11-Apr-2024) (New usage is discouraged.) (Proof modification is discouraged.)

	Ref	Expression
Hypotheses	psrbagev2.d	$$⊢D=\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
	psrbagev2.c	$$⊢C={\mathrm{Base}}_T$$
	psrbagev2.x	$$⊢\underset{\dot{}}{·}={\cdot }_T$$
	psrbagev2.t	$$⊢\phi \to T\in \mathrm{CMnd}$$
	psrbagev2.b	$$⊢\phi \to B\in D$$
	psrbagev2.g	$$⊢\phi \to G:I⟶C$$
	psrbagev2OLD.i	$$⊢\phi \to I\in W$$
Assertion	psrbagev2OLD	$$⊢\phi \to {\sum }_T\left(B{\underset{\dot{}}{·}}_{f}G\right)\in C$$

Proof

Step	Hyp	Ref	Expression
1		psrbagev2.d	$$⊢D=\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
2		psrbagev2.c	$$⊢C={\mathrm{Base}}_T$$
3		psrbagev2.x	$$⊢\underset{\dot{}}{·}={\cdot }_T$$
4		psrbagev2.t	$$⊢\phi \to T\in \mathrm{CMnd}$$
5		psrbagev2.b	$$⊢\phi \to B\in D$$
6		psrbagev2.g	$$⊢\phi \to G:I⟶C$$
7		psrbagev2OLD.i	$$⊢\phi \to I\in W$$
8		eqid	$$⊢0_T=0_T$$
9	1 2 3 8 4 5 6 7	psrbagev1OLD	$$⊢\phi \to \left(\left(B{\underset{\dot{}}{·}}_{f}G\right):I⟶C\wedge {finSupp}_{0_T}\left(\left(B{\underset{\dot{}}{·}}_{f}G\right)\right)\right)$$
10	9	simpld	$$⊢\phi \to \left(B{\underset{\dot{}}{·}}_{f}G\right):I⟶C$$
11	9	simprd	$$⊢\phi \to {finSupp}_{0_T}\left(\left(B{\underset{\dot{}}{·}}_{f}G\right)\right)$$
12	2 8 4 7 10 11	gsumcl	$$⊢\phi \to {\sum }_T\left(B{\underset{\dot{}}{·}}_{f}G\right)\in C$$