Theorem ply1plusgfvi

Description: Protection compatibility of the univariate polynomial addition. (Contributed by Stefan O'Rear, 27-Mar-2015)

	Ref	Expression
Assertion	ply1plusgfvi	$$⊢{+}_{{\mathrm{Poly}}_1\left(R\right)}={+}_{{\mathrm{Poly}}_1\left(\mathrm{I}\left(R\right)\right)}$$

Proof

Step	Hyp	Ref	Expression
1		fvi	$$⊢R\in \mathrm{V}\to \mathrm{I}\left(R\right)=R$$
2	1	fveq2d	$$⊢R\in \mathrm{V}\to {\mathrm{Poly}}_1\left(\mathrm{I}\left(R\right)\right)={\mathrm{Poly}}_1\left(R\right)$$
3	2	fveq2d	$$⊢R\in \mathrm{V}\to {+}_{{\mathrm{Poly}}_1\left(\mathrm{I}\left(R\right)\right)}={+}_{{\mathrm{Poly}}_1\left(R\right)}$$
4		eqid	$$⊢{\mathrm{Poly}}_1\left(\varnothing \right)={\mathrm{Poly}}_1\left(\varnothing \right)$$
5		eqid	$$⊢1_{𝑜}\mathrm{mPoly}\varnothing =1_{𝑜}\mathrm{mPoly}\varnothing$$
6		eqid	$$⊢{+}_{{\mathrm{Poly}}_1\left(\varnothing \right)}={+}_{{\mathrm{Poly}}_1\left(\varnothing \right)}$$
7	4 5 6	ply1plusg	$$⊢{+}_{{\mathrm{Poly}}_1\left(\varnothing \right)}={+}_{\left(1_{𝑜}\mathrm{mPoly}\varnothing \right)}$$
8		eqid	$$⊢1_{𝑜}\mathrm{mPwSer}\varnothing =1_{𝑜}\mathrm{mPwSer}\varnothing$$
9		eqid	$$⊢{+}_{\left(1_{𝑜}\mathrm{mPoly}\varnothing \right)}={+}_{\left(1_{𝑜}\mathrm{mPoly}\varnothing \right)}$$
10	5 8 9	mplplusg	$$⊢{+}_{\left(1_{𝑜}\mathrm{mPoly}\varnothing \right)}={+}_{\left(1_{𝑜}\mathrm{mPwSer}\varnothing \right)}$$
11		base0	$$⊢\varnothing ={\mathrm{Base}}_{\varnothing }$$
12		psr1baslem	$$⊢{{\mathbb{N}}_0}^{1_{𝑜}}=\left\{a\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)|a^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
13		eqid	$$⊢{\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPwSer}\varnothing \right)}={\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPwSer}\varnothing \right)}$$
14		1on	$$⊢1_{𝑜}\in \mathrm{On}$$
15	14	a1i	$$⊢\top \to 1_{𝑜}\in \mathrm{On}$$
16	8 11 12 13 15	psrbas	$$⊢\top \to {\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPwSer}\varnothing \right)}={\varnothing }^{\left({{\mathbb{N}}_0}^{1_{𝑜}}\right)}$$
17	16	mptru	$$⊢{\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPwSer}\varnothing \right)}={\varnothing }^{\left({{\mathbb{N}}_0}^{1_{𝑜}}\right)}$$
18		0nn0	$$⊢0\in {\mathbb{N}}_0$$
19	18	fconst6	$$⊢\left(1_{𝑜}\times \left\{0\right\}\right):1_{𝑜}⟶{\mathbb{N}}_0$$
20		nn0ex	$$⊢{\mathbb{N}}_0\in \mathrm{V}$$
21		1oex	$$⊢1_{𝑜}\in \mathrm{V}$$
22	20 21	elmap	$$⊢1_{𝑜}\times \left\{0\right\}\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)\leftrightarrow \left(1_{𝑜}\times \left\{0\right\}\right):1_{𝑜}⟶{\mathbb{N}}_0$$
23	19 22	mpbir	$$⊢1_{𝑜}\times \left\{0\right\}\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)$$
24		ne0i	$$⊢1_{𝑜}\times \left\{0\right\}\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)\to {{\mathbb{N}}_0}^{1_{𝑜}}\ne \varnothing$$
25		map0b	$$⊢{{\mathbb{N}}_0}^{1_{𝑜}}\ne \varnothing \to {\varnothing }^{\left({{\mathbb{N}}_0}^{1_{𝑜}}\right)}=\varnothing$$
26	23 24 25	mp2b	$$⊢{\varnothing }^{\left({{\mathbb{N}}_0}^{1_{𝑜}}\right)}=\varnothing$$
27	17 26	eqtr2i	$$⊢\varnothing ={\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPwSer}\varnothing \right)}$$
28		eqid	$$⊢{+}_{\varnothing }={+}_{\varnothing }$$
29		eqid	$$⊢{+}_{\left(1_{𝑜}\mathrm{mPwSer}\varnothing \right)}={+}_{\left(1_{𝑜}\mathrm{mPwSer}\varnothing \right)}$$
30	8 27 28 29	psrplusg	$$⊢{+}_{\left(1_{𝑜}\mathrm{mPwSer}\varnothing \right)}={{\circ }_f{+}_{\varnothing }\upharpoonright }_{\left(\varnothing \times \varnothing \right)}$$
31		xp0	$$⊢\varnothing \times \varnothing =\varnothing$$
32	31	reseq2i	$$⊢{{\circ }_f{+}_{\varnothing }\upharpoonright }_{\left(\varnothing \times \varnothing \right)}={{\circ }_f{+}_{\varnothing }\upharpoonright }_{\varnothing }$$
33	10 30 32	3eqtri	$$⊢{+}_{\left(1_{𝑜}\mathrm{mPoly}\varnothing \right)}={{\circ }_f{+}_{\varnothing }\upharpoonright }_{\varnothing }$$
34		res0	$$⊢{{\circ }_f{+}_{\varnothing }\upharpoonright }_{\varnothing }=\varnothing$$
35		df-plusg	$$⊢{+}_{𝑔}=\mathrm{Slot}2$$
36	35	str0	$$⊢\varnothing ={+}_{\varnothing }$$
37	34 36	eqtri	$$⊢{{\circ }_f{+}_{\varnothing }\upharpoonright }_{\varnothing }={+}_{\varnothing }$$
38	7 33 37	3eqtri	$$⊢{+}_{{\mathrm{Poly}}_1\left(\varnothing \right)}={+}_{\varnothing }$$
39		fvprc	$$⊢\neg R\in \mathrm{V}\to \mathrm{I}\left(R\right)=\varnothing$$
40	39	fveq2d	$$⊢\neg R\in \mathrm{V}\to {\mathrm{Poly}}_1\left(\mathrm{I}\left(R\right)\right)={\mathrm{Poly}}_1\left(\varnothing \right)$$
41	40	fveq2d	$$⊢\neg R\in \mathrm{V}\to {+}_{{\mathrm{Poly}}_1\left(\mathrm{I}\left(R\right)\right)}={+}_{{\mathrm{Poly}}_1\left(\varnothing \right)}$$
42		fvprc	$$⊢\neg R\in \mathrm{V}\to {\mathrm{Poly}}_1\left(R\right)=\varnothing$$
43	42	fveq2d	$$⊢\neg R\in \mathrm{V}\to {+}_{{\mathrm{Poly}}_1\left(R\right)}={+}_{\varnothing }$$
44	38 41 43	3eqtr4a	$$⊢\neg R\in \mathrm{V}\to {+}_{{\mathrm{Poly}}_1\left(\mathrm{I}\left(R\right)\right)}={+}_{{\mathrm{Poly}}_1\left(R\right)}$$
45	3 44	pm2.61i	$$⊢{+}_{{\mathrm{Poly}}_1\left(\mathrm{I}\left(R\right)\right)}={+}_{{\mathrm{Poly}}_1\left(R\right)}$$
46	45	eqcomi	$$⊢{+}_{{\mathrm{Poly}}_1\left(R\right)}={+}_{{\mathrm{Poly}}_1\left(\mathrm{I}\left(R\right)\right)}$$