riccrng1

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

		Ref	Expression
	Assertion	riccrng1	$⊢ (R ≃_{𝑟} S \land R \in CRing) \to S \in CRing$

Proof

Step	Hyp	Ref	Expression
1		brric	$⊢ R ≃_{𝑟} S \leftrightarrow R RingIso S \neq \emptyset$
2		n0	$⊢ R RingIso S \neq \emptyset \leftrightarrow \exists f f \in (R RingIso S)$
3	1 2	bitri	$⊢ R ≃_{𝑟} S \leftrightarrow \exists f f \in (R RingIso S)$
4		eqid	$⊢ {Base}_{R} = {Base}_{R}$
5		eqid	$⊢ {Base}_{S} = {Base}_{S}$
6	4 5	rimf1o	$⊢ f \in (R RingIso S) \to f : {Base}_{R} \underset{1-1 onto}{⟶} {Base}_{S}$
7		f1ofo	$⊢ f : {Base}_{R} \underset{1-1 onto}{⟶} {Base}_{S} \to f : {Base}_{R} \underset{onto}{⟶} {Base}_{S}$
8		foima	$⊢ f : {Base}_{R} \underset{onto}{⟶} {Base}_{S} \to f [{Base}_{R}] = {Base}_{S}$
9	6 7 8	3syl	$⊢ f \in (R RingIso S) \to f [{Base}_{R}] = {Base}_{S}$
10	9	oveq2d	$⊢ f \in (R RingIso S) \to S ↾_{𝑠} f [{Base}_{R}] = S ↾_{𝑠} {Base}_{S}$
11		rimrcl2	$⊢ f \in (R RingIso S) \to S \in Ring$
12	5	ressid	$⊢ S \in Ring \to S ↾_{𝑠} {Base}_{S} = S$
13	11 12	syl	$⊢ f \in (R RingIso S) \to S ↾_{𝑠} {Base}_{S} = S$
14	10 13	eqtr2d	$⊢ f \in (R RingIso S) \to S = S ↾_{𝑠} f [{Base}_{R}]$
15	14	adantr	$⊢ (f \in (R RingIso S) \land R \in CRing) \to S = S ↾_{𝑠} f [{Base}_{R}]$
16		eqid	$⊢ S ↾_{𝑠} f [{Base}_{R}] = S ↾_{𝑠} f [{Base}_{R}]$
17		rimrhm	$⊢ f \in (R RingIso S) \to f \in (R RingHom S)$
18	17	adantr	$⊢ (f \in (R RingIso S) \land R \in CRing) \to f \in (R RingHom S)$
19		simpr	$⊢ (f \in (R RingIso S) \land R \in CRing) \to R \in CRing$
20	19	crngringd	$⊢ (f \in (R RingIso S) \land R \in CRing) \to R \in Ring$
21	4	subrgid	$⊢ R \in Ring \to {Base}_{R} \in SubRing (R)$
22	20 21	syl	$⊢ (f \in (R RingIso S) \land R \in CRing) \to {Base}_{R} \in SubRing (R)$
23	16 18 19 22	imacrhmcl	$⊢ (f \in (R RingIso S) \land R \in CRing) \to S ↾_{𝑠} f [{Base}_{R}] \in CRing$
24	15 23	eqeltrd	$⊢ (f \in (R RingIso S) \land R \in CRing) \to S \in CRing$
25	24	ex	$⊢ f \in (R RingIso S) \to (R \in CRing \to S \in CRing)$
26	25	exlimiv	$⊢ \exists f f \in (R RingIso S) \to (R \in CRing \to S \in CRing)$
27	26	imp	$⊢ (\exists f f \in (R RingIso S) \land R \in CRing) \to S \in CRing$
28	3 27	sylanb	$⊢ (R ≃_{𝑟} S \land R \in CRing) \to S \in CRing$

Metamath Proof Explorer

Theorem riccrng1

Proof