Theorem coe1add

Description: The coefficient vector of an addition. (Contributed by Stefan O'Rear, 24-Mar-2015)

	Ref	Expression
Hypotheses	coe1add.y	$$⊢Y={\mathrm{Poly}}_1\left(R\right)$$
	coe1add.b	$$⊢B={\mathrm{Base}}_Y$$
	coe1add.p	$$⊢\underset{\dot{}}{✚}={+}_Y$$
	coe1add.q	$$⊢\underset{\dot{}}{+}={+}_R$$
Assertion	coe1add	$$⊢\left(R\in \mathrm{Ring}\wedge F\in B\wedge G\in B\right)\to {\mathrm{coe}}_1\left(F\underset{\dot{}}{✚}G\right)={\mathrm{coe}}_1\left(F\right){\underset{\dot{}}{+}}_f{\mathrm{coe}}_1\left(G\right)$$

Proof

Step	Hyp	Ref	Expression
1		coe1add.y	$$⊢Y={\mathrm{Poly}}_1\left(R\right)$$
2		coe1add.b	$$⊢B={\mathrm{Base}}_Y$$
3		coe1add.p	$$⊢\underset{\dot{}}{✚}={+}_Y$$
4		coe1add.q	$$⊢\underset{\dot{}}{+}={+}_R$$
5		eqid	$$⊢1_{𝑜}\mathrm{mPoly}R=1_{𝑜}\mathrm{mPoly}R$$
6		eqid	$$⊢{\mathrm{PwSer}}_1\left(R\right)={\mathrm{PwSer}}_1\left(R\right)$$
7	1 6 2	ply1bas	$$⊢B={\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}R\right)}$$
8	1 5 3	ply1plusg	$$⊢\underset{\dot{}}{✚}={+}_{\left(1_{𝑜}\mathrm{mPoly}R\right)}$$
9		simp2	$$⊢\left(R\in \mathrm{Ring}\wedge F\in B\wedge G\in B\right)\to F\in B$$
10		simp3	$$⊢\left(R\in \mathrm{Ring}\wedge F\in B\wedge G\in B\right)\to G\in B$$
11	5 7 4 8 9 10	mpladd	$$⊢\left(R\in \mathrm{Ring}\wedge F\in B\wedge G\in B\right)\to F\underset{\dot{}}{✚}G=F{\underset{\dot{}}{+}}_{f}G$$
12	11	coeq1d	$$⊢\left(R\in \mathrm{Ring}\wedge F\in B\wedge G\in B\right)\to \left(F\underset{\dot{}}{✚}G\right)\circ \left(a\in {\mathbb{N}}_0⟼1_{𝑜}\times \left\{a\right\}\right)=\left(F{\underset{\dot{}}{+}}_{f}G\right)\circ \left(a\in {\mathbb{N}}_0⟼1_{𝑜}\times \left\{a\right\}\right)$$
13		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
14	1 2 13	ply1basf	$$⊢F\in B\to F:{{\mathbb{N}}_0}^{1_{𝑜}}⟶{\mathrm{Base}}_R$$
15	14	ffnd	$$⊢F\in B\to FFn\left({{\mathbb{N}}_0}^{1_{𝑜}}\right)$$
16	15	3ad2ant2	$$⊢\left(R\in \mathrm{Ring}\wedge F\in B\wedge G\in B\right)\to FFn\left({{\mathbb{N}}_0}^{1_{𝑜}}\right)$$
17	1 2 13	ply1basf	$$⊢G\in B\to G:{{\mathbb{N}}_0}^{1_{𝑜}}⟶{\mathrm{Base}}_R$$
18	17	ffnd	$$⊢G\in B\to GFn\left({{\mathbb{N}}_0}^{1_{𝑜}}\right)$$
19	18	3ad2ant3	$$⊢\left(R\in \mathrm{Ring}\wedge F\in B\wedge G\in B\right)\to GFn\left({{\mathbb{N}}_0}^{1_{𝑜}}\right)$$
20		df1o2	$$⊢1_{𝑜}=\left\{\varnothing \right\}$$
21		nn0ex	$$⊢{\mathbb{N}}_0\in \mathrm{V}$$
22		0ex	$$⊢\varnothing \in \mathrm{V}$$
23		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)$$
24	20 21 22 23	mapsnf1o3	$$⊢\left(a\in {\mathbb{N}}_0⟼1_{𝑜}\times \left\{a\right\}\right):{\mathbb{N}}_0\underset{1-1\; onto}{⟶}{{\mathbb{N}}_0}^{1_{𝑜}}$$
25		f1of	$$⊢\left(a\in {\mathbb{N}}_0⟼1_{𝑜}\times \left\{a\right\}\right):{\mathbb{N}}_0\underset{1-1\; onto}{⟶}{{\mathbb{N}}_0}^{1_{𝑜}}\to \left(a\in {\mathbb{N}}_0⟼1_{𝑜}\times \left\{a\right\}\right):{\mathbb{N}}_0⟶{{\mathbb{N}}_0}^{1_{𝑜}}$$
26	24 25	mp1i	$$⊢\left(R\in \mathrm{Ring}\wedge F\in B\wedge G\in B\right)\to \left(a\in {\mathbb{N}}_0⟼1_{𝑜}\times \left\{a\right\}\right):{\mathbb{N}}_0⟶{{\mathbb{N}}_0}^{1_{𝑜}}$$
27		ovexd	$$⊢\left(R\in \mathrm{Ring}\wedge F\in B\wedge G\in B\right)\to {{\mathbb{N}}_0}^{1_{𝑜}}\in \mathrm{V}$$
28	21	a1i	$$⊢\left(R\in \mathrm{Ring}\wedge F\in B\wedge G\in B\right)\to {\mathbb{N}}_0\in \mathrm{V}$$
29		inidm	$$⊢\left({{\mathbb{N}}_0}^{1_{𝑜}}\right)\cap \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)={{\mathbb{N}}_0}^{1_{𝑜}}$$
30	16 19 26 27 27 28 29	ofco	$$⊢\left(R\in \mathrm{Ring}\wedge F\in B\wedge G\in B\right)\to \left(F{\underset{\dot{}}{+}}_{f}G\right)\circ \left(a\in {\mathbb{N}}_0⟼1_{𝑜}\times \left\{a\right\}\right)=\left(F\circ \left(a\in {\mathbb{N}}_0⟼1_{𝑜}\times \left\{a\right\}\right)\right){\underset{\dot{}}{+}}_f\left(G\circ \left(a\in {\mathbb{N}}_0⟼1_{𝑜}\times \left\{a\right\}\right)\right)$$
31	12 30	eqtrd	$$⊢\left(R\in \mathrm{Ring}\wedge F\in B\wedge G\in B\right)\to \left(F\underset{\dot{}}{✚}G\right)\circ \left(a\in {\mathbb{N}}_0⟼1_{𝑜}\times \left\{a\right\}\right)=\left(F\circ \left(a\in {\mathbb{N}}_0⟼1_{𝑜}\times \left\{a\right\}\right)\right){\underset{\dot{}}{+}}_f\left(G\circ \left(a\in {\mathbb{N}}_0⟼1_{𝑜}\times \left\{a\right\}\right)\right)$$
32	1	ply1ring	$$⊢R\in \mathrm{Ring}\to Y\in \mathrm{Ring}$$
33	2 3	ringacl	$$⊢\left(Y\in \mathrm{Ring}\wedge F\in B\wedge G\in B\right)\to F\underset{\dot{}}{✚}G\in B$$
34	32 33	syl3an1	$$⊢\left(R\in \mathrm{Ring}\wedge F\in B\wedge G\in B\right)\to F\underset{\dot{}}{✚}G\in B$$
35		eqid	$$⊢{\mathrm{coe}}_1\left(F\underset{\dot{}}{✚}G\right)={\mathrm{coe}}_1\left(F\underset{\dot{}}{✚}G\right)$$
36	35 2 1 23	coe1fval2	$$⊢F\underset{\dot{}}{✚}G\in B\to {\mathrm{coe}}_1\left(F\underset{\dot{}}{✚}G\right)=\left(F\underset{\dot{}}{✚}G\right)\circ \left(a\in {\mathbb{N}}_0⟼1_{𝑜}\times \left\{a\right\}\right)$$
37	34 36	syl	$$⊢\left(R\in \mathrm{Ring}\wedge F\in B\wedge G\in B\right)\to {\mathrm{coe}}_1\left(F\underset{\dot{}}{✚}G\right)=\left(F\underset{\dot{}}{✚}G\right)\circ \left(a\in {\mathbb{N}}_0⟼1_{𝑜}\times \left\{a\right\}\right)$$
38		eqid	$$⊢{\mathrm{coe}}_1\left(F\right)={\mathrm{coe}}_1\left(F\right)$$
39	38 2 1 23	coe1fval2	$$⊢F\in B\to {\mathrm{coe}}_1\left(F\right)=F\circ \left(a\in {\mathbb{N}}_0⟼1_{𝑜}\times \left\{a\right\}\right)$$
40	39	3ad2ant2	$$⊢\left(R\in \mathrm{Ring}\wedge F\in B\wedge G\in B\right)\to {\mathrm{coe}}_1\left(F\right)=F\circ \left(a\in {\mathbb{N}}_0⟼1_{𝑜}\times \left\{a\right\}\right)$$
41		eqid	$$⊢{\mathrm{coe}}_1\left(G\right)={\mathrm{coe}}_1\left(G\right)$$
42	41 2 1 23	coe1fval2	$$⊢G\in B\to {\mathrm{coe}}_1\left(G\right)=G\circ \left(a\in {\mathbb{N}}_0⟼1_{𝑜}\times \left\{a\right\}\right)$$
43	42	3ad2ant3	$$⊢\left(R\in \mathrm{Ring}\wedge F\in B\wedge G\in B\right)\to {\mathrm{coe}}_1\left(G\right)=G\circ \left(a\in {\mathbb{N}}_0⟼1_{𝑜}\times \left\{a\right\}\right)$$
44	40 43	oveq12d	$$⊢\left(R\in \mathrm{Ring}\wedge F\in B\wedge G\in B\right)\to {\mathrm{coe}}_1\left(F\right){\underset{\dot{}}{+}}_f{\mathrm{coe}}_1\left(G\right)=\left(F\circ \left(a\in {\mathbb{N}}_0⟼1_{𝑜}\times \left\{a\right\}\right)\right){\underset{\dot{}}{+}}_f\left(G\circ \left(a\in {\mathbb{N}}_0⟼1_{𝑜}\times \left\{a\right\}\right)\right)$$
45	31 37 44	3eqtr4d	$$⊢\left(R\in \mathrm{Ring}\wedge F\in B\wedge G\in B\right)\to {\mathrm{coe}}_1\left(F\underset{\dot{}}{✚}G\right)={\mathrm{coe}}_1\left(F\right){\underset{\dot{}}{+}}_f{\mathrm{coe}}_1\left(G\right)$$