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 ⊢ 𝑃 = ( 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 eqtrid ⊢ ( ( 𝑅 ∈ 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 ‘ 𝑃 ) )