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 |`s T )
ressmpl.u
|- U = ( I mPoly H )
ressmpl.b
|- B = ( Base ` U )
ressmpl.1
|- ( ph -> I e. V )
ressmpl.2
|- ( ph -> T e. ( SubRing ` R ) )
ressmpl.p
|- P = ( S |`s B )
Assertion ressmplbas
|- ( ph -> B = ( Base ` P ) )

Proof

Step Hyp Ref Expression
1 ressmpl.s
 |-  S = ( I mPoly R )
2 ressmpl.h
 |-  H = ( R |`s T )
3 ressmpl.u
 |-  U = ( I mPoly H )
4 ressmpl.b
 |-  B = ( Base ` U )
5 ressmpl.1
 |-  ( ph -> I e. V )
6 ressmpl.2
 |-  ( ph -> T e. ( SubRing ` R ) )
7 ressmpl.p
 |-  P = ( S |`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
 |-  ( ph -> B = ( ( Base ` ( I mPwSer H ) ) i^i ( Base ` S ) ) )
12 inss2
 |-  ( ( Base ` ( I mPwSer H ) ) i^i ( Base ` S ) ) C_ ( Base ` S )
13 11 12 eqsstrdi
 |-  ( ph -> B C_ ( Base ` S ) )
14 7 10 ressbas2
 |-  ( B C_ ( Base ` S ) -> B = ( Base ` P ) )
15 13 14 syl
 |-  ( ph -> B = ( Base ` P ) )