Metamath Proof Explorer


Theorem mplcoe2

Description: Decompose a monomial into a finite product of powers of variables. (The assumption that R is a commutative ring is not strictly necessary, because the submonoid of monomials is in the center of the multiplicative monoid of polynomials, but it simplifies the proof.) (Contributed by Mario Carneiro, 10-Jan-2015) (Proof shortened by AV, 18-Oct-2019)

Ref Expression
Hypotheses mplcoe1.p
|- P = ( I mPoly R )
mplcoe1.d
|- D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
mplcoe1.z
|- .0. = ( 0g ` R )
mplcoe1.o
|- .1. = ( 1r ` R )
mplcoe1.i
|- ( ph -> I e. W )
mplcoe2.g
|- G = ( mulGrp ` P )
mplcoe2.m
|- .^ = ( .g ` G )
mplcoe2.v
|- V = ( I mVar R )
mplcoe2.r
|- ( ph -> R e. CRing )
mplcoe2.y
|- ( ph -> Y e. D )
Assertion mplcoe2
|- ( ph -> ( y e. D |-> if ( y = Y , .1. , .0. ) ) = ( G gsum ( k e. I |-> ( ( Y ` k ) .^ ( V ` k ) ) ) ) )

Proof

Step Hyp Ref Expression
1 mplcoe1.p
 |-  P = ( I mPoly R )
2 mplcoe1.d
 |-  D = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
3 mplcoe1.z
 |-  .0. = ( 0g ` R )
4 mplcoe1.o
 |-  .1. = ( 1r ` R )
5 mplcoe1.i
 |-  ( ph -> I e. W )
6 mplcoe2.g
 |-  G = ( mulGrp ` P )
7 mplcoe2.m
 |-  .^ = ( .g ` G )
8 mplcoe2.v
 |-  V = ( I mVar R )
9 mplcoe2.r
 |-  ( ph -> R e. CRing )
10 mplcoe2.y
 |-  ( ph -> Y e. D )
11 crngring
 |-  ( R e. CRing -> R e. Ring )
12 9 11 syl
 |-  ( ph -> R e. Ring )
13 1 mplcrng
 |-  ( ( I e. W /\ R e. CRing ) -> P e. CRing )
14 5 9 13 syl2anc
 |-  ( ph -> P e. CRing )
15 14 adantr
 |-  ( ( ph /\ ( x e. I /\ y e. I ) ) -> P e. CRing )
16 eqid
 |-  ( Base ` P ) = ( Base ` P )
17 5 adantr
 |-  ( ( ph /\ ( x e. I /\ y e. I ) ) -> I e. W )
18 12 adantr
 |-  ( ( ph /\ ( x e. I /\ y e. I ) ) -> R e. Ring )
19 simprr
 |-  ( ( ph /\ ( x e. I /\ y e. I ) ) -> y e. I )
20 1 8 16 17 18 19 mvrcl
 |-  ( ( ph /\ ( x e. I /\ y e. I ) ) -> ( V ` y ) e. ( Base ` P ) )
21 simprl
 |-  ( ( ph /\ ( x e. I /\ y e. I ) ) -> x e. I )
22 1 8 16 17 18 21 mvrcl
 |-  ( ( ph /\ ( x e. I /\ y e. I ) ) -> ( V ` x ) e. ( Base ` P ) )
23 eqid
 |-  ( .r ` P ) = ( .r ` P )
24 6 23 mgpplusg
 |-  ( .r ` P ) = ( +g ` G )
25 24 eqcomi
 |-  ( +g ` G ) = ( .r ` P )
26 16 25 crngcom
 |-  ( ( P e. CRing /\ ( V ` y ) e. ( Base ` P ) /\ ( V ` x ) e. ( Base ` P ) ) -> ( ( V ` y ) ( +g ` G ) ( V ` x ) ) = ( ( V ` x ) ( +g ` G ) ( V ` y ) ) )
27 15 20 22 26 syl3anc
 |-  ( ( ph /\ ( x e. I /\ y e. I ) ) -> ( ( V ` y ) ( +g ` G ) ( V ` x ) ) = ( ( V ` x ) ( +g ` G ) ( V ` y ) ) )
28 27 ralrimivva
 |-  ( ph -> A. x e. I A. y e. I ( ( V ` y ) ( +g ` G ) ( V ` x ) ) = ( ( V ` x ) ( +g ` G ) ( V ` y ) ) )
29 1 2 3 4 5 6 7 8 12 10 28 mplcoe5
 |-  ( ph -> ( y e. D |-> if ( y = Y , .1. , .0. ) ) = ( G gsum ( k e. I |-> ( ( Y ` k ) .^ ( V ` k ) ) ) ) )