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 ↑_{𝑠} I$
	Assertion	pwscrng	$⊢ (R \in CRing \land I \in V) \to Y \in CRing$

Step	Hyp	Ref	Expression
1		pwscrng.y	$⊢ Y = R ↑_{𝑠} I$
2		eqid	$⊢ Scalar (R) = Scalar (R)$
3	1 2	pwsval	$⊢ (R \in CRing \land I \in V) \to Y = Scalar (R) ⨉_{𝑠} (I \times \{R\})$
4		eqid	$⊢ Scalar (R) ⨉_{𝑠} (I \times \{R\}) = Scalar (R) ⨉_{𝑠} (I \times \{R\})$
5		simpr	$⊢ (R \in CRing \land I \in V) \to I \in V$
6		fvexd	$⊢ (R \in CRing \land I \in V) \to Scalar (R) \in V$
7		fconst6g	$⊢ R \in CRing \to (I \times \{R\}) : I ⟶ CRing$
8	7	adantr	$⊢ (R \in CRing \land I \in V) \to (I \times \{R\}) : I ⟶ CRing$
9	4 5 6 8	prdscrngd	$⊢ (R \in CRing \land I \in V) \to Scalar (R) ⨉_{𝑠} (I \times \{R\}) \in CRing$
10	3 9	eqeltrd	$⊢ (R \in CRing \land I \in V) \to Y \in CRing$

Metamath Proof Explorer