Theorem coe1z

Description: The coefficient vector of 0. (Contributed by Stefan O'Rear, 23-Mar-2015)

	Ref	Expression
Hypotheses	coe1z.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
	coe1z.z	$$⊢\underset{\dot{}}{0}=0_P$$
	coe1z.y	$$⊢Y=0_R$$
Assertion	coe1z	$$⊢R\in \mathrm{Ring}\to {\mathrm{coe}}_1\left(\underset{\dot{}}{0}\right)={\mathbb{N}}_0\times \left\{Y\right\}$$

Proof

Step	Hyp	Ref	Expression
1		coe1z.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
2		coe1z.z	$$⊢\underset{\dot{}}{0}=0_P$$
3		coe1z.y	$$⊢Y=0_R$$
4		fconst6g	$$⊢a\in {\mathbb{N}}_0\to \left(1_{𝑜}\times \left\{a\right\}\right):1_{𝑜}⟶{\mathbb{N}}_0$$
5	4	adantl	$$⊢\left(R\in \mathrm{Ring}\wedge a\in {\mathbb{N}}_0\right)\to \left(1_{𝑜}\times \left\{a\right\}\right):1_{𝑜}⟶{\mathbb{N}}_0$$
6		nn0ex	$$⊢{\mathbb{N}}_0\in \mathrm{V}$$
7		1oex	$$⊢1_{𝑜}\in \mathrm{V}$$
8	6 7	elmap	$$⊢1_{𝑜}\times \left\{a\right\}\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)\leftrightarrow \left(1_{𝑜}\times \left\{a\right\}\right):1_{𝑜}⟶{\mathbb{N}}_0$$
9	5 8	sylibr	$$⊢\left(R\in \mathrm{Ring}\wedge a\in {\mathbb{N}}_0\right)\to 1_{𝑜}\times \left\{a\right\}\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)$$
10		eqidd	$$⊢R\in \mathrm{Ring}\to \left(a\in {\mathbb{N}}_0⟼1_{𝑜}\times \left\{a\right\}\right)=\left(a\in {\mathbb{N}}_0⟼1_{𝑜}\times \left\{a\right\}\right)$$
11		eqid	$$⊢1_{𝑜}\mathrm{mPoly}R=1_{𝑜}\mathrm{mPoly}R$$
12		psr1baslem	$$⊢{{\mathbb{N}}_0}^{1_{𝑜}}=\left\{c\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)|c^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
13	11 1 2	ply1mpl0	$$⊢\underset{\dot{}}{0}=0_{\left(1_{𝑜}\mathrm{mPoly}R\right)}$$
14		1on	$$⊢1_{𝑜}\in \mathrm{On}$$
15	14	a1i	$$⊢R\in \mathrm{Ring}\to 1_{𝑜}\in \mathrm{On}$$
16		ringgrp	$$⊢R\in \mathrm{Ring}\to R\in \mathrm{Grp}$$
17	11 12 3 13 15 16	mpl0	$$⊢R\in \mathrm{Ring}\to \underset{\dot{}}{0}=\left({{\mathbb{N}}_0}^{1_{𝑜}}\right)\times \left\{Y\right\}$$
18		fconstmpt	$$⊢\left({{\mathbb{N}}_0}^{1_{𝑜}}\right)\times \left\{Y\right\}=\left(b\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)⟼Y\right)$$
19	17 18	eqtrdi	$$⊢R\in \mathrm{Ring}\to \underset{\dot{}}{0}=\left(b\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)⟼Y\right)$$
20		eqidd	$$⊢b=1_{𝑜}\times \left\{a\right\}\to Y=Y$$
21	9 10 19 20	fmptco	$$⊢R\in \mathrm{Ring}\to \underset{\dot{}}{0}\circ \left(a\in {\mathbb{N}}_0⟼1_{𝑜}\times \left\{a\right\}\right)=\left(a\in {\mathbb{N}}_0⟼Y\right)$$
22	1	ply1ring	$$⊢R\in \mathrm{Ring}\to P\in \mathrm{Ring}$$
23		eqid	$$⊢{\mathrm{Base}}_P={\mathrm{Base}}_P$$
24	23 2	ring0cl	$$⊢P\in \mathrm{Ring}\to \underset{\dot{}}{0}\in {\mathrm{Base}}_P$$
25		eqid	$$⊢{\mathrm{coe}}_1\left(\underset{\dot{}}{0}\right)={\mathrm{coe}}_1\left(\underset{\dot{}}{0}\right)$$
26		eqid	$$⊢\left(a\in {\mathbb{N}}_0⟼1_{𝑜}\times \left\{a\right\}\right)=\left(a\in {\mathbb{N}}_0⟼1_{𝑜}\times \left\{a\right\}\right)$$
27	25 23 1 26	coe1fval2	$$⊢\underset{\dot{}}{0}\in {\mathrm{Base}}_P\to {\mathrm{coe}}_1\left(\underset{\dot{}}{0}\right)=\underset{\dot{}}{0}\circ \left(a\in {\mathbb{N}}_0⟼1_{𝑜}\times \left\{a\right\}\right)$$
28	22 24 27	3syl	$$⊢R\in \mathrm{Ring}\to {\mathrm{coe}}_1\left(\underset{\dot{}}{0}\right)=\underset{\dot{}}{0}\circ \left(a\in {\mathbb{N}}_0⟼1_{𝑜}\times \left\{a\right\}\right)$$
29		fconstmpt	$$⊢{\mathbb{N}}_0\times \left\{Y\right\}=\left(a\in {\mathbb{N}}_0⟼Y\right)$$
30	29	a1i	$$⊢R\in \mathrm{Ring}\to {\mathbb{N}}_0\times \left\{Y\right\}=\left(a\in {\mathbb{N}}_0⟼Y\right)$$
31	21 28 30	3eqtr4d	$$⊢R\in \mathrm{Ring}\to {\mathrm{coe}}_1\left(\underset{\dot{}}{0}\right)={\mathbb{N}}_0\times \left\{Y\right\}$$