Theorem coe1sclmul2

Description: Coefficient vector of a polynomial multiplied on the right by a scalar. (Contributed by Stefan O'Rear, 29-Mar-2015)

	Ref	Expression
Hypotheses	coe1sclmul.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	coe1sclmul.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
	coe1sclmul.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
	coe1sclmul.a	⊢ 𝐴 = ( algSc ‘ 𝑃 )
	coe1sclmul.t	⊢ ∙ = ( .r ‘ 𝑃 )
	coe1sclmul.u	⊢ · = ( .r ‘ 𝑅 )
Assertion	coe1sclmul2	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) → ( coe1 ‘ ( 𝑌 ∙ ( 𝐴 ‘ 𝑋 ) ) ) = ( ( coe1 ‘ 𝑌 ) ∘f · ( ℕ0 × { 𝑋 } ) ) )

Proof

Step	Hyp	Ref	Expression
1		coe1sclmul.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2		coe1sclmul.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
3		coe1sclmul.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
4		coe1sclmul.a	⊢ 𝐴 = ( algSc ‘ 𝑃 )
5		coe1sclmul.t	⊢ ∙ = ( .r ‘ 𝑃 )
6		coe1sclmul.u	⊢ · = ( .r ‘ 𝑅 )
7		eqid	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
8		eqid	⊢ ( var1 ‘ 𝑅 ) = ( var1 ‘ 𝑅 )
9		eqid	⊢ ( ·𝑠 ‘ 𝑃 ) = ( ·𝑠 ‘ 𝑃 )
10		eqid	⊢ ( mulGrp ‘ 𝑃 ) = ( mulGrp ‘ 𝑃 )
11		eqid	⊢ ( .g ‘ ( mulGrp ‘ 𝑃 ) ) = ( .g ‘ ( mulGrp ‘ 𝑃 ) )
12		simp3	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) → 𝑌 ∈ 𝐵 )
13		simp1	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) → 𝑅 ∈ Ring )
14		simp2	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) → 𝑋 ∈ 𝐾 )
15		0nn0	⊢ 0 ∈ ℕ0
16	15	a1i	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) → 0 ∈ ℕ0 )
17	7 3 1 8 9 10 11 2 5 6 12 13 14 16	coe1tmmul2	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) → ( coe1 ‘ ( 𝑌 ∙ ( 𝑋 ( ·𝑠 ‘ 𝑃 ) ( 0 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) ) = ( 𝑥 ∈ ℕ0 ↦ if ( 0 ≤ 𝑥 , ( ( ( coe1 ‘ 𝑌 ) ‘ ( 𝑥 − 0 ) ) · 𝑋 ) , ( 0g ‘ 𝑅 ) ) ) )
18	3 1 8 9 10 11 4	ply1scltm	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐾 ) → ( 𝐴 ‘ 𝑋 ) = ( 𝑋 ( ·𝑠 ‘ 𝑃 ) ( 0 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) )
19	18	3adant3	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) → ( 𝐴 ‘ 𝑋 ) = ( 𝑋 ( ·𝑠 ‘ 𝑃 ) ( 0 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) )
20	19	oveq2d	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑌 ∙ ( 𝐴 ‘ 𝑋 ) ) = ( 𝑌 ∙ ( 𝑋 ( ·𝑠 ‘ 𝑃 ) ( 0 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) )
21	20	fveq2d	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) → ( coe1 ‘ ( 𝑌 ∙ ( 𝐴 ‘ 𝑋 ) ) ) = ( coe1 ‘ ( 𝑌 ∙ ( 𝑋 ( ·𝑠 ‘ 𝑃 ) ( 0 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ) ) )
22		nn0ex	⊢ ℕ0 ∈ V
23	22	a1i	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) → ℕ0 ∈ V )
24		fvexd	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑥 ∈ ℕ0 ) → ( ( coe1 ‘ 𝑌 ) ‘ 𝑥 ) ∈ V )
25		simpl2	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑥 ∈ ℕ0 ) → 𝑋 ∈ 𝐾 )
26		eqid	⊢ ( coe1 ‘ 𝑌 ) = ( coe1 ‘ 𝑌 )
27	26 2 1 3	coe1f	⊢ ( 𝑌 ∈ 𝐵 → ( coe1 ‘ 𝑌 ) : ℕ0 ⟶ 𝐾 )
28	27	feqmptd	⊢ ( 𝑌 ∈ 𝐵 → ( coe1 ‘ 𝑌 ) = ( 𝑥 ∈ ℕ0 ↦ ( ( coe1 ‘ 𝑌 ) ‘ 𝑥 ) ) )
29	28	3ad2ant3	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) → ( coe1 ‘ 𝑌 ) = ( 𝑥 ∈ ℕ0 ↦ ( ( coe1 ‘ 𝑌 ) ‘ 𝑥 ) ) )
30		fconstmpt	⊢ ( ℕ0 × { 𝑋 } ) = ( 𝑥 ∈ ℕ0 ↦ 𝑋 )
31	30	a1i	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) → ( ℕ0 × { 𝑋 } ) = ( 𝑥 ∈ ℕ0 ↦ 𝑋 ) )
32	23 24 25 29 31	offval2	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) → ( ( coe1 ‘ 𝑌 ) ∘f · ( ℕ0 × { 𝑋 } ) ) = ( 𝑥 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝑌 ) ‘ 𝑥 ) · 𝑋 ) ) )
33		nn0ge0	⊢ ( 𝑥 ∈ ℕ0 → 0 ≤ 𝑥 )
34	33	iftrued	⊢ ( 𝑥 ∈ ℕ0 → if ( 0 ≤ 𝑥 , ( ( ( coe1 ‘ 𝑌 ) ‘ ( 𝑥 − 0 ) ) · 𝑋 ) , ( 0g ‘ 𝑅 ) ) = ( ( ( coe1 ‘ 𝑌 ) ‘ ( 𝑥 − 0 ) ) · 𝑋 ) )
35		nn0cn	⊢ ( 𝑥 ∈ ℕ0 → 𝑥 ∈ ℂ )
36	35	subid1d	⊢ ( 𝑥 ∈ ℕ0 → ( 𝑥 − 0 ) = 𝑥 )
37	36	fveq2d	⊢ ( 𝑥 ∈ ℕ0 → ( ( coe1 ‘ 𝑌 ) ‘ ( 𝑥 − 0 ) ) = ( ( coe1 ‘ 𝑌 ) ‘ 𝑥 ) )
38	37	oveq1d	⊢ ( 𝑥 ∈ ℕ0 → ( ( ( coe1 ‘ 𝑌 ) ‘ ( 𝑥 − 0 ) ) · 𝑋 ) = ( ( ( coe1 ‘ 𝑌 ) ‘ 𝑥 ) · 𝑋 ) )
39	34 38	eqtrd	⊢ ( 𝑥 ∈ ℕ0 → if ( 0 ≤ 𝑥 , ( ( ( coe1 ‘ 𝑌 ) ‘ ( 𝑥 − 0 ) ) · 𝑋 ) , ( 0g ‘ 𝑅 ) ) = ( ( ( coe1 ‘ 𝑌 ) ‘ 𝑥 ) · 𝑋 ) )
40	39	mpteq2ia	⊢ ( 𝑥 ∈ ℕ0 ↦ if ( 0 ≤ 𝑥 , ( ( ( coe1 ‘ 𝑌 ) ‘ ( 𝑥 − 0 ) ) · 𝑋 ) , ( 0g ‘ 𝑅 ) ) ) = ( 𝑥 ∈ ℕ0 ↦ ( ( ( coe1 ‘ 𝑌 ) ‘ 𝑥 ) · 𝑋 ) )
41	32 40	eqtr4di	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) → ( ( coe1 ‘ 𝑌 ) ∘f · ( ℕ0 × { 𝑋 } ) ) = ( 𝑥 ∈ ℕ0 ↦ if ( 0 ≤ 𝑥 , ( ( ( coe1 ‘ 𝑌 ) ‘ ( 𝑥 − 0 ) ) · 𝑋 ) , ( 0g ‘ 𝑅 ) ) ) )
42	17 21 41	3eqtr4d	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) → ( coe1 ‘ ( 𝑌 ∙ ( 𝐴 ‘ 𝑋 ) ) ) = ( ( coe1 ‘ 𝑌 ) ∘f · ( ℕ0 × { 𝑋 } ) ) )