Theorem evl0

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

	Ref	Expression
Hypotheses	evl0.q	$$⊢Q=I\mathrm{eval}R$$
	evl0.b	$$⊢B={\mathrm{Base}}_R$$
	evl0.w	$$⊢W=I\mathrm{mPoly}R$$
	evl0.o	$$⊢O=0_R$$
	evl0.0	$$⊢\underset{\dot{}}{0}=0_W$$
	evl0.i	$$⊢\phi \to I\in V$$
	evl0.r	$$⊢\phi \to R\in \mathrm{CRing}$$
Assertion	evl0	$$⊢\phi \to Q\left(\underset{\dot{}}{0}\right)=\left(B^I\right)\times \left\{O\right\}$$

Proof

Step	Hyp	Ref	Expression
1		evl0.q	$$⊢Q=I\mathrm{eval}R$$
2		evl0.b	$$⊢B={\mathrm{Base}}_R$$
3		evl0.w	$$⊢W=I\mathrm{mPoly}R$$
4		evl0.o	$$⊢O=0_R$$
5		evl0.0	$$⊢\underset{\dot{}}{0}=0_W$$
6		evl0.i	$$⊢\phi \to I\in V$$
7		evl0.r	$$⊢\phi \to R\in \mathrm{CRing}$$
8		eqid	$$⊢\mathrm{algSc}\left(W\right)=\mathrm{algSc}\left(W\right)$$
9	7	crngringd	$$⊢\phi \to R\in \mathrm{Ring}$$
10	3 8 4 5 6 9	mplascl0	$$⊢\phi \to \mathrm{algSc}\left(W\right)\left(O\right)=\underset{\dot{}}{0}$$
11	10	fveq2d	$$⊢\phi \to Q\left(\mathrm{algSc}\left(W\right)\left(O\right)\right)=Q\left(\underset{\dot{}}{0}\right)$$
12	2 4	ring0cl	$$⊢R\in \mathrm{Ring}\to O\in B$$
13	9 12	syl	$$⊢\phi \to O\in B$$
14	1 3 2 8 6 7 13	evlsca	$$⊢\phi \to Q\left(\mathrm{algSc}\left(W\right)\left(O\right)\right)=\left(B^I\right)\times \left\{O\right\}$$
15	11 14	eqtr3d	$$⊢\phi \to Q\left(\underset{\dot{}}{0}\right)=\left(B^I\right)\times \left\{O\right\}$$