This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem psrnzr

Description: The ring of power series over a nonzero ring form a nonzero ring. (Contributed by Thierry Arnoux, 4-May-2026)

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

Proof

Step Hyp Ref Expression
1 psrnzr.s 
 |-  S = ( I mPwSer R )
2 psrnzr.i 
 |-  ( ph -> I e. V )
3 psrnzr.r 
 |-  ( ph -> R e. NzRing )
4 nzrring 
 |-  ( R e. NzRing -> R e. Ring )
5 3 4 syl 
 |-  ( ph -> R e. Ring )
6 1 2 5 psrring 
 |-  ( ph -> S e. Ring )
7 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
8 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
9 7 8 nzrnz 
 |-  ( R e. NzRing -> ( 1r ` R ) =/= ( 0g ` R ) )
10 3 9 syl 
 |-  ( ph -> ( 1r ` R ) =/= ( 0g ` R ) )
11 eqid 
 |-  { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
12 eqid 
 |-  ( 1r ` S ) = ( 1r ` S )
13 1 2 5 11 8 7 12 psr1 
 |-  ( ph -> ( 1r ` S ) = ( x e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } |-> if ( x = ( I X. { 0 } ) , ( 1r ` R ) , ( 0g ` R ) ) ) )
14 simpr 
 |-  ( ( ph /\ x = ( I X. { 0 } ) ) -> x = ( I X. { 0 } ) )
15 14 iftrued 
 |-  ( ( ph /\ x = ( I X. { 0 } ) ) -> if ( x = ( I X. { 0 } ) , ( 1r ` R ) , ( 0g ` R ) ) = ( 1r ` R ) )
16 11 psrbag0 
 |-  ( I e. V -> ( I X. { 0 } ) e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } )
17 2 16 syl 
 |-  ( ph -> ( I X. { 0 } ) e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } )
18 fvexd 
 |-  ( ph -> ( 1r ` R ) e. _V )
19 13 15 17 18 fvmptd 
 |-  ( ph -> ( ( 1r ` S ) ` ( I X. { 0 } ) ) = ( 1r ` R ) )
20 5 ringgrpd 
 |-  ( ph -> R e. Grp )
21 eqid 
 |-  ( 0g ` S ) = ( 0g ` S )
22 1 2 20 11 8 21 psr0 
 |-  ( ph -> ( 0g ` S ) = ( { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } X. { ( 0g ` R ) } ) )
23 22 fveq1d 
 |-  ( ph -> ( ( 0g ` S ) ` ( I X. { 0 } ) ) = ( ( { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } X. { ( 0g ` R ) } ) ` ( I X. { 0 } ) ) )
24 fvex 
 |-  ( 0g ` R ) e. _V
25 24 fvconst2 
 |-  ( ( I X. { 0 } ) e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } -> ( ( { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } X. { ( 0g ` R ) } ) ` ( I X. { 0 } ) ) = ( 0g ` R ) )
26 17 25 syl 
 |-  ( ph -> ( ( { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } X. { ( 0g ` R ) } ) ` ( I X. { 0 } ) ) = ( 0g ` R ) )
27 23 26 eqtrd 
 |-  ( ph -> ( ( 0g ` S ) ` ( I X. { 0 } ) ) = ( 0g ` R ) )
28 10 19 27 3netr4d 
 |-  ( ph -> ( ( 1r ` S ) ` ( I X. { 0 } ) ) =/= ( ( 0g ` S ) ` ( I X. { 0 } ) ) )
29 fveq1 
 |-  ( ( 1r ` S ) = ( 0g ` S ) -> ( ( 1r ` S ) ` ( I X. { 0 } ) ) = ( ( 0g ` S ) ` ( I X. { 0 } ) ) )
30 29 necon3i 
 |-  ( ( ( 1r ` S ) ` ( I X. { 0 } ) ) =/= ( ( 0g ` S ) ` ( I X. { 0 } ) ) -> ( 1r ` S ) =/= ( 0g ` S ) )
31 28 30 syl 
 |-  ( ph -> ( 1r ` S ) =/= ( 0g ` S ) )
32 12 21 isnzr 
 |-  ( S e. NzRing <-> ( S e. Ring /\ ( 1r ` S ) =/= ( 0g ` S ) ) )
33 6 31 32 sylanbrc 
 |-  ( ph -> S e. NzRing )