Theorem deg1val

Description: Value of the univariate degree as a supremum. (Contributed by Stefan O'Rear, 29-Mar-2015) (Revised by AV, 25-Jul-2019)

	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	deg1val	$$⊢F\in B\to D\left(F\right)=sup\left(A\mathrm{supp}\underset{\dot{}}{0},{ℝ}^{*},<\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\{y\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)|y^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
11		tdeglem2	$$⊢\left(x\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)⟼x\left(\varnothing \right)\right)=\left(x\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)⟼{\sum }_{{ℂ}_{\mathrm{fld}}}x\right)$$
12	6 7 9 4 10 11	mdegval	$$⊢F\in B\to D\left(F\right)=sup\left(\left(x\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)⟼x\left(\varnothing \right)\right)\left[F\mathrm{supp}\underset{\dot{}}{0}\right],{ℝ}^{*},<\right)$$
13	4	fvexi	$$⊢\underset{\dot{}}{0}\in \mathrm{V}$$
14		suppimacnv	$$⊢\left(F\in B\wedge \underset{\dot{}}{0}\in \mathrm{V}\right)\to F\mathrm{supp}\underset{\dot{}}{0}=F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]$$
15	13 14	mpan2	$$⊢F\in B\to F\mathrm{supp}\underset{\dot{}}{0}=F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]$$
16	15	imaeq2d	$$⊢F\in B\to \left(x\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)⟼x\left(\varnothing \right)\right)\left[F\mathrm{supp}\underset{\dot{}}{0}\right]=\left(x\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)⟼x\left(\varnothing \right)\right)\left[F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right]$$
17		imaco	$$⊢\left(\left(x\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)⟼x\left(\varnothing \right)\right)\circ F^{-1}\right)\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]=\left(x\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)⟼x\left(\varnothing \right)\right)\left[F^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]\right]$$
18	16 17	eqtr4di	$$⊢F\in B\to \left(x\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)⟼x\left(\varnothing \right)\right)\left[F\mathrm{supp}\underset{\dot{}}{0}\right]=\left(\left(x\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)⟼x\left(\varnothing \right)\right)\circ F^{-1}\right)\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]$$
19		df1o2	$$⊢1_{𝑜}=\left\{\varnothing \right\}$$
20		nn0ex	$$⊢{\mathbb{N}}_0\in \mathrm{V}$$
21		0ex	$$⊢\varnothing \in \mathrm{V}$$
22		eqid	$$⊢\left(x\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)⟼x\left(\varnothing \right)\right)=\left(x\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)⟼x\left(\varnothing \right)\right)$$
23	19 20 21 22	mapsncnv	$$⊢{\left(x\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)⟼x\left(\varnothing \right)\right)}^{-1}=\left(y\in {\mathbb{N}}_0⟼1_{𝑜}\times \left\{y\right\}\right)$$
24	5 3 2 23	coe1fval2	$$⊢F\in B\to A=F\circ {\left(x\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)⟼x\left(\varnothing \right)\right)}^{-1}$$
25	24	cnveqd	$$⊢F\in B\to A^{-1}={\left(F\circ {\left(x\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)⟼x\left(\varnothing \right)\right)}^{-1}\right)}^{-1}$$
26		cnvco	$$⊢{\left(F\circ {\left(x\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)⟼x\left(\varnothing \right)\right)}^{-1}\right)}^{-1}={{\left(x\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)⟼x\left(\varnothing \right)\right)}^{-1}}^{-1}\circ F^{-1}$$
27		cocnvcnv1	$$⊢{{\left(x\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)⟼x\left(\varnothing \right)\right)}^{-1}}^{-1}\circ F^{-1}=\left(x\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)⟼x\left(\varnothing \right)\right)\circ F^{-1}$$
28	26 27	eqtri	$$⊢{\left(F\circ {\left(x\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)⟼x\left(\varnothing \right)\right)}^{-1}\right)}^{-1}=\left(x\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)⟼x\left(\varnothing \right)\right)\circ F^{-1}$$
29	25 28	eqtr2di	$$⊢F\in B\to \left(x\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)⟼x\left(\varnothing \right)\right)\circ F^{-1}=A^{-1}$$
30	29	imaeq1d	$$⊢F\in B\to \left(\left(x\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)⟼x\left(\varnothing \right)\right)\circ F^{-1}\right)\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]=A^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]$$
31	18 30	eqtrd	$$⊢F\in B\to \left(x\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)⟼x\left(\varnothing \right)\right)\left[F\mathrm{supp}\underset{\dot{}}{0}\right]=A^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]$$
32	5	fvexi	$$⊢A\in \mathrm{V}$$
33		suppimacnv	$$⊢\left(A\in \mathrm{V}\wedge \underset{\dot{}}{0}\in \mathrm{V}\right)\to A\mathrm{supp}\underset{\dot{}}{0}=A^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]$$
34	33	eqcomd	$$⊢\left(A\in \mathrm{V}\wedge \underset{\dot{}}{0}\in \mathrm{V}\right)\to A^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]=A\mathrm{supp}\underset{\dot{}}{0}$$
35	32 13 34	mp2an	$$⊢A^{-1}\left[\mathrm{V}\setminus \left\{\underset{\dot{}}{0}\right\}\right]=A\mathrm{supp}\underset{\dot{}}{0}$$
36	31 35	eqtrdi	$$⊢F\in B\to \left(x\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)⟼x\left(\varnothing \right)\right)\left[F\mathrm{supp}\underset{\dot{}}{0}\right]=A\mathrm{supp}\underset{\dot{}}{0}$$
37	36	supeq1d	$$⊢F\in B\to sup\left(\left(x\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)⟼x\left(\varnothing \right)\right)\left[F\mathrm{supp}\underset{\dot{}}{0}\right],{ℝ}^{*},<\right)=sup\left(A\mathrm{supp}\underset{\dot{}}{0},{ℝ}^{*},<\right)$$
38	12 37	eqtrd	$$⊢F\in B\to D\left(F\right)=sup\left(A\mathrm{supp}\underset{\dot{}}{0},{ℝ}^{*},<\right)$$