Theorem psrbagev1OLD

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

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

Proof

Step	Hyp	Ref	Expression
1		psrbagev1.d	$$⊢D=\left\{h\in \left({{\mathbb{N}}_0}^I\right)|h^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
2		psrbagev1.c	$$⊢C={\mathrm{Base}}_T$$
3		psrbagev1.x	$$⊢\underset{\dot{}}{·}={\cdot }_T$$
4		psrbagev1.z	$$⊢\underset{\dot{}}{0}=0_T$$
5		psrbagev1.t	$$⊢\phi \to T\in \mathrm{CMnd}$$
6		psrbagev1.b	$$⊢\phi \to B\in D$$
7		psrbagev1.g	$$⊢\phi \to G:I⟶C$$
8		psrbagev1.i	$$⊢\phi \to I\in W$$
9	5	cmnmndd	$$⊢\phi \to T\in \mathrm{Mnd}$$
10	2 3	mulgnn0cl	$$⊢\left(T\in \mathrm{Mnd}\wedge y\in {\mathbb{N}}_0\wedge z\in C\right)\to y\underset{\dot{}}{·}z\in C$$
11	10	3expb	$$⊢\left(T\in \mathrm{Mnd}\wedge \left(y\in {\mathbb{N}}_0\wedge z\in C\right)\right)\to y\underset{\dot{}}{·}z\in C$$
12	9 11	sylan	$$⊢\left(\phi \wedge \left(y\in {\mathbb{N}}_0\wedge z\in C\right)\right)\to y\underset{\dot{}}{·}z\in C$$
13	1	psrbagfOLD	$$⊢\left(I\in W\wedge B\in D\right)\to B:I⟶{\mathbb{N}}_0$$
14	8 6 13	syl2anc	$$⊢\phi \to B:I⟶{\mathbb{N}}_0$$
15		inidm	$$⊢I\cap I=I$$
16	12 14 7 8 8 15	off	$$⊢\phi \to \left(B{\underset{\dot{}}{·}}_{f}G\right):I⟶C$$
17		ovexd	$$⊢\phi \to B{\underset{\dot{}}{·}}_{f}G\in \mathrm{V}$$
18	14	ffnd	$$⊢\phi \to BFnI$$
19	7	ffnd	$$⊢\phi \to GFnI$$
20	18 19 8 8	offun	$$⊢\phi \to \mathrm{Fun}\left(B{\underset{\dot{}}{·}}_{f}G\right)$$
21	4	fvexi	$$⊢\underset{\dot{}}{0}\in \mathrm{V}$$
22	21	a1i	$$⊢\phi \to \underset{\dot{}}{0}\in \mathrm{V}$$
23	1	psrbagfsuppOLD	$$⊢\left(B\in D\wedge I\in W\right)\to {finSupp}_0\left(B\right)$$
24	6 8 23	syl2anc	$$⊢\phi \to {finSupp}_0\left(B\right)$$
25	24	fsuppimpd	$$⊢\phi \to B\mathrm{supp}0\in \mathrm{Fin}$$
26		ssidd	$$⊢\phi \to B\mathrm{supp}0\subseteq B\mathrm{supp}0$$
27	2 4 3	mulg0	$$⊢z\in C\to 0\underset{\dot{}}{·}z=\underset{\dot{}}{0}$$
28	27	adantl	$$⊢\left(\phi \wedge z\in C\right)\to 0\underset{\dot{}}{·}z=\underset{\dot{}}{0}$$
29		c0ex	$$⊢0\in \mathrm{V}$$
30	29	a1i	$$⊢\phi \to 0\in \mathrm{V}$$
31	26 28 14 7 8 30	suppssof1	$$⊢\phi \to \left(B{\underset{\dot{}}{·}}_{f}G\right)\mathrm{supp}\underset{\dot{}}{0}\subseteq B\mathrm{supp}0$$
32		suppssfifsupp	$$⊢\left(\left(B{\underset{\dot{}}{·}}_{f}G\in \mathrm{V}\wedge \mathrm{Fun}\left(B{\underset{\dot{}}{·}}_{f}G\right)\wedge \underset{\dot{}}{0}\in \mathrm{V}\right)\wedge \left(B\mathrm{supp}0\in \mathrm{Fin}\wedge \left(B{\underset{\dot{}}{·}}_{f}G\right)\mathrm{supp}\underset{\dot{}}{0}\subseteq B\mathrm{supp}0\right)\right)\to {finSupp}_{\underset{\dot{}}{0}}\left(\left(B{\underset{\dot{}}{·}}_{f}G\right)\right)$$
33	17 20 22 25 31 32	syl32anc	$$⊢\phi \to {finSupp}_{\underset{\dot{}}{0}}\left(\left(B{\underset{\dot{}}{·}}_{f}G\right)\right)$$
34	16 33	jca	$$⊢\phi \to \left(\left(B{\underset{\dot{}}{·}}_{f}G\right):I⟶C\wedge {finSupp}_{\underset{\dot{}}{0}}\left(\left(B{\underset{\dot{}}{·}}_{f}G\right)\right)\right)$$