Metamath Proof Explorer

Theorem ply1lss

Description: Univariate polynomials form a linear subspace 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 ply1lss 
|- ( R e. Ring -> U e. ( LSubSp ` 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 mpllss 
 |-  ( R e. Ring -> U e. ( LSubSp ` ( 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 ssv 
 |-  ( Base ` ( 1o mPwSer R ) ) C_ _V
17 16 a1i 
 |-  ( R e. Ring -> ( Base ` ( 1o mPwSer R ) ) C_ _V )
18 4 12 14 opsrplusg 
 |-  ( R e. Ring -> ( +g ` ( 1o mPwSer R ) ) = ( +g ` S ) )
19 18 oveqdr 
 |-  ( ( R e. Ring /\ ( x e. _V /\ y e. _V ) ) -> ( x ( +g ` ( 1o mPwSer R ) ) y ) = ( x ( +g ` S ) y ) )
20 ovexd 
 |-  ( ( R e. Ring /\ ( x e. ( Base ` R ) /\ y e. ( Base ` ( 1o mPwSer R ) ) ) ) -> ( x ( .s ` ( 1o mPwSer R ) ) y ) e. _V )
21 4 12 14 opsrvsca 
 |-  ( R e. Ring -> ( .s ` ( 1o mPwSer R ) ) = ( .s ` S ) )
22 21 oveqdr 
 |-  ( ( R e. Ring /\ ( x e. ( Base ` R ) /\ y e. ( Base ` ( 1o mPwSer R ) ) ) ) -> ( x ( .s ` ( 1o mPwSer R ) ) y ) = ( x ( .s ` S ) y ) )
23 4 8 9 psrsca 
 |-  ( R e. Ring -> R = ( Scalar ` ( 1o mPwSer R ) ) )
24 23 fveq2d 
 |-  ( R e. Ring -> ( Base ` R ) = ( Base ` ( Scalar ` ( 1o mPwSer R ) ) ) )
25 4 12 14 8 9 opsrsca 
 |-  ( R e. Ring -> R = ( Scalar ` S ) )
26 25 fveq2d 
 |-  ( R e. Ring -> ( Base ` R ) = ( Base ` ( Scalar ` S ) ) )
27 11 15 17 19 20 22 24 26 lsspropd 
 |-  ( R e. Ring -> ( LSubSp ` ( 1o mPwSer R ) ) = ( LSubSp ` S ) )
28 10 27 eleqtrd 
 |-  ( R e. Ring -> U e. ( LSubSp ` S ) )