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	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	ply10s0.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
	ply10s0.m	⊢ ∗ = ( ·𝑠 ‘ 𝑃 )
	ply10s0.e	⊢ 0 = ( 0g ‘ 𝑅 )
Assertion	ply10s0	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( 0 ∗ 𝑀 ) = ( 0g ‘ 𝑃 ) )

Proof

Step	Hyp	Ref	Expression
1		ply10s0.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2		ply10s0.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
3		ply10s0.m	⊢ ∗ = ( ·𝑠 ‘ 𝑃 )
4		ply10s0.e	⊢ 0 = ( 0g ‘ 𝑅 )
5	1	ply1sca	⊢ ( 𝑅 ∈ Ring → 𝑅 = ( Scalar ‘ 𝑃 ) )
6	5	adantr	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → 𝑅 = ( Scalar ‘ 𝑃 ) )
7	6	fveq2d	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( 0g ‘ 𝑅 ) = ( 0g ‘ ( Scalar ‘ 𝑃 ) ) )
8	4 7	syl5eq	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → 0 = ( 0g ‘ ( Scalar ‘ 𝑃 ) ) )
9	8	oveq1d	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( 0 ∗ 𝑀 ) = ( ( 0g ‘ ( Scalar ‘ 𝑃 ) ) ∗ 𝑀 ) )
10	1	ply1lmod	⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ LMod )
11		eqid	⊢ ( Scalar ‘ 𝑃 ) = ( Scalar ‘ 𝑃 )
12		eqid	⊢ ( 0g ‘ ( Scalar ‘ 𝑃 ) ) = ( 0g ‘ ( Scalar ‘ 𝑃 ) )
13		eqid	⊢ ( 0g ‘ 𝑃 ) = ( 0g ‘ 𝑃 )
14	2 11 3 12 13	lmod0vs	⊢ ( ( 𝑃 ∈ LMod ∧ 𝑀 ∈ 𝐵 ) → ( ( 0g ‘ ( Scalar ‘ 𝑃 ) ) ∗ 𝑀 ) = ( 0g ‘ 𝑃 ) )
15	10 14	sylan	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( ( 0g ‘ ( Scalar ‘ 𝑃 ) ) ∗ 𝑀 ) = ( 0g ‘ 𝑃 ) )
16	9 15	eqtrd	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵 ) → ( 0 ∗ 𝑀 ) = ( 0g ‘ 𝑃 ) )