Metamath Proof Explorer

Theorem psrring

Description: The ring of power series is a ring. (Contributed by Mario Carneiro, 29-Dec-2014)

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

Proof

Step Hyp Ref Expression
1 psrring.s 
 |-  S = ( I mPwSer R )
2 psrring.i 
 |-  ( ph -> I e. V )
3 psrring.r 
 |-  ( ph -> R e. Ring )
4 eqidd 
 |-  ( ph -> ( Base ` S ) = ( Base ` S ) )
5 eqidd 
 |-  ( ph -> ( +g ` S ) = ( +g ` S ) )
6 eqidd 
 |-  ( ph -> ( .r ` S ) = ( .r ` S ) )
7 ringgrp 
 |-  ( R e. Ring -> R e. Grp )
8 3 7 syl 
 |-  ( ph -> R e. Grp )
9 1 2 8 psrgrp 
 |-  ( ph -> S e. Grp )
10 eqid 
 |-  ( Base ` S ) = ( Base ` S )
11 eqid 
 |-  ( .r ` S ) = ( .r ` S )
12 3 3ad2ant1 
 |-  ( ( ph /\ x e. ( Base ` S ) /\ y e. ( Base ` S ) ) -> R e. Ring )
13 simp2 
 |-  ( ( ph /\ x e. ( Base ` S ) /\ y e. ( Base ` S ) ) -> x e. ( Base ` S ) )
14 simp3 
 |-  ( ( ph /\ x e. ( Base ` S ) /\ y e. ( Base ` S ) ) -> y e. ( Base ` S ) )
15 1 10 11 12 13 14 psrmulcl 
 |-  ( ( ph /\ x e. ( Base ` S ) /\ y e. ( Base ` S ) ) -> ( x ( .r ` S ) y ) e. ( Base ` S ) )
16 2 adantr 
 |-  ( ( ph /\ ( x e. ( Base ` S ) /\ y e. ( Base ` S ) /\ z e. ( Base ` S ) ) ) -> I e. V )
17 3 adantr 
 |-  ( ( ph /\ ( x e. ( Base ` S ) /\ y e. ( Base ` S ) /\ z 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 simpr1 
 |-  ( ( ph /\ ( x e. ( Base ` S ) /\ y e. ( Base ` S ) /\ z e. ( Base ` S ) ) ) -> x e. ( Base ` S ) )
20 simpr2 
 |-  ( ( ph /\ ( x e. ( Base ` S ) /\ y e. ( Base ` S ) /\ z e. ( Base ` S ) ) ) -> y e. ( Base ` S ) )
21 simpr3 
 |-  ( ( ph /\ ( x e. ( Base ` S ) /\ y e. ( Base ` S ) /\ z e. ( Base ` S ) ) ) -> z e. ( Base ` S ) )
22 1 16 17 18 11 10 19 20 21 psrass1 
 |-  ( ( ph /\ ( x e. ( Base ` S ) /\ y e. ( Base ` S ) /\ z e. ( Base ` S ) ) ) -> ( ( x ( .r ` S ) y ) ( .r ` S ) z ) = ( x ( .r ` S ) ( y ( .r ` S ) z ) ) )
23 eqid 
 |-  ( +g ` S ) = ( +g ` S )
24 1 16 17 18 11 10 19 20 21 23 psrdi 
 |-  ( ( ph /\ ( x e. ( Base ` S ) /\ y e. ( Base ` S ) /\ z e. ( Base ` S ) ) ) -> ( x ( .r ` S ) ( y ( +g ` S ) z ) ) = ( ( x ( .r ` S ) y ) ( +g ` S ) ( x ( .r ` S ) z ) ) )
25 1 16 17 18 11 10 19 20 21 23 psrdir 
 |-  ( ( ph /\ ( x e. ( Base ` S ) /\ y e. ( Base ` S ) /\ z e. ( Base ` S ) ) ) -> ( ( x ( +g ` S ) y ) ( .r ` S ) z ) = ( ( x ( .r ` S ) z ) ( +g ` S ) ( y ( .r ` S ) z ) ) )
26 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
27 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
28 eqid 
 |-  ( r e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } |-> if ( r = ( I X. { 0 } ) , ( 1r ` R ) , ( 0g ` R ) ) ) = ( r e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } |-> if ( r = ( I X. { 0 } ) , ( 1r ` R ) , ( 0g ` R ) ) )
29 1 2 3 18 26 27 28 10 psr1cl 
 |-  ( ph -> ( r e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } |-> if ( r = ( I X. { 0 } ) , ( 1r ` R ) , ( 0g ` R ) ) ) e. ( Base ` S ) )
30 2 adantr 
 |-  ( ( ph /\ x e. ( Base ` S ) ) -> I e. V )
31 3 adantr 
 |-  ( ( ph /\ x e. ( Base ` S ) ) -> R e. Ring )
32 simpr 
 |-  ( ( ph /\ x e. ( Base ` S ) ) -> x e. ( Base ` S ) )
33 1 30 31 18 26 27 28 10 11 32 psrlidm 
 |-  ( ( ph /\ x e. ( Base ` S ) ) -> ( ( r e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } |-> if ( r = ( I X. { 0 } ) , ( 1r ` R ) , ( 0g ` R ) ) ) ( .r ` S ) x ) = x )
34 1 30 31 18 26 27 28 10 11 32 psrridm 
 |-  ( ( ph /\ x e. ( Base ` S ) ) -> ( x ( .r ` S ) ( r e. { f e. ( NN0 ^m I ) | ( `' f " NN ) e. Fin } |-> if ( r = ( I X. { 0 } ) , ( 1r ` R ) , ( 0g ` R ) ) ) ) = x )
35 4 5 6 9 15 22 24 25 29 33 34 isringd 
 |-  ( ph -> S e. Ring )