Metamath Proof Explorer


Theorem evl1vsd

Description: Polynomial evaluation builder for scalar multiplication of polynomials. (Contributed by Mario Carneiro, 4-Jul-2015)

Ref Expression
Hypotheses evl1addd.q O=eval1R
evl1addd.p P=Poly1R
evl1addd.b B=BaseR
evl1addd.u U=BaseP
evl1addd.1 φRCRing
evl1addd.2 φYB
evl1addd.3 φMUOMY=V
evl1vsd.4 φNB
evl1vsd.s ˙=P
evl1vsd.t ·˙=R
Assertion evl1vsd φN˙MUON˙MY=N·˙V

Proof

Step Hyp Ref Expression
1 evl1addd.q O=eval1R
2 evl1addd.p P=Poly1R
3 evl1addd.b B=BaseR
4 evl1addd.u U=BaseP
5 evl1addd.1 φRCRing
6 evl1addd.2 φYB
7 evl1addd.3 φMUOMY=V
8 evl1vsd.4 φNB
9 evl1vsd.s ˙=P
10 evl1vsd.t ·˙=R
11 eqid algScP=algScP
12 1 2 3 11 4 5 8 6 evl1scad φalgScPNUOalgScPNY=N
13 eqid P=P
14 1 2 3 4 5 6 12 7 13 10 evl1muld φalgScPNPMUOalgScPNPMY=N·˙V
15 2 ply1assa RCRingPAssAlg
16 5 15 syl φPAssAlg
17 2 ply1sca RCRingR=ScalarP
18 5 17 syl φR=ScalarP
19 18 fveq2d φBaseR=BaseScalarP
20 3 19 eqtrid φB=BaseScalarP
21 8 20 eleqtrd φNBaseScalarP
22 7 simpld φMU
23 eqid ScalarP=ScalarP
24 eqid BaseScalarP=BaseScalarP
25 11 23 24 4 13 9 asclmul1 PAssAlgNBaseScalarPMUalgScPNPM=N˙M
26 16 21 22 25 syl3anc φalgScPNPM=N˙M
27 26 eleq1d φalgScPNPMUN˙MU
28 26 fveq2d φOalgScPNPM=ON˙M
29 28 fveq1d φOalgScPNPMY=ON˙MY
30 29 eqeq1d φOalgScPNPMY=N·˙VON˙MY=N·˙V
31 27 30 anbi12d φalgScPNPMUOalgScPNPMY=N·˙VN˙MUON˙MY=N·˙V
32 14 31 mpbid φN˙MUON˙MY=N·˙V