Definition df-mpl 19179

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 19174	. 2 class mPoly
2		vi	. . 3 setvar 𝑖
3		vr	. . 3 setvar 𝑟
4		cvv 3173	. . 3 class V
5		vw	. . . 4 setvar 𝑤
6	2	cv 1474	. . . . 5 class 𝑖
7	3	cv 1474	. . . . 5 class 𝑟
8		cmps 19172	. . . . 5 class mPwSer
9	6, 7, 8	co 6549	. . . 4 class (𝑖 mPwSer 𝑟)
10	5	cv 1474	. . . . 5 class 𝑤
11		vf	. . . . . . . 8 setvar 𝑓
12	11	cv 1474	. . . . . . 7 class 𝑓
13		c0g 15923	. . . . . . . 8 class 0g
14	7, 13	cfv 5804	. . . . . . 7 class (0g‘𝑟)
15		cfsupp 8158	. . . . . . 7 class finSupp
16	12, 14, 15	wbr 4583	. . . . . 6 wff 𝑓 finSupp (0g‘𝑟)
17		cbs 15695	. . . . . . 7 class Base
18	10, 17	cfv 5804	. . . . . 6 class (Base‘𝑤)
19	16, 11, 18	crab 2900	. . . . 5 class {𝑓 ∈ (Base‘𝑤) ∣ 𝑓 finSupp (0g‘𝑟)}
20		cress 15696	. . . . 5 class ↾s
21	10, 19, 20	co 6549	. . . 4 class (𝑤 ↾s {𝑓 ∈ (Base‘𝑤) ∣ 𝑓 finSupp (0g‘𝑟)})
22	5, 9, 21	csb 3499	. . 3 class ⦋(𝑖 mPwSer 𝑟) / 𝑤⦌(𝑤 ↾s {𝑓 ∈ (Base‘𝑤) ∣ 𝑓 finSupp (0g‘𝑟)})
23	2, 3, 4, 4, 22	cmpt2 6551	. 2 class (𝑖 ∈ V, 𝑟 ∈ V ↦ ⦋(𝑖 mPwSer 𝑟) / 𝑤⦌(𝑤 ↾s {𝑓 ∈ (Base‘𝑤) ∣ 𝑓 finSupp (0g‘𝑟)}))
24	1, 23	wceq 1475	1 wff mPoly = (𝑖 ∈ V, 𝑟 ∈ V ↦ ⦋(𝑖 mPwSer 𝑟) / 𝑤⦌(𝑤 ↾s {𝑓 ∈ (Base‘𝑤) ∣ 𝑓 finSupp (0g‘𝑟)}))

This definition is referenced by:  reldmmpl  19248  mplval  19249