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

Metamath Proof Explorer

Theorem ressmplbas

Description: A restricted polynomial algebra has the same base set. (Contributed by Mario Carneiro, 3-Jul-2015)

Ref Expression
Hypotheses ressmpl.s ⊢ S = I mPoly R
ressmpl.h ⊢ H = R ↾ 𝑠 T
ressmpl.u ⊢ U = I mPoly H
ressmpl.b ⊢ B = Base U
ressmpl.1 ⊢ φ → I ∈ V
ressmpl.2 ⊢ φ → T ∈ SubRing ⁡ R
ressmpl.p ⊢ P = S ↾ 𝑠 B
Assertion ressmplbas ⊢ φ → B = Base P

Proof

Step Hyp Ref Expression
1 ressmpl.s ⊢ S = I mPoly R
2 ressmpl.h ⊢ H = R ↾ 𝑠 T
3 ressmpl.u ⊢ U = I mPoly H
4 ressmpl.b ⊢ B = Base U
5 ressmpl.1 ⊢ φ → I ∈ V
6 ressmpl.2 ⊢ φ → T ∈ SubRing ⁡ R
7 ressmpl.p ⊢ P = S ↾ 𝑠 B
8 eqid ⊢ I mPwSer H = I mPwSer H
9 eqid ⊢ Base I mPwSer H = Base I mPwSer H
10 eqid ⊢ Base S = Base S
11 1 2 3 4 5 6 8 9 10 ressmplbas2 ⊢ φ → B = Base I mPwSer H ∩ Base S
12 inss2 ⊢ Base I mPwSer H ∩ Base S ⊆ Base S
13 11 12 eqsstrdi ⊢ φ → B ⊆ Base S
14 7 10 ressbas2 ⊢ B ⊆ Base S → B = Base P
15 13 14 syl ⊢ φ → B = Base P