Metamath Proof Explorer

Theorem 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 → R ∈ Field ↔ S ∈ Field

Proof

Step Hyp Ref Expression
1 ricdrng ⊢ R ≃ 𝑟 S → R ∈ DivRing ↔ S ∈ DivRing
2 riccrng ⊢ R ≃ 𝑟 S → R ∈ CRing ↔ S ∈ CRing
3 1 2 anbi12d ⊢ R ≃ 𝑟 S → R ∈ DivRing ∧ R ∈ CRing ↔ S ∈ DivRing ∧ S ∈ CRing
4 isfld ⊢ R ∈ Field ↔ R ∈ DivRing ∧ R ∈ CRing
5 isfld ⊢ S ∈ Field ↔ S ∈ DivRing ∧ S ∈ CRing
6 3 4 5 3bitr4g ⊢ R ≃ 𝑟 S → R ∈ Field ↔ S ∈ Field