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 )