Metamath Proof Explorer

Theorem ply1subrg

Description: Univariate polynomials form a subring of the set of univariate power series. (Contributed by Mario Carneiro, 9-Feb-2015)

Ref Expression
Hypotheses ply1val.1 
|- P = ( Poly1 ` R )
ply1val.2 
|- S = ( PwSer1 ` R )
ply1bas.u 
|- U = ( Base ` P )
Assertion ply1subrg 
|- ( R e. Ring -> U e. ( SubRing ` S ) )

Proof

Step Hyp Ref Expression
1 ply1val.1 
 |-  P = ( Poly1 ` R )
2 ply1val.2 
 |-  S = ( PwSer1 ` R )
3 ply1bas.u 
 |-  U = ( Base ` P )
4 eqid 
 |-  ( 1o mPwSer R ) = ( 1o mPwSer R )
5 eqid 
 |-  ( 1o mPoly R ) = ( 1o mPoly R )
6 1 2 3 ply1bas 
 |-  U = ( Base ` ( 1o mPoly R ) )
7 1on 
 |-  1o e. On
8 7 a1i 
 |-  ( R e. Ring -> 1o e. On )
9 id 
 |-  ( R e. Ring -> R e. Ring )
10 4 5 6 8 9 mplsubrg 
 |-  ( R e. Ring -> U e. ( SubRing ` ( 1o mPwSer R ) ) )
11 eqidd 
 |-  ( R e. Ring -> ( Base ` ( 1o mPwSer R ) ) = ( Base ` ( 1o mPwSer R ) ) )
12 2 psr1val 
 |-  S = ( ( 1o ordPwSer R ) ` (/) )
13 0ss 
 |-  (/) C_ ( 1o X. 1o )
14 13 a1i 
 |-  ( R e. Ring -> (/) C_ ( 1o X. 1o ) )
15 4 12 14 opsrbas 
 |-  ( R e. Ring -> ( Base ` ( 1o mPwSer R ) ) = ( Base ` S ) )
16 4 12 14 opsrplusg 
 |-  ( R e. Ring -> ( +g ` ( 1o mPwSer R ) ) = ( +g ` S ) )
17 16 oveqdr 
 |-  ( ( R e. Ring /\ ( x e. ( Base ` ( 1o mPwSer R ) ) /\ y e. ( Base ` ( 1o mPwSer R ) ) ) ) -> ( x ( +g ` ( 1o mPwSer R ) ) y ) = ( x ( +g ` S ) y ) )
18 4 12 14 opsrmulr 
 |-  ( R e. Ring -> ( .r ` ( 1o mPwSer R ) ) = ( .r ` S ) )
19 18 oveqdr 
 |-  ( ( R e. Ring /\ ( x e. ( Base ` ( 1o mPwSer R ) ) /\ y e. ( Base ` ( 1o mPwSer R ) ) ) ) -> ( x ( .r ` ( 1o mPwSer R ) ) y ) = ( x ( .r ` S ) y ) )
20 11 15 17 19 subrgpropd 
 |-  ( R e. Ring -> ( SubRing ` ( 1o mPwSer R ) ) = ( SubRing ` S ) )
21 10 20 eleqtrd 
 |-  ( R e. Ring -> U e. ( SubRing ` S ) )