Theorem ply1ascl

Description: The univariate polynomial ring inherits the multivariate ring's scalar function. (Contributed by Stefan O'Rear, 28-Mar-2015) (Proof shortened by Fan Zheng, 26-Jun-2016)

	Ref	Expression
Hypotheses	ply1ascl.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
	ply1ascl.a	$$⊢A=\mathrm{algSc}\left(P\right)$$
Assertion	ply1ascl	$$⊢A=\mathrm{algSc}\left(1_{𝑜}\mathrm{mPoly}R\right)$$

Proof

Step	Hyp	Ref	Expression
1		ply1ascl.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
2		ply1ascl.a	$$⊢A=\mathrm{algSc}\left(P\right)$$
3		eqid	$$⊢\mathrm{Scalar}\left(P\right)=\mathrm{Scalar}\left(P\right)$$
4		eqid	$$⊢\mathrm{Scalar}\left(1_{𝑜}\mathrm{mPoly}R\right)=\mathrm{Scalar}\left(1_{𝑜}\mathrm{mPoly}R\right)$$
5	1	ply1sca	$$⊢R\in \mathrm{V}\to R=\mathrm{Scalar}\left(P\right)$$
6	5	fveq2d	$$⊢R\in \mathrm{V}\to {\mathrm{Base}}_R={\mathrm{Base}}_{\mathrm{Scalar}\left(P\right)}$$
7		eqid	$$⊢1_{𝑜}\mathrm{mPoly}R=1_{𝑜}\mathrm{mPoly}R$$
8		1on	$$⊢1_{𝑜}\in \mathrm{On}$$
9	8	a1i	$$⊢R\in \mathrm{V}\to 1_{𝑜}\in \mathrm{On}$$
10		id	$$⊢R\in \mathrm{V}\to R\in \mathrm{V}$$
11	7 9 10	mplsca	$$⊢R\in \mathrm{V}\to R=\mathrm{Scalar}\left(1_{𝑜}\mathrm{mPoly}R\right)$$
12	11	fveq2d	$$⊢R\in \mathrm{V}\to {\mathrm{Base}}_R={\mathrm{Base}}_{\mathrm{Scalar}\left(1_{𝑜}\mathrm{mPoly}R\right)}$$
13		eqid	$$⊢{\cdot }_P={\cdot }_P$$
14	1 7 13	ply1vsca	$$⊢{\cdot }_P={\cdot }_{\left(1_{𝑜}\mathrm{mPoly}R\right)}$$
15	14	a1i	$$⊢R\in \mathrm{V}\to {\cdot }_P={\cdot }_{\left(1_{𝑜}\mathrm{mPoly}R\right)}$$
16	15	oveqdr	$$⊢\left(R\in \mathrm{V}\wedge \left(x\in {\mathrm{Base}}_R\wedge y\in \mathrm{V}\right)\right)\to x{\cdot }_{P}y=x{\cdot }_{\left(1_{𝑜}\mathrm{mPoly}R\right)}y$$
17		eqid	$$⊢1_P=1_P$$
18	7 1 17	ply1mpl1	$$⊢1_P=1_{\left(1_{𝑜}\mathrm{mPoly}R\right)}$$
19	18	a1i	$$⊢R\in \mathrm{V}\to 1_P=1_{\left(1_{𝑜}\mathrm{mPoly}R\right)}$$
20		fvexd	$$⊢R\in \mathrm{V}\to 1_P\in \mathrm{V}$$
21	3 4 6 12 16 19 20	asclpropd	$$⊢R\in \mathrm{V}\to \mathrm{algSc}\left(P\right)=\mathrm{algSc}\left(1_{𝑜}\mathrm{mPoly}R\right)$$
22		fvprc	$$⊢\neg R\in \mathrm{V}\to {\mathrm{Poly}}_1\left(R\right)=\varnothing$$
23	1 22	syl5eq	$$⊢\neg R\in \mathrm{V}\to P=\varnothing$$
24		reldmmpl	$$⊢\mathrm{Rel}\mathrm{dom}\mathrm{mPoly}$$
25	24	ovprc2	$$⊢\neg R\in \mathrm{V}\to 1_{𝑜}\mathrm{mPoly}R=\varnothing$$
26	23 25	eqtr4d	$$⊢\neg R\in \mathrm{V}\to P=1_{𝑜}\mathrm{mPoly}R$$
27	26	fveq2d	$$⊢\neg R\in \mathrm{V}\to \mathrm{algSc}\left(P\right)=\mathrm{algSc}\left(1_{𝑜}\mathrm{mPoly}R\right)$$
28	21 27	pm2.61i	$$⊢\mathrm{algSc}\left(P\right)=\mathrm{algSc}\left(1_{𝑜}\mathrm{mPoly}R\right)$$
29	2 28	eqtri	$$⊢A=\mathrm{algSc}\left(1_{𝑜}\mathrm{mPoly}R\right)$$