Definition df-mplcoe 15050

Description: Define the subalgebra of the power series algebra generated by the variables; this is the polynomial algebra (the set of power series with finite degree).

The index set (which has an element for each variable) is 𝑖, the coefficients are in ring 𝑟, and for each variable there is a "degree" such that the coefficient is zero for a term where the powers are all greater than those degrees. (Degree is in quotes because there is no guarantee that coefficients below that degree are nonzero, as we do not assume decidable equality for 𝑟). (Contributed by Mario Carneiro, 7-Jan-2015.) (Revised by AV, 25-Jun-2019.) (Revised by Jim Kingdon, 7-Oct-2025.)

Assertion

Ref	Expression
df-mplcoe	⊢ mPoly = (𝑖 ∈ V, 𝑟 ∈ V ↦ ⦋(𝑖 mPwSer 𝑟) / 𝑤⦌(𝑤 ↾s {𝑓 ∈ (Base‘𝑤) ∣ ∃𝑎 ∈ (ℕ0 ↑𝑚 𝑖)∀𝑏 ∈ (ℕ0 ↑𝑚 𝑖)(∀𝑘 ∈ 𝑖 (𝑎‘𝑘) < (𝑏‘𝑘) → (𝑓‘𝑏) = (0g‘𝑟))}))

Distinct variable group:   𝑎,𝑏,𝑓,𝑖,𝑘,𝑟,𝑤

Detailed syntax breakdown of Definition df-mplcoe

Step	Hyp	Ref	Expression
1		cmpl 15048	. 2 class mPoly
2		vi	. . 3 setvar 𝑖
3		vr	. . 3 setvar 𝑟
4		cvv 2821	. . 3 class V
5		vw	. . . 4 setvar 𝑤
6	2	cv 1401	. . . . 5 class 𝑖
7	3	cv 1401	. . . . 5 class 𝑟
8		cmps 15047	. . . . 5 class mPwSer
9	6, 7, 8	co 6085	. . . 4 class (𝑖 mPwSer 𝑟)
10	5	cv 1401	. . . . 5 class 𝑤
11		vk	. . . . . . . . . . . . 13 setvar 𝑘
12	11	cv 1401	. . . . . . . . . . . 12 class 𝑘
13		va	. . . . . . . . . . . . 13 setvar 𝑎
14	13	cv 1401	. . . . . . . . . . . 12 class 𝑎
15	12, 14	cfv 5377	. . . . . . . . . . 11 class (𝑎‘𝑘)
16		vb	. . . . . . . . . . . . 13 setvar 𝑏
17	16	cv 1401	. . . . . . . . . . . 12 class 𝑏
18	12, 17	cfv 5377	. . . . . . . . . . 11 class (𝑏‘𝑘)
19		clt 8360	. . . . . . . . . . 11 class <
20	15, 18, 19	wbr 4130	. . . . . . . . . 10 wff (𝑎‘𝑘) < (𝑏‘𝑘)
21	20, 11, 6	wral 2528	. . . . . . . . 9 wff ∀𝑘 ∈ 𝑖 (𝑎‘𝑘) < (𝑏‘𝑘)
22		vf	. . . . . . . . . . . 12 setvar 𝑓
23	22	cv 1401	. . . . . . . . . . 11 class 𝑓
24	17, 23	cfv 5377	. . . . . . . . . 10 class (𝑓‘𝑏)
25		c0g 13612	. . . . . . . . . . 11 class 0g
26	7, 25	cfv 5377	. . . . . . . . . 10 class (0g‘𝑟)
27	24, 26	wceq 1402	. . . . . . . . 9 wff (𝑓‘𝑏) = (0g‘𝑟)
28	21, 27	wi 4	. . . . . . . 8 wff (∀𝑘 ∈ 𝑖 (𝑎‘𝑘) < (𝑏‘𝑘) → (𝑓‘𝑏) = (0g‘𝑟))
29		cn0 9565	. . . . . . . . 9 class ℕ0
30		cmap 6922	. . . . . . . . 9 class ↑𝑚
31	29, 6, 30	co 6085	. . . . . . . 8 class (ℕ0 ↑𝑚 𝑖)
32	28, 16, 31	wral 2528	. . . . . . 7 wff ∀𝑏 ∈ (ℕ0 ↑𝑚 𝑖)(∀𝑘 ∈ 𝑖 (𝑎‘𝑘) < (𝑏‘𝑘) → (𝑓‘𝑏) = (0g‘𝑟))
33	32, 13, 31	wrex 2529	. . . . . 6 wff ∃𝑎 ∈ (ℕ0 ↑𝑚 𝑖)∀𝑏 ∈ (ℕ0 ↑𝑚 𝑖)(∀𝑘 ∈ 𝑖 (𝑎‘𝑘) < (𝑏‘𝑘) → (𝑓‘𝑏) = (0g‘𝑟))
34		cbs 13354	. . . . . . 7 class Base
35	10, 34	cfv 5377	. . . . . 6 class (Base‘𝑤)
36	33, 22, 35	crab 2532	. . . . 5 class {𝑓 ∈ (Base‘𝑤) ∣ ∃𝑎 ∈ (ℕ0 ↑𝑚 𝑖)∀𝑏 ∈ (ℕ0 ↑𝑚 𝑖)(∀𝑘 ∈ 𝑖 (𝑎‘𝑘) < (𝑏‘𝑘) → (𝑓‘𝑏) = (0g‘𝑟))}
37		cress 13355	. . . . 5 class ↾s
38	10, 36, 37	co 6085	. . . 4 class (𝑤 ↾s {𝑓 ∈ (Base‘𝑤) ∣ ∃𝑎 ∈ (ℕ0 ↑𝑚 𝑖)∀𝑏 ∈ (ℕ0 ↑𝑚 𝑖)(∀𝑘 ∈ 𝑖 (𝑎‘𝑘) < (𝑏‘𝑘) → (𝑓‘𝑏) = (0g‘𝑟))})
39	5, 9, 38	csb 3147	. . 3 class ⦋(𝑖 mPwSer 𝑟) / 𝑤⦌(𝑤 ↾s {𝑓 ∈ (Base‘𝑤) ∣ ∃𝑎 ∈ (ℕ0 ↑𝑚 𝑖)∀𝑏 ∈ (ℕ0 ↑𝑚 𝑖)(∀𝑘 ∈ 𝑖 (𝑎‘𝑘) < (𝑏‘𝑘) → (𝑓‘𝑏) = (0g‘𝑟))})
40	2, 3, 4, 4, 39	cmpo 6087	. 2 class (𝑖 ∈ V, 𝑟 ∈ V ↦ ⦋(𝑖 mPwSer 𝑟) / 𝑤⦌(𝑤 ↾s {𝑓 ∈ (Base‘𝑤) ∣ ∃𝑎 ∈ (ℕ0 ↑𝑚 𝑖)∀𝑏 ∈ (ℕ0 ↑𝑚 𝑖)(∀𝑘 ∈ 𝑖 (𝑎‘𝑘) < (𝑏‘𝑘) → (𝑓‘𝑏) = (0g‘𝑟))}))
41	1, 40	wceq 1402	1 wff mPoly = (𝑖 ∈ V, 𝑟 ∈ V ↦ ⦋(𝑖 mPwSer 𝑟) / 𝑤⦌(𝑤 ↾s {𝑓 ∈ (Base‘𝑤) ∣ ∃𝑎 ∈ (ℕ0 ↑𝑚 𝑖)∀𝑏 ∈ (ℕ0 ↑𝑚 𝑖)(∀𝑘 ∈ 𝑖 (𝑎‘𝑘) < (𝑏‘𝑘) → (𝑓‘𝑏) = (0g‘𝑟))}))

This definition is used by:  reldmmpl  15082  mplvalcoe  15083  fnmpl  15086