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 = ( 𝑖 ∈ V , 𝑟 ∈ V ↦ ( 𝑖 mPwSer 𝑟 ) / 𝑤 ( 𝑤s { 𝑓 ∈ ( Base ‘ 𝑤 ) ∣ 𝑓 finSupp ( 0g𝑟 ) } ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmpl mPoly
1 vi 𝑖
2 cvv V
3 vr 𝑟
4 1 cv 𝑖
5 cmps mPwSer
6 3 cv 𝑟
7 4 6 5 co ( 𝑖 mPwSer 𝑟 )
8 vw 𝑤
9 8 cv 𝑤
10 cress s
11 vf 𝑓
12 cbs Base
13 9 12 cfv ( Base ‘ 𝑤 )
14 11 cv 𝑓
15 cfsupp finSupp
16 c0g 0g
17 6 16 cfv ( 0g𝑟 )
18 14 17 15 wbr 𝑓 finSupp ( 0g𝑟 )
19 18 11 13 crab { 𝑓 ∈ ( Base ‘ 𝑤 ) ∣ 𝑓 finSupp ( 0g𝑟 ) }
20 9 19 10 co ( 𝑤s { 𝑓 ∈ ( Base ‘ 𝑤 ) ∣ 𝑓 finSupp ( 0g𝑟 ) } )
21 8 7 20 csb ( 𝑖 mPwSer 𝑟 ) / 𝑤 ( 𝑤s { 𝑓 ∈ ( Base ‘ 𝑤 ) ∣ 𝑓 finSupp ( 0g𝑟 ) } )
22 1 3 2 2 21 cmpo ( 𝑖 ∈ V , 𝑟 ∈ V ↦ ( 𝑖 mPwSer 𝑟 ) / 𝑤 ( 𝑤s { 𝑓 ∈ ( Base ‘ 𝑤 ) ∣ 𝑓 finSupp ( 0g𝑟 ) } ) )
23 0 22 wceq mPoly = ( 𝑖 ∈ V , 𝑟 ∈ V ↦ ( 𝑖 mPwSer 𝑟 ) / 𝑤 ( 𝑤s { 𝑓 ∈ ( Base ‘ 𝑤 ) ∣ 𝑓 finSupp ( 0g𝑟 ) } ) )