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