MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-mpl Structured version   Visualization version   GIF version

Definition df-mpl 19561
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.)
Assertion
Ref Expression
df-mpl mPoly = (𝑖 ∈ V, 𝑟 ∈ V ↦ (𝑖 mPwSer 𝑟) / 𝑤(𝑤s {𝑓 ∈ (Base‘𝑤) ∣ 𝑓 finSupp (0g𝑟)}))
Distinct variable group:   𝑓,𝑖,𝑟,𝑤

Detailed syntax breakdown of Definition df-mpl
StepHypRef Expression
1 cmpl 19556 . 2 class mPoly
2 vi . . 3 setvar 𝑖
3 vr . . 3 setvar 𝑟
4 cvv 3387 . . 3 class V
5 vw . . . 4 setvar 𝑤
62cv 1636 . . . . 5 class 𝑖
73cv 1636 . . . . 5 class 𝑟
8 cmps 19554 . . . . 5 class mPwSer
96, 7, 8co 6868 . . . 4 class (𝑖 mPwSer 𝑟)
105cv 1636 . . . . 5 class 𝑤
11 vf . . . . . . . 8 setvar 𝑓
1211cv 1636 . . . . . . 7 class 𝑓
13 c0g 16299 . . . . . . . 8 class 0g
147, 13cfv 6095 . . . . . . 7 class (0g𝑟)
15 cfsupp 8508 . . . . . . 7 class finSupp
1612, 14, 15wbr 4837 . . . . . 6 wff 𝑓 finSupp (0g𝑟)
17 cbs 16062 . . . . . . 7 class Base
1810, 17cfv 6095 . . . . . 6 class (Base‘𝑤)
1916, 11, 18crab 3096 . . . . 5 class {𝑓 ∈ (Base‘𝑤) ∣ 𝑓 finSupp (0g𝑟)}
20 cress 16063 . . . . 5 class s
2110, 19, 20co 6868 . . . 4 class (𝑤s {𝑓 ∈ (Base‘𝑤) ∣ 𝑓 finSupp (0g𝑟)})
225, 9, 21csb 3722 . . 3 class (𝑖 mPwSer 𝑟) / 𝑤(𝑤s {𝑓 ∈ (Base‘𝑤) ∣ 𝑓 finSupp (0g𝑟)})
232, 3, 4, 4, 22cmpt2 6870 . 2 class (𝑖 ∈ V, 𝑟 ∈ V ↦ (𝑖 mPwSer 𝑟) / 𝑤(𝑤s {𝑓 ∈ (Base‘𝑤) ∣ 𝑓 finSupp (0g𝑟)}))
241, 23wceq 1637 1 wff mPoly = (𝑖 ∈ V, 𝑟 ∈ V ↦ (𝑖 mPwSer 𝑟) / 𝑤(𝑤s {𝑓 ∈ (Base‘𝑤) ∣ 𝑓 finSupp (0g𝑟)}))
Colors of variables: wff setvar class
This definition is referenced by:  reldmmpl  19630  mplval  19631
  Copyright terms: Public domain W3C validator