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

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 ⊢ 𝑃 = ( 𝐼 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 ( 𝑥 ∈ 𝐴 ↦ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑖 ) ) ) ) ) )