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

Metamath Proof Explorer

Theorem mplascl0

Description: The zero scalar as a polynomial. (Contributed by SN, 23-Nov-2024)

Ref Expression
Hypotheses mplascl0.w ⊢ 𝑊 = ( 𝐼 mPoly 𝑅 )
mplascl0.a ⊢ 𝐴 = ( algSc ‘ 𝑊 )
mplascl0.o ⊢ 𝑂 = ( 0g ‘ 𝑅 )
mplascl0.0 ⊢ 0 = ( 0g ‘ 𝑊 )
mplascl0.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
mplascl0.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
Assertion mplascl0 ( 𝜑 → ( 𝐴 ‘ 𝑂 ) = 0 )

Proof

Step Hyp Ref Expression
1 mplascl0.w ⊢ 𝑊 = ( 𝐼 mPoly 𝑅 )
2 mplascl0.a ⊢ 𝐴 = ( algSc ‘ 𝑊 )
3 mplascl0.o ⊢ 𝑂 = ( 0g ‘ 𝑅 )
4 mplascl0.0 ⊢ 0 = ( 0g ‘ 𝑊 )
5 mplascl0.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
6 mplascl0.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
7 1 5 6 mplsca ⊢ ( 𝜑 → 𝑅 = ( Scalar ‘ 𝑊 ) )
8 7 fveq2d ⊢ ( 𝜑 → ( 0g ‘ 𝑅 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
9 3 8 eqtrid ⊢ ( 𝜑 → 𝑂 = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
10 9 fveq2d ⊢ ( 𝜑 → ( 𝐴 ‘ 𝑂 ) = ( 𝐴 ‘ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) )
11 eqid ⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
12 1 5 6 mpllmodd ⊢ ( 𝜑 → 𝑊 ∈ LMod )
13 1 5 6 mplringd ⊢ ( 𝜑 → 𝑊 ∈ Ring )
14 2 11 12 13 ascl0 ⊢ ( 𝜑 → ( 𝐴 ‘ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) = ( 0g ‘ 𝑊 ) )
15 10 14 eqtrd ⊢ ( 𝜑 → ( 𝐴 ‘ 𝑂 ) = ( 0g ‘ 𝑊 ) )
16 15 4 eqtr4di ⊢ ( 𝜑 → ( 𝐴 ‘ 𝑂 ) = 0 )