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	⊢ 𝑊 = ( 𝐼 mPoly 𝑈 )
	mplsubrgcl.u	⊢ 𝑈 = ( 𝑆 ↾s 𝑅 )
	mplsubrgcl.b	⊢ 𝐵 = ( Base ‘ 𝑊 )
	mplsubrgcl.p	⊢ 𝑃 = ( 𝐼 mPoly 𝑆 )
	mplsubrgcl.c	⊢ 𝐶 = ( Base ‘ 𝑃 )
	mplsubrgcl.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
	mplsubrgcl.r	⊢ ( 𝜑 → 𝑅 ∈ ( SubRing ‘ 𝑆 ) )
	mplsubrgcl.f	⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
Assertion	mplsubrgcl	⊢ ( 𝜑 → 𝐹 ∈ 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		mplsubrgcl.w	⊢ 𝑊 = ( 𝐼 mPoly 𝑈 )
2		mplsubrgcl.u	⊢ 𝑈 = ( 𝑆 ↾s 𝑅 )
3		mplsubrgcl.b	⊢ 𝐵 = ( Base ‘ 𝑊 )
4		mplsubrgcl.p	⊢ 𝑃 = ( 𝐼 mPoly 𝑆 )
5		mplsubrgcl.c	⊢ 𝐶 = ( Base ‘ 𝑃 )
6		mplsubrgcl.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
7		mplsubrgcl.r	⊢ ( 𝜑 → 𝑅 ∈ ( SubRing ‘ 𝑆 ) )
8		mplsubrgcl.f	⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
9		eqid	⊢ ( 𝑃 ↾s 𝐵 ) = ( 𝑃 ↾s 𝐵 )
10	4 2 1 3 6 7 9	ressmplbas	⊢ ( 𝜑 → 𝐵 = ( Base ‘ ( 𝑃 ↾s 𝐵 ) ) )
11	9 5	ressbasss	⊢ ( Base ‘ ( 𝑃 ↾s 𝐵 ) ) ⊆ 𝐶
12	10 11	eqsstrdi	⊢ ( 𝜑 → 𝐵 ⊆ 𝐶 )
13	12 8	sseldd	⊢ ( 𝜑 → 𝐹 ∈ 𝐶 )