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		eqid	$$⊢{\mathrm{PwSer}}_1\left(R\right)={\mathrm{PwSer}}_1\left(R\right)$$
9	2 8 3	ply1bas	$$⊢B={\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}R\right)}$$
10		psr1baslem	$$⊢{{\mathbb{N}}_0}^{1_{𝑜}}=\left\{a\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
11		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)$$
12	6 7 9 4 10 11	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)$$
13		df1o2	$$⊢1_{𝑜}=\left\{\varnothing \right\}$$
14		nn0ex	$$⊢{\mathbb{N}}_0\in \mathrm{V}$$
15		0ex	$$⊢\varnothing \in \mathrm{V}$$
16		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)$$
17	13 14 15 16	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$$
18		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$$
19		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)$$
20		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)$$
21	19 20	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)$$
22	21	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)$$
23	17 18 22	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)$$
24		fveq1	$$⊢b=y\to b\left(\varnothing \right)=y\left(\varnothing \right)$$
25		fvex	$$⊢y\left(\varnothing \right)\in \mathrm{V}$$
26	24 16 25	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)$$
27	26	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)$$
28	27	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)$$
29	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)$$
30	29	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)$$
31	28 30	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)$$
32	31	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)$$
33	32	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)$$
34	33	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)$$
35	23 34	syl5bbr	$$⊢\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)$$
36	12 35	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)$$