Metamath Proof Explorer

Theorem mplmonprod

Description: Finite product of monomials. Here the function G maps a bag of variables to the corresponding monomial. (Contributed by Thierry Arnoux, 16-Mar-2026)

Ref Expression
Hypotheses mplmonprod.p 
|- P = ( I mPoly R )
mplmonprod.b 
|- B = ( Base ` P )
mplmonprod.r 
|- ( ph -> R e. CRing )
mplmonprod.i 
|- ( ph -> I e. V )
mplmonprod.d 
|- D = { h e. ( NN0 ^m I ) | h finSupp 0 }
mplmonprod.a 
|- ( ph -> A e. Fin )
mplmonprod.f 
|- ( ph -> F : A --> D )
mplmonprod.1 
|- .1. = ( 1r ` R )
mplmonprod.0 
|- .0. = ( 0g ` R )
mplmonprod.m 
|- M = ( mulGrp ` P )
mplmonprod.g 
|- G = ( y e. D |-> ( z e. D |-> if ( z = y , .1. , .0. ) ) )
Assertion mplmonprod 
|- ( ph -> ( M gsum ( G o. F ) ) = ( G ` ( i e. I |-> ( CCfld gsum ( x e. A |-> ( ( F ` x ) ` i ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 mplmonprod.p 
 |-  P = ( I mPoly R )
2 mplmonprod.b 
 |-  B = ( Base ` P )
3 mplmonprod.r 
 |-  ( ph -> R e. CRing )
4 mplmonprod.i 
 |-  ( ph -> I e. V )
5 mplmonprod.d 
 |-  D = { h e. ( NN0 ^m I ) | h finSupp 0 }
6 mplmonprod.a 
 |-  ( ph -> A e. Fin )
7 mplmonprod.f 
 |-  ( ph -> F : A --> D )
8 mplmonprod.1 
 |-  .1. = ( 1r ` R )
9 mplmonprod.0 
 |-  .0. = ( 0g ` R )
10 mplmonprod.m 
 |-  M = ( mulGrp ` P )
11 mplmonprod.g 
 |-  G = ( y e. D |-> ( z e. D |-> if ( z = y , .1. , .0. ) ) )
12 eqid 
 |-  ( mulGrp ` ( I mPwSer R ) ) = ( mulGrp ` ( I mPwSer R ) )
13 eqid 
 |-  ( Base ` ( I mPwSer R ) ) = ( Base ` ( I mPwSer R ) )
14 12 13 mgpbas 
 |-  ( Base ` ( I mPwSer R ) ) = ( Base ` ( mulGrp ` ( I mPwSer R ) ) )
15 eqid 
 |-  ( I mPwSer R ) = ( I mPwSer R )
16 eqid 
 |-  ( .r ` P ) = ( .r ` P )
17 1 15 16 mplmulr 
 |-  ( .r ` P ) = ( .r ` ( I mPwSer R ) )
18 12 17 mgpplusg 
 |-  ( .r ` P ) = ( +g ` ( mulGrp ` ( I mPwSer R ) ) )
19 ovex 
 |-  ( I mPwSer R ) e. _V
20 2 fvexi 
 |-  B e. _V
21 1 15 2 mplval2 
 |-  P = ( ( I mPwSer R ) |`s B )
22 21 12 mgpress 
 |-  ( ( ( I mPwSer R ) e. _V /\ B e. _V ) -> ( ( mulGrp ` ( I mPwSer R ) ) |`s B ) = ( mulGrp ` P ) )
23 19 20 22 mp2an 
 |-  ( ( mulGrp ` ( I mPwSer R ) ) |`s B ) = ( mulGrp ` P )
24 10 23 eqtr4i 
 |-  M = ( ( mulGrp ` ( I mPwSer R ) ) |`s B )
25 fvexd 
 |-  ( ph -> ( mulGrp ` ( I mPwSer R ) ) e. _V )
26 1 15 2 13 mplbasss 
 |-  B C_ ( Base ` ( I mPwSer R ) )
27 26 a1i 
 |-  ( ph -> B C_ ( Base ` ( I mPwSer R ) ) )
28 fvexd 
 |-  ( ( ph /\ y e. D ) -> ( Base ` R ) e. _V )
29 ovex 
 |-  ( NN0 ^m I ) e. _V
30 5 29 rabex2 
 |-  D e. _V
31 30 a1i 
 |-  ( ( ph /\ y e. D ) -> D e. _V )
32 eqid 
 |-  ( Base ` R ) = ( Base ` R )
33 3 crngringd 
 |-  ( ph -> R e. Ring )
34 32 8 33 ringidcld 
 |-  ( ph -> .1. e. ( Base ` R ) )
35 3 crnggrpd 
 |-  ( ph -> R e. Grp )
36 32 9 grpidcl 
 |-  ( R e. Grp -> .0. e. ( Base ` R ) )
37 35 36 syl 
 |-  ( ph -> .0. e. ( Base ` R ) )
38 34 37 ifcld 
 |-  ( ph -> if ( z = y , .1. , .0. ) e. ( Base ` R ) )
39 38 ad2antrr 
 |-  ( ( ( ph /\ y e. D ) /\ z e. D ) -> if ( z = y , .1. , .0. ) e. ( Base ` R ) )
40 eqid 
 |-  ( z e. D |-> if ( z = y , .1. , .0. ) ) = ( z e. D |-> if ( z = y , .1. , .0. ) )
41 39 40 fmptd 
 |-  ( ( ph /\ y e. D ) -> ( z e. D |-> if ( z = y , .1. , .0. ) ) : D --> ( Base ` R ) )
42 28 31 41 elmapdd 
 |-  ( ( ph /\ y e. D ) -> ( z e. D |-> if ( z = y , .1. , .0. ) ) e. ( ( Base ` R ) ^m D ) )
43 5 psrbasfsupp 
 |-  D = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
44 4 adantr 
 |-  ( ( ph /\ y e. D ) -> I e. V )
45 15 32 43 13 44 psrbas 
 |-  ( ( ph /\ y e. D ) -> ( Base ` ( I mPwSer R ) ) = ( ( Base ` R ) ^m D ) )
46 42 45 eleqtrrd 
 |-  ( ( ph /\ y e. D ) -> ( z e. D |-> if ( z = y , .1. , .0. ) ) e. ( Base ` ( I mPwSer R ) ) )
47 velsn 
 |-  ( z e. { y } <-> z = y )
48 47 bicomi 
 |-  ( z = y <-> z e. { y } )
49 48 a1i 
 |-  ( z e. D -> ( z = y <-> z e. { y } ) )
50 49 ifbid 
 |-  ( z e. D -> if ( z = y , .1. , .0. ) = if ( z e. { y } , .1. , .0. ) )
51 50 mpteq2ia 
 |-  ( z e. D |-> if ( z = y , .1. , .0. ) ) = ( z e. D |-> if ( z e. { y } , .1. , .0. ) )
52 snfi 
 |-  { y } e. Fin
53 52 a1i 
 |-  ( ( ph /\ y e. D ) -> { y } e. Fin )
54 8 fvexi 
 |-  .1. e. _V
55 54 a1i 
 |-  ( ( ( ph /\ y e. D ) /\ z e. { y } ) -> .1. e. _V )
56 9 fvexi 
 |-  .0. e. _V
57 56 a1i 
 |-  ( ( ph /\ y e. D ) -> .0. e. _V )
58 51 31 53 55 57 mptiffisupp 
 |-  ( ( ph /\ y e. D ) -> ( z e. D |-> if ( z = y , .1. , .0. ) ) finSupp .0. )
59 1 15 13 9 2 mplelbas 
 |-  ( ( z e. D |-> if ( z = y , .1. , .0. ) ) e. B <-> ( ( z e. D |-> if ( z = y , .1. , .0. ) ) e. ( Base ` ( I mPwSer R ) ) /\ ( z e. D |-> if ( z = y , .1. , .0. ) ) finSupp .0. ) )
60 46 58 59 sylanbrc 
 |-  ( ( ph /\ y e. D ) -> ( z e. D |-> if ( z = y , .1. , .0. ) ) e. B )
61 60 11 fmptd 
 |-  ( ph -> G : D --> B )
62 61 7 fcod 
 |-  ( ph -> ( G o. F ) : A --> B )
63 15 1 2 4 33 mplsubrg 
 |-  ( ph -> B e. ( SubRing ` ( I mPwSer R ) ) )
64 eqid 
 |-  ( 1r ` ( I mPwSer R ) ) = ( 1r ` ( I mPwSer R ) )
65 64 subrg1cl 
 |-  ( B e. ( SubRing ` ( I mPwSer R ) ) -> ( 1r ` ( I mPwSer R ) ) e. B )
66 63 65 syl 
 |-  ( ph -> ( 1r ` ( I mPwSer R ) ) e. B )
67 15 4 33 psrring 
 |-  ( ph -> ( I mPwSer R ) e. Ring )
68 67 adantr 
 |-  ( ( ph /\ x e. ( Base ` ( I mPwSer R ) ) ) -> ( I mPwSer R ) e. Ring )
69 simpr 
 |-  ( ( ph /\ x e. ( Base ` ( I mPwSer R ) ) ) -> x e. ( Base ` ( I mPwSer R ) ) )
70 13 17 64 68 69 ringlidmd 
 |-  ( ( ph /\ x e. ( Base ` ( I mPwSer R ) ) ) -> ( ( 1r ` ( I mPwSer R ) ) ( .r ` P ) x ) = x )
71 13 17 64 68 69 ringridmd 
 |-  ( ( ph /\ x e. ( Base ` ( I mPwSer R ) ) ) -> ( x ( .r ` P ) ( 1r ` ( I mPwSer R ) ) ) = x )
72 70 71 jca 
 |-  ( ( ph /\ x e. ( Base ` ( I mPwSer R ) ) ) -> ( ( ( 1r ` ( I mPwSer R ) ) ( .r ` P ) x ) = x /\ ( x ( .r ` P ) ( 1r ` ( I mPwSer R ) ) ) = x ) )
73 14 18 24 25 6 27 62 66 72 gsumress 
 |-  ( ph -> ( ( mulGrp ` ( I mPwSer R ) ) gsum ( G o. F ) ) = ( M gsum ( G o. F ) ) )
74 15 13 3 4 5 6 7 8 9 12 11 psrmonprod 
 |-  ( ph -> ( ( mulGrp ` ( I mPwSer R ) ) gsum ( G o. F ) ) = ( G ` ( i e. I |-> ( CCfld gsum ( x e. A |-> ( ( F ` x ) ` i ) ) ) ) ) )
75 73 74 eqtr3d 
 |-  ( ph -> ( M gsum ( G o. F ) ) = ( G ` ( i e. I |-> ( CCfld gsum ( x e. A |-> ( ( F ` x ) ` i ) ) ) ) ) )