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	⊢ 𝑌 = ( 𝑅 ↑s 𝐼 )
Assertion	pwscrng	⊢ ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑉 ) → 𝑌 ∈ CRing )

Proof

Step	Hyp	Ref	Expression
1		pwscrng.y	⊢ 𝑌 = ( 𝑅 ↑s 𝐼 )
2		eqid	⊢ ( Scalar ‘ 𝑅 ) = ( Scalar ‘ 𝑅 )
3	1 2	pwsval	⊢ ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑉 ) → 𝑌 = ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) ) )
4		eqid	⊢ ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) ) = ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) )
5		simpr	⊢ ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑉 ) → 𝐼 ∈ 𝑉 )
6		fvexd	⊢ ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑉 ) → ( Scalar ‘ 𝑅 ) ∈ V )
7		fconst6g	⊢ ( 𝑅 ∈ CRing → ( 𝐼 × { 𝑅 } ) : 𝐼 ⟶ CRing )
8	7	adantr	⊢ ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑉 ) → ( 𝐼 × { 𝑅 } ) : 𝐼 ⟶ CRing )
9	4 5 6 8	prdscrngd	⊢ ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑉 ) → ( ( Scalar ‘ 𝑅 ) Xs ( 𝐼 × { 𝑅 } ) ) ∈ CRing )
10	3 9	eqeltrd	⊢ ( ( 𝑅 ∈ CRing ∧ 𝐼 ∈ 𝑉 ) → 𝑌 ∈ CRing )