Theorem mpl0

Description: The zero polynomial. (Contributed by Mario Carneiro, 9-Jan-2015)

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

Proof

Step	Hyp	Ref	Expression
1		mpl0.p	$$⊢P=I\mathrm{mPoly}R$$
2		mpl0.d	$$⊢D=\left\{f\in \left({{\mathbb{N}}_0}^I\right)|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
3		mpl0.o	$$⊢O=0_R$$
4		mpl0.z	$$⊢\underset{\dot{}}{0}=0_P$$
5		mpl0.i	$$⊢\phi \to I\in W$$
6		mpl0.r	$$⊢\phi \to R\in \mathrm{Grp}$$
7		eqid	$$⊢I\mathrm{mPwSer}R=I\mathrm{mPwSer}R$$
8		eqid	$$⊢{\mathrm{Base}}_P={\mathrm{Base}}_P$$
9	7 1 8 5 6	mplsubg	$$⊢\phi \to {\mathrm{Base}}_P\in \mathrm{SubGrp}\left(I\mathrm{mPwSer}R\right)$$
10	1 7 8	mplval2	$$⊢P=\left(I\mathrm{mPwSer}R\right){\upharpoonright }_{𝑠}{\mathrm{Base}}_P$$
11		eqid	$$⊢0_{\left(I\mathrm{mPwSer}R\right)}=0_{\left(I\mathrm{mPwSer}R\right)}$$
12	10 11	subg0	$$⊢{\mathrm{Base}}_P\in \mathrm{SubGrp}\left(I\mathrm{mPwSer}R\right)\to 0_{\left(I\mathrm{mPwSer}R\right)}=0_P$$
13	9 12	syl	$$⊢\phi \to 0_{\left(I\mathrm{mPwSer}R\right)}=0_P$$
14	7 5 6 2 3 11	psr0	$$⊢\phi \to 0_{\left(I\mathrm{mPwSer}R\right)}=D\times \left\{O\right\}$$
15	13 14	eqtr3d	$$⊢\phi \to 0_P=D\times \left\{O\right\}$$
16	4 15	syl5eq	$$⊢\phi \to \underset{\dot{}}{0}=D\times \left\{O\right\}$$