Theorem mplbaspropd

Description: Property deduction for polynomial base set. (Contributed by Stefan O'Rear, 27-Mar-2015) (Proof shortened by AV, 19-Jul-2019)

	Ref	Expression
Hypotheses	psrplusgpropd.b1	$$⊢\phi \to B={\mathrm{Base}}_R$$
	psrplusgpropd.b2	$$⊢\phi \to B={\mathrm{Base}}_S$$
	psrplusgpropd.p	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to x{+}_{R}y=x{+}_{S}y$$
Assertion	mplbaspropd	$$⊢\phi \to {\mathrm{Base}}_{\left(I\mathrm{mPoly}R\right)}={\mathrm{Base}}_{\left(I\mathrm{mPoly}S\right)}$$

Proof

Step	Hyp	Ref	Expression
1		psrplusgpropd.b1	$$⊢\phi \to B={\mathrm{Base}}_R$$
2		psrplusgpropd.b2	$$⊢\phi \to B={\mathrm{Base}}_S$$
3		psrplusgpropd.p	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to x{+}_{R}y=x{+}_{S}y$$
4	1 2	eqtr3d	$$⊢\phi \to {\mathrm{Base}}_R={\mathrm{Base}}_S$$
5	4	psrbaspropd	$$⊢\phi \to {\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}={\mathrm{Base}}_{\left(I\mathrm{mPwSer}S\right)}$$
6	5	adantr	$$⊢\left(\phi \wedge I\in \mathrm{V}\right)\to {\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}={\mathrm{Base}}_{\left(I\mathrm{mPwSer}S\right)}$$
7	1 2 3	grpidpropd	$$⊢\phi \to 0_R=0_S$$
8	7	breq2d	$$⊢\phi \to \left({finSupp}_{0_R}\left(a\right)\leftrightarrow {finSupp}_{0_S}\left(a\right)\right)$$
9	8	adantr	$$⊢\left(\phi \wedge I\in \mathrm{V}\right)\to \left({finSupp}_{0_R}\left(a\right)\leftrightarrow {finSupp}_{0_S}\left(a\right)\right)$$
10	6 9	rabeqbidv	$$⊢\left(\phi \wedge I\in \mathrm{V}\right)\to \left\{a\in {\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}|{finSupp}_{0_R}\left(a\right)\right\}=\left\{a\in {\mathrm{Base}}_{\left(I\mathrm{mPwSer}S\right)}|{finSupp}_{0_S}\left(a\right)\right\}$$
11		eqid	$$⊢I\mathrm{mPoly}R=I\mathrm{mPoly}R$$
12		eqid	$$⊢I\mathrm{mPwSer}R=I\mathrm{mPwSer}R$$
13		eqid	$$⊢{\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}={\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}$$
14		eqid	$$⊢0_R=0_R$$
15		eqid	$$⊢{\mathrm{Base}}_{\left(I\mathrm{mPoly}R\right)}={\mathrm{Base}}_{\left(I\mathrm{mPoly}R\right)}$$
16	11 12 13 14 15	mplbas	$$⊢{\mathrm{Base}}_{\left(I\mathrm{mPoly}R\right)}=\left\{a\in {\mathrm{Base}}_{\left(I\mathrm{mPwSer}R\right)}|{finSupp}_{0_R}\left(a\right)\right\}$$
17		eqid	$$⊢I\mathrm{mPoly}S=I\mathrm{mPoly}S$$
18		eqid	$$⊢I\mathrm{mPwSer}S=I\mathrm{mPwSer}S$$
19		eqid	$$⊢{\mathrm{Base}}_{\left(I\mathrm{mPwSer}S\right)}={\mathrm{Base}}_{\left(I\mathrm{mPwSer}S\right)}$$
20		eqid	$$⊢0_S=0_S$$
21		eqid	$$⊢{\mathrm{Base}}_{\left(I\mathrm{mPoly}S\right)}={\mathrm{Base}}_{\left(I\mathrm{mPoly}S\right)}$$
22	17 18 19 20 21	mplbas	$$⊢{\mathrm{Base}}_{\left(I\mathrm{mPoly}S\right)}=\left\{a\in {\mathrm{Base}}_{\left(I\mathrm{mPwSer}S\right)}|{finSupp}_{0_S}\left(a\right)\right\}$$
23	10 16 22	3eqtr4g	$$⊢\left(\phi \wedge I\in \mathrm{V}\right)\to {\mathrm{Base}}_{\left(I\mathrm{mPoly}R\right)}={\mathrm{Base}}_{\left(I\mathrm{mPoly}S\right)}$$
24		reldmmpl	$$⊢\mathrm{Rel}\mathrm{dom}\mathrm{mPoly}$$
25	24	ovprc1	$$⊢\neg I\in \mathrm{V}\to I\mathrm{mPoly}R=\varnothing$$
26	24	ovprc1	$$⊢\neg I\in \mathrm{V}\to I\mathrm{mPoly}S=\varnothing$$
27	25 26	eqtr4d	$$⊢\neg I\in \mathrm{V}\to I\mathrm{mPoly}R=I\mathrm{mPoly}S$$
28	27	fveq2d	$$⊢\neg I\in \mathrm{V}\to {\mathrm{Base}}_{\left(I\mathrm{mPoly}R\right)}={\mathrm{Base}}_{\left(I\mathrm{mPoly}S\right)}$$
29	28	adantl	$$⊢\left(\phi \wedge \neg I\in \mathrm{V}\right)\to {\mathrm{Base}}_{\left(I\mathrm{mPoly}R\right)}={\mathrm{Base}}_{\left(I\mathrm{mPoly}S\right)}$$
30	23 29	pm2.61dan	$$⊢\phi \to {\mathrm{Base}}_{\left(I\mathrm{mPoly}R\right)}={\mathrm{Base}}_{\left(I\mathrm{mPoly}S\right)}$$