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 e. _V , r e. _V |-> [_ ( i mPwSer r ) / w ]_ ( w |`s { f e. ( Base ` w ) | f finSupp ( 0g ` r ) } ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
0 | cmpl | |- mPoly |
|
1 | vi | |- i |
|
2 | cvv | |- _V |
|
3 | vr | |- r |
|
4 | 1 | cv | |- i |
5 | cmps | |- mPwSer |
|
6 | 3 | cv | |- r |
7 | 4 6 5 | co | |- ( i mPwSer r ) |
8 | vw | |- w |
|
9 | 8 | cv | |- w |
10 | cress | |- |`s |
|
11 | vf | |- f |
|
12 | cbs | |- Base |
|
13 | 9 12 | cfv | |- ( Base ` w ) |
14 | 11 | cv | |- f |
15 | cfsupp | |- finSupp |
|
16 | c0g | |- 0g |
|
17 | 6 16 | cfv | |- ( 0g ` r ) |
18 | 14 17 15 | wbr | |- f finSupp ( 0g ` r ) |
19 | 18 11 13 | crab | |- { f e. ( Base ` w ) | f finSupp ( 0g ` r ) } |
20 | 9 19 10 | co | |- ( w |`s { f e. ( Base ` w ) | f finSupp ( 0g ` r ) } ) |
21 | 8 7 20 | csb | |- [_ ( i mPwSer r ) / w ]_ ( w |`s { f e. ( Base ` w ) | f finSupp ( 0g ` r ) } ) |
22 | 1 3 2 2 21 | cmpo | |- ( i e. _V , r e. _V |-> [_ ( i mPwSer r ) / w ]_ ( w |`s { f e. ( Base ` w ) | f finSupp ( 0g ` r ) } ) ) |
23 | 0 22 | wceq | |- mPoly = ( i e. _V , r e. _V |-> [_ ( i mPwSer r ) / w ]_ ( w |`s { f e. ( Base ` w ) | f finSupp ( 0g ` r ) } ) ) |