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 = Poly 1 R
ply10s0.b B = Base P
ply10s0.m ˙ = P
ply10s0.e 0 ˙ = 0 R
Assertion ply10s0 R Ring M B 0 ˙ ˙ M = 0 P

Proof

Step Hyp Ref Expression
1 ply10s0.p P = Poly 1 R
2 ply10s0.b B = Base P
3 ply10s0.m ˙ = P
4 ply10s0.e 0 ˙ = 0 R
5 1 ply1sca R Ring R = Scalar P
6 5 adantr R Ring M B R = Scalar P
7 6 fveq2d R Ring M B 0 R = 0 Scalar P
8 4 7 syl5eq R Ring M B 0 ˙ = 0 Scalar P
9 8 oveq1d R Ring M B 0 ˙ ˙ M = 0 Scalar P ˙ M
10 1 ply1lmod R Ring P LMod
11 eqid Scalar P = Scalar P
12 eqid 0 Scalar P = 0 Scalar P
13 eqid 0 P = 0 P
14 2 11 3 12 13 lmod0vs P LMod M B 0 Scalar P ˙ M = 0 P
15 10 14 sylan R Ring M B 0 Scalar P ˙ M = 0 P
16 9 15 eqtrd R Ring M B 0 ˙ ˙ M = 0 P