Metamath Proof Explorer


Theorem riccrng1

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

Ref Expression
Assertion riccrng1 R 𝑟 S R CRing S CRing

Proof

Step Hyp Ref Expression
1 brric R 𝑟 S R RingIso S
2 n0 R RingIso S f f R RingIso S
3 1 2 bitri R 𝑟 S f f R RingIso S
4 eqid Base R = Base R
5 eqid Base S = Base S
6 4 5 rimf1o f 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 R RingIso S f Base R = Base S
10 9 oveq2d f R RingIso S S 𝑠 f Base R = S 𝑠 Base S
11 rimrcl2 f R RingIso S S Ring
12 5 ressid S Ring S 𝑠 Base S = S
13 11 12 syl f R RingIso S S 𝑠 Base S = S
14 10 13 eqtr2d f R RingIso S S = S 𝑠 f Base R
15 14 adantr f R RingIso S R CRing S = S 𝑠 f Base R
16 eqid S 𝑠 f Base R = S 𝑠 f Base R
17 rimrhm f R RingIso S f R RingHom S
18 17 adantr f R RingIso S R CRing f R RingHom S
19 simpr f R RingIso S R CRing R CRing
20 19 crngringd f R RingIso S R CRing R Ring
21 4 subrgid R Ring Base R SubRing R
22 20 21 syl f R RingIso S R CRing Base R SubRing R
23 16 18 19 22 imacrhmcl f R RingIso S R CRing S 𝑠 f Base R CRing
24 15 23 eqeltrd f R RingIso S R CRing S CRing
25 24 ex f R RingIso S R CRing S CRing
26 25 exlimiv f f R RingIso S R CRing S CRing
27 26 imp f f R RingIso S R CRing S CRing
28 3 27 sylanb R 𝑟 S R CRing S CRing