coe1add

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

	Ref	Expression
Hypotheses	coe1add.y	$⊢ Y = {Poly}_{1} (R)$
	coe1add.b	$⊢ B = {Base}_{Y}$
	coe1add.p	$⊢ \underset{˙}{✚} = +_{Y}$
	coe1add.q	$⊢ \underset{˙}{+} = +_{R}$
Assertion	coe1add	$⊢ (R \in Ring \land F \in B \land G \in B) \to {coe}_{1} (F \underset{˙}{✚} G) = {coe}_{1} (F) {\underset{˙}{+}}_{f} {coe}_{1} (G)$

Proof

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

Metamath Proof Explorer

Theorem coe1add

Proof