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

Definition df-ply1 16580
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 16573 . 2  class Poly1
2 vr . . 3  set  r
3 cvv 2958 . . 3  class  _V
42cv 1652 . . . . 5  class  r
5 cps1 16571 . . . . 5  class PwSer1
64, 5cfv 5456 . . . 4  class  (PwSer1 `  r
)
7 c1o 6719 . . . . . 6  class  1o
8 cmpl 16410 . . . . . 6  class mPoly
97, 4, 8co 6083 . . . . 5  class  ( 1o mPoly 
r )
10 cbs 13471 . . . . 5  class  Base
119, 10cfv 5456 . . . 4  class  ( Base `  ( 1o mPoly  r )
)
12 cress 13472 . . . 4  classs
136, 11, 12co 6083 . . 3  class  ( (PwSer1 `  r )s  ( Base `  ( 1o mPoly  r ) ) )
142, 3, 13cmpt 4268 . 2  class  ( r  e.  _V  |->  ( (PwSer1 `  r )s  ( Base `  ( 1o mPoly  r ) ) ) )
151, 14wceq 1653 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  16594
  Copyright terms: Public domain W3C validator