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

Metamath Proof Explorer

Theorem mpl1

Description: The identity element of the ring of polynomials. (Contributed by Mario Carneiro, 10-Jan-2015)

Ref Expression
Hypotheses mpl1.p 
|- P = ( I mPoly R )
mpl1.d 
|- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
mpl1.z 
|- .0. = ( 0g ` R )
mpl1.o 
|- .1. = ( 1r ` R )
mpl1.u 
|- U = ( 1r ` P )
mpl1.i 
|- ( ph -> I e. W )
mpl1.r 
|- ( ph -> R e. Ring )
Assertion mpl1 
|- ( ph -> U = ( x e. D |-> if ( x = ( I X. { 0 } ) , .1. , .0. ) ) )

Proof

Step Hyp Ref Expression
1 mpl1.p 
 |-  P = ( I mPoly R )
2 mpl1.d 
 |-  D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
3 mpl1.z 
 |-  .0. = ( 0g ` R )
4 mpl1.o 
 |-  .1. = ( 1r ` R )
5 mpl1.u 
 |-  U = ( 1r ` P )
6 mpl1.i 
 |-  ( ph -> I e. W )
7 mpl1.r 
 |-  ( ph -> R e. Ring )
8 eqid 
 |-  ( I mPwSer R ) = ( I mPwSer R )
9 eqid 
 |-  ( Base ` P ) = ( Base ` P )
10 8 1 9 6 7 mplsubrg 
 |-  ( ph -> ( Base ` P ) e. ( SubRing ` ( I mPwSer R ) ) )
11 1 8 9 mplval2 
 |-  P = ( ( I mPwSer R ) |`s ( Base ` P ) )
12 eqid 
 |-  ( 1r ` ( I mPwSer R ) ) = ( 1r ` ( I mPwSer R ) )
13 11 12 subrg1 
 |-  ( ( Base ` P ) e. ( SubRing ` ( I mPwSer R ) ) -> ( 1r ` ( I mPwSer R ) ) = ( 1r ` P ) )
14 10 13 syl 
 |-  ( ph -> ( 1r ` ( I mPwSer R ) ) = ( 1r ` P ) )
15 8 6 7 2 3 4 12 psr1 
 |-  ( ph -> ( 1r ` ( I mPwSer R ) ) = ( x e. D |-> if ( x = ( I X. { 0 } ) , .1. , .0. ) ) )
16 14 15 eqtr3d 
 |-  ( ph -> ( 1r ` P ) = ( x e. D |-> if ( x = ( I X. { 0 } ) , .1. , .0. ) ) )
17 5 16 eqtrid 
 |-  ( ph -> U = ( x e. D |-> if ( x = ( I X. { 0 } ) , .1. , .0. ) ) )