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

Metamath Proof Explorer

Theorem isrisc

Description: The ring isomorphism relation. (Contributed by Jeff Madsen, 16-Jun-2011)

Ref Expression
Hypotheses isrisc.1 ⊢ 𝑅 ∈ V
isrisc.2 ⊢ 𝑆 ∈ V
Assertion isrisc ( 𝑅 ≃𝑟 𝑆 ↔ ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ) ∧ ∃ 𝑓 𝑓 ∈ ( 𝑅 RingOpsIso 𝑆 ) ) )

Proof

Step Hyp Ref Expression
1 isrisc.1 ⊢ 𝑅 ∈ V
2 isrisc.2 ⊢ 𝑆 ∈ V
3 isriscg ⊢ ( ( 𝑅 ∈ V ∧ 𝑆 ∈ V ) → ( 𝑅 ≃𝑟 𝑆 ↔ ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ) ∧ ∃ 𝑓 𝑓 ∈ ( 𝑅 RingOpsIso 𝑆 ) ) ) )
4 1 2 3 mp2an ⊢ ( 𝑅 ≃𝑟 𝑆 ↔ ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ) ∧ ∃ 𝑓 𝑓 ∈ ( 𝑅 RingOpsIso 𝑆 ) ) )