Theorem evl0

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

	Ref	Expression
Hypotheses	evl0.q	⊢ 𝑄 = ( 𝐼 eval 𝑅 )
	evl0.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	evl0.w	⊢ 𝑊 = ( 𝐼 mPoly 𝑅 )
	evl0.o	⊢ 𝑂 = ( 0g ‘ 𝑅 )
	evl0.0	⊢ 0 = ( 0g ‘ 𝑊 )
	evl0.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
	evl0.r	⊢ ( 𝜑 → 𝑅 ∈ CRing )
Assertion	evl0	⊢ ( 𝜑 → ( 𝑄 ‘ 0 ) = ( ( 𝐵 ↑m 𝐼 ) × { 𝑂 } ) )

Proof

Step	Hyp	Ref	Expression
1		evl0.q	⊢ 𝑄 = ( 𝐼 eval 𝑅 )
2		evl0.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
3		evl0.w	⊢ 𝑊 = ( 𝐼 mPoly 𝑅 )
4		evl0.o	⊢ 𝑂 = ( 0g ‘ 𝑅 )
5		evl0.0	⊢ 0 = ( 0g ‘ 𝑊 )
6		evl0.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
7		evl0.r	⊢ ( 𝜑 → 𝑅 ∈ CRing )
8		eqid	⊢ ( algSc ‘ 𝑊 ) = ( algSc ‘ 𝑊 )
9	3 8 4 5 6 7	mplascl0	⊢ ( 𝜑 → ( ( algSc ‘ 𝑊 ) ‘ 𝑂 ) = 0 )
10	9	fveq2d	⊢ ( 𝜑 → ( 𝑄 ‘ ( ( algSc ‘ 𝑊 ) ‘ 𝑂 ) ) = ( 𝑄 ‘ 0 ) )
11	7	crngringd	⊢ ( 𝜑 → 𝑅 ∈ Ring )
12	2 4	ring0cl	⊢ ( 𝑅 ∈ Ring → 𝑂 ∈ 𝐵 )
13	11 12	syl	⊢ ( 𝜑 → 𝑂 ∈ 𝐵 )
14	1 3 2 8 6 7 13	evlsca	⊢ ( 𝜑 → ( 𝑄 ‘ ( ( algSc ‘ 𝑊 ) ‘ 𝑂 ) ) = ( ( 𝐵 ↑m 𝐼 ) × { 𝑂 } ) )
15	10 14	eqtr3d	⊢ ( 𝜑 → ( 𝑄 ‘ 0 ) = ( ( 𝐵 ↑m 𝐼 ) × { 𝑂 } ) )