This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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