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 ) )