coe1pwmul

Description: Coefficient vector of a polynomial multiplied on the left by a variable power. (Contributed by Stefan O'Rear, 1-Apr-2015)

	Ref	Expression
Hypotheses	coe1pwmul.z	⊢ 0 = ( 0_g ‘ 𝑅 )
	coe1pwmul.p	⊢ 𝑃 = ( Poly₁ ‘ 𝑅 )
	coe1pwmul.x	⊢ 𝑋 = ( var₁ ‘ 𝑅 )
	coe1pwmul.n	⊢ 𝑁 = ( mulGrp ‘ 𝑃 )
	coe1pwmul.e	⊢ ↑ = ( ._g ‘ 𝑁 )
	coe1pwmul.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
	coe1pwmul.t	⊢ · = ( ._r ‘ 𝑃 )
	coe1pwmul.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
	coe1pwmul.a	⊢ ( 𝜑 → 𝐴 ∈ 𝐵 )
	coe1pwmul.d	⊢ ( 𝜑 → 𝐷 ∈ ℕ₀ )
Assertion	coe1pwmul	⊢ ( 𝜑 → ( coe₁ ‘ ( ( 𝐷 ↑ 𝑋 ) · 𝐴 ) ) = ( 𝑥 ∈ ℕ₀ ↦ if ( 𝐷 ≤ 𝑥 , ( ( coe₁ ‘ 𝐴 ) ‘ ( 𝑥 − 𝐷 ) ) , 0 ) ) )

Proof

Step	Hyp	Ref	Expression
1		coe1pwmul.z	⊢ 0 = ( 0_g ‘ 𝑅 )
2		coe1pwmul.p	⊢ 𝑃 = ( Poly₁ ‘ 𝑅 )
3		coe1pwmul.x	⊢ 𝑋 = ( var₁ ‘ 𝑅 )
4		coe1pwmul.n	⊢ 𝑁 = ( mulGrp ‘ 𝑃 )
5		coe1pwmul.e	⊢ ↑ = ( ._g ‘ 𝑁 )
6		coe1pwmul.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
7		coe1pwmul.t	⊢ · = ( ._r ‘ 𝑃 )
8		coe1pwmul.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
9		coe1pwmul.a	⊢ ( 𝜑 → 𝐴 ∈ 𝐵 )
10		coe1pwmul.d	⊢ ( 𝜑 → 𝐷 ∈ ℕ₀ )
11		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
12		eqid	⊢ ( ·_𝑠 ‘ 𝑃 ) = ( ·_𝑠 ‘ 𝑃 )
13		eqid	⊢ ( ._r ‘ 𝑅 ) = ( ._r ‘ 𝑅 )
14		eqid	⊢ ( 1_r ‘ 𝑅 ) = ( 1_r ‘ 𝑅 )
15	11 14	ringidcl	⊢ ( 𝑅 ∈ Ring → ( 1_r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
16	8 15	syl	⊢ ( 𝜑 → ( 1_r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
17	1 11 2 3 12 4 5 6 7 13 9 8 16 10	coe1tmmul	⊢ ( 𝜑 → ( coe₁ ‘ ( ( ( 1_r ‘ 𝑅 ) ( ·_𝑠 ‘ 𝑃 ) ( 𝐷 ↑ 𝑋 ) ) · 𝐴 ) ) = ( 𝑥 ∈ ℕ₀ ↦ if ( 𝐷 ≤ 𝑥 , ( ( 1_r ‘ 𝑅 ) ( ._r ‘ 𝑅 ) ( ( coe₁ ‘ 𝐴 ) ‘ ( 𝑥 − 𝐷 ) ) ) , 0 ) ) )
18	2	ply1sca	⊢ ( 𝑅 ∈ Ring → 𝑅 = ( Scalar ‘ 𝑃 ) )
19	8 18	syl	⊢ ( 𝜑 → 𝑅 = ( Scalar ‘ 𝑃 ) )
20	19	fveq2d	⊢ ( 𝜑 → ( 1_r ‘ 𝑅 ) = ( 1_r ‘ ( Scalar ‘ 𝑃 ) ) )
21	20	oveq1d	⊢ ( 𝜑 → ( ( 1_r ‘ 𝑅 ) ( ·_𝑠 ‘ 𝑃 ) ( 𝐷 ↑ 𝑋 ) ) = ( ( 1_r ‘ ( Scalar ‘ 𝑃 ) ) ( ·_𝑠 ‘ 𝑃 ) ( 𝐷 ↑ 𝑋 ) ) )
22	2	ply1lmod	⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ LMod )
23	8 22	syl	⊢ ( 𝜑 → 𝑃 ∈ LMod )
24	4 6	mgpbas	⊢ 𝐵 = ( Base ‘ 𝑁 )
25	2	ply1ring	⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ Ring )
26	4	ringmgp	⊢ ( 𝑃 ∈ Ring → 𝑁 ∈ Mnd )
27	8 25 26	3syl	⊢ ( 𝜑 → 𝑁 ∈ Mnd )
28	3 2 6	vr1cl	⊢ ( 𝑅 ∈ Ring → 𝑋 ∈ 𝐵 )
29	8 28	syl	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
30	24 5 27 10 29	mulgnn0cld	⊢ ( 𝜑 → ( 𝐷 ↑ 𝑋 ) ∈ 𝐵 )
31		eqid	⊢ ( Scalar ‘ 𝑃 ) = ( Scalar ‘ 𝑃 )
32		eqid	⊢ ( 1_r ‘ ( Scalar ‘ 𝑃 ) ) = ( 1_r ‘ ( Scalar ‘ 𝑃 ) )
33	6 31 12 32	lmodvs1	⊢ ( ( 𝑃 ∈ LMod ∧ ( 𝐷 ↑ 𝑋 ) ∈ 𝐵 ) → ( ( 1_r ‘ ( Scalar ‘ 𝑃 ) ) ( ·_𝑠 ‘ 𝑃 ) ( 𝐷 ↑ 𝑋 ) ) = ( 𝐷 ↑ 𝑋 ) )
34	23 30 33	syl2anc	⊢ ( 𝜑 → ( ( 1_r ‘ ( Scalar ‘ 𝑃 ) ) ( ·_𝑠 ‘ 𝑃 ) ( 𝐷 ↑ 𝑋 ) ) = ( 𝐷 ↑ 𝑋 ) )
35	21 34	eqtrd	⊢ ( 𝜑 → ( ( 1_r ‘ 𝑅 ) ( ·_𝑠 ‘ 𝑃 ) ( 𝐷 ↑ 𝑋 ) ) = ( 𝐷 ↑ 𝑋 ) )
36	35	fvoveq1d	⊢ ( 𝜑 → ( coe₁ ‘ ( ( ( 1_r ‘ 𝑅 ) ( ·_𝑠 ‘ 𝑃 ) ( 𝐷 ↑ 𝑋 ) ) · 𝐴 ) ) = ( coe₁ ‘ ( ( 𝐷 ↑ 𝑋 ) · 𝐴 ) ) )
37	8	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℕ₀ ) ∧ 𝐷 ≤ 𝑥 ) → 𝑅 ∈ Ring )
38		eqid	⊢ ( coe₁ ‘ 𝐴 ) = ( coe₁ ‘ 𝐴 )
39	38 6 2 11	coe1f	⊢ ( 𝐴 ∈ 𝐵 → ( coe₁ ‘ 𝐴 ) : ℕ₀ ⟶ ( Base ‘ 𝑅 ) )
40	9 39	syl	⊢ ( 𝜑 → ( coe₁ ‘ 𝐴 ) : ℕ₀ ⟶ ( Base ‘ 𝑅 ) )
41	40	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℕ₀ ) ∧ 𝐷 ≤ 𝑥 ) → ( coe₁ ‘ 𝐴 ) : ℕ₀ ⟶ ( Base ‘ 𝑅 ) )
42	10	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℕ₀ ) ∧ 𝐷 ≤ 𝑥 ) → 𝐷 ∈ ℕ₀ )
43		simplr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℕ₀ ) ∧ 𝐷 ≤ 𝑥 ) → 𝑥 ∈ ℕ₀ )
44		simpr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℕ₀ ) ∧ 𝐷 ≤ 𝑥 ) → 𝐷 ≤ 𝑥 )
45		nn0sub2	⊢ ( ( 𝐷 ∈ ℕ₀ ∧ 𝑥 ∈ ℕ₀ ∧ 𝐷 ≤ 𝑥 ) → ( 𝑥 − 𝐷 ) ∈ ℕ₀ )
46	42 43 44 45	syl3anc	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℕ₀ ) ∧ 𝐷 ≤ 𝑥 ) → ( 𝑥 − 𝐷 ) ∈ ℕ₀ )
47	41 46	ffvelcdmd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℕ₀ ) ∧ 𝐷 ≤ 𝑥 ) → ( ( coe₁ ‘ 𝐴 ) ‘ ( 𝑥 − 𝐷 ) ) ∈ ( Base ‘ 𝑅 ) )
48	11 13 14	ringlidm	⊢ ( ( 𝑅 ∈ Ring ∧ ( ( coe₁ ‘ 𝐴 ) ‘ ( 𝑥 − 𝐷 ) ) ∈ ( Base ‘ 𝑅 ) ) → ( ( 1_r ‘ 𝑅 ) ( ._r ‘ 𝑅 ) ( ( coe₁ ‘ 𝐴 ) ‘ ( 𝑥 − 𝐷 ) ) ) = ( ( coe₁ ‘ 𝐴 ) ‘ ( 𝑥 − 𝐷 ) ) )
49	37 47 48	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℕ₀ ) ∧ 𝐷 ≤ 𝑥 ) → ( ( 1_r ‘ 𝑅 ) ( ._r ‘ 𝑅 ) ( ( coe₁ ‘ 𝐴 ) ‘ ( 𝑥 − 𝐷 ) ) ) = ( ( coe₁ ‘ 𝐴 ) ‘ ( 𝑥 − 𝐷 ) ) )
50	49	ifeq1da	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℕ₀ ) → if ( 𝐷 ≤ 𝑥 , ( ( 1_r ‘ 𝑅 ) ( ._r ‘ 𝑅 ) ( ( coe₁ ‘ 𝐴 ) ‘ ( 𝑥 − 𝐷 ) ) ) , 0 ) = if ( 𝐷 ≤ 𝑥 , ( ( coe₁ ‘ 𝐴 ) ‘ ( 𝑥 − 𝐷 ) ) , 0 ) )
51	50	mpteq2dva	⊢ ( 𝜑 → ( 𝑥 ∈ ℕ₀ ↦ if ( 𝐷 ≤ 𝑥 , ( ( 1_r ‘ 𝑅 ) ( ._r ‘ 𝑅 ) ( ( coe₁ ‘ 𝐴 ) ‘ ( 𝑥 − 𝐷 ) ) ) , 0 ) ) = ( 𝑥 ∈ ℕ₀ ↦ if ( 𝐷 ≤ 𝑥 , ( ( coe₁ ‘ 𝐴 ) ‘ ( 𝑥 − 𝐷 ) ) , 0 ) ) )
52	17 36 51	3eqtr3d	⊢ ( 𝜑 → ( coe₁ ‘ ( ( 𝐷 ↑ 𝑋 ) · 𝐴 ) ) = ( 𝑥 ∈ ℕ₀ ↦ if ( 𝐷 ≤ 𝑥 , ( ( coe₁ ‘ 𝐴 ) ‘ ( 𝑥 − 𝐷 ) ) , 0 ) ) )

Metamath Proof Explorer

Theorem coe1pwmul

Proof