Theorem coe1sclmul

Description: Coefficient vector of a polynomial multiplied on the left 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	coe1sclmul	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) → ( coe1 ‘ ( ( 𝐴 ‘ 𝑋 ) ∙ 𝑌 ) ) = ( ( ℕ0 × { 𝑋 } ) ∘f · ( coe1 ‘ 𝑌 ) ) )

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	coe1tmmul	⊢ ( ( 𝑅 ∈ 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	fvoveq1d	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) → ( coe1 ‘ ( ( 𝐴 ‘ 𝑋 ) ∙ 𝑌 ) ) = ( coe1 ‘ ( ( 𝑋 ( ·𝑠 ‘ 𝑃 ) ( 0 ( .g ‘ ( mulGrp ‘ 𝑃 ) ) ( var1 ‘ 𝑅 ) ) ) ∙ 𝑌 ) ) )
21		nn0ex	⊢ ℕ0 ∈ V
22	21	a1i	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) → ℕ0 ∈ V )
23		simpl2	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑥 ∈ ℕ0 ) → 𝑋 ∈ 𝐾 )
24		fvexd	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑥 ∈ ℕ0 ) → ( ( coe1 ‘ 𝑌 ) ‘ 𝑥 ) ∈ V )
25		fconstmpt	⊢ ( ℕ0 × { 𝑋 } ) = ( 𝑥 ∈ ℕ0 ↦ 𝑋 )
26	25	a1i	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) → ( ℕ0 × { 𝑋 } ) = ( 𝑥 ∈ ℕ0 ↦ 𝑋 ) )
27		eqid	⊢ ( coe1 ‘ 𝑌 ) = ( coe1 ‘ 𝑌 )
28	27 2 1 3	coe1f	⊢ ( 𝑌 ∈ 𝐵 → ( coe1 ‘ 𝑌 ) : ℕ0 ⟶ 𝐾 )
29	28	3ad2ant3	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) → ( coe1 ‘ 𝑌 ) : ℕ0 ⟶ 𝐾 )
30	29	feqmptd	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) → ( coe1 ‘ 𝑌 ) = ( 𝑥 ∈ ℕ0 ↦ ( ( coe1 ‘ 𝑌 ) ‘ 𝑥 ) ) )
31	22 23 24 26 30	offval2	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) → ( ( ℕ0 × { 𝑋 } ) ∘f · ( coe1 ‘ 𝑌 ) ) = ( 𝑥 ∈ ℕ0 ↦ ( 𝑋 · ( ( coe1 ‘ 𝑌 ) ‘ 𝑥 ) ) ) )
32		nn0ge0	⊢ ( 𝑥 ∈ ℕ0 → 0 ≤ 𝑥 )
33	32	iftrued	⊢ ( 𝑥 ∈ ℕ0 → if ( 0 ≤ 𝑥 , ( 𝑋 · ( ( coe1 ‘ 𝑌 ) ‘ ( 𝑥 − 0 ) ) ) , ( 0g ‘ 𝑅 ) ) = ( 𝑋 · ( ( coe1 ‘ 𝑌 ) ‘ ( 𝑥 − 0 ) ) ) )
34		nn0cn	⊢ ( 𝑥 ∈ ℕ0 → 𝑥 ∈ ℂ )
35	34	subid1d	⊢ ( 𝑥 ∈ ℕ0 → ( 𝑥 − 0 ) = 𝑥 )
36	35	fveq2d	⊢ ( 𝑥 ∈ ℕ0 → ( ( coe1 ‘ 𝑌 ) ‘ ( 𝑥 − 0 ) ) = ( ( coe1 ‘ 𝑌 ) ‘ 𝑥 ) )
37	36	oveq2d	⊢ ( 𝑥 ∈ ℕ0 → ( 𝑋 · ( ( coe1 ‘ 𝑌 ) ‘ ( 𝑥 − 0 ) ) ) = ( 𝑋 · ( ( coe1 ‘ 𝑌 ) ‘ 𝑥 ) ) )
38	33 37	eqtrd	⊢ ( 𝑥 ∈ ℕ0 → if ( 0 ≤ 𝑥 , ( 𝑋 · ( ( coe1 ‘ 𝑌 ) ‘ ( 𝑥 − 0 ) ) ) , ( 0g ‘ 𝑅 ) ) = ( 𝑋 · ( ( coe1 ‘ 𝑌 ) ‘ 𝑥 ) ) )
39	38	mpteq2ia	⊢ ( 𝑥 ∈ ℕ0 ↦ if ( 0 ≤ 𝑥 , ( 𝑋 · ( ( coe1 ‘ 𝑌 ) ‘ ( 𝑥 − 0 ) ) ) , ( 0g ‘ 𝑅 ) ) ) = ( 𝑥 ∈ ℕ0 ↦ ( 𝑋 · ( ( coe1 ‘ 𝑌 ) ‘ 𝑥 ) ) )
40	31 39	eqtr4di	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) → ( ( ℕ0 × { 𝑋 } ) ∘f · ( coe1 ‘ 𝑌 ) ) = ( 𝑥 ∈ ℕ0 ↦ if ( 0 ≤ 𝑥 , ( 𝑋 · ( ( coe1 ‘ 𝑌 ) ‘ ( 𝑥 − 0 ) ) ) , ( 0g ‘ 𝑅 ) ) ) )
41	17 20 40	3eqtr4d	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐾 ∧ 𝑌 ∈ 𝐵 ) → ( coe1 ‘ ( ( 𝐴 ‘ 𝑋 ) ∙ 𝑌 ) ) = ( ( ℕ0 × { 𝑋 } ) ∘f · ( coe1 ‘ 𝑌 ) ) )