Metamath Proof Explorer


Theorem isrisc

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

Ref Expression
Hypotheses isrisc.1
|- R e. _V
isrisc.2
|- S e. _V
Assertion isrisc
|- ( R ~=R S <-> ( ( R e. RingOps /\ S e. RingOps ) /\ E. f f e. ( R RngIso S ) ) )

Proof

Step Hyp Ref Expression
1 isrisc.1
 |-  R e. _V
2 isrisc.2
 |-  S e. _V
3 isriscg
 |-  ( ( R e. _V /\ S e. _V ) -> ( R ~=R S <-> ( ( R e. RingOps /\ S e. RingOps ) /\ E. f f e. ( R RngIso S ) ) ) )
4 1 2 3 mp2an
 |-  ( R ~=R S <-> ( ( R e. RingOps /\ S e. RingOps ) /\ E. f f e. ( R RngIso S ) ) )