Metamath Proof Explorer


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