Metamath Proof Explorer


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 P = Poly 1 R
coe1sclmul.b B = Base P
coe1sclmul.k K = Base R
coe1sclmul.a A = algSc P
coe1sclmul.t ˙ = P
coe1sclmul.u · ˙ = R
Assertion coe1sclmul2 R Ring X K Y B coe 1 Y ˙ A X = coe 1 Y · ˙ f 0 × X

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 ˙ = P
6 coe1sclmul.u · ˙ = R
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 coe1tmmul2 R Ring X K Y B coe 1 Y ˙ X P 0 mulGrp P var 1 R = x 0 if 0 x coe 1 Y x 0 · ˙ X 0 R
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 oveq2d R Ring X K Y B Y ˙ A X = Y ˙ X P 0 mulGrp P var 1 R
21 20 fveq2d R Ring X K Y B coe 1 Y ˙ A X = coe 1 Y ˙ X P 0 mulGrp P var 1 R
22 nn0ex 0 V
23 22 a1i R Ring X K Y B 0 V
24 fvexd R Ring X K Y B x 0 coe 1 Y x V
25 simpl2 R Ring X K Y B x 0 X K
26 eqid coe 1 Y = coe 1 Y
27 26 2 1 3 coe1f Y B coe 1 Y : 0 K
28 27 feqmptd Y B coe 1 Y = x 0 coe 1 Y x
29 28 3ad2ant3 R Ring X K Y B coe 1 Y = x 0 coe 1 Y x
30 fconstmpt 0 × X = x 0 X
31 30 a1i R Ring X K Y B 0 × X = x 0 X
32 23 24 25 29 31 offval2 R Ring X K Y B coe 1 Y · ˙ f 0 × X = x 0 coe 1 Y x · ˙ X
33 nn0ge0 x 0 0 x
34 33 iftrued x 0 if 0 x coe 1 Y x 0 · ˙ X 0 R = coe 1 Y x 0 · ˙ X
35 nn0cn x 0 x
36 35 subid1d x 0 x 0 = x
37 36 fveq2d x 0 coe 1 Y x 0 = coe 1 Y x
38 37 oveq1d x 0 coe 1 Y x 0 · ˙ X = coe 1 Y x · ˙ X
39 34 38 eqtrd x 0 if 0 x coe 1 Y x 0 · ˙ X 0 R = coe 1 Y x · ˙ X
40 39 mpteq2ia x 0 if 0 x coe 1 Y x 0 · ˙ X 0 R = x 0 coe 1 Y x · ˙ X
41 32 40 eqtr4di R Ring X K Y B coe 1 Y · ˙ f 0 × X = x 0 if 0 x coe 1 Y x 0 · ˙ X 0 R
42 17 21 41 3eqtr4d R Ring X K Y B coe 1 Y ˙ A X = coe 1 Y · ˙ f 0 × X