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	syl5eq	|- ( ph -> U = ( x e. D |-> if ( x = ( I X. { 0 } ) , .1. , .0. ) ) )