mplassa

Description: The polynomial ring is an associative algebra. (Contributed by Mario Carneiro, 9-Jan-2015)

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

Proof

Step	Hyp	Ref	Expression
1		mplgrp.p	$⊢ P = I mPoly R$
2		eqid	$⊢ I mPwSer R = I mPwSer R$
3		eqid	$⊢ {Base}_{P} = {Base}_{P}$
4		simpl	$⊢ (I \in V \land R \in CRing) \to I \in V$
5		crngring	$⊢ R \in CRing \to R \in Ring$
6	5	adantl	$⊢ (I \in V \land R \in CRing) \to R \in Ring$
7	2 1 3 4 6	mplsubrg	$⊢ (I \in V \land R \in CRing) \to {Base}_{P} \in SubRing (I mPwSer R)$
8	2 1 3 4 6	mpllss	$⊢ (I \in V \land R \in CRing) \to {Base}_{P} \in LSubSp (I mPwSer R)$
9		simpr	$⊢ (I \in V \land R \in CRing) \to R \in CRing$
10	2 4 9	psrassa	$⊢ (I \in V \land R \in CRing) \to I mPwSer R \in AssAlg$
11		eqid	$⊢ 1_{(I mPwSer R)} = 1_{(I mPwSer R)}$
12	11	subrg1cl	$⊢ {Base}_{P} \in SubRing (I mPwSer R) \to 1_{(I mPwSer R)} \in {Base}_{P}$
13	7 12	syl	$⊢ (I \in V \land R \in CRing) \to 1_{(I mPwSer R)} \in {Base}_{P}$
14		eqid	$⊢ {Base}_{(I mPwSer R)} = {Base}_{(I mPwSer R)}$
15	14	subrgss	$⊢ {Base}_{P} \in SubRing (I mPwSer R) \to {Base}_{P} \subseteq {Base}_{(I mPwSer R)}$
16	7 15	syl	$⊢ (I \in V \land R \in CRing) \to {Base}_{P} \subseteq {Base}_{(I mPwSer R)}$
17	1 2 3	mplval2	$⊢ P = (I mPwSer R) ↾_{𝑠} {Base}_{P}$
18		eqid	$⊢ LSubSp (I mPwSer R) = LSubSp (I mPwSer R)$
19	17 18 14 11	issubassa	$⊢ (I mPwSer R \in AssAlg \land 1_{(I mPwSer R)} \in {Base}_{P} \land {Base}_{P} \subseteq {Base}_{(I mPwSer R)}) \to (P \in AssAlg \leftrightarrow ({Base}_{P} \in SubRing (I mPwSer R) \land {Base}_{P} \in LSubSp (I mPwSer R)))$
20	10 13 16 19	syl3anc	$⊢ (I \in V \land R \in CRing) \to (P \in AssAlg \leftrightarrow ({Base}_{P} \in SubRing (I mPwSer R) \land {Base}_{P} \in LSubSp (I mPwSer R)))$
21	7 8 20	mpbir2and	$⊢ (I \in V \land R \in CRing) \to P \in AssAlg$

Metamath Proof Explorer

Theorem mplassa

Proof