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

Metamath Proof Explorer

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 )