Theorem mplsubglem2

Description: Lemma for mplsubg and mpllss . (Contributed by AV, 16-Jul-2019)

	Ref	Expression
Hypotheses	mplsubg.s	$$⊢S=I\mathrm{mPwSer}R$$
	mplsubg.p	$$⊢P=I\mathrm{mPoly}R$$
	mplsubg.u	$$⊢U={\mathrm{Base}}_P$$
	mplsubg.i	$$⊢\phi \to I\in W$$
Assertion	mplsubglem2	$$⊢\phi \to U=\left\{g\in {\mathrm{Base}}_S|g\mathrm{supp}{0}_R\in \mathrm{Fin}\right\}$$

Proof

Step	Hyp	Ref	Expression
1		mplsubg.s	$$⊢S=I\mathrm{mPwSer}R$$
2		mplsubg.p	$$⊢P=I\mathrm{mPoly}R$$
3		mplsubg.u	$$⊢U={\mathrm{Base}}_P$$
4		mplsubg.i	$$⊢\phi \to I\in W$$
5		eqid	$$⊢{\mathrm{Base}}_S={\mathrm{Base}}_S$$
6		eqid	$$⊢0_R=0_R$$
7	2 1 5 6 3	mplbas	$$⊢U=\left\{g\in {\mathrm{Base}}_S|{finSupp}_{0_R}\left(g\right)\right\}$$
8	1 5	psrelbasfun	$$⊢g\in {\mathrm{Base}}_S\to \mathrm{Fun}g$$
9	8	adantl	$$⊢\left(\phi \wedge g\in {\mathrm{Base}}_S\right)\to \mathrm{Fun}g$$
10		simpr	$$⊢\left(\phi \wedge g\in {\mathrm{Base}}_S\right)\to g\in {\mathrm{Base}}_S$$
11		fvexd	$$⊢\left(\phi \wedge g\in {\mathrm{Base}}_S\right)\to 0_R\in \mathrm{V}$$
12		funisfsupp	$$⊢\left(\mathrm{Fun}g\wedge g\in {\mathrm{Base}}_S\wedge 0_R\in \mathrm{V}\right)\to \left({finSupp}_{0_R}\left(g\right)\leftrightarrow g\mathrm{supp}{0}_R\in \mathrm{Fin}\right)$$
13	9 10 11 12	syl3anc	$$⊢\left(\phi \wedge g\in {\mathrm{Base}}_S\right)\to \left({finSupp}_{0_R}\left(g\right)\leftrightarrow g\mathrm{supp}{0}_R\in \mathrm{Fin}\right)$$
14	13	rabbidva	$$⊢\phi \to \left\{g\in {\mathrm{Base}}_S|{finSupp}_{0_R}\left(g\right)\right\}=\left\{g\in {\mathrm{Base}}_S|g\mathrm{supp}{0}_R\in \mathrm{Fin}\right\}$$
15	7 14	eqtrid	$$⊢\phi \to U=\left\{g\in {\mathrm{Base}}_S|g\mathrm{supp}{0}_R\in \mathrm{Fin}\right\}$$