rngoisoval

Description: The set of ring isomorphisms. (Contributed by Jeff Madsen, 16-Jun-2011)

	Ref	Expression
Hypotheses	rngisoval.1	$⊢ G = 1^{st} (R)$
	rngisoval.2	$⊢ X = ran G$
	rngisoval.3	$⊢ J = 1^{st} (S)$
	rngisoval.4	$⊢ Y = ran J$
Assertion	rngoisoval	$⊢ (R \in RingOps \land S \in RingOps) \to R RngIso S = \{f \in (R RngHom S) \| f : X \underset{1-1 onto}{⟶} Y\}$

Proof

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

Metamath Proof Explorer

Theorem rngoisoval

Proof