Theorem mplsubrgcl

Description: An element of a polynomial algebra over a subring is an element of the polynomial algebra. (Contributed by SN, 9-Feb-2025)

	Ref	Expression
Hypotheses	mplsubrgcl.w	$$⊢W=I\mathrm{mPoly}U$$
	mplsubrgcl.u	$$⊢U=S{\upharpoonright }_{𝑠}R$$
	mplsubrgcl.b	$$⊢B={\mathrm{Base}}_W$$
	mplsubrgcl.p	$$⊢P=I\mathrm{mPoly}S$$
	mplsubrgcl.c	$$⊢C={\mathrm{Base}}_P$$
	mplsubrgcl.i	$$⊢\phi \to I\in V$$
	mplsubrgcl.r	$$⊢\phi \to R\in \mathrm{SubRing}\left(S\right)$$
	mplsubrgcl.f	$$⊢\phi \to F\in B$$
Assertion	mplsubrgcl	$$⊢\phi \to F\in C$$

Proof

Step	Hyp	Ref	Expression
1		mplsubrgcl.w	$$⊢W=I\mathrm{mPoly}U$$
2		mplsubrgcl.u	$$⊢U=S{\upharpoonright }_{𝑠}R$$
3		mplsubrgcl.b	$$⊢B={\mathrm{Base}}_W$$
4		mplsubrgcl.p	$$⊢P=I\mathrm{mPoly}S$$
5		mplsubrgcl.c	$$⊢C={\mathrm{Base}}_P$$
6		mplsubrgcl.i	$$⊢\phi \to I\in V$$
7		mplsubrgcl.r	$$⊢\phi \to R\in \mathrm{SubRing}\left(S\right)$$
8		mplsubrgcl.f	$$⊢\phi \to F\in B$$
9		eqid	$$⊢P{\upharpoonright }_{𝑠}B=P{\upharpoonright }_{𝑠}B$$
10	4 2 1 3 6 7 9	ressmplbas	$$⊢\phi \to B={\mathrm{Base}}_{\left(P{\upharpoonright }_{𝑠}B\right)}$$
11	9 5	ressbasss	$$⊢{\mathrm{Base}}_{\left(P{\upharpoonright }_{𝑠}B\right)}\subseteq C$$
12	10 11	eqsstrdi	$$⊢\phi \to B\subseteq C$$
13	12 8	sseldd	$$⊢\phi \to F\in C$$