Theorem coe1add

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

	Ref	Expression
Hypotheses	coe1add.y	⊢ 𝑌 = ( Poly1 ‘ 𝑅 )
	coe1add.b	⊢ 𝐵 = ( Base ‘ 𝑌 )
	coe1add.p	⊢ ✚ = ( +g ‘ 𝑌 )
	coe1add.q	⊢ + = ( +g ‘ 𝑅 )
Assertion	coe1add	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → ( coe1 ‘ ( 𝐹 ✚ 𝐺 ) ) = ( ( coe1 ‘ 𝐹 ) ∘f + ( coe1 ‘ 𝐺 ) ) )

Proof

Step	Hyp	Ref	Expression
1		coe1add.y	⊢ 𝑌 = ( Poly1 ‘ 𝑅 )
2		coe1add.b	⊢ 𝐵 = ( Base ‘ 𝑌 )
3		coe1add.p	⊢ ✚ = ( +g ‘ 𝑌 )
4		coe1add.q	⊢ + = ( +g ‘ 𝑅 )
5		eqid	⊢ ( 1o mPoly 𝑅 ) = ( 1o mPoly 𝑅 )
6		eqid	⊢ ( PwSer1 ‘ 𝑅 ) = ( PwSer1 ‘ 𝑅 )
7	1 6 2	ply1bas	⊢ 𝐵 = ( Base ‘ ( 1o mPoly 𝑅 ) )
8	1 5 3	ply1plusg	⊢ ✚ = ( +g ‘ ( 1o mPoly 𝑅 ) )
9		simp2	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → 𝐹 ∈ 𝐵 )
10		simp3	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → 𝐺 ∈ 𝐵 )
11	5 7 4 8 9 10	mpladd	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → ( 𝐹 ✚ 𝐺 ) = ( 𝐹 ∘f + 𝐺 ) )
12	11	coeq1d	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → ( ( 𝐹 ✚ 𝐺 ) ∘ ( 𝑎 ∈ ℕ0 ↦ ( 1o × { 𝑎 } ) ) ) = ( ( 𝐹 ∘f + 𝐺 ) ∘ ( 𝑎 ∈ ℕ0 ↦ ( 1o × { 𝑎 } ) ) ) )
13		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
14	1 2 13	ply1basf	⊢ ( 𝐹 ∈ 𝐵 → 𝐹 : ( ℕ0 ↑m 1o ) ⟶ ( Base ‘ 𝑅 ) )
15	14	ffnd	⊢ ( 𝐹 ∈ 𝐵 → 𝐹 Fn ( ℕ0 ↑m 1o ) )
16	15	3ad2ant2	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → 𝐹 Fn ( ℕ0 ↑m 1o ) )
17	1 2 13	ply1basf	⊢ ( 𝐺 ∈ 𝐵 → 𝐺 : ( ℕ0 ↑m 1o ) ⟶ ( Base ‘ 𝑅 ) )
18	17	ffnd	⊢ ( 𝐺 ∈ 𝐵 → 𝐺 Fn ( ℕ0 ↑m 1o ) )
19	18	3ad2ant3	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → 𝐺 Fn ( ℕ0 ↑m 1o ) )
20		df1o2	⊢ 1o = { ∅ }
21		nn0ex	⊢ ℕ0 ∈ V
22		0ex	⊢ ∅ ∈ V
23		eqid	⊢ ( 𝑎 ∈ ℕ0 ↦ ( 1o × { 𝑎 } ) ) = ( 𝑎 ∈ ℕ0 ↦ ( 1o × { 𝑎 } ) )
24	20 21 22 23	mapsnf1o3	⊢ ( 𝑎 ∈ ℕ0 ↦ ( 1o × { 𝑎 } ) ) : ℕ0 –1-1-onto→ ( ℕ0 ↑m 1o )
25		f1of	⊢ ( ( 𝑎 ∈ ℕ0 ↦ ( 1o × { 𝑎 } ) ) : ℕ0 –1-1-onto→ ( ℕ0 ↑m 1o ) → ( 𝑎 ∈ ℕ0 ↦ ( 1o × { 𝑎 } ) ) : ℕ0 ⟶ ( ℕ0 ↑m 1o ) )
26	24 25	mp1i	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → ( 𝑎 ∈ ℕ0 ↦ ( 1o × { 𝑎 } ) ) : ℕ0 ⟶ ( ℕ0 ↑m 1o ) )
27		ovexd	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → ( ℕ0 ↑m 1o ) ∈ V )
28	21	a1i	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → ℕ0 ∈ V )
29		inidm	⊢ ( ( ℕ0 ↑m 1o ) ∩ ( ℕ0 ↑m 1o ) ) = ( ℕ0 ↑m 1o )
30	16 19 26 27 27 28 29	ofco	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → ( ( 𝐹 ∘f + 𝐺 ) ∘ ( 𝑎 ∈ ℕ0 ↦ ( 1o × { 𝑎 } ) ) ) = ( ( 𝐹 ∘ ( 𝑎 ∈ ℕ0 ↦ ( 1o × { 𝑎 } ) ) ) ∘f + ( 𝐺 ∘ ( 𝑎 ∈ ℕ0 ↦ ( 1o × { 𝑎 } ) ) ) ) )
31	12 30	eqtrd	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → ( ( 𝐹 ✚ 𝐺 ) ∘ ( 𝑎 ∈ ℕ0 ↦ ( 1o × { 𝑎 } ) ) ) = ( ( 𝐹 ∘ ( 𝑎 ∈ ℕ0 ↦ ( 1o × { 𝑎 } ) ) ) ∘f + ( 𝐺 ∘ ( 𝑎 ∈ ℕ0 ↦ ( 1o × { 𝑎 } ) ) ) ) )
32	1	ply1ring	⊢ ( 𝑅 ∈ Ring → 𝑌 ∈ Ring )
33	2 3	ringacl	⊢ ( ( 𝑌 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → ( 𝐹 ✚ 𝐺 ) ∈ 𝐵 )
34	32 33	syl3an1	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → ( 𝐹 ✚ 𝐺 ) ∈ 𝐵 )
35		eqid	⊢ ( coe1 ‘ ( 𝐹 ✚ 𝐺 ) ) = ( coe1 ‘ ( 𝐹 ✚ 𝐺 ) )
36	35 2 1 23	coe1fval2	⊢ ( ( 𝐹 ✚ 𝐺 ) ∈ 𝐵 → ( coe1 ‘ ( 𝐹 ✚ 𝐺 ) ) = ( ( 𝐹 ✚ 𝐺 ) ∘ ( 𝑎 ∈ ℕ0 ↦ ( 1o × { 𝑎 } ) ) ) )
37	34 36	syl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → ( coe1 ‘ ( 𝐹 ✚ 𝐺 ) ) = ( ( 𝐹 ✚ 𝐺 ) ∘ ( 𝑎 ∈ ℕ0 ↦ ( 1o × { 𝑎 } ) ) ) )
38		eqid	⊢ ( coe1 ‘ 𝐹 ) = ( coe1 ‘ 𝐹 )
39	38 2 1 23	coe1fval2	⊢ ( 𝐹 ∈ 𝐵 → ( coe1 ‘ 𝐹 ) = ( 𝐹 ∘ ( 𝑎 ∈ ℕ0 ↦ ( 1o × { 𝑎 } ) ) ) )
40	39	3ad2ant2	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → ( coe1 ‘ 𝐹 ) = ( 𝐹 ∘ ( 𝑎 ∈ ℕ0 ↦ ( 1o × { 𝑎 } ) ) ) )
41		eqid	⊢ ( coe1 ‘ 𝐺 ) = ( coe1 ‘ 𝐺 )
42	41 2 1 23	coe1fval2	⊢ ( 𝐺 ∈ 𝐵 → ( coe1 ‘ 𝐺 ) = ( 𝐺 ∘ ( 𝑎 ∈ ℕ0 ↦ ( 1o × { 𝑎 } ) ) ) )
43	42	3ad2ant3	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → ( coe1 ‘ 𝐺 ) = ( 𝐺 ∘ ( 𝑎 ∈ ℕ0 ↦ ( 1o × { 𝑎 } ) ) ) )
44	40 43	oveq12d	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → ( ( coe1 ‘ 𝐹 ) ∘f + ( coe1 ‘ 𝐺 ) ) = ( ( 𝐹 ∘ ( 𝑎 ∈ ℕ0 ↦ ( 1o × { 𝑎 } ) ) ) ∘f + ( 𝐺 ∘ ( 𝑎 ∈ ℕ0 ↦ ( 1o × { 𝑎 } ) ) ) ) )
45	31 37 44	3eqtr4d	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → ( coe1 ‘ ( 𝐹 ✚ 𝐺 ) ) = ( ( coe1 ‘ 𝐹 ) ∘f + ( coe1 ‘ 𝐺 ) ) )