This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 = ( Poly1 ` R )
ply10s0.b 
|- B = ( Base ` P )
ply10s0.m 
|- .* = ( .s ` P )
ply10s0.e 
|- .0. = ( 0g ` R )
Assertion ply10s0 
|- ( ( R e. Ring /\ M e. B ) -> ( .0. .* M ) = ( 0g ` P ) )

Proof

Step Hyp Ref Expression
1 ply10s0.p 
 |-  P = ( Poly1 ` R )
2 ply10s0.b 
 |-  B = ( Base ` P )
3 ply10s0.m 
 |-  .* = ( .s ` P )
4 ply10s0.e 
 |-  .0. = ( 0g ` R )
5 1 ply1sca 
 |-  ( R e. Ring -> R = ( Scalar ` P ) )
6 5 adantr 
 |-  ( ( R e. Ring /\ M e. B ) -> R = ( Scalar ` P ) )
7 6 fveq2d 
 |-  ( ( R e. Ring /\ M e. B ) -> ( 0g ` R ) = ( 0g ` ( Scalar ` P ) ) )
8 4 7 eqtrid 
 |-  ( ( R e. Ring /\ M e. B ) -> .0. = ( 0g ` ( Scalar ` P ) ) )
9 8 oveq1d 
 |-  ( ( R e. Ring /\ M e. B ) -> ( .0. .* M ) = ( ( 0g ` ( Scalar ` P ) ) .* M ) )
10 1 ply1lmod 
 |-  ( R e. Ring -> P e. LMod )
11 eqid 
 |-  ( Scalar ` P ) = ( Scalar ` P )
12 eqid 
 |-  ( 0g ` ( Scalar ` P ) ) = ( 0g ` ( Scalar ` P ) )
13 eqid 
 |-  ( 0g ` P ) = ( 0g ` P )
14 2 11 3 12 13 lmod0vs 
 |-  ( ( P e. LMod /\ M e. B ) -> ( ( 0g ` ( Scalar ` P ) ) .* M ) = ( 0g ` P ) )
15 10 14 sylan 
 |-  ( ( R e. Ring /\ M e. B ) -> ( ( 0g ` ( Scalar ` P ) ) .* M ) = ( 0g ` P ) )
16 9 15 eqtrd 
 |-  ( ( R e. Ring /\ M e. B ) -> ( .0. .* M ) = ( 0g ` P ) )