This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem mplassa

Description: The polynomial ring is an associative algebra. (Contributed by Mario Carneiro, 9-Jan-2015)

Ref Expression
Hypothesis mplgrp.p 
|- P = ( I mPoly R )
Assertion mplassa 
|- ( ( I e. V /\ R e. CRing ) -> P e. AssAlg )

Proof

Step Hyp Ref Expression
1 mplgrp.p 
 |-  P = ( I mPoly R )
2 eqid 
 |-  ( I mPwSer R ) = ( I mPwSer R )
3 eqid 
 |-  ( Base ` P ) = ( Base ` P )
4 simpl 
 |-  ( ( I e. V /\ R e. CRing ) -> I e. V )
5 crngring 
 |-  ( R e. CRing -> R e. Ring )
6 5 adantl 
 |-  ( ( I e. V /\ R e. CRing ) -> R e. Ring )
7 2 1 3 4 6 mplsubrg 
 |-  ( ( I e. V /\ R e. CRing ) -> ( Base ` P ) e. ( SubRing ` ( I mPwSer R ) ) )
8 2 1 3 4 6 mpllss 
 |-  ( ( I e. V /\ R e. CRing ) -> ( Base ` P ) e. ( LSubSp ` ( I mPwSer R ) ) )
9 simpr 
 |-  ( ( I e. V /\ R e. CRing ) -> R e. CRing )
10 2 4 9 psrassa 
 |-  ( ( I e. V /\ R e. CRing ) -> ( I mPwSer R ) e. AssAlg )
11 eqid 
 |-  ( 1r ` ( I mPwSer R ) ) = ( 1r ` ( I mPwSer R ) )
12 11 subrg1cl 
 |-  ( ( Base ` P ) e. ( SubRing ` ( I mPwSer R ) ) -> ( 1r ` ( I mPwSer R ) ) e. ( Base ` P ) )
13 7 12 syl 
 |-  ( ( I e. V /\ R e. CRing ) -> ( 1r ` ( I mPwSer R ) ) e. ( Base ` P ) )
14 eqid 
 |-  ( Base ` ( I mPwSer R ) ) = ( Base ` ( I mPwSer R ) )
15 14 subrgss 
 |-  ( ( Base ` P ) e. ( SubRing ` ( I mPwSer R ) ) -> ( Base ` P ) C_ ( Base ` ( I mPwSer R ) ) )
16 7 15 syl 
 |-  ( ( I e. V /\ R e. CRing ) -> ( Base ` P ) C_ ( Base ` ( I mPwSer R ) ) )
17 1 2 3 mplval2 
 |-  P = ( ( I mPwSer R ) |`s ( Base ` P ) )
18 eqid 
 |-  ( LSubSp ` ( I mPwSer R ) ) = ( LSubSp ` ( I mPwSer R ) )
19 17 18 14 11 issubassa 
 |-  ( ( ( I mPwSer R ) e. AssAlg /\ ( 1r ` ( I mPwSer R ) ) e. ( Base ` P ) /\ ( Base ` P ) C_ ( Base ` ( I mPwSer R ) ) ) -> ( P e. AssAlg <-> ( ( Base ` P ) e. ( SubRing ` ( I mPwSer R ) ) /\ ( Base ` P ) e. ( LSubSp ` ( I mPwSer R ) ) ) ) )
20 10 13 16 19 syl3anc 
 |-  ( ( I e. V /\ R e. CRing ) -> ( P e. AssAlg <-> ( ( Base ` P ) e. ( SubRing ` ( I mPwSer R ) ) /\ ( Base ` P ) e. ( LSubSp ` ( I mPwSer R ) ) ) ) )
21 7 8 20 mpbir2and 
 |-  ( ( I e. V /\ R e. CRing ) -> P e. AssAlg )