Metamath Proof Explorer


Theorem riccrng1

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

Ref Expression
Assertion riccrng1 ( ( 𝑅𝑟 𝑆𝑅 ∈ CRing ) → 𝑆 ∈ CRing )

Proof

Step Hyp Ref Expression
1 brric ( 𝑅𝑟 𝑆 ↔ ( 𝑅 RingIso 𝑆 ) ≠ ∅ )
2 n0 ( ( 𝑅 RingIso 𝑆 ) ≠ ∅ ↔ ∃ 𝑓 𝑓 ∈ ( 𝑅 RingIso 𝑆 ) )
3 1 2 bitri ( 𝑅𝑟 𝑆 ↔ ∃ 𝑓 𝑓 ∈ ( 𝑅 RingIso 𝑆 ) )
4 eqid ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
5 eqid ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
6 4 5 rimf1o ( 𝑓 ∈ ( 𝑅 RingIso 𝑆 ) → 𝑓 : ( Base ‘ 𝑅 ) –1-1-onto→ ( Base ‘ 𝑆 ) )
7 f1ofo ( 𝑓 : ( Base ‘ 𝑅 ) –1-1-onto→ ( Base ‘ 𝑆 ) → 𝑓 : ( Base ‘ 𝑅 ) –onto→ ( Base ‘ 𝑆 ) )
8 foima ( 𝑓 : ( Base ‘ 𝑅 ) –onto→ ( Base ‘ 𝑆 ) → ( 𝑓 “ ( Base ‘ 𝑅 ) ) = ( Base ‘ 𝑆 ) )
9 6 7 8 3syl ( 𝑓 ∈ ( 𝑅 RingIso 𝑆 ) → ( 𝑓 “ ( Base ‘ 𝑅 ) ) = ( Base ‘ 𝑆 ) )
10 9 oveq2d ( 𝑓 ∈ ( 𝑅 RingIso 𝑆 ) → ( 𝑆s ( 𝑓 “ ( Base ‘ 𝑅 ) ) ) = ( 𝑆s ( Base ‘ 𝑆 ) ) )
11 rimrcl2 ( 𝑓 ∈ ( 𝑅 RingIso 𝑆 ) → 𝑆 ∈ Ring )
12 5 ressid ( 𝑆 ∈ Ring → ( 𝑆s ( Base ‘ 𝑆 ) ) = 𝑆 )
13 11 12 syl ( 𝑓 ∈ ( 𝑅 RingIso 𝑆 ) → ( 𝑆s ( Base ‘ 𝑆 ) ) = 𝑆 )
14 10 13 eqtr2d ( 𝑓 ∈ ( 𝑅 RingIso 𝑆 ) → 𝑆 = ( 𝑆s ( 𝑓 “ ( Base ‘ 𝑅 ) ) ) )
15 14 adantr ( ( 𝑓 ∈ ( 𝑅 RingIso 𝑆 ) ∧ 𝑅 ∈ CRing ) → 𝑆 = ( 𝑆s ( 𝑓 “ ( Base ‘ 𝑅 ) ) ) )
16 eqid ( 𝑆s ( 𝑓 “ ( Base ‘ 𝑅 ) ) ) = ( 𝑆s ( 𝑓 “ ( Base ‘ 𝑅 ) ) )
17 rimrhm ( 𝑓 ∈ ( 𝑅 RingIso 𝑆 ) → 𝑓 ∈ ( 𝑅 RingHom 𝑆 ) )
18 17 adantr ( ( 𝑓 ∈ ( 𝑅 RingIso 𝑆 ) ∧ 𝑅 ∈ CRing ) → 𝑓 ∈ ( 𝑅 RingHom 𝑆 ) )
19 simpr ( ( 𝑓 ∈ ( 𝑅 RingIso 𝑆 ) ∧ 𝑅 ∈ CRing ) → 𝑅 ∈ CRing )
20 19 crngringd ( ( 𝑓 ∈ ( 𝑅 RingIso 𝑆 ) ∧ 𝑅 ∈ CRing ) → 𝑅 ∈ Ring )
21 4 subrgid ( 𝑅 ∈ Ring → ( Base ‘ 𝑅 ) ∈ ( SubRing ‘ 𝑅 ) )
22 20 21 syl ( ( 𝑓 ∈ ( 𝑅 RingIso 𝑆 ) ∧ 𝑅 ∈ CRing ) → ( Base ‘ 𝑅 ) ∈ ( SubRing ‘ 𝑅 ) )
23 16 18 19 22 imacrhmcl ( ( 𝑓 ∈ ( 𝑅 RingIso 𝑆 ) ∧ 𝑅 ∈ CRing ) → ( 𝑆s ( 𝑓 “ ( Base ‘ 𝑅 ) ) ) ∈ CRing )
24 15 23 eqeltrd ( ( 𝑓 ∈ ( 𝑅 RingIso 𝑆 ) ∧ 𝑅 ∈ CRing ) → 𝑆 ∈ CRing )
25 24 ex ( 𝑓 ∈ ( 𝑅 RingIso 𝑆 ) → ( 𝑅 ∈ CRing → 𝑆 ∈ CRing ) )
26 25 exlimiv ( ∃ 𝑓 𝑓 ∈ ( 𝑅 RingIso 𝑆 ) → ( 𝑅 ∈ CRing → 𝑆 ∈ CRing ) )
27 26 imp ( ( ∃ 𝑓 𝑓 ∈ ( 𝑅 RingIso 𝑆 ) ∧ 𝑅 ∈ CRing ) → 𝑆 ∈ CRing )
28 3 27 sylanb ( ( 𝑅𝑟 𝑆𝑅 ∈ CRing ) → 𝑆 ∈ CRing )