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

Metamath Proof Explorer

Theorem ricnzr1

Description: A ring isomorphism maps a nonzero ring to a nonzero ring. (Contributed by Thierry Arnoux, 4-May-2026)

Ref Expression
Assertion ricnzr1 
|- ( ( R ~=r S /\ R e. NzRing ) -> S e. NzRing )

Proof

Step Hyp Ref Expression
1 brric 
 |-  ( R ~=r S <-> ( R RingIso S ) =/= (/) )
2 1 biimpi 
 |-  ( R ~=r S -> ( R RingIso S ) =/= (/) )
3 2 adantr 
 |-  ( ( R ~=r S /\ R e. NzRing ) -> ( R RingIso S ) =/= (/) )
4 rimrcl2 
 |-  ( f e. ( R RingIso S ) -> S e. Ring )
5 4 adantl 
 |-  ( ( ( R ~=r S /\ R e. NzRing ) /\ f e. ( R RingIso S ) ) -> S e. Ring )
6 3 5 n0limd 
 |-  ( ( R ~=r S /\ R e. NzRing ) -> 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 9 ad2antlr 
 |-  ( ( ( R ~=r S /\ R e. NzRing ) /\ f e. ( R RingIso S ) ) -> ( 1r ` R ) =/= ( 0g ` R ) )
11 isrim0 
 |-  ( f e. ( R RingIso S ) <-> ( f e. ( R RingHom S ) /\ `' f e. ( S RingHom R ) ) )
12 11 simprbi 
 |-  ( f e. ( R RingIso S ) -> `' f e. ( S RingHom R ) )
13 12 adantl 
 |-  ( ( ( R ~=r S /\ R e. NzRing ) /\ f e. ( R RingIso S ) ) -> `' f e. ( S RingHom R ) )
14 eqid 
 |-  ( 1r ` S ) = ( 1r ` S )
15 14 7 rhm1 
 |-  ( `' f e. ( S RingHom R ) -> ( `' f ` ( 1r ` S ) ) = ( 1r ` R ) )
16 13 15 syl 
 |-  ( ( ( R ~=r S /\ R e. NzRing ) /\ f e. ( R RingIso S ) ) -> ( `' f ` ( 1r ` S ) ) = ( 1r ` R ) )
17 rhmghm 
 |-  ( `' f e. ( S RingHom R ) -> `' f e. ( S GrpHom R ) )
18 eqid 
 |-  ( 0g ` S ) = ( 0g ` S )
19 18 8 ghmid 
 |-  ( `' f e. ( S GrpHom R ) -> ( `' f ` ( 0g ` S ) ) = ( 0g ` R ) )
20 13 17 19 3syl 
 |-  ( ( ( R ~=r S /\ R e. NzRing ) /\ f e. ( R RingIso S ) ) -> ( `' f ` ( 0g ` S ) ) = ( 0g ` R ) )
21 10 16 20 3netr4d 
 |-  ( ( ( R ~=r S /\ R e. NzRing ) /\ f e. ( R RingIso S ) ) -> ( `' f ` ( 1r ` S ) ) =/= ( `' f ` ( 0g ` S ) ) )
22 fveq2 
 |-  ( ( 1r ` S ) = ( 0g ` S ) -> ( `' f ` ( 1r ` S ) ) = ( `' f ` ( 0g ` S ) ) )
23 22 necon3i 
 |-  ( ( `' f ` ( 1r ` S ) ) =/= ( `' f ` ( 0g ` S ) ) -> ( 1r ` S ) =/= ( 0g ` S ) )
24 21 23 syl 
 |-  ( ( ( R ~=r S /\ R e. NzRing ) /\ f e. ( R RingIso S ) ) -> ( 1r ` S ) =/= ( 0g ` S ) )
25 3 24 n0limd 
 |-  ( ( R ~=r S /\ R e. NzRing ) -> ( 1r ` S ) =/= ( 0g ` S ) )
26 14 18 isnzr 
 |-  ( S e. NzRing <-> ( S e. Ring /\ ( 1r ` S ) =/= ( 0g ` S ) ) )
27 6 25 26 sylanbrc 
 |-  ( ( R ~=r S /\ R e. NzRing ) -> S e. NzRing )