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 ) ) ) ) ) )

Metamath Proof Explorer

Theorem mplmonprod

Proof