mplcrng

Description: The polynomial ring is a commutative ring. (Contributed by Mario Carneiro, 9-Jan-2015)

		Ref	Expression
	Hypothesis	mplgrp.p	$⊢ P = I mPoly R$
	Assertion	mplcrng	$⊢ (I \in V \land R \in CRing) \to P \in CRing$

Step	Hyp	Ref	Expression
1		mplgrp.p	$⊢ P = I mPoly R$
2		eqid	$⊢ I mPwSer R = I mPwSer R$
3		simpl	$⊢ (I \in V \land R \in CRing) \to I \in V$
4		simpr	$⊢ (I \in V \land R \in CRing) \to R \in CRing$
5	2 3 4	psrcrng	$⊢ (I \in V \land R \in CRing) \to I mPwSer R \in CRing$
6		eqid	$⊢ {Base}_{P} = {Base}_{P}$
7		crngring	$⊢ R \in CRing \to R \in Ring$
8	7	adantl	$⊢ (I \in V \land R \in CRing) \to R \in Ring$
9	2 1 6 3 8	mplsubrg	$⊢ (I \in V \land R \in CRing) \to {Base}_{P} \in SubRing (I mPwSer R)$
10	1 2 6	mplval2	$⊢ P = (I mPwSer R) ↾_{𝑠} {Base}_{P}$
11	10	subrgcrng	$⊢ (I mPwSer R \in CRing \land {Base}_{P} \in SubRing (I mPwSer R)) \to P \in CRing$
12	5 9 11	syl2anc	$⊢ (I \in V \land R \in CRing) \to P \in CRing$

Metamath Proof Explorer