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 mPoly U )
	mplsubrgcl.u	|- U = ( S |`s R )
	mplsubrgcl.b	|- B = ( Base ` W )
	mplsubrgcl.p	|- P = ( I mPoly S )
	mplsubrgcl.c	|- C = ( Base ` P )
	mplsubrgcl.i	|- ( ph -> I e. V )
	mplsubrgcl.r	|- ( ph -> R e. ( SubRing ` S ) )
	mplsubrgcl.f	|- ( ph -> F e. B )
Assertion	mplsubrgcl	|- ( ph -> F e. C )

Proof

Step	Hyp	Ref	Expression
1		mplsubrgcl.w	|- W = ( I mPoly U )
2		mplsubrgcl.u	|- U = ( S |`s R )
3		mplsubrgcl.b	|- B = ( Base ` W )
4		mplsubrgcl.p	|- P = ( I mPoly S )
5		mplsubrgcl.c	|- C = ( Base ` P )
6		mplsubrgcl.i	|- ( ph -> I e. V )
7		mplsubrgcl.r	|- ( ph -> R e. ( SubRing ` S ) )
8		mplsubrgcl.f	|- ( ph -> F e. B )
9		eqid	|- ( P |`s B ) = ( P |`s B )
10	4 2 1 3 6 7 9	ressmplbas	|- ( ph -> B = ( Base ` ( P |`s B ) ) )
11	9 5	ressbasss	|- ( Base ` ( P |`s B ) ) C_ C
12	10 11	eqsstrdi	|- ( ph -> B C_ C )
13	12 8	sseldd	|- ( ph -> F e. C )