Metamath Proof Explorer

Definition df-rngohom

Description: Define the function which gives the set of ring homomorphisms between two given rings. (Contributed by Jeff Madsen, 19-Jun-2010)

Ref Expression
Assertion df-rngohom 
|- RngHom = ( r e. RingOps , s e. RingOps |-> { f e. ( ran ( 1st ` s ) ^m ran ( 1st ` r ) ) | ( ( f ` ( GId ` ( 2nd ` r ) ) ) = ( GId ` ( 2nd ` s ) ) /\ A. x e. ran ( 1st ` r ) A. y e. ran ( 1st ` r ) ( ( f ` ( x ( 1st ` r ) y ) ) = ( ( f ` x ) ( 1st ` s ) ( f ` y ) ) /\ ( f ` ( x ( 2nd ` r ) y ) ) = ( ( f ` x ) ( 2nd ` s ) ( f ` y ) ) ) ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 crnghom 
 |-  RngHom
1 vr 
 |-  r
2 crngo 
 |-  RingOps
3 vs 
 |-  s
4 vf 
 |-  f
5 c1st 
 |-  1st
6 3 cv 
 |-  s
7 6 5 cfv 
 |-  ( 1st ` s )
8 7 crn 
 |-  ran ( 1st ` s )
9 cmap 
 |-  ^m
10 1 cv 
 |-  r
11 10 5 cfv 
 |-  ( 1st ` r )
12 11 crn 
 |-  ran ( 1st ` r )
13 8 12 9 co 
 |-  ( ran ( 1st ` s ) ^m ran ( 1st ` r ) )
14 4 cv 
 |-  f
15 cgi 
 |-  GId
16 c2nd 
 |-  2nd
17 10 16 cfv 
 |-  ( 2nd ` r )
18 17 15 cfv 
 |-  ( GId ` ( 2nd ` r ) )
19 18 14 cfv 
 |-  ( f ` ( GId ` ( 2nd ` r ) ) )
20 6 16 cfv 
 |-  ( 2nd ` s )
21 20 15 cfv 
 |-  ( GId ` ( 2nd ` s ) )
22 19 21 wceq 
 |-  ( f ` ( GId ` ( 2nd ` r ) ) ) = ( GId ` ( 2nd ` s ) )
23 vx 
 |-  x
24 vy 
 |-  y
25 23 cv 
 |-  x
26 24 cv 
 |-  y
27 25 26 11 co 
 |-  ( x ( 1st ` r ) y )
28 27 14 cfv 
 |-  ( f ` ( x ( 1st ` r ) y ) )
29 25 14 cfv 
 |-  ( f ` x )
30 26 14 cfv 
 |-  ( f ` y )
31 29 30 7 co 
 |-  ( ( f ` x ) ( 1st ` s ) ( f ` y ) )
32 28 31 wceq 
 |-  ( f ` ( x ( 1st ` r ) y ) ) = ( ( f ` x ) ( 1st ` s ) ( f ` y ) )
33 25 26 17 co 
 |-  ( x ( 2nd ` r ) y )
34 33 14 cfv 
 |-  ( f ` ( x ( 2nd ` r ) y ) )
35 29 30 20 co 
 |-  ( ( f ` x ) ( 2nd ` s ) ( f ` y ) )
36 34 35 wceq 
 |-  ( f ` ( x ( 2nd ` r ) y ) ) = ( ( f ` x ) ( 2nd ` s ) ( f ` y ) )
37 32 36 wa 
 |-  ( ( f ` ( x ( 1st ` r ) y ) ) = ( ( f ` x ) ( 1st ` s ) ( f ` y ) ) /\ ( f ` ( x ( 2nd ` r ) y ) ) = ( ( f ` x ) ( 2nd ` s ) ( f ` y ) ) )
38 37 24 12 wral 
 |-  A. y e. ran ( 1st ` r ) ( ( f ` ( x ( 1st ` r ) y ) ) = ( ( f ` x ) ( 1st ` s ) ( f ` y ) ) /\ ( f ` ( x ( 2nd ` r ) y ) ) = ( ( f ` x ) ( 2nd ` s ) ( f ` y ) ) )
39 38 23 12 wral 
 |-  A. x e. ran ( 1st ` r ) A. y e. ran ( 1st ` r ) ( ( f ` ( x ( 1st ` r ) y ) ) = ( ( f ` x ) ( 1st ` s ) ( f ` y ) ) /\ ( f ` ( x ( 2nd ` r ) y ) ) = ( ( f ` x ) ( 2nd ` s ) ( f ` y ) ) )
40 22 39 wa 
 |-  ( ( f ` ( GId ` ( 2nd ` r ) ) ) = ( GId ` ( 2nd ` s ) ) /\ A. x e. ran ( 1st ` r ) A. y e. ran ( 1st ` r ) ( ( f ` ( x ( 1st ` r ) y ) ) = ( ( f ` x ) ( 1st ` s ) ( f ` y ) ) /\ ( f ` ( x ( 2nd ` r ) y ) ) = ( ( f ` x ) ( 2nd ` s ) ( f ` y ) ) ) )
41 40 4 13 crab 
 |-  { f e. ( ran ( 1st ` s ) ^m ran ( 1st ` r ) ) | ( ( f ` ( GId ` ( 2nd ` r ) ) ) = ( GId ` ( 2nd ` s ) ) /\ A. x e. ran ( 1st ` r ) A. y e. ran ( 1st ` r ) ( ( f ` ( x ( 1st ` r ) y ) ) = ( ( f ` x ) ( 1st ` s ) ( f ` y ) ) /\ ( f ` ( x ( 2nd ` r ) y ) ) = ( ( f ` x ) ( 2nd ` s ) ( f ` y ) ) ) ) }
42 1 3 2 2 41 cmpo 
 |-  ( r e. RingOps , s e. RingOps |-> { f e. ( ran ( 1st ` s ) ^m ran ( 1st ` r ) ) | ( ( f ` ( GId ` ( 2nd ` r ) ) ) = ( GId ` ( 2nd ` s ) ) /\ A. x e. ran ( 1st ` r ) A. y e. ran ( 1st ` r ) ( ( f ` ( x ( 1st ` r ) y ) ) = ( ( f ` x ) ( 1st ` s ) ( f ` y ) ) /\ ( f ` ( x ( 2nd ` r ) y ) ) = ( ( f ` x ) ( 2nd ` s ) ( f ` y ) ) ) ) } )
43 0 42 wceq 
 |-  RngHom = ( r e. RingOps , s e. RingOps |-> { f e. ( ran ( 1st ` s ) ^m ran ( 1st ` r ) ) | ( ( f ` ( GId ` ( 2nd ` r ) ) ) = ( GId ` ( 2nd ` s ) ) /\ A. x e. ran ( 1st ` r ) A. y e. ran ( 1st ` r ) ( ( f ` ( x ( 1st ` r ) y ) ) = ( ( f ` x ) ( 1st ` s ) ( f ` y ) ) /\ ( f ` ( x ( 2nd ` r ) y ) ) = ( ( f ` x ) ( 2nd ` s ) ( f ` y ) ) ) ) } )