Definition df-mplcoe 14593

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 14591	. 2 class mPoly
2		vi	. . 3 setvar 𝑖
3		vr	. . 3 setvar 𝑟
4		cvv 2779	. . 3 class V
5		vw	. . . 4 setvar 𝑤
6	2	cv 1374	. . . . 5 class 𝑖
7	3	cv 1374	. . . . 5 class 𝑟
8		cmps 14590	. . . . 5 class mPwSer
9	6, 7, 8	co 5974	. . . 4 class (𝑖 mPwSer 𝑟)
10	5	cv 1374	. . . . 5 class 𝑤
11		vk	. . . . . . . . . . . . 13 setvar 𝑘
12	11	cv 1374	. . . . . . . . . . . 12 class 𝑘
13		va	. . . . . . . . . . . . 13 setvar 𝑎
14	13	cv 1374	. . . . . . . . . . . 12 class 𝑎
15	12, 14	cfv 5294	. . . . . . . . . . 11 class (𝑎‘𝑘)
16		vb	. . . . . . . . . . . . 13 setvar 𝑏
17	16	cv 1374	. . . . . . . . . . . 12 class 𝑏
18	12, 17	cfv 5294	. . . . . . . . . . 11 class (𝑏‘𝑘)
19		clt 8149	. . . . . . . . . . 11 class <
20	15, 18, 19	wbr 4062	. . . . . . . . . 10 wff (𝑎‘𝑘) < (𝑏‘𝑘)
21	20, 11, 6	wral 2488	. . . . . . . . 9 wff ∀𝑘 ∈ 𝑖 (𝑎‘𝑘) < (𝑏‘𝑘)
22		vf	. . . . . . . . . . . 12 setvar 𝑓
23	22	cv 1374	. . . . . . . . . . 11 class 𝑓
24	17, 23	cfv 5294	. . . . . . . . . 10 class (𝑓‘𝑏)
25		c0g 13255	. . . . . . . . . . 11 class 0g
26	7, 25	cfv 5294	. . . . . . . . . 10 class (0g‘𝑟)
27	24, 26	wceq 1375	. . . . . . . . 9 wff (𝑓‘𝑏) = (0g‘𝑟)
28	21, 27	wi 4	. . . . . . . 8 wff (∀𝑘 ∈ 𝑖 (𝑎‘𝑘) < (𝑏‘𝑘) → (𝑓‘𝑏) = (0g‘𝑟))
29		cn0 9337	. . . . . . . . 9 class ℕ0
30		cmap 6765	. . . . . . . . 9 class ↑𝑚
31	29, 6, 30	co 5974	. . . . . . . 8 class (ℕ0 ↑𝑚 𝑖)
32	28, 16, 31	wral 2488	. . . . . . 7 wff ∀𝑏 ∈ (ℕ0 ↑𝑚 𝑖)(∀𝑘 ∈ 𝑖 (𝑎‘𝑘) < (𝑏‘𝑘) → (𝑓‘𝑏) = (0g‘𝑟))
33	32, 13, 31	wrex 2489	. . . . . 6 wff ∃𝑎 ∈ (ℕ0 ↑𝑚 𝑖)∀𝑏 ∈ (ℕ0 ↑𝑚 𝑖)(∀𝑘 ∈ 𝑖 (𝑎‘𝑘) < (𝑏‘𝑘) → (𝑓‘𝑏) = (0g‘𝑟))
34		cbs 12998	. . . . . . 7 class Base
35	10, 34	cfv 5294	. . . . . 6 class (Base‘𝑤)
36	33, 22, 35	crab 2492	. . . . 5 class {𝑓 ∈ (Base‘𝑤) ∣ ∃𝑎 ∈ (ℕ0 ↑𝑚 𝑖)∀𝑏 ∈ (ℕ0 ↑𝑚 𝑖)(∀𝑘 ∈ 𝑖 (𝑎‘𝑘) < (𝑏‘𝑘) → (𝑓‘𝑏) = (0g‘𝑟))}
37		cress 12999	. . . . 5 class ↾s
38	10, 36, 37	co 5974	. . . 4 class (𝑤 ↾s {𝑓 ∈ (Base‘𝑤) ∣ ∃𝑎 ∈ (ℕ0 ↑𝑚 𝑖)∀𝑏 ∈ (ℕ0 ↑𝑚 𝑖)(∀𝑘 ∈ 𝑖 (𝑎‘𝑘) < (𝑏‘𝑘) → (𝑓‘𝑏) = (0g‘𝑟))})
39	5, 9, 38	csb 3104	. . 3 class ⦋(𝑖 mPwSer 𝑟) / 𝑤⦌(𝑤 ↾s {𝑓 ∈ (Base‘𝑤) ∣ ∃𝑎 ∈ (ℕ0 ↑𝑚 𝑖)∀𝑏 ∈ (ℕ0 ↑𝑚 𝑖)(∀𝑘 ∈ 𝑖 (𝑎‘𝑘) < (𝑏‘𝑘) → (𝑓‘𝑏) = (0g‘𝑟))})
40	2, 3, 4, 4, 39	cmpo 5976	. 2 class (𝑖 ∈ V, 𝑟 ∈ V ↦ ⦋(𝑖 mPwSer 𝑟) / 𝑤⦌(𝑤 ↾s {𝑓 ∈ (Base‘𝑤) ∣ ∃𝑎 ∈ (ℕ0 ↑𝑚 𝑖)∀𝑏 ∈ (ℕ0 ↑𝑚 𝑖)(∀𝑘 ∈ 𝑖 (𝑎‘𝑘) < (𝑏‘𝑘) → (𝑓‘𝑏) = (0g‘𝑟))}))
41	1, 40	wceq 1375	1 wff mPoly = (𝑖 ∈ V, 𝑟 ∈ V ↦ ⦋(𝑖 mPwSer 𝑟) / 𝑤⦌(𝑤 ↾s {𝑓 ∈ (Base‘𝑤) ∣ ∃𝑎 ∈ (ℕ0 ↑𝑚 𝑖)∀𝑏 ∈ (ℕ0 ↑𝑚 𝑖)(∀𝑘 ∈ 𝑖 (𝑎‘𝑘) < (𝑏‘𝑘) → (𝑓‘𝑏) = (0g‘𝑟))}))

This definition is referenced by:  reldmmpl  14618  mplvalcoe  14619  fnmpl  14622