Theorem pwscrng

Description: A structure power of a commutative ring is a commutative ring. (Contributed by Mario Carneiro, 11-Mar-2015)

	Ref	Expression
Hypothesis	pwscrng.y	|- Y = ( R ^s I )
Assertion	pwscrng	|- ( ( R e. CRing /\ I e. V ) -> Y e. CRing )

Proof

Step	Hyp	Ref	Expression
1		pwscrng.y	|- Y = ( R ^s I )
2		eqid	|- ( Scalar ` R ) = ( Scalar ` R )
3	1 2	pwsval	|- ( ( R e. CRing /\ I e. V ) -> Y = ( ( Scalar ` R ) Xs_ ( I X. { R } ) ) )
4		eqid	|- ( ( Scalar ` R ) Xs_ ( I X. { R } ) ) = ( ( Scalar ` R ) Xs_ ( I X. { R } ) )
5		simpr	|- ( ( R e. CRing /\ I e. V ) -> I e. V )
6		fvexd	|- ( ( R e. CRing /\ I e. V ) -> ( Scalar ` R ) e. _V )
7		fconst6g	|- ( R e. CRing -> ( I X. { R } ) : I --> CRing )
8	7	adantr	|- ( ( R e. CRing /\ I e. V ) -> ( I X. { R } ) : I --> CRing )
9	4 5 6 8	prdscrngd	|- ( ( R e. CRing /\ I e. V ) -> ( ( Scalar ` R ) Xs_ ( I X. { R } ) ) e. CRing )
10	3 9	eqeltrd	|- ( ( R e. CRing /\ I e. V ) -> Y e. CRing )