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