ressmplbas2

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	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 ) )
	ressmplbas2.w	\|- W = ( I mPwSer H )
	ressmplbas2.c	\|- C = ( Base ` W )
	ressmplbas2.k	\|- K = ( Base ` S )
Assertion	ressmplbas2	\|- ( ph -> B = ( C i^i K ) )

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		ressmplbas2.w	\|- W = ( I mPwSer H )
8		ressmplbas2.c	\|- C = ( Base ` W )
9		ressmplbas2.k	\|- K = ( Base ` S )
10		eqid	\|- ( I mPwSer R ) = ( I mPwSer R )
11	10 2 7 8	subrgpsr	\|- ( ( I e. V /\ T e. ( SubRing ` R ) ) -> C e. ( SubRing ` ( I mPwSer R ) ) )
12	5 6 11	syl2anc	\|- ( ph -> C e. ( SubRing ` ( I mPwSer R ) ) )
13		eqid	\|- ( Base ` ( I mPwSer R ) ) = ( Base ` ( I mPwSer R ) )
14	13	subrgss	\|- ( C e. ( SubRing ` ( I mPwSer R ) ) -> C C_ ( Base ` ( I mPwSer R ) ) )
15	12 14	syl	\|- ( ph -> C C_ ( Base ` ( I mPwSer R ) ) )
16		dfss2	\|- ( C C_ ( Base ` ( I mPwSer R ) ) <-> ( C i^i ( Base ` ( I mPwSer R ) ) ) = C )
17	15 16	sylib	\|- ( ph -> ( C i^i ( Base ` ( I mPwSer R ) ) ) = C )
18		eqid	\|- ( 0g ` R ) = ( 0g ` R )
19	2 18	subrg0	\|- ( T e. ( SubRing ` R ) -> ( 0g ` R ) = ( 0g ` H ) )
20	6 19	syl	\|- ( ph -> ( 0g ` R ) = ( 0g ` H ) )
21	20	breq2d	\|- ( ph -> ( f finSupp ( 0g ` R ) <-> f finSupp ( 0g ` H ) ) )
22	21	abbidv	\|- ( ph -> { f \| f finSupp ( 0g ` R ) } = { f \| f finSupp ( 0g ` H ) } )
23	17 22	ineq12d	\|- ( ph -> ( ( C i^i ( Base ` ( I mPwSer R ) ) ) i^i { f \| f finSupp ( 0g ` R ) } ) = ( C i^i { f \| f finSupp ( 0g ` H ) } ) )
24	23	eqcomd	\|- ( ph -> ( C i^i { f \| f finSupp ( 0g ` H ) } ) = ( ( C i^i ( Base ` ( I mPwSer R ) ) ) i^i { f \| f finSupp ( 0g ` R ) } ) )
25		eqid	\|- ( 0g ` H ) = ( 0g ` H )
26	3 7 8 25 4	mplbas	\|- B = { f e. C \| f finSupp ( 0g ` H ) }
27		dfrab3	\|- { f e. C \| f finSupp ( 0g ` H ) } = ( C i^i { f \| f finSupp ( 0g ` H ) } )
28	26 27	eqtri	\|- B = ( C i^i { f \| f finSupp ( 0g ` H ) } )
29	1 10 13 18 9	mplbas	\|- K = { f e. ( Base ` ( I mPwSer R ) ) \| f finSupp ( 0g ` R ) }
30		dfrab3	\|- { f e. ( Base ` ( I mPwSer R ) ) \| f finSupp ( 0g ` R ) } = ( ( Base ` ( I mPwSer R ) ) i^i { f \| f finSupp ( 0g ` R ) } )
31	29 30	eqtri	\|- K = ( ( Base ` ( I mPwSer R ) ) i^i { f \| f finSupp ( 0g ` R ) } )
32	31	ineq2i	\|- ( C i^i K ) = ( C i^i ( ( Base ` ( I mPwSer R ) ) i^i { f \| f finSupp ( 0g ` R ) } ) )
33		inass	\|- ( ( C i^i ( Base ` ( I mPwSer R ) ) ) i^i { f \| f finSupp ( 0g ` R ) } ) = ( C i^i ( ( Base ` ( I mPwSer R ) ) i^i { f \| f finSupp ( 0g ` R ) } ) )
34	32 33	eqtr4i	\|- ( C i^i K ) = ( ( C i^i ( Base ` ( I mPwSer R ) ) ) i^i { f \| f finSupp ( 0g ` R ) } )
35	24 28 34	3eqtr4g	\|- ( ph -> B = ( C i^i K ) )

Metamath Proof Explorer

Theorem ressmplbas2

Proof