Metamath Proof Explorer

Theorem brric

Description: The relation "is isomorphic to" for (unital) rings. (Contributed by AV, 24-Dec-2019)

Ref Expression
Assertion brric ⊢ R ≃ 𝑟 S ↔ R RingIso S ≠ ∅

Proof

Step Hyp Ref Expression
1 df-ric ⊢ ≃ 𝑟 = RingIso -1 V ∖ 1 𝑜
2 ovex ⊢ r RingHom s ∈ V
3 rabexg ⊢ r RingHom s ∈ V → h ∈ r RingHom s | h -1 ∈ s RingHom r ∈ V
4 2 3 mp1i ⊢ r ∈ V ∧ s ∈ V → h ∈ r RingHom s | h -1 ∈ s RingHom r ∈ V
5 4 rgen2 ⊢ ∀ r ∈ V ∀ s ∈ V h ∈ r RingHom s | h -1 ∈ s RingHom r ∈ V
6 df-rim ⊢ RingIso = r ∈ V , s ∈ V ⟼ h ∈ r RingHom s | h -1 ∈ s RingHom r
7 6 fnmpo ⊢ ∀ r ∈ V ∀ s ∈ V h ∈ r RingHom s | h -1 ∈ s RingHom r ∈ V → RingIso Fn V × V
8 5 7 ax-mp ⊢ RingIso Fn V × V
9 1 8 brwitnlem ⊢ R ≃ 𝑟 S ↔ R RingIso S ≠ ∅