This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem brric2

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

Ref Expression
Assertion brric2 ( 𝑅 ≃𝑟 𝑆 ↔ ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ Ring ) ∧ ∃ 𝑓 𝑓 ∈ ( 𝑅 RingIso 𝑆 ) ) )

Proof

Step Hyp Ref Expression
1 brric ⊢ ( 𝑅 ≃𝑟 𝑆 ↔ ( 𝑅 RingIso 𝑆 ) ≠ ∅ )
2 n0 ⊢ ( ( 𝑅 RingIso 𝑆 ) ≠ ∅ ↔ ∃ 𝑓 𝑓 ∈ ( 𝑅 RingIso 𝑆 ) )
3 rimrhm ⊢ ( 𝑓 ∈ ( 𝑅 RingIso 𝑆 ) → 𝑓 ∈ ( 𝑅 RingHom 𝑆 ) )
4 eqid ⊢ ( mulGrp ‘ 𝑅 ) = ( mulGrp ‘ 𝑅 )
5 eqid ⊢ ( mulGrp ‘ 𝑆 ) = ( mulGrp ‘ 𝑆 )
6 4 5 isrhm ⊢ ( 𝑓 ∈ ( 𝑅 RingHom 𝑆 ) ↔ ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ Ring ) ∧ ( 𝑓 ∈ ( 𝑅 GrpHom 𝑆 ) ∧ 𝑓 ∈ ( ( mulGrp ‘ 𝑅 ) MndHom ( mulGrp ‘ 𝑆 ) ) ) ) )
7 6 simplbi ⊢ ( 𝑓 ∈ ( 𝑅 RingHom 𝑆 ) → ( 𝑅 ∈ Ring ∧ 𝑆 ∈ Ring ) )
8 3 7 syl ⊢ ( 𝑓 ∈ ( 𝑅 RingIso 𝑆 ) → ( 𝑅 ∈ Ring ∧ 𝑆 ∈ Ring ) )
9 8 exlimiv ⊢ ( ∃ 𝑓 𝑓 ∈ ( 𝑅 RingIso 𝑆 ) → ( 𝑅 ∈ Ring ∧ 𝑆 ∈ Ring ) )
10 9 pm4.71ri ⊢ ( ∃ 𝑓 𝑓 ∈ ( 𝑅 RingIso 𝑆 ) ↔ ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ Ring ) ∧ ∃ 𝑓 𝑓 ∈ ( 𝑅 RingIso 𝑆 ) ) )
11 1 2 10 3bitri ⊢ ( 𝑅 ≃𝑟 𝑆 ↔ ( ( 𝑅 ∈ Ring ∧ 𝑆 ∈ Ring ) ∧ ∃ 𝑓 𝑓 ∈ ( 𝑅 RingIso 𝑆 ) ) )