Theorem subrg1asclcl

Description: The scalars in a polynomial algebra are in the subring algebra iff the scalar value is in the subring. (Contributed by Mario Carneiro, 4-Jul-2015)

	Ref	Expression
Hypotheses	subrg1ascl.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
	subrg1ascl.a	$$⊢A=\mathrm{algSc}\left(P\right)$$
	subrg1ascl.h	$$⊢H=R{\upharpoonright }_{𝑠}T$$
	subrg1ascl.u	$$⊢U={\mathrm{Poly}}_1\left(H\right)$$
	subrg1ascl.r	$$⊢\phi \to T\in \mathrm{SubRing}\left(R\right)$$
	subrg1asclcl.b	$$⊢B={\mathrm{Base}}_U$$
	subrg1asclcl.k	$$⊢K={\mathrm{Base}}_R$$
	subrg1asclcl.x	$$⊢\phi \to X\in K$$
Assertion	subrg1asclcl	$$⊢\phi \to \left(A\left(X\right)\in B\leftrightarrow X\in T\right)$$

Proof

Step	Hyp	Ref	Expression
1		subrg1ascl.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
2		subrg1ascl.a	$$⊢A=\mathrm{algSc}\left(P\right)$$
3		subrg1ascl.h	$$⊢H=R{\upharpoonright }_{𝑠}T$$
4		subrg1ascl.u	$$⊢U={\mathrm{Poly}}_1\left(H\right)$$
5		subrg1ascl.r	$$⊢\phi \to T\in \mathrm{SubRing}\left(R\right)$$
6		subrg1asclcl.b	$$⊢B={\mathrm{Base}}_U$$
7		subrg1asclcl.k	$$⊢K={\mathrm{Base}}_R$$
8		subrg1asclcl.x	$$⊢\phi \to X\in K$$
9		eqid	$$⊢1_{𝑜}\mathrm{mPoly}R=1_{𝑜}\mathrm{mPoly}R$$
10	1 2	ply1ascl	$$⊢A=\mathrm{algSc}\left(1_{𝑜}\mathrm{mPoly}R\right)$$
11		eqid	$$⊢1_{𝑜}\mathrm{mPoly}H=1_{𝑜}\mathrm{mPoly}H$$
12		1on	$$⊢1_{𝑜}\in \mathrm{On}$$
13	12	a1i	$$⊢\phi \to 1_{𝑜}\in \mathrm{On}$$
14		eqid	$$⊢{\mathrm{PwSer}}_1\left(H\right)={\mathrm{PwSer}}_1\left(H\right)$$
15	4 14 6	ply1bas	$$⊢B={\mathrm{Base}}_{\left(1_{𝑜}\mathrm{mPoly}H\right)}$$
16	9 10 3 11 13 5 15 7 8	subrgasclcl	$$⊢\phi \to \left(A\left(X\right)\in B\leftrightarrow X\in T\right)$$