Description: The ring isomorphism relation. (Contributed by Jeff Madsen, 16-Jun-2011)
Ref | Expression | ||
---|---|---|---|
Assertion | risc | ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ) → ( 𝑅 ≃𝑟 𝑆 ↔ ∃ 𝑓 𝑓 ∈ ( 𝑅 RngIso 𝑆 ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | isriscg | ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ) → ( 𝑅 ≃𝑟 𝑆 ↔ ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ) ∧ ∃ 𝑓 𝑓 ∈ ( 𝑅 RngIso 𝑆 ) ) ) ) | |
2 | 1 | bianabs | ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ) → ( 𝑅 ≃𝑟 𝑆 ↔ ∃ 𝑓 𝑓 ∈ ( 𝑅 RngIso 𝑆 ) ) ) |