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

Metamath Proof Explorer

Theorem mplcoe4

Description: Decompose a polynomial into a finite sum of scaled monomials. (Contributed by Stefan O'Rear, 8-Mar-2015)

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

Proof

Step Hyp Ref Expression
1 mplcoe4.p 
 |-  P = ( I mPoly R )
2 mplcoe4.d 
 |-  D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
3 mplcoe4.z 
 |-  .0. = ( 0g ` R )
4 mplcoe4.b 
 |-  B = ( Base ` P )
5 mplcoe4.i 
 |-  ( ph -> I e. W )
6 mplcoe4.r 
 |-  ( ph -> R e. Ring )
7 mplcoe4.x 
 |-  ( ph -> X e. B )
8 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
9 eqid 
 |-  ( .s ` P ) = ( .s ` P )
10 1 2 3 8 5 4 9 6 7 mplcoe1 
 |-  ( ph -> X = ( P gsum ( k e. D |-> ( ( X ` k ) ( .s ` P ) ( y e. D |-> if ( y = k , ( 1r ` R ) , .0. ) ) ) ) ) )
11 eqid 
 |-  ( Base ` R ) = ( Base ` R )
12 5 adantr 
 |-  ( ( ph /\ k e. D ) -> I e. W )
13 6 adantr 
 |-  ( ( ph /\ k e. D ) -> R e. Ring )
14 simpr 
 |-  ( ( ph /\ k e. D ) -> k e. D )
15 1 11 4 2 7 mplelf 
 |-  ( ph -> X : D --> ( Base ` R ) )
16 15 ffvelcdmda 
 |-  ( ( ph /\ k e. D ) -> ( X ` k ) e. ( Base ` R ) )
17 1 9 2 8 3 11 12 13 14 16 mplmon2 
 |-  ( ( ph /\ k e. D ) -> ( ( X ` k ) ( .s ` P ) ( y e. D |-> if ( y = k , ( 1r ` R ) , .0. ) ) ) = ( y e. D |-> if ( y = k , ( X ` k ) , .0. ) ) )
18 17 mpteq2dva 
 |-  ( ph -> ( k e. D |-> ( ( X ` k ) ( .s ` P ) ( y e. D |-> if ( y = k , ( 1r ` R ) , .0. ) ) ) ) = ( k e. D |-> ( y e. D |-> if ( y = k , ( X ` k ) , .0. ) ) ) )
19 18 oveq2d 
 |-  ( ph -> ( P gsum ( k e. D |-> ( ( X ` k ) ( .s ` P ) ( y e. D |-> if ( y = k , ( 1r ` R ) , .0. ) ) ) ) ) = ( P gsum ( k e. D |-> ( y e. D |-> if ( y = k , ( X ` k ) , .0. ) ) ) ) )
20 10 19 eqtrd 
 |-  ( ph -> X = ( P gsum ( k e. D |-> ( y e. D |-> if ( y = k , ( X ` k ) , .0. ) ) ) ) )