Metamath Proof Explorer

Definition df-psr1

Description: Define the algebra of univariate power series. (Contributed by Mario Carneiro, 29-Dec-2014)

Ref Expression
Assertion df-psr1 
|- PwSer1 = ( r e. _V |-> ( ( 1o ordPwSer r ) ` (/) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cps1 
 |-  PwSer1
1 vr 
 |-  r
2 cvv 
 |-  _V
3 c1o 
 |-  1o
4 copws 
 |-  ordPwSer
5 1 cv 
 |-  r
6 3 5 4 co 
 |-  ( 1o ordPwSer r )
7 c0 
 |-  (/)
8 7 6 cfv 
 |-  ( ( 1o ordPwSer r ) ` (/) )
9 1 2 8 cmpt 
 |-  ( r e. _V |-> ( ( 1o ordPwSer r ) ` (/) ) )
10 0 9 wceq 
 |-  PwSer1 = ( r e. _V |-> ( ( 1o ordPwSer r ) ` (/) ) )