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 
|- 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 7 crngringd 
 |-  ( ph -> R e. Ring )
10 3 8 4 5 6 9 mplascl0 
 |-  ( ph -> ( ( algSc ` W ) ` O ) = .0. )
11 10 fveq2d 
 |-  ( ph -> ( Q ` ( ( algSc ` W ) ` O ) ) = ( Q ` .0. ) )
12 2 4 ring0cl 
 |-  ( R e. Ring -> O e. B )
13 9 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 11 14 eqtr3d 
 |-  ( ph -> ( Q ` .0. ) = ( ( B ^m I ) X. { O } ) )