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