ricfld

Description: A ring is a field if and only if an isomorphic ring is a field. (Contributed by SN, 18-Feb-2025)

		Ref	Expression
	Assertion	ricfld	$⊢ R ≃_{𝑟} S \to (R \in Field \leftrightarrow S \in Field)$

Step	Hyp	Ref	Expression
1		ricdrng	$⊢ R ≃_{𝑟} S \to (R \in DivRing \leftrightarrow S \in DivRing)$
2		riccrng	$⊢ R ≃_{𝑟} S \to (R \in CRing \leftrightarrow S \in CRing)$
3	1 2	anbi12d	$⊢ R ≃_{𝑟} S \to ((R \in DivRing \land R \in CRing) \leftrightarrow (S \in DivRing \land S \in CRing))$
4		isfld	$⊢ R \in Field \leftrightarrow (R \in DivRing \land R \in CRing)$
5		isfld	$⊢ S \in Field \leftrightarrow (S \in DivRing \land S \in CRing)$
6	3 4 5	3bitr4g	$⊢ R ≃_{𝑟} S \to (R \in Field \leftrightarrow S \in Field)$

Metamath Proof Explorer