Theorem mdegnn0cl

Description: Degree of a nonzero polynomial. (Contributed by Stefan O'Rear, 23-Mar-2015)

	Ref	Expression
Hypotheses	mdeg0.d	$$⊢D=I\mathrm{mDeg}R$$
	mdeg0.p	$$⊢P=I\mathrm{mPoly}R$$
	mdeg0.z	$$⊢\underset{\dot{}}{0}=0_P$$
	mdegnn0cl.b	$$⊢B={\mathrm{Base}}_P$$
Assertion	mdegnn0cl	$$⊢\left(R\in \mathrm{Ring}\wedge F\in B\wedge F\ne \underset{\dot{}}{0}\right)\to D\left(F\right)\in {\mathbb{N}}_0$$

Proof

Step	Hyp	Ref	Expression
1		mdeg0.d	$$⊢D=I\mathrm{mDeg}R$$
2		mdeg0.p	$$⊢P=I\mathrm{mPoly}R$$
3		mdeg0.z	$$⊢\underset{\dot{}}{0}=0_P$$
4		mdegnn0cl.b	$$⊢B={\mathrm{Base}}_P$$
5		eqid	$$⊢0_R=0_R$$
6		eqid	$$⊢\left\{m\in \left({{\mathbb{N}}_0}^I\right)|m^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}=\left\{m\in \left({{\mathbb{N}}_0}^I\right)|m^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
7		eqid	$$⊢\left(h\in \left\{m\in \left({{\mathbb{N}}_0}^I\right)|m^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼{\sum }_{{ℂ}_{\mathrm{fld}}}h\right)=\left(h\in \left\{m\in \left({{\mathbb{N}}_0}^I\right)|m^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼{\sum }_{{ℂ}_{\mathrm{fld}}}h\right)$$
8	1 2 4 5 6 7 3	mdegldg	$$⊢\left(R\in \mathrm{Ring}\wedge F\in B\wedge F\ne \underset{\dot{}}{0}\right)\to \exists x\in \left\{m\in \left({{\mathbb{N}}_0}^I\right)|m^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\left(F\left(x\right)\ne 0_R\wedge \left(h\in \left\{m\in \left({{\mathbb{N}}_0}^I\right)|m^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼{\sum }_{{ℂ}_{\mathrm{fld}}}h\right)\left(x\right)=D\left(F\right)\right)$$
9	6 7	tdeglem1	$$⊢\left(h\in \left\{m\in \left({{\mathbb{N}}_0}^I\right)|m^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼{\sum }_{{ℂ}_{\mathrm{fld}}}h\right):\left\{m\in \left({{\mathbb{N}}_0}^I\right)|m^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟶{\mathbb{N}}_0$$
10	9	a1i	$$⊢\left(R\in \mathrm{Ring}\wedge F\in B\wedge F\ne \underset{\dot{}}{0}\right)\to \left(h\in \left\{m\in \left({{\mathbb{N}}_0}^I\right)|m^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼{\sum }_{{ℂ}_{\mathrm{fld}}}h\right):\left\{m\in \left({{\mathbb{N}}_0}^I\right)|m^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟶{\mathbb{N}}_0$$
11	10	ffvelcdmda	$$⊢\left(\left(R\in \mathrm{Ring}\wedge F\in B\wedge F\ne \underset{\dot{}}{0}\right)\wedge x\in \left\{m\in \left({{\mathbb{N}}_0}^I\right)|m^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\to \left(h\in \left\{m\in \left({{\mathbb{N}}_0}^I\right)|m^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼{\sum }_{{ℂ}_{\mathrm{fld}}}h\right)\left(x\right)\in {\mathbb{N}}_0$$
12		eleq1	$$⊢\left(h\in \left\{m\in \left({{\mathbb{N}}_0}^I\right)|m^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼{\sum }_{{ℂ}_{\mathrm{fld}}}h\right)\left(x\right)=D\left(F\right)\to \left(\left(h\in \left\{m\in \left({{\mathbb{N}}_0}^I\right)|m^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼{\sum }_{{ℂ}_{\mathrm{fld}}}h\right)\left(x\right)\in {\mathbb{N}}_0\leftrightarrow D\left(F\right)\in {\mathbb{N}}_0\right)$$
13	11 12	syl5ibcom	$$⊢\left(\left(R\in \mathrm{Ring}\wedge F\in B\wedge F\ne \underset{\dot{}}{0}\right)\wedge x\in \left\{m\in \left({{\mathbb{N}}_0}^I\right)|m^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\to \left(\left(h\in \left\{m\in \left({{\mathbb{N}}_0}^I\right)|m^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼{\sum }_{{ℂ}_{\mathrm{fld}}}h\right)\left(x\right)=D\left(F\right)\to D\left(F\right)\in {\mathbb{N}}_0\right)$$
14	13	adantld	$$⊢\left(\left(R\in \mathrm{Ring}\wedge F\in B\wedge F\ne \underset{\dot{}}{0}\right)\wedge x\in \left\{m\in \left({{\mathbb{N}}_0}^I\right)|m^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\right)\to \left(\left(F\left(x\right)\ne 0_R\wedge \left(h\in \left\{m\in \left({{\mathbb{N}}_0}^I\right)|m^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼{\sum }_{{ℂ}_{\mathrm{fld}}}h\right)\left(x\right)=D\left(F\right)\right)\to D\left(F\right)\in {\mathbb{N}}_0\right)$$
15	14	rexlimdva	$$⊢\left(R\in \mathrm{Ring}\wedge F\in B\wedge F\ne \underset{\dot{}}{0}\right)\to \left(\exists x\in \left\{m\in \left({{\mathbb{N}}_0}^I\right)|m^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}\left(F\left(x\right)\ne 0_R\wedge \left(h\in \left\{m\in \left({{\mathbb{N}}_0}^I\right)|m^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}⟼{\sum }_{{ℂ}_{\mathrm{fld}}}h\right)\left(x\right)=D\left(F\right)\right)\to D\left(F\right)\in {\mathbb{N}}_0\right)$$
16	8 15	mpd	$$⊢\left(R\in \mathrm{Ring}\wedge F\in B\wedge F\ne \underset{\dot{}}{0}\right)\to D\left(F\right)\in {\mathbb{N}}_0$$