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 = ( 0g ` R )
	mplascl0.0	|- .0. = ( 0g ` W )
	mplascl0.i	|- ( ph -> I e. V )
	mplascl0.r	|- ( ph -> R e. Ring )
Assertion	mplascl0	|- ( ph -> ( 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 = ( 0g ` R )
4		mplascl0.0	|- .0. = ( 0g ` W )
5		mplascl0.i	|- ( ph -> I e. V )
6		mplascl0.r	|- ( ph -> R e. Ring )
7	1 5 6	mplsca	|- ( ph -> R = ( Scalar ` W ) )
8	7	fveq2d	|- ( ph -> ( 0g ` R ) = ( 0g ` ( Scalar ` W ) ) )
9	3 8	eqtrid	|- ( ph -> O = ( 0g ` ( Scalar ` W ) ) )
10	9	fveq2d	|- ( ph -> ( A ` O ) = ( A ` ( 0g ` ( Scalar ` W ) ) ) )
11		eqid	|- ( Scalar ` W ) = ( Scalar ` W )
12	1 5 6	mpllmodd	|- ( ph -> W e. LMod )
13	1 5 6	mplringd	|- ( ph -> W e. Ring )
14	2 11 12 13	ascl0	|- ( ph -> ( A ` ( 0g ` ( Scalar ` W ) ) ) = ( 0g ` W ) )
15	10 14	eqtrd	|- ( ph -> ( A ` O ) = ( 0g ` W ) )
16	15 4	eqtr4di	|- ( ph -> ( A ` O ) = .0. )