This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 7 crngringd ⊢ ( 𝜑 → 𝑅 ∈ Ring )
10 3 8 4 5 6 9 mplascl0 ⊢ ( 𝜑 → ( ( algSc ‘ 𝑊 ) ‘ 𝑂 ) = 0 )
11 10 fveq2d ⊢ ( 𝜑 → ( 𝑄 ‘ ( ( algSc ‘ 𝑊 ) ‘ 𝑂 ) ) = ( 𝑄 ‘ 0 ) )
12 2 4 ring0cl ⊢ ( 𝑅 ∈ Ring → 𝑂 ∈ 𝐵 )
13 9 12 syl ⊢ ( 𝜑 → 𝑂 ∈ 𝐵 )
14 1 3 2 8 6 7 13 evlsca ⊢ ( 𝜑 → ( 𝑄 ‘ ( ( algSc ‘ 𝑊 ) ‘ 𝑂 ) ) = ( ( 𝐵 ↑m 𝐼 ) × { 𝑂 } ) )
15 11 14 eqtr3d ⊢ ( 𝜑 → ( 𝑄 ‘ 0 ) = ( ( 𝐵 ↑m 𝐼 ) × { 𝑂 } ) )