Theorem ply1assa

Description: The ring of univariate polynomials is an associative algebra. (Contributed by Mario Carneiro, 9-Feb-2015)

	Ref	Expression
Hypothesis	ply1val.1	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
Assertion	ply1assa	$$⊢R\in \mathrm{CRing}\to P\in \mathrm{AssAlg}$$

Proof

Step	Hyp	Ref	Expression
1		ply1val.1	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
2		crngring	$$⊢R\in \mathrm{CRing}\to R\in \mathrm{Ring}$$
3		eqid	$$⊢{\mathrm{PwSer}}_1\left(R\right)={\mathrm{PwSer}}_1\left(R\right)$$
4		eqid	$$⊢{\mathrm{Base}}_P={\mathrm{Base}}_P$$
5	1 3 4	ply1subrg	$$⊢R\in \mathrm{Ring}\to {\mathrm{Base}}_P\in \mathrm{SubRing}\left({\mathrm{PwSer}}_1\left(R\right)\right)$$
6	2 5	syl	$$⊢R\in \mathrm{CRing}\to {\mathrm{Base}}_P\in \mathrm{SubRing}\left({\mathrm{PwSer}}_1\left(R\right)\right)$$
7	1 3 4	ply1lss	$$⊢R\in \mathrm{Ring}\to {\mathrm{Base}}_P\in \mathrm{LSubSp}\left({\mathrm{PwSer}}_1\left(R\right)\right)$$
8	2 7	syl	$$⊢R\in \mathrm{CRing}\to {\mathrm{Base}}_P\in \mathrm{LSubSp}\left({\mathrm{PwSer}}_1\left(R\right)\right)$$
9	3	psr1assa	$$⊢R\in \mathrm{CRing}\to {\mathrm{PwSer}}_1\left(R\right)\in \mathrm{AssAlg}$$
10		eqid	$$⊢1_{{\mathrm{PwSer}}_1\left(R\right)}=1_{{\mathrm{PwSer}}_1\left(R\right)}$$
11	10	subrg1cl	$$⊢{\mathrm{Base}}_P\in \mathrm{SubRing}\left({\mathrm{PwSer}}_1\left(R\right)\right)\to 1_{{\mathrm{PwSer}}_1\left(R\right)}\in {\mathrm{Base}}_P$$
12	6 11	syl	$$⊢R\in \mathrm{CRing}\to 1_{{\mathrm{PwSer}}_1\left(R\right)}\in {\mathrm{Base}}_P$$
13		eqid	$$⊢{\mathrm{Base}}_{{\mathrm{PwSer}}_1\left(R\right)}={\mathrm{Base}}_{{\mathrm{PwSer}}_1\left(R\right)}$$
14	13	subrgss	$$⊢{\mathrm{Base}}_P\in \mathrm{SubRing}\left({\mathrm{PwSer}}_1\left(R\right)\right)\to {\mathrm{Base}}_P\subseteq {\mathrm{Base}}_{{\mathrm{PwSer}}_1\left(R\right)}$$
15	6 14	syl	$$⊢R\in \mathrm{CRing}\to {\mathrm{Base}}_P\subseteq {\mathrm{Base}}_{{\mathrm{PwSer}}_1\left(R\right)}$$
16	1 3	ply1val	$$⊢P={\mathrm{PwSer}}_1\left(R\right){\upharpoonright }_{𝑠}{\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}R\right)}$$
17	1 4	ply1bas	$$⊢{\mathrm{Base}}_P={\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}R\right)}$$
18	17	oveq2i	$$⊢{\mathrm{PwSer}}_1\left(R\right){\upharpoonright }_{𝑠}{\mathrm{Base}}_P={\mathrm{PwSer}}_1\left(R\right){\upharpoonright }_{𝑠}{\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}R\right)}$$
19	16 18	eqtr4i	$$⊢P={\mathrm{PwSer}}_1\left(R\right){\upharpoonright }_{𝑠}{\mathrm{Base}}_P$$
20		eqid	$$⊢\mathrm{LSubSp}\left({\mathrm{PwSer}}_1\left(R\right)\right)=\mathrm{LSubSp}\left({\mathrm{PwSer}}_1\left(R\right)\right)$$
21	19 20 13 10	issubassa	$$⊢\left({\mathrm{PwSer}}_1\left(R\right)\in \mathrm{AssAlg}\wedge 1_{{\mathrm{PwSer}}_1\left(R\right)}\in {\mathrm{Base}}_P\wedge {\mathrm{Base}}_P\subseteq {\mathrm{Base}}_{{\mathrm{PwSer}}_1\left(R\right)}\right)\to \left(P\in \mathrm{AssAlg}\leftrightarrow \left({\mathrm{Base}}_P\in \mathrm{SubRing}\left({\mathrm{PwSer}}_1\left(R\right)\right)\wedge {\mathrm{Base}}_P\in \mathrm{LSubSp}\left({\mathrm{PwSer}}_1\left(R\right)\right)\right)\right)$$
22	9 12 15 21	syl3anc	$$⊢R\in \mathrm{CRing}\to \left(P\in \mathrm{AssAlg}\leftrightarrow \left({\mathrm{Base}}_P\in \mathrm{SubRing}\left({\mathrm{PwSer}}_1\left(R\right)\right)\wedge {\mathrm{Base}}_P\in \mathrm{LSubSp}\left({\mathrm{PwSer}}_1\left(R\right)\right)\right)\right)$$
23	6 8 22	mpbir2and	$$⊢R\in \mathrm{CRing}\to P\in \mathrm{AssAlg}$$