# Metamath Proof Explorer

## Theorem brric2

Description: The relation "is isomorphic to" for (unital) rings. This theorem corresponds to the definition df-risc of the ring isomorphism relation in JM's mathbox. (Contributed by AV, 24-Dec-2019)

Ref Expression
Assertion brric2 ${⊢}{R}{\simeq }_{𝑟}{S}↔\left(\left({R}\in \mathrm{Ring}\wedge {S}\in \mathrm{Ring}\right)\wedge \exists {f}\phantom{\rule{.4em}{0ex}}{f}\in \left({R}\mathrm{RingIso}{S}\right)\right)$

### Proof

Step Hyp Ref Expression
1 brric ${⊢}{R}{\simeq }_{𝑟}{S}↔{R}\mathrm{RingIso}{S}\ne \varnothing$
2 n0 ${⊢}{R}\mathrm{RingIso}{S}\ne \varnothing ↔\exists {f}\phantom{\rule{.4em}{0ex}}{f}\in \left({R}\mathrm{RingIso}{S}\right)$
3 rimrcl ${⊢}{f}\in \left({R}\mathrm{RingIso}{S}\right)\to \left({R}\in \mathrm{V}\wedge {S}\in \mathrm{V}\right)$
4 isrim0 ${⊢}\left({R}\in \mathrm{V}\wedge {S}\in \mathrm{V}\right)\to \left({f}\in \left({R}\mathrm{RingIso}{S}\right)↔\left({f}\in \left({R}\mathrm{RingHom}{S}\right)\wedge {{f}}^{-1}\in \left({S}\mathrm{RingHom}{R}\right)\right)\right)$
5 eqid ${⊢}{\mathrm{mulGrp}}_{{R}}={\mathrm{mulGrp}}_{{R}}$
6 eqid ${⊢}{\mathrm{mulGrp}}_{{S}}={\mathrm{mulGrp}}_{{S}}$
7 5 6 isrhm ${⊢}{f}\in \left({R}\mathrm{RingHom}{S}\right)↔\left(\left({R}\in \mathrm{Ring}\wedge {S}\in \mathrm{Ring}\right)\wedge \left({f}\in \left({R}\mathrm{GrpHom}{S}\right)\wedge {f}\in \left({\mathrm{mulGrp}}_{{R}}\mathrm{MndHom}{\mathrm{mulGrp}}_{{S}}\right)\right)\right)$
8 7 simplbi ${⊢}{f}\in \left({R}\mathrm{RingHom}{S}\right)\to \left({R}\in \mathrm{Ring}\wedge {S}\in \mathrm{Ring}\right)$
9 8 adantr ${⊢}\left({f}\in \left({R}\mathrm{RingHom}{S}\right)\wedge {{f}}^{-1}\in \left({S}\mathrm{RingHom}{R}\right)\right)\to \left({R}\in \mathrm{Ring}\wedge {S}\in \mathrm{Ring}\right)$
10 4 9 syl6bi ${⊢}\left({R}\in \mathrm{V}\wedge {S}\in \mathrm{V}\right)\to \left({f}\in \left({R}\mathrm{RingIso}{S}\right)\to \left({R}\in \mathrm{Ring}\wedge {S}\in \mathrm{Ring}\right)\right)$
11 3 10 mpcom ${⊢}{f}\in \left({R}\mathrm{RingIso}{S}\right)\to \left({R}\in \mathrm{Ring}\wedge {S}\in \mathrm{Ring}\right)$
12 11 exlimiv ${⊢}\exists {f}\phantom{\rule{.4em}{0ex}}{f}\in \left({R}\mathrm{RingIso}{S}\right)\to \left({R}\in \mathrm{Ring}\wedge {S}\in \mathrm{Ring}\right)$
13 12 pm4.71ri ${⊢}\exists {f}\phantom{\rule{.4em}{0ex}}{f}\in \left({R}\mathrm{RingIso}{S}\right)↔\left(\left({R}\in \mathrm{Ring}\wedge {S}\in \mathrm{Ring}\right)\wedge \exists {f}\phantom{\rule{.4em}{0ex}}{f}\in \left({R}\mathrm{RingIso}{S}\right)\right)$
14 1 2 13 3bitri ${⊢}{R}{\simeq }_{𝑟}{S}↔\left(\left({R}\in \mathrm{Ring}\wedge {S}\in \mathrm{Ring}\right)\wedge \exists {f}\phantom{\rule{.4em}{0ex}}{f}\in \left({R}\mathrm{RingIso}{S}\right)\right)$