Metamath Proof Explorer

Theorem isriscg

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

Ref Expression
Assertion isriscg 
|- ( ( R e. A /\ S e. B ) -> ( R ~=R S <-> ( ( R e. RingOps /\ S e. RingOps ) /\ E. f f e. ( R RngIso S ) ) ) )

Proof

Step Hyp Ref Expression
1 eleq1 
 |-  ( r = R -> ( r e. RingOps <-> R e. RingOps ) )
2 1 anbi1d 
 |-  ( r = R -> ( ( r e. RingOps /\ s e. RingOps ) <-> ( R e. RingOps /\ s e. RingOps ) ) )
3 oveq1 
 |-  ( r = R -> ( r RngIso s ) = ( R RngIso s ) )
4 3 eleq2d 
 |-  ( r = R -> ( f e. ( r RngIso s ) <-> f e. ( R RngIso s ) ) )
5 4 exbidv 
 |-  ( r = R -> ( E. f f e. ( r RngIso s ) <-> E. f f e. ( R RngIso s ) ) )
6 2 5 anbi12d 
 |-  ( r = R -> ( ( ( r e. RingOps /\ s e. RingOps ) /\ E. f f e. ( r RngIso s ) ) <-> ( ( R e. RingOps /\ s e. RingOps ) /\ E. f f e. ( R RngIso s ) ) ) )
7 eleq1 
 |-  ( s = S -> ( s e. RingOps <-> S e. RingOps ) )
8 7 anbi2d 
 |-  ( s = S -> ( ( R e. RingOps /\ s e. RingOps ) <-> ( R e. RingOps /\ S e. RingOps ) ) )
9 oveq2 
 |-  ( s = S -> ( R RngIso s ) = ( R RngIso S ) )
10 9 eleq2d 
 |-  ( s = S -> ( f e. ( R RngIso s ) <-> f e. ( R RngIso S ) ) )
11 10 exbidv 
 |-  ( s = S -> ( E. f f e. ( R RngIso s ) <-> E. f f e. ( R RngIso S ) ) )
12 8 11 anbi12d 
 |-  ( s = S -> ( ( ( R e. RingOps /\ s e. RingOps ) /\ E. f f e. ( R RngIso s ) ) <-> ( ( R e. RingOps /\ S e. RingOps ) /\ E. f f e. ( R RngIso S ) ) ) )
13 df-risc 
 |-  ~=R = { <. r , s >. | ( ( r e. RingOps /\ s e. RingOps ) /\ E. f f e. ( r RngIso s ) ) }
14 6 12 13 brabg 
 |-  ( ( R e. A /\ S e. B ) -> ( R ~=R S <-> ( ( R e. RingOps /\ S e. RingOps ) /\ E. f f e. ( R RngIso S ) ) ) )