Metamath Proof Explorer

Theorem 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 df-ss 
 |-  ( 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 ) )