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 ( ( 𝑅 ≃𝑟 𝑆 ∧ 𝑅 ∈ 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 )