Users' Mathboxes Mathbox for Jeff Madsen < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-rngohom Structured version   Unicode version

Definition df-rngohom 26581
Description: Define the function which gives the set of ring homomorphisms between two given rings. (Contributed by Jeff Madsen, 19-Jun-2010.)
Assertion
Ref Expression
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 ) ) ) ) } )
Distinct variable group:    s, r, f, x, y

Detailed syntax breakdown of Definition df-rngohom
StepHypRef Expression
1 crnghom 26578 . 2  class  RngHom
2 vr . . 3  set  r
3 vs . . 3  set  s
4 crngo 21965 . . 3  class  RingOps
52cv 1652 . . . . . . . . 9  class  r
6 c2nd 6350 . . . . . . . . 9  class  2nd
75, 6cfv 5456 . . . . . . . 8  class  ( 2nd `  r )
8 cgi 21777 . . . . . . . 8  class GId
97, 8cfv 5456 . . . . . . 7  class  (GId `  ( 2nd `  r ) )
10 vf . . . . . . . 8  set  f
1110cv 1652 . . . . . . 7  class  f
129, 11cfv 5456 . . . . . 6  class  ( f `
 (GId `  ( 2nd `  r ) ) )
133cv 1652 . . . . . . . 8  class  s
1413, 6cfv 5456 . . . . . . 7  class  ( 2nd `  s )
1514, 8cfv 5456 . . . . . 6  class  (GId `  ( 2nd `  s ) )
1612, 15wceq 1653 . . . . 5  wff  ( f `
 (GId `  ( 2nd `  r ) ) )  =  (GId `  ( 2nd `  s ) )
17 vx . . . . . . . . . . . 12  set  x
1817cv 1652 . . . . . . . . . . 11  class  x
19 vy . . . . . . . . . . . 12  set  y
2019cv 1652 . . . . . . . . . . 11  class  y
21 c1st 6349 . . . . . . . . . . . 12  class  1st
225, 21cfv 5456 . . . . . . . . . . 11  class  ( 1st `  r )
2318, 20, 22co 6083 . . . . . . . . . 10  class  ( x ( 1st `  r
) y )
2423, 11cfv 5456 . . . . . . . . 9  class  ( f `
 ( x ( 1st `  r ) y ) )
2518, 11cfv 5456 . . . . . . . . . 10  class  ( f `
 x )
2620, 11cfv 5456 . . . . . . . . . 10  class  ( f `
 y )
2713, 21cfv 5456 . . . . . . . . . 10  class  ( 1st `  s )
2825, 26, 27co 6083 . . . . . . . . 9  class  ( ( f `  x ) ( 1st `  s
) ( f `  y ) )
2924, 28wceq 1653 . . . . . . . 8  wff  ( f `
 ( x ( 1st `  r ) y ) )  =  ( ( f `  x ) ( 1st `  s ) ( f `
 y ) )
3018, 20, 7co 6083 . . . . . . . . . 10  class  ( x ( 2nd `  r
) y )
3130, 11cfv 5456 . . . . . . . . 9  class  ( f `
 ( x ( 2nd `  r ) y ) )
3225, 26, 14co 6083 . . . . . . . . 9  class  ( ( f `  x ) ( 2nd `  s
) ( f `  y ) )
3331, 32wceq 1653 . . . . . . . 8  wff  ( f `
 ( x ( 2nd `  r ) y ) )  =  ( ( f `  x ) ( 2nd `  s ) ( f `
 y ) )
3429, 33wa 360 . . . . . . 7  wff  ( ( f `  ( x ( 1st `  r
) y ) )  =  ( ( f `
 x ) ( 1st `  s ) ( f `  y
) )  /\  (
f `  ( x
( 2nd `  r
) y ) )  =  ( ( f `
 x ) ( 2nd `  s ) ( f `  y
) ) )
3522crn 4881 . . . . . . 7  class  ran  ( 1st `  r )
3634, 19, 35wral 2707 . . . . . 6  wff  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 ) ) )
3736, 17, 35wral 2707 . . . . 5  wff  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 ) ) )
3816, 37wa 360 . . . 4  wff  ( ( 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 ) ) ) )
3927crn 4881 . . . . 5  class  ran  ( 1st `  s )
40 cmap 7020 . . . . 5  class  ^m
4139, 35, 40co 6083 . . . 4  class  ( ran  ( 1st `  s
)  ^m  ran  ( 1st `  r ) )
4238, 10, 41crab 2711 . . 3  class  { 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
) ) ) ) }
432, 3, 4, 4, 42cmpt2 6085 . 2  class  ( 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
) ) ) ) } )
441, 43wceq 1653 1  wff  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 ) ) ) ) } )
Colors of variables: wff set class
This definition is referenced by:  rngohomval  26582
  Copyright terms: Public domain W3C validator