Theorem subrg1ascl

Description: The scalar injection function in a subring algebra is the same up to a restriction to 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)$$
	subrg1ascl.c	$$⊢C=\mathrm{algSc}\left(U\right)$$
Assertion	subrg1ascl	$$⊢\phi \to C={A\upharpoonright }_T$$

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		subrg1ascl.c	$$⊢C=\mathrm{algSc}\left(U\right)$$
7		eqid	$$⊢1_{𝑜}\mathrm{mPoly}R=1_{𝑜}\mathrm{mPoly}R$$
8	1 2	ply1ascl	$$⊢A=\mathrm{algSc}\left(1_{𝑜}\mathrm{mPoly}R\right)$$
9		eqid	$$⊢1_{𝑜}\mathrm{mPoly}H=1_{𝑜}\mathrm{mPoly}H$$
10		1on	$$⊢1_{𝑜}\in \mathrm{On}$$
11	10	a1i	$$⊢\phi \to 1_{𝑜}\in \mathrm{On}$$
12	4 6	ply1ascl	$$⊢C=\mathrm{algSc}\left(1_{𝑜}\mathrm{mPoly}H\right)$$
13	7 8 3 9 11 5 12	subrgascl	$$⊢\phi \to C={A\upharpoonright }_T$$