Theorem ressply1bas

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

	Ref	Expression
Hypotheses	ressply1.s	|- S = ( Poly1 ` R )
	ressply1.h	|- H = ( R |`s T )
	ressply1.u	|- U = ( Poly1 ` H )
	ressply1.b	|- B = ( Base ` U )
	ressply1.2	|- ( ph -> T e. ( SubRing ` R ) )
	ressply1.p	|- P = ( S |`s B )
Assertion	ressply1bas	|- ( ph -> B = ( Base ` P ) )

Proof

Step	Hyp	Ref	Expression
1		ressply1.s	|- S = ( Poly1 ` R )
2		ressply1.h	|- H = ( R |`s T )
3		ressply1.u	|- U = ( Poly1 ` H )
4		ressply1.b	|- B = ( Base ` U )
5		ressply1.2	|- ( ph -> T e. ( SubRing ` R ) )
6		ressply1.p	|- P = ( S |`s B )
7		eqid	|- ( PwSer1 ` H ) = ( PwSer1 ` H )
8		eqid	|- ( Base ` ( PwSer1 ` H ) ) = ( Base ` ( PwSer1 ` H ) )
9		eqid	|- ( Base ` S ) = ( Base ` S )
10	1 2 3 4 5 7 8 9	ressply1bas2	|- ( ph -> B = ( ( Base ` ( PwSer1 ` H ) ) i^i ( Base ` S ) ) )
11		inss2	|- ( ( Base ` ( PwSer1 ` H ) ) i^i ( Base ` S ) ) C_ ( Base ` S )
12	10 11	eqsstrdi	|- ( ph -> B C_ ( Base ` S ) )
13	6 9	ressbas2	|- ( B C_ ( Base ` S ) -> B = ( Base ` P ) )
14	12 13	syl	|- ( ph -> B = ( Base ` P ) )