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 )