Metamath Proof Explorer

Theorem riscer

Description: Ring isomorphism is an equivalence relation. (Contributed by Jeff Madsen, 16-Jun-2011) (Revised by Mario Carneiro, 12-Aug-2015)

Ref Expression
Assertion riscer 
|- ~=R Er dom ~=R

Proof

Step Hyp Ref Expression
1 df-risc 
 |-  ~=R = { <. r , s >. | ( ( r e. RingOps /\ s e. RingOps ) /\ E. f f e. ( r RngIso s ) ) }
2 1 relopabiv 
 |-  Rel ~=R
3 eqid 
 |-  dom ~=R = dom ~=R
4 vex 
 |-  r e. _V
5 vex 
 |-  s e. _V
6 4 5 isrisc 
 |-  ( r ~=R s <-> ( ( r e. RingOps /\ s e. RingOps ) /\ E. f f e. ( r RngIso s ) ) )
7 rngoisocnv 
 |-  ( ( r e. RingOps /\ s e. RingOps /\ f e. ( r RngIso s ) ) -> `' f e. ( s RngIso r ) )
8 7 3expia 
 |-  ( ( r e. RingOps /\ s e. RingOps ) -> ( f e. ( r RngIso s ) -> `' f e. ( s RngIso r ) ) )
9 risci 
 |-  ( ( s e. RingOps /\ r e. RingOps /\ `' f e. ( s RngIso r ) ) -> s ~=R r )
10 9 3expia 
 |-  ( ( s e. RingOps /\ r e. RingOps ) -> ( `' f e. ( s RngIso r ) -> s ~=R r ) )
11 10 ancoms 
 |-  ( ( r e. RingOps /\ s e. RingOps ) -> ( `' f e. ( s RngIso r ) -> s ~=R r ) )
12 8 11 syld 
 |-  ( ( r e. RingOps /\ s e. RingOps ) -> ( f e. ( r RngIso s ) -> s ~=R r ) )
13 12 exlimdv 
 |-  ( ( r e. RingOps /\ s e. RingOps ) -> ( E. f f e. ( r RngIso s ) -> s ~=R r ) )
14 13 imp 
 |-  ( ( ( r e. RingOps /\ s e. RingOps ) /\ E. f f e. ( r RngIso s ) ) -> s ~=R r )
15 6 14 sylbi 
 |-  ( r ~=R s -> s ~=R r )
16 vex 
 |-  t e. _V
17 5 16 isrisc 
 |-  ( s ~=R t <-> ( ( s e. RingOps /\ t e. RingOps ) /\ E. g g e. ( s RngIso t ) ) )
18 exdistrv 
 |-  ( E. f E. g ( f e. ( r RngIso s ) /\ g e. ( s RngIso t ) ) <-> ( E. f f e. ( r RngIso s ) /\ E. g g e. ( s RngIso t ) ) )
19 rngoisoco 
 |-  ( ( ( r e. RingOps /\ s e. RingOps /\ t e. RingOps ) /\ ( f e. ( r RngIso s ) /\ g e. ( s RngIso t ) ) ) -> ( g o. f ) e. ( r RngIso t ) )
20 19 ex 
 |-  ( ( r e. RingOps /\ s e. RingOps /\ t e. RingOps ) -> ( ( f e. ( r RngIso s ) /\ g e. ( s RngIso t ) ) -> ( g o. f ) e. ( r RngIso t ) ) )
21 risci 
 |-  ( ( r e. RingOps /\ t e. RingOps /\ ( g o. f ) e. ( r RngIso t ) ) -> r ~=R t )
22 21 3expia 
 |-  ( ( r e. RingOps /\ t e. RingOps ) -> ( ( g o. f ) e. ( r RngIso t ) -> r ~=R t ) )
23 22 3adant2 
 |-  ( ( r e. RingOps /\ s e. RingOps /\ t e. RingOps ) -> ( ( g o. f ) e. ( r RngIso t ) -> r ~=R t ) )
24 20 23 syld 
 |-  ( ( r e. RingOps /\ s e. RingOps /\ t e. RingOps ) -> ( ( f e. ( r RngIso s ) /\ g e. ( s RngIso t ) ) -> r ~=R t ) )
25 24 exlimdvv 
 |-  ( ( r e. RingOps /\ s e. RingOps /\ t e. RingOps ) -> ( E. f E. g ( f e. ( r RngIso s ) /\ g e. ( s RngIso t ) ) -> r ~=R t ) )
26 18 25 syl5bir 
 |-  ( ( r e. RingOps /\ s e. RingOps /\ t e. RingOps ) -> ( ( E. f f e. ( r RngIso s ) /\ E. g g e. ( s RngIso t ) ) -> r ~=R t ) )
27 26 3expb 
 |-  ( ( r e. RingOps /\ ( s e. RingOps /\ t e. RingOps ) ) -> ( ( E. f f e. ( r RngIso s ) /\ E. g g e. ( s RngIso t ) ) -> r ~=R t ) )
28 27 adantlr 
 |-  ( ( ( r e. RingOps /\ s e. RingOps ) /\ ( s e. RingOps /\ t e. RingOps ) ) -> ( ( E. f f e. ( r RngIso s ) /\ E. g g e. ( s RngIso t ) ) -> r ~=R t ) )
29 28 imp 
 |-  ( ( ( ( r e. RingOps /\ s e. RingOps ) /\ ( s e. RingOps /\ t e. RingOps ) ) /\ ( E. f f e. ( r RngIso s ) /\ E. g g e. ( s RngIso t ) ) ) -> r ~=R t )
30 29 an4s 
 |-  ( ( ( ( r e. RingOps /\ s e. RingOps ) /\ E. f f e. ( r RngIso s ) ) /\ ( ( s e. RingOps /\ t e. RingOps ) /\ E. g g e. ( s RngIso t ) ) ) -> r ~=R t )
31 6 17 30 syl2anb 
 |-  ( ( r ~=R s /\ s ~=R t ) -> r ~=R t )
32 15 31 pm3.2i 
 |-  ( ( r ~=R s -> s ~=R r ) /\ ( ( r ~=R s /\ s ~=R t ) -> r ~=R t ) )
33 32 ax-gen 
 |-  A. t ( ( r ~=R s -> s ~=R r ) /\ ( ( r ~=R s /\ s ~=R t ) -> r ~=R t ) )
34 33 gen2 
 |-  A. r A. s A. t ( ( r ~=R s -> s ~=R r ) /\ ( ( r ~=R s /\ s ~=R t ) -> r ~=R t ) )
35 dfer2 
 |-  ( ~=R Er dom ~=R <-> ( Rel ~=R /\ dom ~=R = dom ~=R /\ A. r A. s A. t ( ( r ~=R s -> s ~=R r ) /\ ( ( r ~=R s /\ s ~=R t ) -> r ~=R t ) ) ) )
36 2 3 34 35 mpbir3an 
 |-  ~=R Er dom ~=R