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