Theorem deg1leb

Description: Property of being of limited degree. (Contributed by Stefan O'Rear, 23-Mar-2015)

	Ref	Expression
Hypotheses	deg1leb.d	$$⊢D={\mathrm{deg}}_1\left(R\right)$$
	deg1leb.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
	deg1leb.b	$$⊢B={\mathrm{Base}}_P$$
	deg1leb.y	$$⊢\underset{\dot{}}{0}=0_R$$
	deg1leb.a	$$⊢A={\mathrm{coe}}_1\left(F\right)$$
Assertion	deg1leb	$$⊢\left(F\in B\wedge G\in {ℝ}^{*}\right)\to \left(D\left(F\right)\le G\leftrightarrow \forall x\in {\mathbb{N}}_0\left(G<x\to A\left(x\right)=\underset{\dot{}}{0}\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		deg1leb.d	$$⊢D={\mathrm{deg}}_1\left(R\right)$$
2		deg1leb.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
3		deg1leb.b	$$⊢B={\mathrm{Base}}_P$$
4		deg1leb.y	$$⊢\underset{\dot{}}{0}=0_R$$
5		deg1leb.a	$$⊢A={\mathrm{coe}}_1\left(F\right)$$
6	1	deg1fval	$$⊢D=1_{𝑜}\mathrm{mDeg}R$$
7		eqid	$$⊢1_{𝑜}\mathrm{mPoly}R=1_{𝑜}\mathrm{mPoly}R$$
8	2 3	ply1bas	$$⊢B={\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}R\right)}$$
9		psr1baslem	$$⊢{{\mathbb{N}}_0}^{1_{𝑜}}=\left\{a\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
10		tdeglem2	$$⊢\left(b\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)⟼b\left(\varnothing \right)\right)=\left(b\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)⟼{\sum }_{{ℂ}_{\mathrm{fld}}}b\right)$$
11	6 7 8 4 9 10	mdegleb	$$⊢\left(F\in B\wedge G\in {ℝ}^{*}\right)\to \left(D\left(F\right)\le G\leftrightarrow \forall y\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)\left(G<\left(b\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)⟼b\left(\varnothing \right)\right)\left(y\right)\to F\left(y\right)=\underset{\dot{}}{0}\right)\right)$$
12		df1o2	$$⊢1_{𝑜}=\left\{\varnothing \right\}$$
13		nn0ex	$$⊢{\mathbb{N}}_0\in \mathrm{V}$$
14		0ex	$$⊢\varnothing \in \mathrm{V}$$
15		eqid	$$⊢\left(b\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)⟼b\left(\varnothing \right)\right)=\left(b\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)⟼b\left(\varnothing \right)\right)$$
16	12 13 14 15	mapsnf1o2	$$⊢\left(b\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)⟼b\left(\varnothing \right)\right):{{\mathbb{N}}_0}^{1_{𝑜}}\underset{1-1\; onto}{⟶}{\mathbb{N}}_0$$
17		f1ofo	$$⊢\left(b\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)⟼b\left(\varnothing \right)\right):{{\mathbb{N}}_0}^{1_{𝑜}}\underset{1-1\; onto}{⟶}{\mathbb{N}}_0\to \left(b\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)⟼b\left(\varnothing \right)\right):{{\mathbb{N}}_0}^{1_{𝑜}}\underset{onto}{⟶}{\mathbb{N}}_0$$
18		breq2	$$⊢\left(b\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)⟼b\left(\varnothing \right)\right)\left(y\right)=x\to \left(G<\left(b\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)⟼b\left(\varnothing \right)\right)\left(y\right)\leftrightarrow G<x\right)$$
19		fveqeq2	$$⊢\left(b\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)⟼b\left(\varnothing \right)\right)\left(y\right)=x\to \left(A\left(\left(b\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)⟼b\left(\varnothing \right)\right)\left(y\right)\right)=\underset{\dot{}}{0}\leftrightarrow A\left(x\right)=\underset{\dot{}}{0}\right)$$
20	18 19	imbi12d	$$⊢\left(b\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)⟼b\left(\varnothing \right)\right)\left(y\right)=x\to \left(\left(G<\left(b\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)⟼b\left(\varnothing \right)\right)\left(y\right)\to A\left(\left(b\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)⟼b\left(\varnothing \right)\right)\left(y\right)\right)=\underset{\dot{}}{0}\right)\leftrightarrow \left(G<x\to A\left(x\right)=\underset{\dot{}}{0}\right)\right)$$
21	20	cbvfo	$$⊢\left(b\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)⟼b\left(\varnothing \right)\right):{{\mathbb{N}}_0}^{1_{𝑜}}\underset{onto}{⟶}{\mathbb{N}}_0\to \left(\forall y\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)\left(G<\left(b\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)⟼b\left(\varnothing \right)\right)\left(y\right)\to A\left(\left(b\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)⟼b\left(\varnothing \right)\right)\left(y\right)\right)=\underset{\dot{}}{0}\right)\leftrightarrow \forall x\in {\mathbb{N}}_0\left(G<x\to A\left(x\right)=\underset{\dot{}}{0}\right)\right)$$
22	16 17 21	mp2b	$$⊢\forall y\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)\left(G<\left(b\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)⟼b\left(\varnothing \right)\right)\left(y\right)\to A\left(\left(b\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)⟼b\left(\varnothing \right)\right)\left(y\right)\right)=\underset{\dot{}}{0}\right)\leftrightarrow \forall x\in {\mathbb{N}}_0\left(G<x\to A\left(x\right)=\underset{\dot{}}{0}\right)$$
23		fveq1	$$⊢b=y\to b\left(\varnothing \right)=y\left(\varnothing \right)$$
24		fvex	$$⊢y\left(\varnothing \right)\in \mathrm{V}$$
25	23 15 24	fvmpt	$$⊢y\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)\to \left(b\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)⟼b\left(\varnothing \right)\right)\left(y\right)=y\left(\varnothing \right)$$
26	25	fveq2d	$$⊢y\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)\to A\left(\left(b\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)⟼b\left(\varnothing \right)\right)\left(y\right)\right)=A\left(y\left(\varnothing \right)\right)$$
27	26	adantl	$$⊢\left(\left(F\in B\wedge G\in {ℝ}^{*}\right)\wedge y\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)\right)\to A\left(\left(b\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)⟼b\left(\varnothing \right)\right)\left(y\right)\right)=A\left(y\left(\varnothing \right)\right)$$
28	5	fvcoe1	$$⊢\left(F\in B\wedge y\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)\right)\to F\left(y\right)=A\left(y\left(\varnothing \right)\right)$$
29	28	adantlr	$$⊢\left(\left(F\in B\wedge G\in {ℝ}^{*}\right)\wedge y\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)\right)\to F\left(y\right)=A\left(y\left(\varnothing \right)\right)$$
30	27 29	eqtr4d	$$⊢\left(\left(F\in B\wedge G\in {ℝ}^{*}\right)\wedge y\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)\right)\to A\left(\left(b\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)⟼b\left(\varnothing \right)\right)\left(y\right)\right)=F\left(y\right)$$
31	30	eqeq1d	$$⊢\left(\left(F\in B\wedge G\in {ℝ}^{*}\right)\wedge y\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)\right)\to \left(A\left(\left(b\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)⟼b\left(\varnothing \right)\right)\left(y\right)\right)=\underset{\dot{}}{0}\leftrightarrow F\left(y\right)=\underset{\dot{}}{0}\right)$$
32	31	imbi2d	$$⊢\left(\left(F\in B\wedge G\in {ℝ}^{*}\right)\wedge y\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)\right)\to \left(\left(G<\left(b\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)⟼b\left(\varnothing \right)\right)\left(y\right)\to A\left(\left(b\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)⟼b\left(\varnothing \right)\right)\left(y\right)\right)=\underset{\dot{}}{0}\right)\leftrightarrow \left(G<\left(b\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)⟼b\left(\varnothing \right)\right)\left(y\right)\to F\left(y\right)=\underset{\dot{}}{0}\right)\right)$$
33	32	ralbidva	$$⊢\left(F\in B\wedge G\in {ℝ}^{*}\right)\to \left(\forall y\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)\left(G<\left(b\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)⟼b\left(\varnothing \right)\right)\left(y\right)\to A\left(\left(b\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)⟼b\left(\varnothing \right)\right)\left(y\right)\right)=\underset{\dot{}}{0}\right)\leftrightarrow \forall y\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)\left(G<\left(b\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)⟼b\left(\varnothing \right)\right)\left(y\right)\to F\left(y\right)=\underset{\dot{}}{0}\right)\right)$$
34	22 33	bitr3id	$$⊢\left(F\in B\wedge G\in {ℝ}^{*}\right)\to \left(\forall x\in {\mathbb{N}}_0\left(G<x\to A\left(x\right)=\underset{\dot{}}{0}\right)\leftrightarrow \forall y\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)\left(G<\left(b\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)⟼b\left(\varnothing \right)\right)\left(y\right)\to F\left(y\right)=\underset{\dot{}}{0}\right)\right)$$
35	11 34	bitr4d	$$⊢\left(F\in B\wedge G\in {ℝ}^{*}\right)\to \left(D\left(F\right)\le G\leftrightarrow \forall x\in {\mathbb{N}}_0\left(G<x\to A\left(x\right)=\underset{\dot{}}{0}\right)\right)$$