Metamath Proof Explorer


Theorem coe1sclmulfv

Description: A single coefficient of a polynomial multiplied on the left by a scalar. (Contributed by Stefan O'Rear, 1-Apr-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 coe1sclmulfv R Ring X K Y B 0 ˙ 0 coe 1 A X ˙ Y 0 ˙ = X · ˙ coe 1 Y 0 ˙

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 1 2 3 4 5 6 coe1sclmul R Ring X K Y B coe 1 A X ˙ Y = 0 × X · ˙ f coe 1 Y
8 7 3expb R Ring X K Y B coe 1 A X ˙ Y = 0 × X · ˙ f coe 1 Y
9 8 3adant3 R Ring X K Y B 0 ˙ 0 coe 1 A X ˙ Y = 0 × X · ˙ f coe 1 Y
10 9 fveq1d R Ring X K Y B 0 ˙ 0 coe 1 A X ˙ Y 0 ˙ = 0 × X · ˙ f coe 1 Y 0 ˙
11 simp3 R Ring X K Y B 0 ˙ 0 0 ˙ 0
12 nn0ex 0 V
13 12 a1i R Ring X K Y B 0 ˙ 0 0 V
14 simp2l R Ring X K Y B 0 ˙ 0 X K
15 simp2r R Ring X K Y B 0 ˙ 0 Y B
16 eqid coe 1 Y = coe 1 Y
17 eqid Base R = Base R
18 16 2 1 17 coe1f Y B coe 1 Y : 0 Base R
19 ffn coe 1 Y : 0 Base R coe 1 Y Fn 0
20 15 18 19 3syl R Ring X K Y B 0 ˙ 0 coe 1 Y Fn 0
21 eqidd R Ring X K Y B 0 ˙ 0 0 ˙ 0 coe 1 Y 0 ˙ = coe 1 Y 0 ˙
22 13 14 20 21 ofc1 R Ring X K Y B 0 ˙ 0 0 ˙ 0 0 × X · ˙ f coe 1 Y 0 ˙ = X · ˙ coe 1 Y 0 ˙
23 11 22 mpdan R Ring X K Y B 0 ˙ 0 0 × X · ˙ f coe 1 Y 0 ˙ = X · ˙ coe 1 Y 0 ˙
24 10 23 eqtrd R Ring X K Y B 0 ˙ 0 coe 1 A X ˙ Y 0 ˙ = X · ˙ coe 1 Y 0 ˙