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 ) ) ) |
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 ) ) ) |