This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ‘ 𝑟 ) } ) )