Theorem evl0

Description: The zero polynomial evaluates to zero. (Contributed by SN, 23-Nov-2024)

	Ref	Expression
Hypotheses	evl0.q	|- Q = ( I eval R )
	evl0.b	|- B = ( Base ` R )
	evl0.w	|- W = ( I mPoly R )
	evl0.o	|- O = ( 0g ` R )
	evl0.0	|- .0. = ( 0g ` W )
	evl0.i	|- ( ph -> I e. V )
	evl0.r	|- ( ph -> R e. CRing )
Assertion	evl0	|- ( ph -> ( Q ` .0. ) = ( ( B ^m I ) X. { O } ) )

Proof

Step	Hyp	Ref	Expression
1		evl0.q	|- Q = ( I eval R )
2		evl0.b	|- B = ( Base ` R )
3		evl0.w	|- W = ( I mPoly R )
4		evl0.o	|- O = ( 0g ` R )
5		evl0.0	|- .0. = ( 0g ` W )
6		evl0.i	|- ( ph -> I e. V )
7		evl0.r	|- ( ph -> R e. CRing )
8		eqid	|- ( algSc ` W ) = ( algSc ` W )
9	3 8 4 5 6 7	mplascl0	|- ( ph -> ( ( algSc ` W ) ` O ) = .0. )
10	9	fveq2d	|- ( ph -> ( Q ` ( ( algSc ` W ) ` O ) ) = ( Q ` .0. ) )
11	7	crngringd	|- ( ph -> R e. Ring )
12	2 4	ring0cl	|- ( R e. Ring -> O e. B )
13	11 12	syl	|- ( ph -> O e. B )
14	1 3 2 8 6 7 13	evlsca	|- ( ph -> ( Q ` ( ( algSc ` W ) ` O ) ) = ( ( B ^m I ) X. { O } ) )
15	10 14	eqtr3d	|- ( ph -> ( Q ` .0. ) = ( ( B ^m I ) X. { O } ) )