Theorem opsrcrng

Description: The ring of ordered power series is commutative ring. (Contributed by Mario Carneiro, 10-Jan-2015)

	Ref	Expression
Hypotheses	opsrcrng.o	|- O = ( ( I ordPwSer R ) ` T )
	opsrcrng.i	|- ( ph -> I e. V )
	opsrcrng.r	|- ( ph -> R e. CRing )
	opsrcrng.t	|- ( ph -> T C_ ( I X. I ) )
Assertion	opsrcrng	|- ( ph -> O e. CRing )

Proof

Step	Hyp	Ref	Expression
1		opsrcrng.o	|- O = ( ( I ordPwSer R ) ` T )
2		opsrcrng.i	|- ( ph -> I e. V )
3		opsrcrng.r	|- ( ph -> R e. CRing )
4		opsrcrng.t	|- ( ph -> T C_ ( I X. I ) )
5		eqid	|- ( I mPwSer R ) = ( I mPwSer R )
6	5 2 3	psrcrng	|- ( ph -> ( I mPwSer R ) e. CRing )
7		eqidd	|- ( ph -> ( Base ` ( I mPwSer R ) ) = ( Base ` ( I mPwSer R ) ) )
8	5 1 4	opsrbas	|- ( ph -> ( Base ` ( I mPwSer R ) ) = ( Base ` O ) )
9	5 1 4	opsrplusg	|- ( ph -> ( +g ` ( I mPwSer R ) ) = ( +g ` O ) )
10	9	oveqdr	|- ( ( ph /\ ( x e. ( Base ` ( I mPwSer R ) ) /\ y e. ( Base ` ( I mPwSer R ) ) ) ) -> ( x ( +g ` ( I mPwSer R ) ) y ) = ( x ( +g ` O ) y ) )
11	5 1 4	opsrmulr	|- ( ph -> ( .r ` ( I mPwSer R ) ) = ( .r ` O ) )
12	11	oveqdr	|- ( ( ph /\ ( x e. ( Base ` ( I mPwSer R ) ) /\ y e. ( Base ` ( I mPwSer R ) ) ) ) -> ( x ( .r ` ( I mPwSer R ) ) y ) = ( x ( .r ` O ) y ) )
13	7 8 10 12	crngpropd	|- ( ph -> ( ( I mPwSer R ) e. CRing <-> O e. CRing ) )
14	6 13	mpbid	|- ( ph -> O e. CRing )