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

Definition df-ply1 19322
Description: Define the algebra of univariate polynomials. (Contributed by Mario Carneiro, 9-Feb-2015.)
Assertion
Ref Expression
df-ply1 Poly1 = (𝑟 ∈ V ↦ ((PwSer1𝑟) ↾s (Base‘(1𝑜 mPoly 𝑟))))

Detailed syntax breakdown of Definition df-ply1
StepHypRef Expression
1 cpl1 19317 . 2 class Poly1
2 vr . . 3 setvar 𝑟
3 cvv 3173 . . 3 class V
42cv 1474 . . . . 5 class 𝑟
5 cps1 19315 . . . . 5 class PwSer1
64, 5cfv 5790 . . . 4 class (PwSer1𝑟)
7 c1o 7418 . . . . . 6 class 1𝑜
8 cmpl 19123 . . . . . 6 class mPoly
97, 4, 8co 6527 . . . . 5 class (1𝑜 mPoly 𝑟)
10 cbs 15644 . . . . 5 class Base
119, 10cfv 5790 . . . 4 class (Base‘(1𝑜 mPoly 𝑟))
12 cress 15645 . . . 4 class s
136, 11, 12co 6527 . . 3 class ((PwSer1𝑟) ↾s (Base‘(1𝑜 mPoly 𝑟)))
142, 3, 13cmpt 4638 . 2 class (𝑟 ∈ V ↦ ((PwSer1𝑟) ↾s (Base‘(1𝑜 mPoly 𝑟))))
151, 14wceq 1475 1 wff Poly1 = (𝑟 ∈ V ↦ ((PwSer1𝑟) ↾s (Base‘(1𝑜 mPoly 𝑟))))
Colors of variables: wff setvar class
This definition is referenced by:  ply1val  19334
  Copyright terms: Public domain W3C validator