Metamath Proof Explorer

Theorem ply1assa

Description: The ring of univariate polynomials is an associative algebra. (Contributed by Mario Carneiro, 9-Feb-2015)

Ref Expression
Hypothesis ply1val.1 
|- P = ( Poly1 ` R )
Assertion ply1assa 
|- ( R e. CRing -> P e. AssAlg )

Proof

Step Hyp Ref Expression
1 ply1val.1 
 |-  P = ( Poly1 ` R )
2 crngring 
 |-  ( R e. CRing -> R e. Ring )
3 eqid 
 |-  ( PwSer1 ` R ) = ( PwSer1 ` R )
4 eqid 
 |-  ( Base ` P ) = ( Base ` P )
5 1 3 4 ply1subrg 
 |-  ( R e. Ring -> ( Base ` P ) e. ( SubRing ` ( PwSer1 ` R ) ) )
6 2 5 syl 
 |-  ( R e. CRing -> ( Base ` P ) e. ( SubRing ` ( PwSer1 ` R ) ) )
7 1 3 4 ply1lss 
 |-  ( R e. Ring -> ( Base ` P ) e. ( LSubSp ` ( PwSer1 ` R ) ) )
8 2 7 syl 
 |-  ( R e. CRing -> ( Base ` P ) e. ( LSubSp ` ( PwSer1 ` R ) ) )
9 3 psr1assa 
 |-  ( R e. CRing -> ( PwSer1 ` R ) e. AssAlg )
10 eqid 
 |-  ( 1r ` ( PwSer1 ` R ) ) = ( 1r ` ( PwSer1 ` R ) )
11 10 subrg1cl 
 |-  ( ( Base ` P ) e. ( SubRing ` ( PwSer1 ` R ) ) -> ( 1r ` ( PwSer1 ` R ) ) e. ( Base ` P ) )
12 6 11 syl 
 |-  ( R e. CRing -> ( 1r ` ( PwSer1 ` R ) ) e. ( Base ` P ) )
13 eqid 
 |-  ( Base ` ( PwSer1 ` R ) ) = ( Base ` ( PwSer1 ` R ) )
14 13 subrgss 
 |-  ( ( Base ` P ) e. ( SubRing ` ( PwSer1 ` R ) ) -> ( Base ` P ) C_ ( Base ` ( PwSer1 ` R ) ) )
15 6 14 syl 
 |-  ( R e. CRing -> ( Base ` P ) C_ ( Base ` ( PwSer1 ` R ) ) )
16 1 3 ply1val 
 |-  P = ( ( PwSer1 ` R ) |`s ( Base ` ( 1o mPoly R ) ) )
17 1 4 ply1bas 
 |-  ( Base ` P ) = ( Base ` ( 1o mPoly R ) )
18 17 oveq2i 
 |-  ( ( PwSer1 ` R ) |`s ( Base ` P ) ) = ( ( PwSer1 ` R ) |`s ( Base ` ( 1o mPoly R ) ) )
19 16 18 eqtr4i 
 |-  P = ( ( PwSer1 ` R ) |`s ( Base ` P ) )
20 eqid 
 |-  ( LSubSp ` ( PwSer1 ` R ) ) = ( LSubSp ` ( PwSer1 ` R ) )
21 19 20 13 10 issubassa 
 |-  ( ( ( PwSer1 ` R ) e. AssAlg /\ ( 1r ` ( PwSer1 ` R ) ) e. ( Base ` P ) /\ ( Base ` P ) C_ ( Base ` ( PwSer1 ` R ) ) ) -> ( P e. AssAlg <-> ( ( Base ` P ) e. ( SubRing ` ( PwSer1 ` R ) ) /\ ( Base ` P ) e. ( LSubSp ` ( PwSer1 ` R ) ) ) ) )
22 9 12 15 21 syl3anc 
 |-  ( R e. CRing -> ( P e. AssAlg <-> ( ( Base ` P ) e. ( SubRing ` ( PwSer1 ` R ) ) /\ ( Base ` P ) e. ( LSubSp ` ( PwSer1 ` R ) ) ) ) )
23 6 8 22 mpbir2and 
 |-  ( R e. CRing -> P e. AssAlg )