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 ⊢ W = I mPoly R
mplascl0.a ⊢ A = algSc ⁡ W
mplascl0.o ⊢ O = 0 R
mplascl0.0 ⊢ 0 ˙ = 0 W
mplascl0.i ⊢ φ → I ∈ V
mplascl0.r ⊢ φ → R ∈ Ring
Assertion mplascl0 ⊢ φ → A ⁡ O = 0 ˙

Proof

Step Hyp Ref Expression
1 mplascl0.w ⊢ W = I mPoly R
2 mplascl0.a ⊢ A = algSc ⁡ W
3 mplascl0.o ⊢ O = 0 R
4 mplascl0.0 ⊢ 0 ˙ = 0 W
5 mplascl0.i ⊢ φ → I ∈ V
6 mplascl0.r ⊢ φ → R ∈ Ring
7 1 5 6 mplsca ⊢ φ → R = Scalar ⁡ W
8 7 fveq2d ⊢ φ → 0 R = 0 Scalar ⁡ W
9 3 8 eqtrid ⊢ φ → O = 0 Scalar ⁡ W
10 9 fveq2d ⊢ φ → A ⁡ O = A ⁡ 0 Scalar ⁡ W
11 eqid ⊢ Scalar ⁡ W = Scalar ⁡ W
12 1 5 6 mpllmodd ⊢ φ → W ∈ LMod
13 1 5 6 mplringd ⊢ φ → W ∈ Ring
14 2 11 12 13 ascl0 ⊢ φ → A ⁡ 0 Scalar ⁡ W = 0 W
15 10 14 eqtrd ⊢ φ → A ⁡ O = 0 W
16 15 4 eqtr4di ⊢ φ → A ⁡ O = 0 ˙