Theorem rngoisocnv

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

	Ref	Expression
Assertion	rngoisocnv	Could not format assertion : No typesetting found for |- ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RingOpsIso S ) ) -> `' F e. ( S RingOpsIso R ) ) with typecode |-

Proof

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