Theorem mdegpropd

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

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

Proof

Step	Hyp	Ref	Expression
1		mdegpropd.b1	$$⊢\phi \to B={\mathrm{Base}}_R$$
2		mdegpropd.b2	$$⊢\phi \to B={\mathrm{Base}}_S$$
3		mdegpropd.p	$$⊢\left(\phi \wedge \left(x\in B\wedge y\in B\right)\right)\to x{+}_{R}y=x{+}_{S}y$$
4	1 2 3	mplbaspropd	$$⊢\phi \to {\mathrm{Base}}_{\left(I\mathrm{mPoly}R\right)}={\mathrm{Base}}_{\left(I\mathrm{mPoly}S\right)}$$
5	1 2 3	grpidpropd	$$⊢\phi \to 0_R=0_S$$
6	5	oveq2d	$$⊢\phi \to c\mathrm{supp}{0}_R=c\mathrm{supp}{0}_S$$
7	6	imaeq2d	$$⊢\phi \to \left(b\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼{\sum }_{{ℂ}_{\mathrm{fld}}}b\right)\left[c\mathrm{supp}{0}_R\right]=\left(b\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼{\sum }_{{ℂ}_{\mathrm{fld}}}b\right)\left[c\mathrm{supp}{0}_S\right]$$
8	7	supeq1d	$$⊢\phi \to sup\left(\left(b\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼{\sum }_{{ℂ}_{\mathrm{fld}}}b\right)\left[c\mathrm{supp}{0}_R\right],{ℝ}^{*},<\right)=sup\left(\left(b\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼{\sum }_{{ℂ}_{\mathrm{fld}}}b\right)\left[c\mathrm{supp}{0}_S\right],{ℝ}^{*},<\right)$$
9	4 8	mpteq12dv	$$⊢\phi \to \left(c\in {\mathrm{Base}}_{\left(I\mathrm{mPoly}R\right)}⟼sup\left(\left(b\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼{\sum }_{{ℂ}_{\mathrm{fld}}}b\right)\left[c\mathrm{supp}{0}_R\right],{ℝ}^{*},<\right)\right)=\left(c\in {\mathrm{Base}}_{\left(I\mathrm{mPoly}S\right)}⟼sup\left(\left(b\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼{\sum }_{{ℂ}_{\mathrm{fld}}}b\right)\left[c\mathrm{supp}{0}_S\right],{ℝ}^{*},<\right)\right)$$
10		eqid	$$⊢I\mathrm{mDeg}R=I\mathrm{mDeg}R$$
11		eqid	$$⊢I\mathrm{mPoly}R=I\mathrm{mPoly}R$$
12		eqid	$$⊢{\mathrm{Base}}_{\left(I\mathrm{mPoly}R\right)}={\mathrm{Base}}_{\left(I\mathrm{mPoly}R\right)}$$
13		eqid	$$⊢0_R=0_R$$
14		eqid	$$⊢\left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}=\left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
15		eqid	$$⊢\left(b\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼{\sum }_{{ℂ}_{\mathrm{fld}}}b\right)=\left(b\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼{\sum }_{{ℂ}_{\mathrm{fld}}}b\right)$$
16	10 11 12 13 14 15	mdegfval	$$⊢I\mathrm{mDeg}R=\left(c\in {\mathrm{Base}}_{\left(I\mathrm{mPoly}R\right)}⟼sup\left(\left(b\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼{\sum }_{{ℂ}_{\mathrm{fld}}}b\right)\left[c\mathrm{supp}{0}_R\right],{ℝ}^{*},<\right)\right)$$
17		eqid	$$⊢I\mathrm{mDeg}S=I\mathrm{mDeg}S$$
18		eqid	$$⊢I\mathrm{mPoly}S=I\mathrm{mPoly}S$$
19		eqid	$$⊢{\mathrm{Base}}_{\left(I\mathrm{mPoly}S\right)}={\mathrm{Base}}_{\left(I\mathrm{mPoly}S\right)}$$
20		eqid	$$⊢0_S=0_S$$
21	17 18 19 20 14 15	mdegfval	$$⊢I\mathrm{mDeg}S=\left(c\in {\mathrm{Base}}_{\left(I\mathrm{mPoly}S\right)}⟼sup\left(\left(b\in \left\{a\in \left({{\mathbb{N}}_0}^I\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼{\sum }_{{ℂ}_{\mathrm{fld}}}b\right)\left[c\mathrm{supp}{0}_S\right],{ℝ}^{*},<\right)\right)$$
22	9 16 21	3eqtr4g	$$⊢\phi \to I\mathrm{mDeg}R=I\mathrm{mDeg}S$$