Metamath Proof Explorer


Definition df-mpl

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)

Ref Expression
Assertion df-mpl mPoly = i V , r V i mPwSer r / w w 𝑠 f Base w | finSupp 0 r f

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmpl class mPoly
1 vi setvar i
2 cvv class V
3 vr setvar r
4 1 cv setvar i
5 cmps class mPwSer
6 3 cv setvar r
7 4 6 5 co class i mPwSer r
8 vw setvar w
9 8 cv setvar w
10 cress class 𝑠
11 vf setvar f
12 cbs class Base
13 9 12 cfv class Base w
14 11 cv setvar f
15 cfsupp class finSupp
16 c0g class 0 𝑔
17 6 16 cfv class 0 r
18 14 17 15 wbr wff finSupp 0 r f
19 18 11 13 crab class f Base w | finSupp 0 r f
20 9 19 10 co class w 𝑠 f Base w | finSupp 0 r f
21 8 7 20 csb class i mPwSer r / w w 𝑠 f Base w | finSupp 0 r f
22 1 3 2 2 21 cmpo class i V , r V i mPwSer r / w w 𝑠 f Base w | finSupp 0 r f
23 0 22 wceq wff mPoly = i V , r V i mPwSer r / w w 𝑠 f Base w | finSupp 0 r f