Metamath Proof Explorer


Theorem mplvscaval

Description: The scalar multiplication operation on multivariate polynomials. (Contributed by Mario Carneiro, 9-Jan-2015)

Ref Expression
Hypotheses mplvsca.p P = I mPoly R
mplvsca.n ˙ = P
mplvsca.k K = Base R
mplvsca.b B = Base P
mplvsca.m · ˙ = R
mplvsca.d D = h 0 I | h -1 Fin
mplvsca.x φ X K
mplvsca.f φ F B
mplvscaval.y φ Y D
Assertion mplvscaval φ X ˙ F Y = X · ˙ F Y

Proof

Step Hyp Ref Expression
1 mplvsca.p P = I mPoly R
2 mplvsca.n ˙ = P
3 mplvsca.k K = Base R
4 mplvsca.b B = Base P
5 mplvsca.m · ˙ = R
6 mplvsca.d D = h 0 I | h -1 Fin
7 mplvsca.x φ X K
8 mplvsca.f φ F B
9 mplvscaval.y φ Y D
10 1 2 3 4 5 6 7 8 mplvsca φ X ˙ F = D × X · ˙ f F
11 10 fveq1d φ X ˙ F Y = D × X · ˙ f F Y
12 ovex 0 I V
13 6 12 rabex2 D V
14 13 a1i φ D V
15 eqid Base R = Base R
16 1 15 4 6 8 mplelf φ F : D Base R
17 16 ffnd φ F Fn D
18 eqidd φ Y D F Y = F Y
19 14 7 17 18 ofc1 φ Y D D × X · ˙ f F Y = X · ˙ F Y
20 9 19 mpdan φ D × X · ˙ f F Y = X · ˙ F Y
21 11 20 eqtrd φ X ˙ F Y = X · ˙ F Y