Theorem mpl1

Description: The identity element of the ring of polynomials. (Contributed by Mario Carneiro, 10-Jan-2015)

	Ref	Expression
Hypotheses	mpl1.p	$$⊢P=I\mathrm{mPoly}R$$
	mpl1.d	$$⊢D=\left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
	mpl1.z	$$⊢\underset{\dot{}}{0}=0_R$$
	mpl1.o	$$⊢\underset{\dot{}}{1}=1_R$$
	mpl1.u	$$⊢U=1_P$$
	mpl1.i	$$⊢\phi \to I\in W$$
	mpl1.r	$$⊢\phi \to R\in \mathrm{Ring}$$
Assertion	mpl1	$$⊢\phi \to U=\left(x\in D⟼if\left(x=I\times \left\{0\right\},\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		mpl1.p	$$⊢P=I\mathrm{mPoly}R$$
2		mpl1.d	$$⊢D=\left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
3		mpl1.z	$$⊢\underset{\dot{}}{0}=0_R$$
4		mpl1.o	$$⊢\underset{\dot{}}{1}=1_R$$
5		mpl1.u	$$⊢U=1_P$$
6		mpl1.i	$$⊢\phi \to I\in W$$
7		mpl1.r	$$⊢\phi \to R\in \mathrm{Ring}$$
8		eqid	$$⊢I\mathrm{mPwSer}R=I\mathrm{mPwSer}R$$
9		eqid	$$⊢{\mathrm{Base}}_P={\mathrm{Base}}_P$$
10	8 1 9 6 7	mplsubrg	$$⊢\phi \to {\mathrm{Base}}_P\in \mathrm{SubRing}\left(I\mathrm{mPwSer}R\right)$$
11	1 8 9	mplval2	$$⊢P=\left(I\mathrm{mPwSer}R\right){\upharpoonright }_{𝑠}{\mathrm{Base}}_P$$
12		eqid	$$⊢1_{\left(I\mathrm{mPwSer}R\right)}=1_{\left(I\mathrm{mPwSer}R\right)}$$
13	11 12	subrg1	$$⊢{\mathrm{Base}}_P\in \mathrm{SubRing}\left(I\mathrm{mPwSer}R\right)\to 1_{\left(I\mathrm{mPwSer}R\right)}=1_P$$
14	10 13	syl	$$⊢\phi \to 1_{\left(I\mathrm{mPwSer}R\right)}=1_P$$
15	8 6 7 2 3 4 12	psr1	$$⊢\phi \to 1_{\left(I\mathrm{mPwSer}R\right)}=\left(x\in D⟼if\left(x=I\times \left\{0\right\},\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)$$
16	14 15	eqtr3d	$$⊢\phi \to 1_P=\left(x\in D⟼if\left(x=I\times \left\{0\right\},\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)$$
17	5 16	syl5eq	$$⊢\phi \to U=\left(x\in D⟼if\left(x=I\times \left\{0\right\},\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)$$