Metamath Proof Explorer

Theorem mplmon2

Description: Express a scaled monomial. (Contributed by Stefan O'Rear, 8-Mar-2015)

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

Proof

Step Hyp Ref Expression
1 mplmon2.p 
 |-  P = ( I mPoly R )
2 mplmon2.v 
 |-  .x. = ( .s ` P )
3 mplmon2.d 
 |-  D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
4 mplmon2.o 
 |-  .1. = ( 1r ` R )
5 mplmon2.z 
 |-  .0. = ( 0g ` R )
6 mplmon2.b 
 |-  B = ( Base ` R )
7 mplmon2.i 
 |-  ( ph -> I e. W )
8 mplmon2.r 
 |-  ( ph -> R e. Ring )
9 mplmon2.k 
 |-  ( ph -> K e. D )
10 mplmon2.x 
 |-  ( ph -> X e. B )
11 eqid 
 |-  ( Base ` P ) = ( Base ` P )
12 eqid 
 |-  ( .r ` R ) = ( .r ` R )
13 1 11 5 4 3 7 8 9 mplmon 
 |-  ( ph -> ( y e. D |-> if ( y = K , .1. , .0. ) ) e. ( Base ` P ) )
14 1 2 6 11 12 3 10 13 mplvsca 
 |-  ( ph -> ( X .x. ( y e. D |-> if ( y = K , .1. , .0. ) ) ) = ( ( D X. { X } ) oF ( .r ` R ) ( y e. D |-> if ( y = K , .1. , .0. ) ) ) )
15 ovex 
 |-  ( NN0 ^m I ) e. _V
16 3 15 rabex2 
 |-  D e. _V
17 16 a1i 
 |-  ( ph -> D e. _V )
18 10 adantr 
 |-  ( ( ph /\ y e. D ) -> X e. B )
19 4 fvexi 
 |-  .1. e. _V
20 5 fvexi 
 |-  .0. e. _V
21 19 20 ifex 
 |-  if ( y = K , .1. , .0. ) e. _V
22 21 a1i 
 |-  ( ( ph /\ y e. D ) -> if ( y = K , .1. , .0. ) e. _V )
23 fconstmpt 
 |-  ( D X. { X } ) = ( y e. D |-> X )
24 23 a1i 
 |-  ( ph -> ( D X. { X } ) = ( y e. D |-> X ) )
25 eqidd 
 |-  ( ph -> ( y e. D |-> if ( y = K , .1. , .0. ) ) = ( y e. D |-> if ( y = K , .1. , .0. ) ) )
26 17 18 22 24 25 offval2 
 |-  ( ph -> ( ( D X. { X } ) oF ( .r ` R ) ( y e. D |-> if ( y = K , .1. , .0. ) ) ) = ( y e. D |-> ( X ( .r ` R ) if ( y = K , .1. , .0. ) ) ) )
27 oveq2 
 |-  ( .1. = if ( y = K , .1. , .0. ) -> ( X ( .r ` R ) .1. ) = ( X ( .r ` R ) if ( y = K , .1. , .0. ) ) )
28 27 eqeq1d 
 |-  ( .1. = if ( y = K , .1. , .0. ) -> ( ( X ( .r ` R ) .1. ) = if ( y = K , X , .0. ) <-> ( X ( .r ` R ) if ( y = K , .1. , .0. ) ) = if ( y = K , X , .0. ) ) )
29 oveq2 
 |-  ( .0. = if ( y = K , .1. , .0. ) -> ( X ( .r ` R ) .0. ) = ( X ( .r ` R ) if ( y = K , .1. , .0. ) ) )
30 29 eqeq1d 
 |-  ( .0. = if ( y = K , .1. , .0. ) -> ( ( X ( .r ` R ) .0. ) = if ( y = K , X , .0. ) <-> ( X ( .r ` R ) if ( y = K , .1. , .0. ) ) = if ( y = K , X , .0. ) ) )
31 6 12 4 ringridm 
 |-  ( ( R e. Ring /\ X e. B ) -> ( X ( .r ` R ) .1. ) = X )
32 8 10 31 syl2anc 
 |-  ( ph -> ( X ( .r ` R ) .1. ) = X )
33 iftrue 
 |-  ( y = K -> if ( y = K , X , .0. ) = X )
34 33 eqcomd 
 |-  ( y = K -> X = if ( y = K , X , .0. ) )
35 32 34 sylan9eq 
 |-  ( ( ph /\ y = K ) -> ( X ( .r ` R ) .1. ) = if ( y = K , X , .0. ) )
36 6 12 5 ringrz 
 |-  ( ( R e. Ring /\ X e. B ) -> ( X ( .r ` R ) .0. ) = .0. )
37 8 10 36 syl2anc 
 |-  ( ph -> ( X ( .r ` R ) .0. ) = .0. )
38 iffalse 
 |-  ( -. y = K -> if ( y = K , X , .0. ) = .0. )
39 38 eqcomd 
 |-  ( -. y = K -> .0. = if ( y = K , X , .0. ) )
40 37 39 sylan9eq 
 |-  ( ( ph /\ -. y = K ) -> ( X ( .r ` R ) .0. ) = if ( y = K , X , .0. ) )
41 28 30 35 40 ifbothda 
 |-  ( ph -> ( X ( .r ` R ) if ( y = K , .1. , .0. ) ) = if ( y = K , X , .0. ) )
42 41 mpteq2dv 
 |-  ( ph -> ( y e. D |-> ( X ( .r ` R ) if ( y = K , .1. , .0. ) ) ) = ( y e. D |-> if ( y = K , X , .0. ) ) )
43 14 26 42 3eqtrd 
 |-  ( ph -> ( X .x. ( y e. D |-> if ( y = K , .1. , .0. ) ) ) = ( y e. D |-> if ( y = K , X , .0. ) ) )