Description: Define the function which gives the set of ring isomorphisms between two given rings. (Contributed by Jeff Madsen, 16-Jun-2011)
Ref | Expression | ||
---|---|---|---|
Assertion | df-rngoiso | |- RngIso = ( r e. RingOps , s e. RingOps |-> { f e. ( r RngHom s ) | f : ran ( 1st ` r ) -1-1-onto-> ran ( 1st ` s ) } ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
0 | crngiso | |- RngIso |
|
1 | vr | |- r |
|
2 | crngo | |- RingOps |
|
3 | vs | |- s |
|
4 | vf | |- f |
|
5 | 1 | cv | |- r |
6 | crnghom | |- RngHom |
|
7 | 3 | cv | |- s |
8 | 5 7 6 | co | |- ( r RngHom s ) |
9 | 4 | cv | |- f |
10 | c1st | |- 1st |
|
11 | 5 10 | cfv | |- ( 1st ` r ) |
12 | 11 | crn | |- ran ( 1st ` r ) |
13 | 7 10 | cfv | |- ( 1st ` s ) |
14 | 13 | crn | |- ran ( 1st ` s ) |
15 | 12 14 9 | wf1o | |- f : ran ( 1st ` r ) -1-1-onto-> ran ( 1st ` s ) |
16 | 15 4 8 | crab | |- { f e. ( r RngHom s ) | f : ran ( 1st ` r ) -1-1-onto-> ran ( 1st ` s ) } |
17 | 1 3 2 2 16 | cmpo | |- ( r e. RingOps , s e. RingOps |-> { f e. ( r RngHom s ) | f : ran ( 1st ` r ) -1-1-onto-> ran ( 1st ` s ) } ) |
18 | 0 17 | wceq | |- RngIso = ( r e. RingOps , s e. RingOps |-> { f e. ( r RngHom s ) | f : ran ( 1st ` r ) -1-1-onto-> ran ( 1st ` s ) } ) |