Theorem mplascl

Description: Value of the scalar injection into the polynomial algebra. (Contributed by Stefan O'Rear, 9-Mar-2015)

	Ref	Expression
Hypotheses	mplascl.p	|- P = ( I mPoly R )
	mplascl.d	|- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
	mplascl.z	|- .0. = ( 0g ` R )
	mplascl.b	|- B = ( Base ` R )
	mplascl.a	|- A = ( algSc ` P )
	mplascl.i	|- ( ph -> I e. W )
	mplascl.r	|- ( ph -> R e. Ring )
	mplascl.x	|- ( ph -> X e. B )
Assertion	mplascl	|- ( ph -> ( A ` X ) = ( y e. D |-> if ( y = ( I X. { 0 } ) , X , .0. ) ) )

Proof

Step	Hyp	Ref	Expression
1		mplascl.p	|- P = ( I mPoly R )
2		mplascl.d	|- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
3		mplascl.z	|- .0. = ( 0g ` R )
4		mplascl.b	|- B = ( Base ` R )
5		mplascl.a	|- A = ( algSc ` P )
6		mplascl.i	|- ( ph -> I e. W )
7		mplascl.r	|- ( ph -> R e. Ring )
8		mplascl.x	|- ( ph -> X e. B )
9	1 6 7	mplsca	|- ( ph -> R = ( Scalar ` P ) )
10	9	fveq2d	|- ( ph -> ( Base ` R ) = ( Base ` ( Scalar ` P ) ) )
11	4 10	eqtrid	|- ( ph -> B = ( Base ` ( Scalar ` P ) ) )
12	8 11	eleqtrd	|- ( ph -> X e. ( Base ` ( Scalar ` P ) ) )
13		eqid	|- ( Scalar ` P ) = ( Scalar ` P )
14		eqid	|- ( Base ` ( Scalar ` P ) ) = ( Base ` ( Scalar ` P ) )
15		eqid	|- ( .s ` P ) = ( .s ` P )
16		eqid	|- ( 1r ` P ) = ( 1r ` P )
17	5 13 14 15 16	asclval	|- ( X e. ( Base ` ( Scalar ` P ) ) -> ( A ` X ) = ( X ( .s ` P ) ( 1r ` P ) ) )
18	12 17	syl	|- ( ph -> ( A ` X ) = ( X ( .s ` P ) ( 1r ` P ) ) )
19		eqid	|- ( 1r ` R ) = ( 1r ` R )
20	1 2 3 19 16 6 7	mpl1	|- ( ph -> ( 1r ` P ) = ( y e. D |-> if ( y = ( I X. { 0 } ) , ( 1r ` R ) , .0. ) ) )
21	20	oveq2d	|- ( ph -> ( X ( .s ` P ) ( 1r ` P ) ) = ( X ( .s ` P ) ( y e. D |-> if ( y = ( I X. { 0 } ) , ( 1r ` R ) , .0. ) ) ) )
22	2	psrbag0	|- ( I e. W -> ( I X. { 0 } ) e. D )
23	6 22	syl	|- ( ph -> ( I X. { 0 } ) e. D )
24	1 15 2 19 3 4 6 7 23 8	mplmon2	|- ( ph -> ( X ( .s ` P ) ( y e. D |-> if ( y = ( I X. { 0 } ) , ( 1r ` R ) , .0. ) ) ) = ( y e. D |-> if ( y = ( I X. { 0 } ) , X , .0. ) ) )
25	18 21 24	3eqtrd	|- ( ph -> ( A ` X ) = ( y e. D |-> if ( y = ( I X. { 0 } ) , X , .0. ) ) )