Metamath Proof Explorer

Theorem rngoisocnv

Description: The inverse of a ring isomorphism is a ring isomorphism. (Contributed by Jeff Madsen, 16-Jun-2011)

Ref Expression
Assertion rngoisocnv 
|- ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RngIso S ) ) -> `' F e. ( S RngIso R ) )

Proof

Step Hyp Ref Expression
1 f1ocnv 
 |-  ( F : ran ( 1st ` R ) -1-1-onto-> ran ( 1st ` S ) -> `' F : ran ( 1st ` S ) -1-1-onto-> ran ( 1st ` R ) )
2 f1of 
 |-  ( `' F : ran ( 1st ` S ) -1-1-onto-> ran ( 1st ` R ) -> `' F : ran ( 1st ` S ) --> ran ( 1st ` R ) )
3 1 2 syl 
 |-  ( F : ran ( 1st ` R ) -1-1-onto-> ran ( 1st ` S ) -> `' F : ran ( 1st ` S ) --> ran ( 1st ` R ) )
4 3 ad2antll 
 |-  ( ( ( R e. RingOps /\ S e. RingOps ) /\ ( F e. ( R RngHom S ) /\ F : ran ( 1st ` R ) -1-1-onto-> ran ( 1st ` S ) ) ) -> `' F : ran ( 1st ` S ) --> ran ( 1st ` R ) )
5 eqid 
 |-  ( 2nd ` R ) = ( 2nd ` R )
6 eqid 
 |-  ( GId ` ( 2nd ` R ) ) = ( GId ` ( 2nd ` R ) )
7 eqid 
 |-  ( 2nd ` S ) = ( 2nd ` S )
8 eqid 
 |-  ( GId ` ( 2nd ` S ) ) = ( GId ` ( 2nd ` S ) )
9 5 6 7 8 rngohom1 
 |-  ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RngHom S ) ) -> ( F ` ( GId ` ( 2nd ` R ) ) ) = ( GId ` ( 2nd ` S ) ) )
10 9 3expa 
 |-  ( ( ( R e. RingOps /\ S e. RingOps ) /\ F e. ( R RngHom S ) ) -> ( F ` ( GId ` ( 2nd ` R ) ) ) = ( GId ` ( 2nd ` S ) ) )
11 10 adantrr 
 |-  ( ( ( R e. RingOps /\ S e. RingOps ) /\ ( F e. ( R RngHom S ) /\ F : ran ( 1st ` R ) -1-1-onto-> ran ( 1st ` S ) ) ) -> ( F ` ( GId ` ( 2nd ` R ) ) ) = ( GId ` ( 2nd ` S ) ) )
12 eqid 
 |-  ran ( 1st ` R ) = ran ( 1st ` R )
13 12 5 6 rngo1cl 
 |-  ( R e. RingOps -> ( GId ` ( 2nd ` R ) ) e. ran ( 1st ` R ) )
14 f1ocnvfv 
 |-  ( ( F : ran ( 1st ` R ) -1-1-onto-> ran ( 1st ` S ) /\ ( GId ` ( 2nd ` R ) ) e. ran ( 1st ` R ) ) -> ( ( F ` ( GId ` ( 2nd ` R ) ) ) = ( GId ` ( 2nd ` S ) ) -> ( `' F ` ( GId ` ( 2nd ` S ) ) ) = ( GId ` ( 2nd ` R ) ) ) )
15 13 14 sylan2 
 |-  ( ( F : ran ( 1st ` R ) -1-1-onto-> ran ( 1st ` S ) /\ R e. RingOps ) -> ( ( F ` ( GId ` ( 2nd ` R ) ) ) = ( GId ` ( 2nd ` S ) ) -> ( `' F ` ( GId ` ( 2nd ` S ) ) ) = ( GId ` ( 2nd ` R ) ) ) )
16 15 ancoms 
 |-  ( ( R e. RingOps /\ F : ran ( 1st ` R ) -1-1-onto-> ran ( 1st ` S ) ) -> ( ( F ` ( GId ` ( 2nd ` R ) ) ) = ( GId ` ( 2nd ` S ) ) -> ( `' F ` ( GId ` ( 2nd ` S ) ) ) = ( GId ` ( 2nd ` R ) ) ) )
17 16 ad2ant2rl 
 |-  ( ( ( R e. RingOps /\ S e. RingOps ) /\ ( F e. ( R RngHom S ) /\ F : ran ( 1st ` R ) -1-1-onto-> ran ( 1st ` S ) ) ) -> ( ( F ` ( GId ` ( 2nd ` R ) ) ) = ( GId ` ( 2nd ` S ) ) -> ( `' F ` ( GId ` ( 2nd ` S ) ) ) = ( GId ` ( 2nd ` R ) ) ) )
18 11 17 mpd 
 |-  ( ( ( R e. RingOps /\ S e. RingOps ) /\ ( F e. ( R RngHom S ) /\ F : ran ( 1st ` R ) -1-1-onto-> ran ( 1st ` S ) ) ) -> ( `' F ` ( GId ` ( 2nd ` S ) ) ) = ( GId ` ( 2nd ` R ) ) )
19 f1ocnvfv2 
 |-  ( ( F : ran ( 1st ` R ) -1-1-onto-> ran ( 1st ` S ) /\ x e. ran ( 1st ` S ) ) -> ( F ` ( `' F ` x ) ) = x )
20 f1ocnvfv2 
 |-  ( ( F : ran ( 1st ` R ) -1-1-onto-> ran ( 1st ` S ) /\ y e. ran ( 1st ` S ) ) -> ( F ` ( `' F ` y ) ) = y )
21 19 20 anim12dan 
 |-  ( ( F : ran ( 1st ` R ) -1-1-onto-> ran ( 1st ` S ) /\ ( x e. ran ( 1st ` S ) /\ y e. ran ( 1st ` S ) ) ) -> ( ( F ` ( `' F ` x ) ) = x /\ ( F ` ( `' F ` y ) ) = y ) )
22 oveq12 
 |-  ( ( ( F ` ( `' F ` x ) ) = x /\ ( F ` ( `' F ` y ) ) = y ) -> ( ( F ` ( `' F ` x ) ) ( 1st ` S ) ( F ` ( `' F ` y ) ) ) = ( x ( 1st ` S ) y ) )
23 21 22 syl 
 |-  ( ( F : ran ( 1st ` R ) -1-1-onto-> ran ( 1st ` S ) /\ ( x e. ran ( 1st ` S ) /\ y e. ran ( 1st ` S ) ) ) -> ( ( F ` ( `' F ` x ) ) ( 1st ` S ) ( F ` ( `' F ` y ) ) ) = ( x ( 1st ` S ) y ) )
24 23 adantll 
 |-  ( ( ( F e. ( R RngHom S ) /\ F : ran ( 1st ` R ) -1-1-onto-> ran ( 1st ` S ) ) /\ ( x e. ran ( 1st ` S ) /\ y e. ran ( 1st ` S ) ) ) -> ( ( F ` ( `' F ` x ) ) ( 1st ` S ) ( F ` ( `' F ` y ) ) ) = ( x ( 1st ` S ) y ) )
25 24 adantll 
 |-  ( ( ( ( R e. RingOps /\ S e. RingOps ) /\ ( F e. ( R RngHom S ) /\ F : ran ( 1st ` R ) -1-1-onto-> ran ( 1st ` S ) ) ) /\ ( x e. ran ( 1st ` S ) /\ y e. ran ( 1st ` S ) ) ) -> ( ( F ` ( `' F ` x ) ) ( 1st ` S ) ( F ` ( `' F ` y ) ) ) = ( x ( 1st ` S ) y ) )
26 f1ocnvdm 
 |-  ( ( F : ran ( 1st ` R ) -1-1-onto-> ran ( 1st ` S ) /\ x e. ran ( 1st ` S ) ) -> ( `' F ` x ) e. ran ( 1st ` R ) )
27 f1ocnvdm 
 |-  ( ( F : ran ( 1st ` R ) -1-1-onto-> ran ( 1st ` S ) /\ y e. ran ( 1st ` S ) ) -> ( `' F ` y ) e. ran ( 1st ` R ) )
28 26 27 anim12dan 
 |-  ( ( F : ran ( 1st ` R ) -1-1-onto-> ran ( 1st ` S ) /\ ( x e. ran ( 1st ` S ) /\ y e. ran ( 1st ` S ) ) ) -> ( ( `' F ` x ) e. ran ( 1st ` R ) /\ ( `' F ` y ) e. ran ( 1st ` R ) ) )
29 eqid 
 |-  ( 1st ` R ) = ( 1st ` R )
30 eqid 
 |-  ( 1st ` S ) = ( 1st ` S )
31 29 12 30 rngohomadd 
 |-  ( ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RngHom S ) ) /\ ( ( `' F ` x ) e. ran ( 1st ` R ) /\ ( `' F ` y ) e. ran ( 1st ` R ) ) ) -> ( F ` ( ( `' F ` x ) ( 1st ` R ) ( `' F ` y ) ) ) = ( ( F ` ( `' F ` x ) ) ( 1st ` S ) ( F ` ( `' F ` y ) ) ) )
32 28 31 sylan2 
 |-  ( ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RngHom S ) ) /\ ( F : ran ( 1st ` R ) -1-1-onto-> ran ( 1st ` S ) /\ ( x e. ran ( 1st ` S ) /\ y e. ran ( 1st ` S ) ) ) ) -> ( F ` ( ( `' F ` x ) ( 1st ` R ) ( `' F ` y ) ) ) = ( ( F ` ( `' F ` x ) ) ( 1st ` S ) ( F ` ( `' F ` y ) ) ) )
33 32 exp32 
 |-  ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RngHom S ) ) -> ( F : ran ( 1st ` R ) -1-1-onto-> ran ( 1st ` S ) -> ( ( x e. ran ( 1st ` S ) /\ y e. ran ( 1st ` S ) ) -> ( F ` ( ( `' F ` x ) ( 1st ` R ) ( `' F ` y ) ) ) = ( ( F ` ( `' F ` x ) ) ( 1st ` S ) ( F ` ( `' F ` y ) ) ) ) ) )
34 33 3expa 
 |-  ( ( ( R e. RingOps /\ S e. RingOps ) /\ F e. ( R RngHom S ) ) -> ( F : ran ( 1st ` R ) -1-1-onto-> ran ( 1st ` S ) -> ( ( x e. ran ( 1st ` S ) /\ y e. ran ( 1st ` S ) ) -> ( F ` ( ( `' F ` x ) ( 1st ` R ) ( `' F ` y ) ) ) = ( ( F ` ( `' F ` x ) ) ( 1st ` S ) ( F ` ( `' F ` y ) ) ) ) ) )
35 34 impr 
 |-  ( ( ( R e. RingOps /\ S e. RingOps ) /\ ( F e. ( R RngHom S ) /\ F : ran ( 1st ` R ) -1-1-onto-> ran ( 1st ` S ) ) ) -> ( ( x e. ran ( 1st ` S ) /\ y e. ran ( 1st ` S ) ) -> ( F ` ( ( `' F ` x ) ( 1st ` R ) ( `' F ` y ) ) ) = ( ( F ` ( `' F ` x ) ) ( 1st ` S ) ( F ` ( `' F ` y ) ) ) ) )
36 35 imp 
 |-  ( ( ( ( R e. RingOps /\ S e. RingOps ) /\ ( F e. ( R RngHom S ) /\ F : ran ( 1st ` R ) -1-1-onto-> ran ( 1st ` S ) ) ) /\ ( x e. ran ( 1st ` S ) /\ y e. ran ( 1st ` S ) ) ) -> ( F ` ( ( `' F ` x ) ( 1st ` R ) ( `' F ` y ) ) ) = ( ( F ` ( `' F ` x ) ) ( 1st ` S ) ( F ` ( `' F ` y ) ) ) )
37 eqid 
 |-  ran ( 1st ` S ) = ran ( 1st ` S )
38 30 37 rngogcl 
 |-  ( ( S e. RingOps /\ x e. ran ( 1st ` S ) /\ y e. ran ( 1st ` S ) ) -> ( x ( 1st ` S ) y ) e. ran ( 1st ` S ) )
39 38 3expb 
 |-  ( ( S e. RingOps /\ ( x e. ran ( 1st ` S ) /\ y e. ran ( 1st ` S ) ) ) -> ( x ( 1st ` S ) y ) e. ran ( 1st ` S ) )
40 f1ocnvfv2 
 |-  ( ( F : ran ( 1st ` R ) -1-1-onto-> ran ( 1st ` S ) /\ ( x ( 1st ` S ) y ) e. ran ( 1st ` S ) ) -> ( F ` ( `' F ` ( x ( 1st ` S ) y ) ) ) = ( x ( 1st ` S ) y ) )
41 40 ancoms 
 |-  ( ( ( x ( 1st ` S ) y ) e. ran ( 1st ` S ) /\ F : ran ( 1st ` R ) -1-1-onto-> ran ( 1st ` S ) ) -> ( F ` ( `' F ` ( x ( 1st ` S ) y ) ) ) = ( x ( 1st ` S ) y ) )
42 39 41 sylan 
 |-  ( ( ( S e. RingOps /\ ( x e. ran ( 1st ` S ) /\ y e. ran ( 1st ` S ) ) ) /\ F : ran ( 1st ` R ) -1-1-onto-> ran ( 1st ` S ) ) -> ( F ` ( `' F ` ( x ( 1st ` S ) y ) ) ) = ( x ( 1st ` S ) y ) )
43 42 an32s 
 |-  ( ( ( S e. RingOps /\ F : ran ( 1st ` R ) -1-1-onto-> ran ( 1st ` S ) ) /\ ( x e. ran ( 1st ` S ) /\ y e. ran ( 1st ` S ) ) ) -> ( F ` ( `' F ` ( x ( 1st ` S ) y ) ) ) = ( x ( 1st ` S ) y ) )
44 43 adantlll 
 |-  ( ( ( ( R e. RingOps /\ S e. RingOps ) /\ F : ran ( 1st ` R ) -1-1-onto-> ran ( 1st ` S ) ) /\ ( x e. ran ( 1st ` S ) /\ y e. ran ( 1st ` S ) ) ) -> ( F ` ( `' F ` ( x ( 1st ` S ) y ) ) ) = ( x ( 1st ` S ) y ) )
45 44 adantlrl 
 |-  ( ( ( ( R e. RingOps /\ S e. RingOps ) /\ ( F e. ( R RngHom S ) /\ F : ran ( 1st ` R ) -1-1-onto-> ran ( 1st ` S ) ) ) /\ ( x e. ran ( 1st ` S ) /\ y e. ran ( 1st ` S ) ) ) -> ( F ` ( `' F ` ( x ( 1st ` S ) y ) ) ) = ( x ( 1st ` S ) y ) )
46 25 36 45 3eqtr4rd 
 |-  ( ( ( ( R e. RingOps /\ S e. RingOps ) /\ ( F e. ( R RngHom S ) /\ F : ran ( 1st ` R ) -1-1-onto-> ran ( 1st ` S ) ) ) /\ ( x e. ran ( 1st ` S ) /\ y e. ran ( 1st ` S ) ) ) -> ( F ` ( `' F ` ( x ( 1st ` S ) y ) ) ) = ( F ` ( ( `' F ` x ) ( 1st ` R ) ( `' F ` y ) ) ) )
47 f1of1 
 |-  ( F : ran ( 1st ` R ) -1-1-onto-> ran ( 1st ` S ) -> F : ran ( 1st ` R ) -1-1-> ran ( 1st ` S ) )
48 47 ad2antlr 
 |-  ( ( ( ( R e. RingOps /\ S e. RingOps ) /\ F : ran ( 1st ` R ) -1-1-onto-> ran ( 1st ` S ) ) /\ ( x e. ran ( 1st ` S ) /\ y e. ran ( 1st ` S ) ) ) -> F : ran ( 1st ` R ) -1-1-> ran ( 1st ` S ) )
49 f1ocnvdm 
 |-  ( ( F : ran ( 1st ` R ) -1-1-onto-> ran ( 1st ` S ) /\ ( x ( 1st ` S ) y ) e. ran ( 1st ` S ) ) -> ( `' F ` ( x ( 1st ` S ) y ) ) e. ran ( 1st ` R ) )
50 49 ancoms 
 |-  ( ( ( x ( 1st ` S ) y ) e. ran ( 1st ` S ) /\ F : ran ( 1st ` R ) -1-1-onto-> ran ( 1st ` S ) ) -> ( `' F ` ( x ( 1st ` S ) y ) ) e. ran ( 1st ` R ) )
51 39 50 sylan 
 |-  ( ( ( S e. RingOps /\ ( x e. ran ( 1st ` S ) /\ y e. ran ( 1st ` S ) ) ) /\ F : ran ( 1st ` R ) -1-1-onto-> ran ( 1st ` S ) ) -> ( `' F ` ( x ( 1st ` S ) y ) ) e. ran ( 1st ` R ) )
52 51 an32s 
 |-  ( ( ( S e. RingOps /\ F : ran ( 1st ` R ) -1-1-onto-> ran ( 1st ` S ) ) /\ ( x e. ran ( 1st ` S ) /\ y e. ran ( 1st ` S ) ) ) -> ( `' F ` ( x ( 1st ` S ) y ) ) e. ran ( 1st ` R ) )
53 52 adantlll 
 |-  ( ( ( ( R e. RingOps /\ S e. RingOps ) /\ F : ran ( 1st ` R ) -1-1-onto-> ran ( 1st ` S ) ) /\ ( x e. ran ( 1st ` S ) /\ y e. ran ( 1st ` S ) ) ) -> ( `' F ` ( x ( 1st ` S ) y ) ) e. ran ( 1st ` R ) )
54 29 12 rngogcl 
 |-  ( ( R e. RingOps /\ ( `' F ` x ) e. ran ( 1st ` R ) /\ ( `' F ` y ) e. ran ( 1st ` R ) ) -> ( ( `' F ` x ) ( 1st ` R ) ( `' F ` y ) ) e. ran ( 1st ` R ) )
55 54 3expb 
 |-  ( ( R e. RingOps /\ ( ( `' F ` x ) e. ran ( 1st ` R ) /\ ( `' F ` y ) e. ran ( 1st ` R ) ) ) -> ( ( `' F ` x ) ( 1st ` R ) ( `' F ` y ) ) e. ran ( 1st ` R ) )
56 28 55 sylan2 
 |-  ( ( R e. RingOps /\ ( F : ran ( 1st ` R ) -1-1-onto-> ran ( 1st ` S ) /\ ( x e. ran ( 1st ` S ) /\ y e. ran ( 1st ` S ) ) ) ) -> ( ( `' F ` x ) ( 1st ` R ) ( `' F ` y ) ) e. ran ( 1st ` R ) )
57 56 anassrs 
 |-  ( ( ( R e. RingOps /\ F : ran ( 1st ` R ) -1-1-onto-> ran ( 1st ` S ) ) /\ ( x e. ran ( 1st ` S ) /\ y e. ran ( 1st ` S ) ) ) -> ( ( `' F ` x ) ( 1st ` R ) ( `' F ` y ) ) e. ran ( 1st ` R ) )
58 57 adantllr 
 |-  ( ( ( ( R e. RingOps /\ S e. RingOps ) /\ F : ran ( 1st ` R ) -1-1-onto-> ran ( 1st ` S ) ) /\ ( x e. ran ( 1st ` S ) /\ y e. ran ( 1st ` S ) ) ) -> ( ( `' F ` x ) ( 1st ` R ) ( `' F ` y ) ) e. ran ( 1st ` R ) )
59 f1fveq 
 |-  ( ( F : ran ( 1st ` R ) -1-1-> ran ( 1st ` S ) /\ ( ( `' F ` ( x ( 1st ` S ) y ) ) e. ran ( 1st ` R ) /\ ( ( `' F ` x ) ( 1st ` R ) ( `' F ` y ) ) e. ran ( 1st ` R ) ) ) -> ( ( F ` ( `' F ` ( x ( 1st ` S ) y ) ) ) = ( F ` ( ( `' F ` x ) ( 1st ` R ) ( `' F ` y ) ) ) <-> ( `' F ` ( x ( 1st ` S ) y ) ) = ( ( `' F ` x ) ( 1st ` R ) ( `' F ` y ) ) ) )
60 48 53 58 59 syl12anc 
 |-  ( ( ( ( R e. RingOps /\ S e. RingOps ) /\ F : ran ( 1st ` R ) -1-1-onto-> ran ( 1st ` S ) ) /\ ( x e. ran ( 1st ` S ) /\ y e. ran ( 1st ` S ) ) ) -> ( ( F ` ( `' F ` ( x ( 1st ` S ) y ) ) ) = ( F ` ( ( `' F ` x ) ( 1st ` R ) ( `' F ` y ) ) ) <-> ( `' F ` ( x ( 1st ` S ) y ) ) = ( ( `' F ` x ) ( 1st ` R ) ( `' F ` y ) ) ) )
61 60 adantlrl 
 |-  ( ( ( ( R e. RingOps /\ S e. RingOps ) /\ ( F e. ( R RngHom S ) /\ F : ran ( 1st ` R ) -1-1-onto-> ran ( 1st ` S ) ) ) /\ ( x e. ran ( 1st ` S ) /\ y e. ran ( 1st ` S ) ) ) -> ( ( F ` ( `' F ` ( x ( 1st ` S ) y ) ) ) = ( F ` ( ( `' F ` x ) ( 1st ` R ) ( `' F ` y ) ) ) <-> ( `' F ` ( x ( 1st ` S ) y ) ) = ( ( `' F ` x ) ( 1st ` R ) ( `' F ` y ) ) ) )
62 46 61 mpbid 
 |-  ( ( ( ( R e. RingOps /\ S e. RingOps ) /\ ( F e. ( R RngHom S ) /\ F : ran ( 1st ` R ) -1-1-onto-> ran ( 1st ` S ) ) ) /\ ( x e. ran ( 1st ` S ) /\ y e. ran ( 1st ` S ) ) ) -> ( `' F ` ( x ( 1st ` S ) y ) ) = ( ( `' F ` x ) ( 1st ` R ) ( `' F ` y ) ) )
63 oveq12 
 |-  ( ( ( F ` ( `' F ` x ) ) = x /\ ( F ` ( `' F ` y ) ) = y ) -> ( ( F ` ( `' F ` x ) ) ( 2nd ` S ) ( F ` ( `' F ` y ) ) ) = ( x ( 2nd ` S ) y ) )
64 21 63 syl 
 |-  ( ( F : ran ( 1st ` R ) -1-1-onto-> ran ( 1st ` S ) /\ ( x e. ran ( 1st ` S ) /\ y e. ran ( 1st ` S ) ) ) -> ( ( F ` ( `' F ` x ) ) ( 2nd ` S ) ( F ` ( `' F ` y ) ) ) = ( x ( 2nd ` S ) y ) )
65 64 adantll 
 |-  ( ( ( F e. ( R RngHom S ) /\ F : ran ( 1st ` R ) -1-1-onto-> ran ( 1st ` S ) ) /\ ( x e. ran ( 1st ` S ) /\ y e. ran ( 1st ` S ) ) ) -> ( ( F ` ( `' F ` x ) ) ( 2nd ` S ) ( F ` ( `' F ` y ) ) ) = ( x ( 2nd ` S ) y ) )
66 65 adantll 
 |-  ( ( ( ( R e. RingOps /\ S e. RingOps ) /\ ( F e. ( R RngHom S ) /\ F : ran ( 1st ` R ) -1-1-onto-> ran ( 1st ` S ) ) ) /\ ( x e. ran ( 1st ` S ) /\ y e. ran ( 1st ` S ) ) ) -> ( ( F ` ( `' F ` x ) ) ( 2nd ` S ) ( F ` ( `' F ` y ) ) ) = ( x ( 2nd ` S ) y ) )
67 29 12 5 7 rngohommul 
 |-  ( ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RngHom S ) ) /\ ( ( `' F ` x ) e. ran ( 1st ` R ) /\ ( `' F ` y ) e. ran ( 1st ` R ) ) ) -> ( F ` ( ( `' F ` x ) ( 2nd ` R ) ( `' F ` y ) ) ) = ( ( F ` ( `' F ` x ) ) ( 2nd ` S ) ( F ` ( `' F ` y ) ) ) )
68 28 67 sylan2 
 |-  ( ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RngHom S ) ) /\ ( F : ran ( 1st ` R ) -1-1-onto-> ran ( 1st ` S ) /\ ( x e. ran ( 1st ` S ) /\ y e. ran ( 1st ` S ) ) ) ) -> ( F ` ( ( `' F ` x ) ( 2nd ` R ) ( `' F ` y ) ) ) = ( ( F ` ( `' F ` x ) ) ( 2nd ` S ) ( F ` ( `' F ` y ) ) ) )
69 68 exp32 
 |-  ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RngHom S ) ) -> ( F : ran ( 1st ` R ) -1-1-onto-> ran ( 1st ` S ) -> ( ( x e. ran ( 1st ` S ) /\ y e. ran ( 1st ` S ) ) -> ( F ` ( ( `' F ` x ) ( 2nd ` R ) ( `' F ` y ) ) ) = ( ( F ` ( `' F ` x ) ) ( 2nd ` S ) ( F ` ( `' F ` y ) ) ) ) ) )
70 69 3expa 
 |-  ( ( ( R e. RingOps /\ S e. RingOps ) /\ F e. ( R RngHom S ) ) -> ( F : ran ( 1st ` R ) -1-1-onto-> ran ( 1st ` S ) -> ( ( x e. ran ( 1st ` S ) /\ y e. ran ( 1st ` S ) ) -> ( F ` ( ( `' F ` x ) ( 2nd ` R ) ( `' F ` y ) ) ) = ( ( F ` ( `' F ` x ) ) ( 2nd ` S ) ( F ` ( `' F ` y ) ) ) ) ) )
71 70 impr 
 |-  ( ( ( R e. RingOps /\ S e. RingOps ) /\ ( F e. ( R RngHom S ) /\ F : ran ( 1st ` R ) -1-1-onto-> ran ( 1st ` S ) ) ) -> ( ( x e. ran ( 1st ` S ) /\ y e. ran ( 1st ` S ) ) -> ( F ` ( ( `' F ` x ) ( 2nd ` R ) ( `' F ` y ) ) ) = ( ( F ` ( `' F ` x ) ) ( 2nd ` S ) ( F ` ( `' F ` y ) ) ) ) )
72 71 imp 
 |-  ( ( ( ( R e. RingOps /\ S e. RingOps ) /\ ( F e. ( R RngHom S ) /\ F : ran ( 1st ` R ) -1-1-onto-> ran ( 1st ` S ) ) ) /\ ( x e. ran ( 1st ` S ) /\ y e. ran ( 1st ` S ) ) ) -> ( F ` ( ( `' F ` x ) ( 2nd ` R ) ( `' F ` y ) ) ) = ( ( F ` ( `' F ` x ) ) ( 2nd ` S ) ( F ` ( `' F ` y ) ) ) )
73 30 7 37 rngocl 
 |-  ( ( S e. RingOps /\ x e. ran ( 1st ` S ) /\ y e. ran ( 1st ` S ) ) -> ( x ( 2nd ` S ) y ) e. ran ( 1st ` S ) )
74 73 3expb 
 |-  ( ( S e. RingOps /\ ( x e. ran ( 1st ` S ) /\ y e. ran ( 1st ` S ) ) ) -> ( x ( 2nd ` S ) y ) e. ran ( 1st ` S ) )
75 f1ocnvfv2 
 |-  ( ( F : ran ( 1st ` R ) -1-1-onto-> ran ( 1st ` S ) /\ ( x ( 2nd ` S ) y ) e. ran ( 1st ` S ) ) -> ( F ` ( `' F ` ( x ( 2nd ` S ) y ) ) ) = ( x ( 2nd ` S ) y ) )
76 75 ancoms 
 |-  ( ( ( x ( 2nd ` S ) y ) e. ran ( 1st ` S ) /\ F : ran ( 1st ` R ) -1-1-onto-> ran ( 1st ` S ) ) -> ( F ` ( `' F ` ( x ( 2nd ` S ) y ) ) ) = ( x ( 2nd ` S ) y ) )
77 74 76 sylan 
 |-  ( ( ( S e. RingOps /\ ( x e. ran ( 1st ` S ) /\ y e. ran ( 1st ` S ) ) ) /\ F : ran ( 1st ` R ) -1-1-onto-> ran ( 1st ` S ) ) -> ( F ` ( `' F ` ( x ( 2nd ` S ) y ) ) ) = ( x ( 2nd ` S ) y ) )
78 77 an32s 
 |-  ( ( ( S e. RingOps /\ F : ran ( 1st ` R ) -1-1-onto-> ran ( 1st ` S ) ) /\ ( x e. ran ( 1st ` S ) /\ y e. ran ( 1st ` S ) ) ) -> ( F ` ( `' F ` ( x ( 2nd ` S ) y ) ) ) = ( x ( 2nd ` S ) y ) )
79 78 adantlll 
 |-  ( ( ( ( R e. RingOps /\ S e. RingOps ) /\ F : ran ( 1st ` R ) -1-1-onto-> ran ( 1st ` S ) ) /\ ( x e. ran ( 1st ` S ) /\ y e. ran ( 1st ` S ) ) ) -> ( F ` ( `' F ` ( x ( 2nd ` S ) y ) ) ) = ( x ( 2nd ` S ) y ) )
80 79 adantlrl 
 |-  ( ( ( ( R e. RingOps /\ S e. RingOps ) /\ ( F e. ( R RngHom S ) /\ F : ran ( 1st ` R ) -1-1-onto-> ran ( 1st ` S ) ) ) /\ ( x e. ran ( 1st ` S ) /\ y e. ran ( 1st ` S ) ) ) -> ( F ` ( `' F ` ( x ( 2nd ` S ) y ) ) ) = ( x ( 2nd ` S ) y ) )
81 66 72 80 3eqtr4rd 
 |-  ( ( ( ( R e. RingOps /\ S e. RingOps ) /\ ( F e. ( R RngHom S ) /\ F : ran ( 1st ` R ) -1-1-onto-> ran ( 1st ` S ) ) ) /\ ( x e. ran ( 1st ` S ) /\ y e. ran ( 1st ` S ) ) ) -> ( F ` ( `' F ` ( x ( 2nd ` S ) y ) ) ) = ( F ` ( ( `' F ` x ) ( 2nd ` R ) ( `' F ` y ) ) ) )
82 f1ocnvdm 
 |-  ( ( F : ran ( 1st ` R ) -1-1-onto-> ran ( 1st ` S ) /\ ( x ( 2nd ` S ) y ) e. ran ( 1st ` S ) ) -> ( `' F ` ( x ( 2nd ` S ) y ) ) e. ran ( 1st ` R ) )
83 82 ancoms 
 |-  ( ( ( x ( 2nd ` S ) y ) e. ran ( 1st ` S ) /\ F : ran ( 1st ` R ) -1-1-onto-> ran ( 1st ` S ) ) -> ( `' F ` ( x ( 2nd ` S ) y ) ) e. ran ( 1st ` R ) )
84 74 83 sylan 
 |-  ( ( ( S e. RingOps /\ ( x e. ran ( 1st ` S ) /\ y e. ran ( 1st ` S ) ) ) /\ F : ran ( 1st ` R ) -1-1-onto-> ran ( 1st ` S ) ) -> ( `' F ` ( x ( 2nd ` S ) y ) ) e. ran ( 1st ` R ) )
85 84 an32s 
 |-  ( ( ( S e. RingOps /\ F : ran ( 1st ` R ) -1-1-onto-> ran ( 1st ` S ) ) /\ ( x e. ran ( 1st ` S ) /\ y e. ran ( 1st ` S ) ) ) -> ( `' F ` ( x ( 2nd ` S ) y ) ) e. ran ( 1st ` R ) )
86 85 adantlll 
 |-  ( ( ( ( R e. RingOps /\ S e. RingOps ) /\ F : ran ( 1st ` R ) -1-1-onto-> ran ( 1st ` S ) ) /\ ( x e. ran ( 1st ` S ) /\ y e. ran ( 1st ` S ) ) ) -> ( `' F ` ( x ( 2nd ` S ) y ) ) e. ran ( 1st ` R ) )
87 29 5 12 rngocl 
 |-  ( ( R e. RingOps /\ ( `' F ` x ) e. ran ( 1st ` R ) /\ ( `' F ` y ) e. ran ( 1st ` R ) ) -> ( ( `' F ` x ) ( 2nd ` R ) ( `' F ` y ) ) e. ran ( 1st ` R ) )
88 87 3expb 
 |-  ( ( R e. RingOps /\ ( ( `' F ` x ) e. ran ( 1st ` R ) /\ ( `' F ` y ) e. ran ( 1st ` R ) ) ) -> ( ( `' F ` x ) ( 2nd ` R ) ( `' F ` y ) ) e. ran ( 1st ` R ) )
89 28 88 sylan2 
 |-  ( ( R e. RingOps /\ ( F : ran ( 1st ` R ) -1-1-onto-> ran ( 1st ` S ) /\ ( x e. ran ( 1st ` S ) /\ y e. ran ( 1st ` S ) ) ) ) -> ( ( `' F ` x ) ( 2nd ` R ) ( `' F ` y ) ) e. ran ( 1st ` R ) )
90 89 anassrs 
 |-  ( ( ( R e. RingOps /\ F : ran ( 1st ` R ) -1-1-onto-> ran ( 1st ` S ) ) /\ ( x e. ran ( 1st ` S ) /\ y e. ran ( 1st ` S ) ) ) -> ( ( `' F ` x ) ( 2nd ` R ) ( `' F ` y ) ) e. ran ( 1st ` R ) )
91 90 adantllr 
 |-  ( ( ( ( R e. RingOps /\ S e. RingOps ) /\ F : ran ( 1st ` R ) -1-1-onto-> ran ( 1st ` S ) ) /\ ( x e. ran ( 1st ` S ) /\ y e. ran ( 1st ` S ) ) ) -> ( ( `' F ` x ) ( 2nd ` R ) ( `' F ` y ) ) e. ran ( 1st ` R ) )
92 f1fveq 
 |-  ( ( F : ran ( 1st ` R ) -1-1-> ran ( 1st ` S ) /\ ( ( `' F ` ( x ( 2nd ` S ) y ) ) e. ran ( 1st ` R ) /\ ( ( `' F ` x ) ( 2nd ` R ) ( `' F ` y ) ) e. ran ( 1st ` R ) ) ) -> ( ( F ` ( `' F ` ( x ( 2nd ` S ) y ) ) ) = ( F ` ( ( `' F ` x ) ( 2nd ` R ) ( `' F ` y ) ) ) <-> ( `' F ` ( x ( 2nd ` S ) y ) ) = ( ( `' F ` x ) ( 2nd ` R ) ( `' F ` y ) ) ) )
93 48 86 91 92 syl12anc 
 |-  ( ( ( ( R e. RingOps /\ S e. RingOps ) /\ F : ran ( 1st ` R ) -1-1-onto-> ran ( 1st ` S ) ) /\ ( x e. ran ( 1st ` S ) /\ y e. ran ( 1st ` S ) ) ) -> ( ( F ` ( `' F ` ( x ( 2nd ` S ) y ) ) ) = ( F ` ( ( `' F ` x ) ( 2nd ` R ) ( `' F ` y ) ) ) <-> ( `' F ` ( x ( 2nd ` S ) y ) ) = ( ( `' F ` x ) ( 2nd ` R ) ( `' F ` y ) ) ) )
94 93 adantlrl 
 |-  ( ( ( ( R e. RingOps /\ S e. RingOps ) /\ ( F e. ( R RngHom S ) /\ F : ran ( 1st ` R ) -1-1-onto-> ran ( 1st ` S ) ) ) /\ ( x e. ran ( 1st ` S ) /\ y e. ran ( 1st ` S ) ) ) -> ( ( F ` ( `' F ` ( x ( 2nd ` S ) y ) ) ) = ( F ` ( ( `' F ` x ) ( 2nd ` R ) ( `' F ` y ) ) ) <-> ( `' F ` ( x ( 2nd ` S ) y ) ) = ( ( `' F ` x ) ( 2nd ` R ) ( `' F ` y ) ) ) )
95 81 94 mpbid 
 |-  ( ( ( ( R e. RingOps /\ S e. RingOps ) /\ ( F e. ( R RngHom S ) /\ F : ran ( 1st ` R ) -1-1-onto-> ran ( 1st ` S ) ) ) /\ ( x e. ran ( 1st ` S ) /\ y e. ran ( 1st ` S ) ) ) -> ( `' F ` ( x ( 2nd ` S ) y ) ) = ( ( `' F ` x ) ( 2nd ` R ) ( `' F ` y ) ) )
96 62 95 jca 
 |-  ( ( ( ( R e. RingOps /\ S e. RingOps ) /\ ( F e. ( R RngHom S ) /\ F : ran ( 1st ` R ) -1-1-onto-> ran ( 1st ` S ) ) ) /\ ( x e. ran ( 1st ` S ) /\ y e. ran ( 1st ` S ) ) ) -> ( ( `' F ` ( x ( 1st ` S ) y ) ) = ( ( `' F ` x ) ( 1st ` R ) ( `' F ` y ) ) /\ ( `' F ` ( x ( 2nd ` S ) y ) ) = ( ( `' F ` x ) ( 2nd ` R ) ( `' F ` y ) ) ) )
97 96 ralrimivva 
 |-  ( ( ( R e. RingOps /\ S e. RingOps ) /\ ( F e. ( R RngHom S ) /\ F : ran ( 1st ` R ) -1-1-onto-> ran ( 1st ` S ) ) ) -> A. x e. ran ( 1st ` S ) A. y e. ran ( 1st ` S ) ( ( `' F ` ( x ( 1st ` S ) y ) ) = ( ( `' F ` x ) ( 1st ` R ) ( `' F ` y ) ) /\ ( `' F ` ( x ( 2nd ` S ) y ) ) = ( ( `' F ` x ) ( 2nd ` R ) ( `' F ` y ) ) ) )
98 30 7 37 8 29 5 12 6 isrngohom 
 |-  ( ( S e. RingOps /\ R e. RingOps ) -> ( `' F e. ( S RngHom R ) <-> ( `' F : ran ( 1st ` S ) --> ran ( 1st ` R ) /\ ( `' F ` ( GId ` ( 2nd ` S ) ) ) = ( GId ` ( 2nd ` R ) ) /\ A. x e. ran ( 1st ` S ) A. y e. ran ( 1st ` S ) ( ( `' F ` ( x ( 1st ` S ) y ) ) = ( ( `' F ` x ) ( 1st ` R ) ( `' F ` y ) ) /\ ( `' F ` ( x ( 2nd ` S ) y ) ) = ( ( `' F ` x ) ( 2nd ` R ) ( `' F ` y ) ) ) ) ) )
99 98 ancoms 
 |-  ( ( R e. RingOps /\ S e. RingOps ) -> ( `' F e. ( S RngHom R ) <-> ( `' F : ran ( 1st ` S ) --> ran ( 1st ` R ) /\ ( `' F ` ( GId ` ( 2nd ` S ) ) ) = ( GId ` ( 2nd ` R ) ) /\ A. x e. ran ( 1st ` S ) A. y e. ran ( 1st ` S ) ( ( `' F ` ( x ( 1st ` S ) y ) ) = ( ( `' F ` x ) ( 1st ` R ) ( `' F ` y ) ) /\ ( `' F ` ( x ( 2nd ` S ) y ) ) = ( ( `' F ` x ) ( 2nd ` R ) ( `' F ` y ) ) ) ) ) )
100 99 adantr 
 |-  ( ( ( R e. RingOps /\ S e. RingOps ) /\ ( F e. ( R RngHom S ) /\ F : ran ( 1st ` R ) -1-1-onto-> ran ( 1st ` S ) ) ) -> ( `' F e. ( S RngHom R ) <-> ( `' F : ran ( 1st ` S ) --> ran ( 1st ` R ) /\ ( `' F ` ( GId ` ( 2nd ` S ) ) ) = ( GId ` ( 2nd ` R ) ) /\ A. x e. ran ( 1st ` S ) A. y e. ran ( 1st ` S ) ( ( `' F ` ( x ( 1st ` S ) y ) ) = ( ( `' F ` x ) ( 1st ` R ) ( `' F ` y ) ) /\ ( `' F ` ( x ( 2nd ` S ) y ) ) = ( ( `' F ` x ) ( 2nd ` R ) ( `' F ` y ) ) ) ) ) )
101 4 18 97 100 mpbir3and 
 |-  ( ( ( R e. RingOps /\ S e. RingOps ) /\ ( F e. ( R RngHom S ) /\ F : ran ( 1st ` R ) -1-1-onto-> ran ( 1st ` S ) ) ) -> `' F e. ( S RngHom R ) )
102 1 ad2antll 
 |-  ( ( ( R e. RingOps /\ S e. RingOps ) /\ ( F e. ( R RngHom S ) /\ F : ran ( 1st ` R ) -1-1-onto-> ran ( 1st ` S ) ) ) -> `' F : ran ( 1st ` S ) -1-1-onto-> ran ( 1st ` R ) )
103 101 102 jca 
 |-  ( ( ( R e. RingOps /\ S e. RingOps ) /\ ( F e. ( R RngHom S ) /\ F : ran ( 1st ` R ) -1-1-onto-> ran ( 1st ` S ) ) ) -> ( `' F e. ( S RngHom R ) /\ `' F : ran ( 1st ` S ) -1-1-onto-> ran ( 1st ` R ) ) )
104 103 ex 
 |-  ( ( R e. RingOps /\ S e. RingOps ) -> ( ( F e. ( R RngHom S ) /\ F : ran ( 1st ` R ) -1-1-onto-> ran ( 1st ` S ) ) -> ( `' F e. ( S RngHom R ) /\ `' F : ran ( 1st ` S ) -1-1-onto-> ran ( 1st ` R ) ) ) )
105 29 12 30 37 isrngoiso 
 |-  ( ( R e. RingOps /\ S e. RingOps ) -> ( F e. ( R RngIso S ) <-> ( F e. ( R RngHom S ) /\ F : ran ( 1st ` R ) -1-1-onto-> ran ( 1st ` S ) ) ) )
106 30 37 29 12 isrngoiso 
 |-  ( ( S e. RingOps /\ R e. RingOps ) -> ( `' F e. ( S RngIso R ) <-> ( `' F e. ( S RngHom R ) /\ `' F : ran ( 1st ` S ) -1-1-onto-> ran ( 1st ` R ) ) ) )
107 106 ancoms 
 |-  ( ( R e. RingOps /\ S e. RingOps ) -> ( `' F e. ( S RngIso R ) <-> ( `' F e. ( S RngHom R ) /\ `' F : ran ( 1st ` S ) -1-1-onto-> ran ( 1st ` R ) ) ) )
108 104 105 107 3imtr4d 
 |-  ( ( R e. RingOps /\ S e. RingOps ) -> ( F e. ( R RngIso S ) -> `' F e. ( S RngIso R ) ) )
109 108 3impia 
 |-  ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RngIso S ) ) -> `' F e. ( S RngIso R ) )