Theorem ressply1bas2

Description: The base set of a restricted polynomial algebra consists of power series in the subring which are also polynomials (in the parent ring). (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 ) )
	ressply1bas2.w	|- W = ( PwSer1 ` H )
	ressply1bas2.c	|- C = ( Base ` W )
	ressply1bas2.k	|- K = ( Base ` S )
Assertion	ressply1bas2	|- ( ph -> B = ( C i^i K ) )

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		ressply1bas2.w	|- W = ( PwSer1 ` H )
7		ressply1bas2.c	|- C = ( Base ` W )
8		ressply1bas2.k	|- K = ( Base ` S )
9		eqid	|- ( 1o mPoly R ) = ( 1o mPoly R )
10		eqid	|- ( 1o mPoly H ) = ( 1o mPoly H )
11	3 6 4	ply1bas	|- B = ( Base ` ( 1o mPoly H ) )
12		1on	|- 1o e. On
13	12	a1i	|- ( ph -> 1o e. On )
14		eqid	|- ( 1o mPwSer H ) = ( 1o mPwSer H )
15	6 7 14	psr1bas2	|- C = ( Base ` ( 1o mPwSer H ) )
16		eqid	|- ( PwSer1 ` R ) = ( PwSer1 ` R )
17	1 16 8	ply1bas	|- K = ( Base ` ( 1o mPoly R ) )
18	9 2 10 11 13 5 14 15 17	ressmplbas2	|- ( ph -> B = ( C i^i K ) )