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 ˙ = P
coe1sclmul.u · ˙ = R
Assertion coe1sclmul R Ring X K Y B coe 1 A X ˙ Y = 0 × X · ˙ f coe 1 Y

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 coe1tmmul R Ring X K Y B coe 1 X P 0 mulGrp P var 1 R ˙ Y = x 0 if 0 x X · ˙ coe 1 Y x 0 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 fvoveq1d R Ring X K Y B coe 1 A X ˙ Y = coe 1 X P 0 mulGrp P var 1 R ˙ Y
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 R Ring X K Y B 0 × X · ˙ f coe 1 Y = x 0 X · ˙ coe 1 Y x
32 nn0ge0 x 0 0 x
33 32 iftrued x 0 if 0 x X · ˙ coe 1 Y x 0 0 R = X · ˙ coe 1 Y x 0
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 x 0 X · ˙ coe 1 Y x 0 = X · ˙ coe 1 Y x
38 33 37 eqtrd x 0 if 0 x X · ˙ coe 1 Y x 0 0 R = X · ˙ coe 1 Y x
39 38 mpteq2ia x 0 if 0 x X · ˙ coe 1 Y x 0 0 R = x 0 X · ˙ coe 1 Y x
40 31 39 eqtr4di R Ring X K Y B 0 × X · ˙ f coe 1 Y = x 0 if 0 x X · ˙ coe 1 Y x 0 0 R
41 17 20 40 3eqtr4d R Ring X K Y B coe 1 A X ˙ Y = 0 × X · ˙ f coe 1 Y