Definition df-mpl 22199

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). (Contributed by Mario Carneiro, 7-Jan-2015.) (Revised by AV, 25-Jun-2019.)

Assertion

Ref	Expression
df-mpl	⊢ mPoly = (𝑖 ∈ V, 𝑟 ∈ V ↦ ⦋(𝑖 mPwSer 𝑟) / 𝑤⦌(𝑤 ↾s {𝑓 ∈ (Base‘𝑤) ∣ 𝑓 finSupp (0g‘𝑟)}))

Distinct variable group:   𝑓,𝑖,𝑟,𝑤

Detailed syntax breakdown of Definition df-mpl

Step	Hyp	Ref	Expression
1		cmpl 22194	. 2 class mPoly
2		vi	. . 3 setvar 𝑖
3		vr	. . 3 setvar 𝑟
4		cvv 3451	. . 3 class V
5		vw	. . . 4 setvar 𝑤
6	2	cv 1569	. . . . 5 class 𝑖
7	3	cv 1569	. . . . 5 class 𝑟
8		cmps 22192	. . . . 5 class mPwSer
9	6, 7, 8	co 7412	. . . 4 class (𝑖 mPwSer 𝑟)
10	5	cv 1569	. . . . 5 class 𝑤
11		vf	. . . . . . . 8 setvar 𝑓
12	11	cv 1569	. . . . . . 7 class 𝑓
13		c0g 17590	. . . . . . . 8 class 0g
14	7, 13	cfv 6531	. . . . . . 7 class (0g‘𝑟)
15		cfsupp 9337	. . . . . . 7 class finSupp
16	12, 14, 15	wbr 5103	. . . . . 6 wff 𝑓 finSupp (0g‘𝑟)
17		cbs 17367	. . . . . . 7 class Base
18	10, 17	cfv 6531	. . . . . 6 class (Base‘𝑤)
19	16, 11, 18	crab 3413	. . . . 5 class {𝑓 ∈ (Base‘𝑤) ∣ 𝑓 finSupp (0g‘𝑟)}
20		cress 17388	. . . . 5 class ↾s
21	10, 19, 20	co 7412	. . . 4 class (𝑤 ↾s {𝑓 ∈ (Base‘𝑤) ∣ 𝑓 finSupp (0g‘𝑟)})
22	5, 9, 21	csb 3847	. . 3 class ⦋(𝑖 mPwSer 𝑟) / 𝑤⦌(𝑤 ↾s {𝑓 ∈ (Base‘𝑤) ∣ 𝑓 finSupp (0g‘𝑟)})
23	2, 3, 4, 4, 22	cmpo 7414	. 2 class (𝑖 ∈ V, 𝑟 ∈ V ↦ ⦋(𝑖 mPwSer 𝑟) / 𝑤⦌(𝑤 ↾s {𝑓 ∈ (Base‘𝑤) ∣ 𝑓 finSupp (0g‘𝑟)}))
24	1, 23	wceq 1570	1 wff mPoly = (𝑖 ∈ V, 𝑟 ∈ V ↦ ⦋(𝑖 mPwSer 𝑟) / 𝑤⦌(𝑤 ↾s {𝑓 ∈ (Base‘𝑤) ∣ 𝑓 finSupp (0g‘𝑟)}))

This definition is used by:  reldmmpl  22275  mplval  22276