Metamath Proof Explorer


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 𝑠 R
mplsubrgcl.b B = Base W
mplsubrgcl.p P = I mPoly S
mplsubrgcl.c C = Base P
mplsubrgcl.i φ I V
mplsubrgcl.r φ R SubRing S
mplsubrgcl.f φ F B
Assertion mplsubrgcl φ F C

Proof

Step Hyp Ref Expression
1 mplsubrgcl.w W = I mPoly U
2 mplsubrgcl.u U = S 𝑠 R
3 mplsubrgcl.b B = Base W
4 mplsubrgcl.p P = I mPoly S
5 mplsubrgcl.c C = Base P
6 mplsubrgcl.i φ I V
7 mplsubrgcl.r φ R SubRing S
8 mplsubrgcl.f φ F B
9 eqid P 𝑠 B = P 𝑠 B
10 4 2 1 3 6 7 9 ressmplbas φ B = Base P 𝑠 B
11 9 5 ressbasss Base P 𝑠 B C
12 10 11 eqsstrdi φ B C
13 12 8 sseldd φ F C