Metamath Proof Explorer


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 syl5eq
 |-  ( 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. ) ) )