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	⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
	mplmonprod.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
	mplmonprod.r	⊢ ( 𝜑 → 𝑅 ∈ CRing )
	mplmonprod.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
	mplmonprod.d	⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 }
	mplmonprod.a	⊢ ( 𝜑 → 𝐴 ∈ Fin )
	mplmonprod.f	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐷 )
	mplmonprod.1	⊢ 1 = ( 1r ‘ 𝑅 )
	mplmonprod.0	⊢ 0 = ( 0g ‘ 𝑅 )
	mplmonprod.m	⊢ 𝑀 = ( mulGrp ‘ 𝑃 )
	mplmonprod.g	⊢ 𝐺 = ( 𝑦 ∈ 𝐷 ↦ ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 = 𝑦 , 1 , 0 ) ) )
Assertion	mplmonprod	⊢ ( 𝜑 → ( 𝑀 Σg ( 𝐺 ∘ 𝐹 ) ) = ( 𝐺 ‘ ( 𝑖 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑥 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		mplmonprod.p	⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
2		mplmonprod.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
3		mplmonprod.r	⊢ ( 𝜑 → 𝑅 ∈ CRing )
4		mplmonprod.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
5		mplmonprod.d	⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ℎ finSupp 0 }
6		mplmonprod.a	⊢ ( 𝜑 → 𝐴 ∈ Fin )
7		mplmonprod.f	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐷 )
8		mplmonprod.1	⊢ 1 = ( 1r ‘ 𝑅 )
9		mplmonprod.0	⊢ 0 = ( 0g ‘ 𝑅 )
10		mplmonprod.m	⊢ 𝑀 = ( mulGrp ‘ 𝑃 )
11		mplmonprod.g	⊢ 𝐺 = ( 𝑦 ∈ 𝐷 ↦ ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 = 𝑦 , 1 , 0 ) ) )
12		eqid	⊢ ( mulGrp ‘ ( 𝐼 mPwSer 𝑅 ) ) = ( mulGrp ‘ ( 𝐼 mPwSer 𝑅 ) )
13		eqid	⊢ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) = ( Base ‘ ( 𝐼 mPwSer 𝑅 ) )
14	12 13	mgpbas	⊢ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) = ( Base ‘ ( mulGrp ‘ ( 𝐼 mPwSer 𝑅 ) ) )
15		eqid	⊢ ( 𝐼 mPwSer 𝑅 ) = ( 𝐼 mPwSer 𝑅 )
16		eqid	⊢ ( .r ‘ 𝑃 ) = ( .r ‘ 𝑃 )
17	1 15 16	mplmulr	⊢ ( .r ‘ 𝑃 ) = ( .r ‘ ( 𝐼 mPwSer 𝑅 ) )
18	12 17	mgpplusg	⊢ ( .r ‘ 𝑃 ) = ( +g ‘ ( mulGrp ‘ ( 𝐼 mPwSer 𝑅 ) ) )
19		ovex	⊢ ( 𝐼 mPwSer 𝑅 ) ∈ V
20	2	fvexi	⊢ 𝐵 ∈ V
21	1 15 2	mplval2	⊢ 𝑃 = ( ( 𝐼 mPwSer 𝑅 ) ↾s 𝐵 )
22	21 12	mgpress	⊢ ( ( ( 𝐼 mPwSer 𝑅 ) ∈ V ∧ 𝐵 ∈ V ) → ( ( mulGrp ‘ ( 𝐼 mPwSer 𝑅 ) ) ↾s 𝐵 ) = ( mulGrp ‘ 𝑃 ) )
23	19 20 22	mp2an	⊢ ( ( mulGrp ‘ ( 𝐼 mPwSer 𝑅 ) ) ↾s 𝐵 ) = ( mulGrp ‘ 𝑃 )
24	10 23	eqtr4i	⊢ 𝑀 = ( ( mulGrp ‘ ( 𝐼 mPwSer 𝑅 ) ) ↾s 𝐵 )
25		fvexd	⊢ ( 𝜑 → ( mulGrp ‘ ( 𝐼 mPwSer 𝑅 ) ) ∈ V )
26	1 15 2 13	mplbasss	⊢ 𝐵 ⊆ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) )
27	26	a1i	⊢ ( 𝜑 → 𝐵 ⊆ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) )
28		fvexd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → ( Base ‘ 𝑅 ) ∈ V )
29		ovex	⊢ ( ℕ0 ↑m 𝐼 ) ∈ V
30	5 29	rabex2	⊢ 𝐷 ∈ V
31	30	a1i	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → 𝐷 ∈ V )
32		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
33	3	crngringd	⊢ ( 𝜑 → 𝑅 ∈ Ring )
34	32 8 33	ringidcld	⊢ ( 𝜑 → 1 ∈ ( Base ‘ 𝑅 ) )
35	3	crnggrpd	⊢ ( 𝜑 → 𝑅 ∈ Grp )
36	32 9	grpidcl	⊢ ( 𝑅 ∈ Grp → 0 ∈ ( Base ‘ 𝑅 ) )
37	35 36	syl	⊢ ( 𝜑 → 0 ∈ ( Base ‘ 𝑅 ) )
38	34 37	ifcld	⊢ ( 𝜑 → if ( 𝑧 = 𝑦 , 1 , 0 ) ∈ ( Base ‘ 𝑅 ) )
39	38	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 ∈ 𝐷 ) → if ( 𝑧 = 𝑦 , 1 , 0 ) ∈ ( Base ‘ 𝑅 ) )
40		eqid	⊢ ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 = 𝑦 , 1 , 0 ) ) = ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 = 𝑦 , 1 , 0 ) )
41	39 40	fmptd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 = 𝑦 , 1 , 0 ) ) : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
42	28 31 41	elmapdd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 = 𝑦 , 1 , 0 ) ) ∈ ( ( Base ‘ 𝑅 ) ↑m 𝐷 ) )
43	5	psrbasfsupp	⊢ 𝐷 = { ℎ ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ ℎ “ ℕ ) ∈ Fin }
44	4	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → 𝐼 ∈ 𝑉 )
45	15 32 43 13 44	psrbas	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) = ( ( Base ‘ 𝑅 ) ↑m 𝐷 ) )
46	42 45	eleqtrrd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 = 𝑦 , 1 , 0 ) ) ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) )
47		velsn	⊢ ( 𝑧 ∈ { 𝑦 } ↔ 𝑧 = 𝑦 )
48	47	bicomi	⊢ ( 𝑧 = 𝑦 ↔ 𝑧 ∈ { 𝑦 } )
49	48	a1i	⊢ ( 𝑧 ∈ 𝐷 → ( 𝑧 = 𝑦 ↔ 𝑧 ∈ { 𝑦 } ) )
50	49	ifbid	⊢ ( 𝑧 ∈ 𝐷 → if ( 𝑧 = 𝑦 , 1 , 0 ) = if ( 𝑧 ∈ { 𝑦 } , 1 , 0 ) )
51	50	mpteq2ia	⊢ ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 = 𝑦 , 1 , 0 ) ) = ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 ∈ { 𝑦 } , 1 , 0 ) )
52		snfi	⊢ { 𝑦 } ∈ Fin
53	52	a1i	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → { 𝑦 } ∈ Fin )
54	8	fvexi	⊢ 1 ∈ V
55	54	a1i	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 ∈ { 𝑦 } ) → 1 ∈ V )
56	9	fvexi	⊢ 0 ∈ V
57	56	a1i	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → 0 ∈ V )
58	51 31 53 55 57	mptiffisupp	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 = 𝑦 , 1 , 0 ) ) finSupp 0 )
59	1 15 13 9 2	mplelbas	⊢ ( ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 = 𝑦 , 1 , 0 ) ) ∈ 𝐵 ↔ ( ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 = 𝑦 , 1 , 0 ) ) ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ∧ ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 = 𝑦 , 1 , 0 ) ) finSupp 0 ) )
60	46 58 59	sylanbrc	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐷 ) → ( 𝑧 ∈ 𝐷 ↦ if ( 𝑧 = 𝑦 , 1 , 0 ) ) ∈ 𝐵 )
61	60 11	fmptd	⊢ ( 𝜑 → 𝐺 : 𝐷 ⟶ 𝐵 )
62	61 7	fcod	⊢ ( 𝜑 → ( 𝐺 ∘ 𝐹 ) : 𝐴 ⟶ 𝐵 )
63	15 1 2 4 33	mplsubrg	⊢ ( 𝜑 → 𝐵 ∈ ( SubRing ‘ ( 𝐼 mPwSer 𝑅 ) ) )
64		eqid	⊢ ( 1r ‘ ( 𝐼 mPwSer 𝑅 ) ) = ( 1r ‘ ( 𝐼 mPwSer 𝑅 ) )
65	64	subrg1cl	⊢ ( 𝐵 ∈ ( SubRing ‘ ( 𝐼 mPwSer 𝑅 ) ) → ( 1r ‘ ( 𝐼 mPwSer 𝑅 ) ) ∈ 𝐵 )
66	63 65	syl	⊢ ( 𝜑 → ( 1r ‘ ( 𝐼 mPwSer 𝑅 ) ) ∈ 𝐵 )
67	15 4 33	psrring	⊢ ( 𝜑 → ( 𝐼 mPwSer 𝑅 ) ∈ Ring )
68	67	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ) → ( 𝐼 mPwSer 𝑅 ) ∈ Ring )
69		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ) → 𝑥 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) )
70	13 17 64 68 69	ringlidmd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ) → ( ( 1r ‘ ( 𝐼 mPwSer 𝑅 ) ) ( .r ‘ 𝑃 ) 𝑥 ) = 𝑥 )
71	13 17 64 68 69	ringridmd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ) → ( 𝑥 ( .r ‘ 𝑃 ) ( 1r ‘ ( 𝐼 mPwSer 𝑅 ) ) ) = 𝑥 )
72	70 71	jca	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ) → ( ( ( 1r ‘ ( 𝐼 mPwSer 𝑅 ) ) ( .r ‘ 𝑃 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( .r ‘ 𝑃 ) ( 1r ‘ ( 𝐼 mPwSer 𝑅 ) ) ) = 𝑥 ) )
73	14 18 24 25 6 27 62 66 72	gsumress	⊢ ( 𝜑 → ( ( mulGrp ‘ ( 𝐼 mPwSer 𝑅 ) ) Σg ( 𝐺 ∘ 𝐹 ) ) = ( 𝑀 Σg ( 𝐺 ∘ 𝐹 ) ) )
74	15 13 3 4 5 6 7 8 9 12 11	psrmonprod	⊢ ( 𝜑 → ( ( mulGrp ‘ ( 𝐼 mPwSer 𝑅 ) ) Σg ( 𝐺 ∘ 𝐹 ) ) = ( 𝐺 ‘ ( 𝑖 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑥 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) ) ) ) )
75	73 74	eqtr3d	⊢ ( 𝜑 → ( 𝑀 Σg ( 𝐺 ∘ 𝐹 ) ) = ( 𝐺 ‘ ( 𝑖 ∈ 𝐼 ↦ ( ℂfld Σg ( 𝑥 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) ) ) ) )