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

Metamath Proof Explorer

Theorem riccrng1

Description: Ring isomorphism preserves (multiplicative) commutativity. (Contributed by SN, 10-Jan-2025)

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

Proof

Step Hyp Ref Expression
1 brric 
 |-  ( R ~=r S <-> ( R RingIso S ) =/= (/) )
2 n0 
 |-  ( ( R RingIso S ) =/= (/) <-> E. f f e. ( R RingIso S ) )
3 1 2 bitri 
 |-  ( R ~=r S <-> E. f f e. ( R RingIso S ) )
4 eqid 
 |-  ( Base ` R ) = ( Base ` R )
5 eqid 
 |-  ( Base ` S ) = ( Base ` S )
6 4 5 rimf1o 
 |-  ( f e. ( R RingIso S ) -> f : ( Base ` R ) -1-1-onto-> ( Base ` S ) )
7 f1ofo 
 |-  ( f : ( Base ` R ) -1-1-onto-> ( Base ` S ) -> f : ( Base ` R ) -onto-> ( Base ` S ) )
8 foima 
 |-  ( f : ( Base ` R ) -onto-> ( Base ` S ) -> ( f " ( Base ` R ) ) = ( Base ` S ) )
9 6 7 8 3syl 
 |-  ( f e. ( R RingIso S ) -> ( f " ( Base ` R ) ) = ( Base ` S ) )
10 9 oveq2d 
 |-  ( f e. ( R RingIso S ) -> ( S |`s ( f " ( Base ` R ) ) ) = ( S |`s ( Base ` S ) ) )
11 rimrcl2 
 |-  ( f e. ( R RingIso S ) -> S e. Ring )
12 5 ressid 
 |-  ( S e. Ring -> ( S |`s ( Base ` S ) ) = S )
13 11 12 syl 
 |-  ( f e. ( R RingIso S ) -> ( S |`s ( Base ` S ) ) = S )
14 10 13 eqtr2d 
 |-  ( f e. ( R RingIso S ) -> S = ( S |`s ( f " ( Base ` R ) ) ) )
15 14 adantr 
 |-  ( ( f e. ( R RingIso S ) /\ R e. CRing ) -> S = ( S |`s ( f " ( Base ` R ) ) ) )
16 eqid 
 |-  ( S |`s ( f " ( Base ` R ) ) ) = ( S |`s ( f " ( Base ` R ) ) )
17 rimrhm 
 |-  ( f e. ( R RingIso S ) -> f e. ( R RingHom S ) )
18 17 adantr 
 |-  ( ( f e. ( R RingIso S ) /\ R e. CRing ) -> f e. ( R RingHom S ) )
19 simpr 
 |-  ( ( f e. ( R RingIso S ) /\ R e. CRing ) -> R e. CRing )
20 19 crngringd 
 |-  ( ( f e. ( R RingIso S ) /\ R e. CRing ) -> R e. Ring )
21 4 subrgid 
 |-  ( R e. Ring -> ( Base ` R ) e. ( SubRing ` R ) )
22 20 21 syl 
 |-  ( ( f e. ( R RingIso S ) /\ R e. CRing ) -> ( Base ` R ) e. ( SubRing ` R ) )
23 16 18 19 22 imacrhmcl 
 |-  ( ( f e. ( R RingIso S ) /\ R e. CRing ) -> ( S |`s ( f " ( Base ` R ) ) ) e. CRing )
24 15 23 eqeltrd 
 |-  ( ( f e. ( R RingIso S ) /\ R e. CRing ) -> S e. CRing )
25 24 ex 
 |-  ( f e. ( R RingIso S ) -> ( R e. CRing -> S e. CRing ) )
26 25 exlimiv 
 |-  ( E. f f e. ( R RingIso S ) -> ( R e. CRing -> S e. CRing ) )
27 26 imp 
 |-  ( ( E. f f e. ( R RingIso S ) /\ R e. CRing ) -> S e. CRing )
28 3 27 sylanb 
 |-  ( ( R ~=r S /\ R e. CRing ) -> S e. CRing )