Theorem rngoisoval

Description: Obsolete theorem, use rimval instead. The set of ring isomorphisms. (Contributed by Jeff Madsen, 16-Jun-2011) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypotheses	rngisoval.1	$$⊢G=1^{st}\left(R\right)$$
	rngisoval.2	$$⊢X=\mathrm{ran}G$$
	rngisoval.3	$$⊢J=1^{st}\left(S\right)$$
	rngisoval.4	$$⊢Y=\mathrm{ran}J$$
Assertion	rngoisoval	$$⊢\left(R\in \mathrm{RingOps}\wedge S\in \mathrm{RingOps}\right)\to R\mathrm{RingOpsIso}S=\left\{f\in \left(R\mathrm{RingOpsHom}S\right)|f:X\underset{1-1\; onto}{⟶}Y\right\}$$

Proof

Step	Hyp	Ref	Expression
1		rngisoval.1	$$⊢G=1^{st}\left(R\right)$$
2		rngisoval.2	$$⊢X=\mathrm{ran}G$$
3		rngisoval.3	$$⊢J=1^{st}\left(S\right)$$
4		rngisoval.4	$$⊢Y=\mathrm{ran}J$$
5		oveq12	$$⊢\left(r=R\wedge s=S\right)\to r\mathrm{RingOpsHom}s=R\mathrm{RingOpsHom}S$$
6		fveq2	$$⊢r=R\to 1^{st}\left(r\right)=1^{st}\left(R\right)$$
7	6 1	eqtr4di	$$⊢r=R\to 1^{st}\left(r\right)=G$$
8	7	rneqd	$$⊢r=R\to \mathrm{ran}{1}^{st}\left(r\right)=\mathrm{ran}G$$
9	8 2	eqtr4di	$$⊢r=R\to \mathrm{ran}{1}^{st}\left(r\right)=X$$
10	9	f1oeq2d	$$⊢r=R\to \left(f:\mathrm{ran}{1}^{st}\left(r\right)\underset{1-1\; onto}{⟶}\mathrm{ran}{1}^{st}\left(s\right)\leftrightarrow f:X\underset{1-1\; onto}{⟶}\mathrm{ran}{1}^{st}\left(s\right)\right)$$
11		fveq2	$$⊢s=S\to 1^{st}\left(s\right)=1^{st}\left(S\right)$$
12	11 3	eqtr4di	$$⊢s=S\to 1^{st}\left(s\right)=J$$
13	12	rneqd	$$⊢s=S\to \mathrm{ran}{1}^{st}\left(s\right)=\mathrm{ran}J$$
14	13 4	eqtr4di	$$⊢s=S\to \mathrm{ran}{1}^{st}\left(s\right)=Y$$
15	14	f1oeq3d	$$⊢s=S\to \left(f:X\underset{1-1\; onto}{⟶}\mathrm{ran}{1}^{st}\left(s\right)\leftrightarrow f:X\underset{1-1\; onto}{⟶}Y\right)$$
16	10 15	sylan9bb	$$⊢\left(r=R\wedge s=S\right)\to \left(f:\mathrm{ran}{1}^{st}\left(r\right)\underset{1-1\; onto}{⟶}\mathrm{ran}{1}^{st}\left(s\right)\leftrightarrow f:X\underset{1-1\; onto}{⟶}Y\right)$$
17	5 16	rabeqbidv	$$⊢\left(r=R\wedge s=S\right)\to \left\{f\in \left(r\mathrm{RingOpsHom}s\right)|f:\mathrm{ran}{1}^{st}\left(r\right)\underset{1-1\; onto}{⟶}\mathrm{ran}{1}^{st}\left(s\right)\right\}=\left\{f\in \left(R\mathrm{RingOpsHom}S\right)|f:X\underset{1-1\; onto}{⟶}Y\right\}$$
18		df-rngoiso	$$⊢\mathrm{RingOpsIso}=\left(r\in \mathrm{RingOps},s\in \mathrm{RingOps}⟼\left\{f\in \left(r\mathrm{RingOpsHom}s\right)|f:\mathrm{ran}{1}^{st}\left(r\right)\underset{1-1\; onto}{⟶}\mathrm{ran}{1}^{st}\left(s\right)\right\}\right)$$
19		ovex	$$⊢R\mathrm{RingOpsHom}S\in \mathrm{V}$$
20	19	rabex	$$⊢\left\{f\in \left(R\mathrm{RingOpsHom}S\right)|f:X\underset{1-1\; onto}{⟶}Y\right\}\in \mathrm{V}$$
21	17 18 20	ovmpoa	$$⊢\left(R\in \mathrm{RingOps}\wedge S\in \mathrm{RingOps}\right)\to R\mathrm{RingOpsIso}S=\left\{f\in \left(R\mathrm{RingOpsHom}S\right)|f:X\underset{1-1\; onto}{⟶}Y\right\}$$