Theorem fply1

Description: Conditions for a function to be an univariate polynomial. (Contributed by Thierry Arnoux, 19-Aug-2023)

	Ref	Expression
Hypotheses	fply1.1	$$⊢\underset{\dot{}}{0}=0_R$$
	fply1.2	$$⊢B={\mathrm{Base}}_R$$
	fply1.3	$$⊢P={\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}$$
	fply1.4	$$⊢\phi \to F:{{\mathbb{N}}_0}^{1_{𝑜}}⟶B$$
	fply1.5	$$⊢\phi \to {finSupp}_{\underset{\dot{}}{0}}\left(F\right)$$
Assertion	fply1	$$⊢\phi \to F\in P$$

Proof

Step	Hyp	Ref	Expression
1		fply1.1	$$⊢\underset{\dot{}}{0}=0_R$$
2		fply1.2	$$⊢B={\mathrm{Base}}_R$$
3		fply1.3	$$⊢P={\mathrm{Base}}_{{\mathrm{Poly}}_1\left(R\right)}$$
4		fply1.4	$$⊢\phi \to F:{{\mathbb{N}}_0}^{1_{𝑜}}⟶B$$
5		fply1.5	$$⊢\phi \to {finSupp}_{\underset{\dot{}}{0}}\left(F\right)$$
6	2	fvexi	$$⊢B\in \mathrm{V}$$
7		ovex	$$⊢{{\mathbb{N}}_0}^{1_{𝑜}}\in \mathrm{V}$$
8	6 7	elmap	$$⊢F\in \left(B^{\left({{\mathbb{N}}_0}^{1_{𝑜}}\right)}\right)\leftrightarrow F:{{\mathbb{N}}_0}^{1_{𝑜}}⟶B$$
9	4 8	sylibr	$$⊢\phi \to F\in \left(B^{\left({{\mathbb{N}}_0}^{1_{𝑜}}\right)}\right)$$
10		df1o2	$$⊢1_{𝑜}=\left\{\varnothing \right\}$$
11		snfi	$$⊢\left\{\varnothing \right\}\in \mathrm{Fin}$$
12	10 11	eqeltri	$$⊢1_{𝑜}\in \mathrm{Fin}$$
13	12	a1i	$$⊢f\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)\to 1_{𝑜}\in \mathrm{Fin}$$
14		elmapi	$$⊢f\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)\to f:1_{𝑜}⟶{\mathbb{N}}_0$$
15	13 14	fisuppfi	$$⊢f\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)\to f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}$$
16	15	rabeqc	$$⊢\left\{f\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}={{\mathbb{N}}_0}^{1_{𝑜}}$$
17	16	oveq2i	$$⊢B^{\left\{f\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}}=B^{\left({{\mathbb{N}}_0}^{1_{𝑜}}\right)}$$
18	9 17	eleqtrrdi	$$⊢\phi \to F\in \left(B^{\left\{f\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}}\right)$$
19		eqid	$$⊢1_{𝑜}\mathrm{mPwSer}R=1_{𝑜}\mathrm{mPwSer}R$$
20		eqid	$$⊢\left\{f\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}=\left\{f\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
21		eqid	$$⊢{\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPwSer}R\right)}={\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPwSer}R\right)}$$
22		1oex	$$⊢1_{𝑜}\in \mathrm{V}$$
23	22	a1i	$$⊢\phi \to 1_{𝑜}\in \mathrm{V}$$
24	19 2 20 21 23	psrbas	$$⊢\phi \to {\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPwSer}R\right)}=B^{\left\{f\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}}$$
25	18 24	eleqtrrd	$$⊢\phi \to F\in {\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPwSer}R\right)}$$
26		eqid	$$⊢1_{𝑜}\mathrm{mPoly}R=1_{𝑜}\mathrm{mPoly}R$$
27		eqid	$$⊢{\mathrm{Poly}}_1\left(R\right)={\mathrm{Poly}}_1\left(R\right)$$
28		eqid	$$⊢{\mathrm{PwSer}}_1\left(R\right)={\mathrm{PwSer}}_1\left(R\right)$$
29	27 28 3	ply1bas	$$⊢P={\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}R\right)}$$
30	26 19 21 1 29	mplelbas	$$⊢F\in P\leftrightarrow \left(F\in {\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPwSer}R\right)}\wedge {finSupp}_{\underset{\dot{}}{0}}\left(F\right)\right)$$
31	25 5 30	sylanbrc	$$⊢\phi \to F\in P$$