Metamath Proof Explorer


Theorem risc

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

Ref Expression
Assertion risc R RingOps S RingOps R 𝑟 S f f R RngIso S

Proof

Step Hyp Ref Expression
1 isriscg R RingOps S RingOps R 𝑟 S R RingOps S RingOps f f R RngIso S
2 1 bianabs R RingOps S RingOps R 𝑟 S f f R RngIso S