Metamath Proof Explorer


Theorem 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 RingOps S RingOps R RngIso S = f R RngHom S | f : X 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 s = S r RngHom s = R RngHom S
6 fveq2 r = R 1 st r = 1 st R
7 6 1 eqtr4di r = R 1 st r = G
8 7 rneqd r = R ran 1 st r = ran G
9 8 2 eqtr4di r = R ran 1 st r = X
10 9 f1oeq2d r = R f : ran 1 st r 1-1 onto ran 1 st s f : X 1-1 onto ran 1 st s
11 fveq2 s = S 1 st s = 1 st S
12 11 3 eqtr4di s = S 1 st s = J
13 12 rneqd s = S ran 1 st s = ran J
14 13 4 eqtr4di s = S ran 1 st s = Y
15 14 f1oeq3d s = S f : X 1-1 onto ran 1 st s f : X 1-1 onto Y
16 10 15 sylan9bb r = R s = S f : ran 1 st r 1-1 onto ran 1 st s f : X 1-1 onto Y
17 5 16 rabeqbidv r = R s = S f r RngHom s | f : ran 1 st r 1-1 onto ran 1 st s = f R RngHom S | f : X 1-1 onto Y
18 df-rngoiso RngIso = r RingOps , s RingOps f r RngHom s | f : ran 1 st r 1-1 onto ran 1 st s
19 ovex R RngHom S V
20 19 rabex f R RngHom S | f : X 1-1 onto Y V
21 17 18 20 ovmpoa R RingOps S RingOps R RngIso S = f R RngHom S | f : X 1-1 onto Y