Metamath Proof Explorer

Theorem psrcrng

Description: The ring of power series is commutative ring. (Contributed by Mario Carneiro, 10-Jan-2015)

Ref Expression
Hypotheses psrcnrg.s 
|- S = ( I mPwSer R )
psrcnrg.i 
|- ( ph -> I e. V )
psrcnrg.r 
|- ( ph -> R e. CRing )
Assertion psrcrng 
|- ( ph -> S e. CRing )

Proof

Step Hyp Ref Expression
1 psrcnrg.s 
 |-  S = ( I mPwSer R )
2 psrcnrg.i 
 |-  ( ph -> I e. V )
3 psrcnrg.r 
 |-  ( ph -> R e. CRing )
4 crngring 
 |-  ( R e. CRing -> R e. Ring )
5 3 4 syl 
 |-  ( ph -> R e. Ring )
6 1 2 5 psrring 
 |-  ( ph -> S e. Ring )
7 eqid 
 |-  ( mulGrp ` S ) = ( mulGrp ` S )
8 eqid 
 |-  ( Base ` S ) = ( Base ` S )
9 7 8 mgpbas 
 |-  ( Base ` S ) = ( Base ` ( mulGrp ` S ) )
10 9 a1i 
 |-  ( ph -> ( Base ` S ) = ( Base ` ( mulGrp ` S ) ) )
11 eqid 
 |-  ( .r ` S ) = ( .r ` S )
12 7 11 mgpplusg 
 |-  ( .r ` S ) = ( +g ` ( mulGrp ` S ) )
13 12 a1i 
 |-  ( ph -> ( .r ` S ) = ( +g ` ( mulGrp ` S ) ) )
14 7 ringmgp 
 |-  ( S e. Ring -> ( mulGrp ` S ) e. Mnd )
15 6 14 syl 
 |-  ( ph -> ( mulGrp ` S ) e. Mnd )
16 2 3ad2ant1 
 |-  ( ( ph /\ x e. ( Base ` S ) /\ y e. ( Base ` S ) ) -> I e. V )
17 5 3ad2ant1 
 |-  ( ( ph /\ x e. ( Base ` S ) /\ y e. ( Base ` S ) ) -> R e. Ring )
18 eqid 
 |-  { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } = { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin }
19 simp2 
 |-  ( ( ph /\ x e. ( Base ` S ) /\ y e. ( Base ` S ) ) -> x e. ( Base ` S ) )
20 simp3 
 |-  ( ( ph /\ x e. ( Base ` S ) /\ y e. ( Base ` S ) ) -> y e. ( Base ` S ) )
21 3 3ad2ant1 
 |-  ( ( ph /\ x e. ( Base ` S ) /\ y e. ( Base ` S ) ) -> R e. CRing )
22 1 16 17 18 11 8 19 20 21 psrcom 
 |-  ( ( ph /\ x e. ( Base ` S ) /\ y e. ( Base ` S ) ) -> ( x ( .r ` S ) y ) = ( y ( .r ` S ) x ) )
23 10 13 15 22 iscmnd 
 |-  ( ph -> ( mulGrp ` S ) e. CMnd )
24 7 iscrng 
 |-  ( S e. CRing <-> ( S e. Ring /\ ( mulGrp ` S ) e. CMnd ) )
25 6 23 24 sylanbrc 
 |-  ( ph -> S e. CRing )