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

Definition df-ply1 16533
Description: Define the algebra of univariate polynomials. (Contributed by Mario Carneiro, 9-Feb-2015.)
Assertion
Ref Expression
df-ply1  |- Poly1  =  (
r  e.  _V  |->  ( (PwSer1 `  r )s  ( Base `  ( 1o mPoly  r )
) ) )

Detailed syntax breakdown of Definition df-ply1
StepHypRef Expression
1 cpl1 16526 . 2  class Poly1
2 vr . . 3  set  r
3 cvv 2916 . . 3  class  _V
42cv 1648 . . . . 5  class  r
5 cps1 16524 . . . . 5  class PwSer1
64, 5cfv 5413 . . . 4  class  (PwSer1 `  r
)
7 c1o 6676 . . . . . 6  class  1o
8 cmpl 16363 . . . . . 6  class mPoly
97, 4, 8co 6040 . . . . 5  class  ( 1o mPoly 
r )
10 cbs 13424 . . . . 5  class  Base
119, 10cfv 5413 . . . 4  class  ( Base `  ( 1o mPoly  r )
)
12 cress 13425 . . . 4  classs
136, 11, 12co 6040 . . 3  class  ( (PwSer1 `  r )s  ( Base `  ( 1o mPoly  r ) ) )
142, 3, 13cmpt 4226 . 2  class  ( r  e.  _V  |->  ( (PwSer1 `  r )s  ( Base `  ( 1o mPoly  r ) ) ) )
151, 14wceq 1649 1  wff Poly1  =  (
r  e.  _V  |->  ( (PwSer1 `  r )s  ( Base `  ( 1o mPoly  r )
) ) )
Colors of variables: wff set class
This definition is referenced by:  ply1val  16547
  Copyright terms: Public domain W3C validator