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

Definition df-ply1 16275
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 16268 . 2  class Poly1
2 vr . . 3  set  r
3 cvv 2801 . . 3  class  _V
42cv 1631 . . . . 5  class  r
5 cps1 16266 . . . . 5  class PwSer1
64, 5cfv 5271 . . . 4  class  (PwSer1 `  r
)
7 c1o 6488 . . . . . 6  class  1o
8 cmpl 16105 . . . . . 6  class mPoly
97, 4, 8co 5874 . . . . 5  class  ( 1o mPoly 
r )
10 cbs 13164 . . . . 5  class  Base
119, 10cfv 5271 . . . 4  class  ( Base `  ( 1o mPoly  r )
)
12 cress 13165 . . . 4  classs
136, 11, 12co 5874 . . 3  class  ( (PwSer1 `  r )s  ( Base `  ( 1o mPoly  r ) ) )
142, 3, 13cmpt 4093 . 2  class  ( r  e.  _V  |->  ( (PwSer1 `  r )s  ( Base `  ( 1o mPoly  r ) ) ) )
151, 14wceq 1632 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  16289
  Copyright terms: Public domain W3C validator