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 )