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 )