Definition df-mplcoe 14649

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 14647	. 2 class mPoly
2		vi	. . 3 setvar 𝑖
3		vr	. . 3 setvar 𝑟
4		cvv 2799	. . 3 class V
5		vw	. . . 4 setvar 𝑤
6	2	cv 1394	. . . . 5 class 𝑖
7	3	cv 1394	. . . . 5 class 𝑟
8		cmps 14646	. . . . 5 class mPwSer
9	6, 7, 8	co 6010	. . . 4 class (𝑖 mPwSer 𝑟)
10	5	cv 1394	. . . . 5 class 𝑤
11		vk	. . . . . . . . . . . . 13 setvar 𝑘
12	11	cv 1394	. . . . . . . . . . . 12 class 𝑘
13		va	. . . . . . . . . . . . 13 setvar 𝑎
14	13	cv 1394	. . . . . . . . . . . 12 class 𝑎
15	12, 14	cfv 5321	. . . . . . . . . . 11 class (𝑎‘𝑘)
16		vb	. . . . . . . . . . . . 13 setvar 𝑏
17	16	cv 1394	. . . . . . . . . . . 12 class 𝑏
18	12, 17	cfv 5321	. . . . . . . . . . 11 class (𝑏‘𝑘)
19		clt 8197	. . . . . . . . . . 11 class <
20	15, 18, 19	wbr 4083	. . . . . . . . . 10 wff (𝑎‘𝑘) < (𝑏‘𝑘)
21	20, 11, 6	wral 2508	. . . . . . . . 9 wff ∀𝑘 ∈ 𝑖 (𝑎‘𝑘) < (𝑏‘𝑘)
22		vf	. . . . . . . . . . . 12 setvar 𝑓
23	22	cv 1394	. . . . . . . . . . 11 class 𝑓
24	17, 23	cfv 5321	. . . . . . . . . 10 class (𝑓‘𝑏)
25		c0g 13310	. . . . . . . . . . 11 class 0g
26	7, 25	cfv 5321	. . . . . . . . . 10 class (0g‘𝑟)
27	24, 26	wceq 1395	. . . . . . . . 9 wff (𝑓‘𝑏) = (0g‘𝑟)
28	21, 27	wi 4	. . . . . . . 8 wff (∀𝑘 ∈ 𝑖 (𝑎‘𝑘) < (𝑏‘𝑘) → (𝑓‘𝑏) = (0g‘𝑟))
29		cn0 9385	. . . . . . . . 9 class ℕ0
30		cmap 6808	. . . . . . . . 9 class ↑𝑚
31	29, 6, 30	co 6010	. . . . . . . 8 class (ℕ0 ↑𝑚 𝑖)
32	28, 16, 31	wral 2508	. . . . . . 7 wff ∀𝑏 ∈ (ℕ0 ↑𝑚 𝑖)(∀𝑘 ∈ 𝑖 (𝑎‘𝑘) < (𝑏‘𝑘) → (𝑓‘𝑏) = (0g‘𝑟))
33	32, 13, 31	wrex 2509	. . . . . 6 wff ∃𝑎 ∈ (ℕ0 ↑𝑚 𝑖)∀𝑏 ∈ (ℕ0 ↑𝑚 𝑖)(∀𝑘 ∈ 𝑖 (𝑎‘𝑘) < (𝑏‘𝑘) → (𝑓‘𝑏) = (0g‘𝑟))
34		cbs 13053	. . . . . . 7 class Base
35	10, 34	cfv 5321	. . . . . 6 class (Base‘𝑤)
36	33, 22, 35	crab 2512	. . . . 5 class {𝑓 ∈ (Base‘𝑤) ∣ ∃𝑎 ∈ (ℕ0 ↑𝑚 𝑖)∀𝑏 ∈ (ℕ0 ↑𝑚 𝑖)(∀𝑘 ∈ 𝑖 (𝑎‘𝑘) < (𝑏‘𝑘) → (𝑓‘𝑏) = (0g‘𝑟))}
37		cress 13054	. . . . 5 class ↾s
38	10, 36, 37	co 6010	. . . 4 class (𝑤 ↾s {𝑓 ∈ (Base‘𝑤) ∣ ∃𝑎 ∈ (ℕ0 ↑𝑚 𝑖)∀𝑏 ∈ (ℕ0 ↑𝑚 𝑖)(∀𝑘 ∈ 𝑖 (𝑎‘𝑘) < (𝑏‘𝑘) → (𝑓‘𝑏) = (0g‘𝑟))})
39	5, 9, 38	csb 3124	. . 3 class ⦋(𝑖 mPwSer 𝑟) / 𝑤⦌(𝑤 ↾s {𝑓 ∈ (Base‘𝑤) ∣ ∃𝑎 ∈ (ℕ0 ↑𝑚 𝑖)∀𝑏 ∈ (ℕ0 ↑𝑚 𝑖)(∀𝑘 ∈ 𝑖 (𝑎‘𝑘) < (𝑏‘𝑘) → (𝑓‘𝑏) = (0g‘𝑟))})
40	2, 3, 4, 4, 39	cmpo 6012	. 2 class (𝑖 ∈ V, 𝑟 ∈ V ↦ ⦋(𝑖 mPwSer 𝑟) / 𝑤⦌(𝑤 ↾s {𝑓 ∈ (Base‘𝑤) ∣ ∃𝑎 ∈ (ℕ0 ↑𝑚 𝑖)∀𝑏 ∈ (ℕ0 ↑𝑚 𝑖)(∀𝑘 ∈ 𝑖 (𝑎‘𝑘) < (𝑏‘𝑘) → (𝑓‘𝑏) = (0g‘𝑟))}))
41	1, 40	wceq 1395	1 wff mPoly = (𝑖 ∈ V, 𝑟 ∈ V ↦ ⦋(𝑖 mPwSer 𝑟) / 𝑤⦌(𝑤 ↾s {𝑓 ∈ (Base‘𝑤) ∣ ∃𝑎 ∈ (ℕ0 ↑𝑚 𝑖)∀𝑏 ∈ (ℕ0 ↑𝑚 𝑖)(∀𝑘 ∈ 𝑖 (𝑎‘𝑘) < (𝑏‘𝑘) → (𝑓‘𝑏) = (0g‘𝑟))}))

This definition is referenced by:  reldmmpl  14674  mplvalcoe  14675  fnmpl  14678