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 ) )