Metamath Proof Explorer


Theorem ply10s0

Description: Zero times a univariate polynomial is the zero polynomial ( lmod0vs analog.) (Contributed by AV, 2-Dec-2019)

Ref Expression
Hypotheses ply10s0.p P=Poly1R
ply10s0.b B=BaseP
ply10s0.m ˙=P
ply10s0.e 0˙=0R
Assertion ply10s0 RRingMB0˙˙M=0P

Proof

Step Hyp Ref Expression
1 ply10s0.p P=Poly1R
2 ply10s0.b B=BaseP
3 ply10s0.m ˙=P
4 ply10s0.e 0˙=0R
5 1 ply1sca RRingR=ScalarP
6 5 adantr RRingMBR=ScalarP
7 6 fveq2d RRingMB0R=0ScalarP
8 4 7 eqtrid RRingMB0˙=0ScalarP
9 8 oveq1d RRingMB0˙˙M=0ScalarP˙M
10 1 ply1lmod RRingPLMod
11 eqid ScalarP=ScalarP
12 eqid 0ScalarP=0ScalarP
13 eqid 0P=0P
14 2 11 3 12 13 lmod0vs PLModMB0ScalarP˙M=0P
15 10 14 sylan RRingMB0ScalarP˙M=0P
16 9 15 eqtrd RRingMB0˙˙M=0P