Metamath Proof Explorer

Theorem mplsubrg

Description: The set of polynomials is closed under multiplication, i.e. it is a subring of the set of power series. (Contributed by Mario Carneiro, 9-Jan-2015)

Ref Expression
Hypotheses mplsubg.s 
|- S = ( I mPwSer R )
mplsubg.p 
|- P = ( I mPoly R )
mplsubg.u 
|- U = ( Base ` P )
mplsubg.i 
|- ( ph -> I e. W )
mpllss.r 
|- ( ph -> R e. Ring )
Assertion mplsubrg 
|- ( ph -> U e. ( SubRing ` S ) )

Proof

Step Hyp Ref Expression
1 mplsubg.s 
 |-  S = ( I mPwSer R )
2 mplsubg.p 
 |-  P = ( I mPoly R )
3 mplsubg.u 
 |-  U = ( Base ` P )
4 mplsubg.i 
 |-  ( ph -> I e. W )
5 mpllss.r 
 |-  ( ph -> R e. Ring )
6 ringgrp 
 |-  ( R e. Ring -> R e. Grp )
7 5 6 syl 
 |-  ( ph -> R e. Grp )
8 1 2 3 4 7 mplsubg 
 |-  ( ph -> U e. ( SubGrp ` S ) )
9 1 4 5 psrring 
 |-  ( ph -> S e. Ring )
10 eqid 
 |-  ( Base ` S ) = ( Base ` S )
11 eqid 
 |-  ( 1r ` S ) = ( 1r ` S )
12 10 11 ringidcl 
 |-  ( S e. Ring -> ( 1r ` S ) e. ( Base ` S ) )
13 9 12 syl 
 |-  ( ph -> ( 1r ` S ) e. ( Base ` S ) )
14 eqid 
 |-  { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
15 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
16 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
17 1 4 5 14 15 16 11 psr1 
 |-  ( ph -> ( 1r ` S ) = ( k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } |-> if ( k = ( I X. { 0 } ) , ( 1r ` R ) , ( 0g ` R ) ) ) )
18 ovex 
 |-  ( NN0 ^m I ) e. _V
19 18 mptrabex 
 |-  ( k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } |-> if ( k = ( I X. { 0 } ) , ( 1r ` R ) , ( 0g ` R ) ) ) e. _V
20 funmpt 
 |-  Fun ( k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } |-> if ( k = ( I X. { 0 } ) , ( 1r ` R ) , ( 0g ` R ) ) )
21 fvex 
 |-  ( 0g ` R ) e. _V
22 19 20 21 3pm3.2i 
 |-  ( ( k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } |-> if ( k = ( I X. { 0 } ) , ( 1r ` R ) , ( 0g ` R ) ) ) e. _V /\ Fun ( k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } |-> if ( k = ( I X. { 0 } ) , ( 1r ` R ) , ( 0g ` R ) ) ) /\ ( 0g ` R ) e. _V )
23 22 a1i 
 |-  ( ph -> ( ( k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } |-> if ( k = ( I X. { 0 } ) , ( 1r ` R ) , ( 0g ` R ) ) ) e. _V /\ Fun ( k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } |-> if ( k = ( I X. { 0 } ) , ( 1r ` R ) , ( 0g ` R ) ) ) /\ ( 0g ` R ) e. _V ) )
24 snfi 
 |-  { ( I X. { 0 } ) } e. Fin
25 24 a1i 
 |-  ( ph -> { ( I X. { 0 } ) } e. Fin )
26 eldifsni 
 |-  ( k e. ( { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } \ { ( I X. { 0 } ) } ) -> k =/= ( I X. { 0 } ) )
27 26 adantl 
 |-  ( ( ph /\ k e. ( { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } \ { ( I X. { 0 } ) } ) ) -> k =/= ( I X. { 0 } ) )
28 ifnefalse 
 |-  ( k =/= ( I X. { 0 } ) -> if ( k = ( I X. { 0 } ) , ( 1r ` R ) , ( 0g ` R ) ) = ( 0g ` R ) )
29 27 28 syl 
 |-  ( ( ph /\ k e. ( { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } \ { ( I X. { 0 } ) } ) ) -> if ( k = ( I X. { 0 } ) , ( 1r ` R ) , ( 0g ` R ) ) = ( 0g ` R ) )
30 18 rabex 
 |-  { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } e. _V
31 30 a1i 
 |-  ( ph -> { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } e. _V )
32 29 31 suppss2 
 |-  ( ph -> ( ( k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } |-> if ( k = ( I X. { 0 } ) , ( 1r ` R ) , ( 0g ` R ) ) ) supp ( 0g ` R ) ) C_ { ( I X. { 0 } ) } )
33 suppssfifsupp 
 |-  ( ( ( ( k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } |-> if ( k = ( I X. { 0 } ) , ( 1r ` R ) , ( 0g ` R ) ) ) e. _V /\ Fun ( k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } |-> if ( k = ( I X. { 0 } ) , ( 1r ` R ) , ( 0g ` R ) ) ) /\ ( 0g ` R ) e. _V ) /\ ( { ( I X. { 0 } ) } e. Fin /\ ( ( k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } |-> if ( k = ( I X. { 0 } ) , ( 1r ` R ) , ( 0g ` R ) ) ) supp ( 0g ` R ) ) C_ { ( I X. { 0 } ) } ) ) -> ( k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } |-> if ( k = ( I X. { 0 } ) , ( 1r ` R ) , ( 0g ` R ) ) ) finSupp ( 0g ` R ) )
34 23 25 32 33 syl12anc 
 |-  ( ph -> ( k e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } |-> if ( k = ( I X. { 0 } ) , ( 1r ` R ) , ( 0g ` R ) ) ) finSupp ( 0g ` R ) )
35 17 34 eqbrtrd 
 |-  ( ph -> ( 1r ` S ) finSupp ( 0g ` R ) )
36 2 1 10 15 3 mplelbas 
 |-  ( ( 1r ` S ) e. U <-> ( ( 1r ` S ) e. ( Base ` S ) /\ ( 1r ` S ) finSupp ( 0g ` R ) ) )
37 13 35 36 sylanbrc 
 |-  ( ph -> ( 1r ` S ) e. U )
38 4 adantr 
 |-  ( ( ph /\ ( x e. U /\ y e. U ) ) -> I e. W )
39 5 adantr 
 |-  ( ( ph /\ ( x e. U /\ y e. U ) ) -> R e. Ring )
40 eqid 
 |-  ( oF + " ( ( x supp ( 0g ` R ) ) X. ( y supp ( 0g ` R ) ) ) ) = ( oF + " ( ( x supp ( 0g ` R ) ) X. ( y supp ( 0g ` R ) ) ) )
41 eqid 
 |-  ( .r ` R ) = ( .r ` R )
42 simprl 
 |-  ( ( ph /\ ( x e. U /\ y e. U ) ) -> x e. U )
43 simprr 
 |-  ( ( ph /\ ( x e. U /\ y e. U ) ) -> y e. U )
44 1 2 3 38 39 14 15 40 41 42 43 mplsubrglem 
 |-  ( ( ph /\ ( x e. U /\ y e. U ) ) -> ( x ( .r ` S ) y ) e. U )
45 44 ralrimivva 
 |-  ( ph -> A. x e. U A. y e. U ( x ( .r ` S ) y ) e. U )
46 eqid 
 |-  ( .r ` S ) = ( .r ` S )
47 10 11 46 issubrg2 
 |-  ( S e. Ring -> ( U e. ( SubRing ` S ) <-> ( U e. ( SubGrp ` S ) /\ ( 1r ` S ) e. U /\ A. x e. U A. y e. U ( x ( .r ` S ) y ) e. U ) ) )
48 9 47 syl 
 |-  ( ph -> ( U e. ( SubRing ` S ) <-> ( U e. ( SubGrp ` S ) /\ ( 1r ` S ) e. U /\ A. x e. U A. y e. U ( x ( .r ` S ) y ) e. U ) ) )
49 8 37 45 48 mpbir3and 
 |-  ( ph -> U e. ( SubRing ` S ) )