evl0

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

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 = 0_{R}$
5		evl0.0	$⊢ \underset{˙}{0} = 0_{W}$
6		evl0.i	$⊢ φ \to I \in V$
7		evl0.r	$⊢ φ \to R \in CRing$
8		eqid	$⊢ algSc (W) = algSc (W)$
9	7	crngringd	$⊢ φ \to R \in Ring$
10	3 8 4 5 6 9	mplascl0	$⊢ φ \to algSc (W) (O) = \underset{˙}{0}$
11	10	fveq2d	$⊢ φ \to Q (algSc (W) (O)) = Q (\underset{˙}{0})$
12	2 4	ring0cl	$⊢ R \in Ring \to O \in B$
13	9 12	syl	$⊢ φ \to O \in B$
14	1 3 2 8 6 7 13	evlsca	$⊢ φ \to Q (algSc (W) (O)) = (B^{I}) \times \{O\}$
15	11 14	eqtr3d	$⊢ φ \to Q (\underset{˙}{0}) = (B^{I}) \times \{O\}$

Metamath Proof Explorer