# Metamath Proof Explorer

## 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 $⊢ P = Poly 1 ⁡ R$
coe1sclmul.b $⊢ B = Base P$
coe1sclmul.k $⊢ K = Base R$
coe1sclmul.a $⊢ A = algSc ⁡ P$
coe1sclmul.t
coe1sclmul.u
Assertion coe1sclmul

### Proof

Step Hyp Ref Expression
1 coe1sclmul.p $⊢ P = Poly 1 ⁡ R$
2 coe1sclmul.b $⊢ B = Base P$
3 coe1sclmul.k $⊢ K = Base R$
4 coe1sclmul.a $⊢ A = algSc ⁡ P$
5 coe1sclmul.t
6 coe1sclmul.u
7 eqid $⊢ 0 R = 0 R$
8 eqid $⊢ var 1 ⁡ R = var 1 ⁡ R$
9 eqid $⊢ ⋅ P = ⋅ P$
10 eqid $⊢ mulGrp P = mulGrp P$
11 eqid $⊢ ⋅ mulGrp P = ⋅ mulGrp P$
12 simp3 $⊢ R ∈ Ring ∧ X ∈ K ∧ Y ∈ B → Y ∈ B$
13 simp1 $⊢ R ∈ Ring ∧ X ∈ K ∧ Y ∈ B → R ∈ Ring$
14 simp2 $⊢ R ∈ Ring ∧ X ∈ K ∧ Y ∈ B → X ∈ K$
15 0nn0 $⊢ 0 ∈ ℕ 0$
16 15 a1i $⊢ R ∈ Ring ∧ X ∈ K ∧ Y ∈ B → 0 ∈ ℕ 0$
17 7 3 1 8 9 10 11 2 5 6 12 13 14 16 coe1tmmul
18 3 1 8 9 10 11 4 ply1scltm $⊢ R ∈ Ring ∧ X ∈ K → A ⁡ X = X ⋅ P 0 ⋅ mulGrp P var 1 ⁡ R$
19 18 3adant3 $⊢ R ∈ Ring ∧ X ∈ K ∧ Y ∈ B → A ⁡ X = X ⋅ P 0 ⋅ mulGrp P var 1 ⁡ R$
20 19 fvoveq1d
21 nn0ex $⊢ ℕ 0 ∈ V$
22 21 a1i $⊢ R ∈ Ring ∧ X ∈ K ∧ Y ∈ B → ℕ 0 ∈ V$
23 simpl2 $⊢ R ∈ Ring ∧ X ∈ K ∧ Y ∈ B ∧ x ∈ ℕ 0 → X ∈ K$
24 fvexd $⊢ R ∈ Ring ∧ X ∈ K ∧ Y ∈ B ∧ x ∈ ℕ 0 → coe 1 ⁡ Y ⁡ x ∈ V$
25 fconstmpt $⊢ ℕ 0 × X = x ∈ ℕ 0 ⟼ X$
26 25 a1i $⊢ R ∈ Ring ∧ X ∈ K ∧ Y ∈ B → ℕ 0 × X = x ∈ ℕ 0 ⟼ X$
27 eqid $⊢ coe 1 ⁡ Y = coe 1 ⁡ Y$
28 27 2 1 3 coe1f $⊢ Y ∈ B → coe 1 ⁡ Y : ℕ 0 ⟶ K$
29 28 3ad2ant3 $⊢ R ∈ Ring ∧ X ∈ K ∧ Y ∈ B → coe 1 ⁡ Y : ℕ 0 ⟶ K$
30 29 feqmptd $⊢ R ∈ Ring ∧ X ∈ K ∧ Y ∈ B → coe 1 ⁡ Y = x ∈ ℕ 0 ⟼ coe 1 ⁡ Y ⁡ x$
31 22 23 24 26 30 offval2
32 nn0ge0 $⊢ x ∈ ℕ 0 → 0 ≤ x$
33 32 iftrued
34 nn0cn $⊢ x ∈ ℕ 0 → x ∈ ℂ$
35 34 subid1d $⊢ x ∈ ℕ 0 → x − 0 = x$
36 35 fveq2d $⊢ x ∈ ℕ 0 → coe 1 ⁡ Y ⁡ x − 0 = coe 1 ⁡ Y ⁡ x$
37 36 oveq2d
38 33 37 eqtrd
39 38 mpteq2ia
40 31 39 eqtr4di
41 17 20 40 3eqtr4d