This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem coe1mul

Description: The coefficient vector of multiplication in the univariate polynomial ring. (Contributed by Stefan O'Rear, 25-Mar-2015)

		Ref	Expression
	Hypotheses	coe1mul.s	⊢ 𝑌 = ( Poly₁ ‘ 𝑅 )
		coe1mul.t	⊢ ∙ = ( ._r ‘ 𝑌 )
		coe1mul.u	⊢ · = ( ._r ‘ 𝑅 )
		coe1mul.b	⊢ 𝐵 = ( Base ‘ 𝑌 )
	Assertion	coe1mul	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → ( coe₁ ‘ ( 𝐹 ∙ 𝐺 ) ) = ( 𝑘 ∈ ℕ₀ ↦ ( 𝑅 Σ_g ( 𝑥 ∈ ( 0 ... 𝑘 ) ↦ ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑥 ) · ( ( coe₁ ‘ 𝐺 ) ‘ ( 𝑘 − 𝑥 ) ) ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		coe1mul.s	⊢ 𝑌 = ( Poly₁ ‘ 𝑅 )
2		coe1mul.t	⊢ ∙ = ( ._r ‘ 𝑌 )
3		coe1mul.u	⊢ · = ( ._r ‘ 𝑅 )
4		coe1mul.b	⊢ 𝐵 = ( Base ‘ 𝑌 )
5		id	⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Ring )
6	1 4	ply1bascl	⊢ ( 𝐹 ∈ 𝐵 → 𝐹 ∈ ( Base ‘ ( PwSer₁ ‘ 𝑅 ) ) )
7	1 4	ply1bascl	⊢ ( 𝐺 ∈ 𝐵 → 𝐺 ∈ ( Base ‘ ( PwSer₁ ‘ 𝑅 ) ) )
8		eqid	⊢ ( PwSer₁ ‘ 𝑅 ) = ( PwSer₁ ‘ 𝑅 )
9		eqid	⊢ ( 1_o mPoly 𝑅 ) = ( 1_o mPoly 𝑅 )
10		eqid	⊢ ( 1_o mPwSer 𝑅 ) = ( 1_o mPwSer 𝑅 )
11	1 9 2	ply1mulr	⊢ ∙ = ( ._r ‘ ( 1_o mPoly 𝑅 ) )
12	9 10 11	mplmulr	⊢ ∙ = ( ._r ‘ ( 1_o mPwSer 𝑅 ) )
13		eqid	⊢ ( ._r ‘ ( PwSer₁ ‘ 𝑅 ) ) = ( ._r ‘ ( PwSer₁ ‘ 𝑅 ) )
14	8 10 13	psr1mulr	⊢ ( ._r ‘ ( PwSer₁ ‘ 𝑅 ) ) = ( ._r ‘ ( 1_o mPwSer 𝑅 ) )
15	12 14	eqtr4i	⊢ ∙ = ( ._r ‘ ( PwSer₁ ‘ 𝑅 ) )
16		eqid	⊢ ( Base ‘ ( PwSer₁ ‘ 𝑅 ) ) = ( Base ‘ ( PwSer₁ ‘ 𝑅 ) )
17	8 15 3 16	coe1mul2	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ ( Base ‘ ( PwSer₁ ‘ 𝑅 ) ) ∧ 𝐺 ∈ ( Base ‘ ( PwSer₁ ‘ 𝑅 ) ) ) → ( coe₁ ‘ ( 𝐹 ∙ 𝐺 ) ) = ( 𝑘 ∈ ℕ₀ ↦ ( 𝑅 Σ_g ( 𝑥 ∈ ( 0 ... 𝑘 ) ↦ ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑥 ) · ( ( coe₁ ‘ 𝐺 ) ‘ ( 𝑘 − 𝑥 ) ) ) ) ) ) )
18	5 6 7 17	syl3an	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵 ) → ( coe₁ ‘ ( 𝐹 ∙ 𝐺 ) ) = ( 𝑘 ∈ ℕ₀ ↦ ( 𝑅 Σ_g ( 𝑥 ∈ ( 0 ... 𝑘 ) ↦ ( ( ( coe₁ ‘ 𝐹 ) ‘ 𝑥 ) · ( ( coe₁ ‘ 𝐺 ) ‘ ( 𝑘 − 𝑥 ) ) ) ) ) ) )