MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-rnghom Unicode version

Definition df-rnghom 15512
Description: Define the set of ring homomorphisms from  r to  s. (Contributed by Stefan O'Rear, 7-Mar-2015.)
Assertion
Ref Expression
df-rnghom  |- RingHom  =  ( r  e.  Ring ,  s  e.  Ring  |->  [_ ( Base `  r )  / 
v ]_ [_ ( Base `  s )  /  w ]_ { f  e.  ( w  ^m  v )  |  ( ( f `
 ( 1r `  r ) )  =  ( 1r `  s
)  /\  A. x  e.  v  A. y  e.  v  ( (
f `  ( x
( +g  `  r ) y ) )  =  ( ( f `  x ) ( +g  `  s ) ( f `
 y ) )  /\  ( f `  ( x ( .r
`  r ) y ) )  =  ( ( f `  x
) ( .r `  s ) ( f `
 y ) ) ) ) } )
Distinct variable group:    s, r, v, w, f, x, y

Detailed syntax breakdown of Definition df-rnghom
StepHypRef Expression
1 crh 15510 . 2  class RingHom
2 vr . . 3  set  r
3 vs . . 3  set  s
4 crg 15353 . . 3  class  Ring
5 vv . . . 4  set  v
62cv 1631 . . . . 5  class  r
7 cbs 13164 . . . . 5  class  Base
86, 7cfv 5271 . . . 4  class  ( Base `  r )
9 vw . . . . 5  set  w
103cv 1631 . . . . . 6  class  s
1110, 7cfv 5271 . . . . 5  class  ( Base `  s )
12 cur 15355 . . . . . . . . . 10  class  1r
136, 12cfv 5271 . . . . . . . . 9  class  ( 1r
`  r )
14 vf . . . . . . . . . 10  set  f
1514cv 1631 . . . . . . . . 9  class  f
1613, 15cfv 5271 . . . . . . . 8  class  ( f `
 ( 1r `  r ) )
1710, 12cfv 5271 . . . . . . . 8  class  ( 1r
`  s )
1816, 17wceq 1632 . . . . . . 7  wff  ( f `
 ( 1r `  r ) )  =  ( 1r `  s
)
19 vx . . . . . . . . . . . . . 14  set  x
2019cv 1631 . . . . . . . . . . . . 13  class  x
21 vy . . . . . . . . . . . . . 14  set  y
2221cv 1631 . . . . . . . . . . . . 13  class  y
23 cplusg 13224 . . . . . . . . . . . . . 14  class  +g
246, 23cfv 5271 . . . . . . . . . . . . 13  class  ( +g  `  r )
2520, 22, 24co 5874 . . . . . . . . . . . 12  class  ( x ( +g  `  r
) y )
2625, 15cfv 5271 . . . . . . . . . . 11  class  ( f `
 ( x ( +g  `  r ) y ) )
2720, 15cfv 5271 . . . . . . . . . . . 12  class  ( f `
 x )
2822, 15cfv 5271 . . . . . . . . . . . 12  class  ( f `
 y )
2910, 23cfv 5271 . . . . . . . . . . . 12  class  ( +g  `  s )
3027, 28, 29co 5874 . . . . . . . . . . 11  class  ( ( f `  x ) ( +g  `  s
) ( f `  y ) )
3126, 30wceq 1632 . . . . . . . . . 10  wff  ( f `
 ( x ( +g  `  r ) y ) )  =  ( ( f `  x ) ( +g  `  s ) ( f `
 y ) )
32 cmulr 13225 . . . . . . . . . . . . . 14  class  .r
336, 32cfv 5271 . . . . . . . . . . . . 13  class  ( .r
`  r )
3420, 22, 33co 5874 . . . . . . . . . . . 12  class  ( x ( .r `  r
) y )
3534, 15cfv 5271 . . . . . . . . . . 11  class  ( f `
 ( x ( .r `  r ) y ) )
3610, 32cfv 5271 . . . . . . . . . . . 12  class  ( .r
`  s )
3727, 28, 36co 5874 . . . . . . . . . . 11  class  ( ( f `  x ) ( .r `  s
) ( f `  y ) )
3835, 37wceq 1632 . . . . . . . . . 10  wff  ( f `
 ( x ( .r `  r ) y ) )  =  ( ( f `  x ) ( .r
`  s ) ( f `  y ) )
3931, 38wa 358 . . . . . . . . 9  wff  ( ( f `  ( x ( +g  `  r
) y ) )  =  ( ( f `
 x ) ( +g  `  s ) ( f `  y
) )  /\  (
f `  ( x
( .r `  r
) y ) )  =  ( ( f `
 x ) ( .r `  s ) ( f `  y
) ) )
405cv 1631 . . . . . . . . 9  class  v
4139, 21, 40wral 2556 . . . . . . . 8  wff  A. y  e.  v  ( (
f `  ( x
( +g  `  r ) y ) )  =  ( ( f `  x ) ( +g  `  s ) ( f `
 y ) )  /\  ( f `  ( x ( .r
`  r ) y ) )  =  ( ( f `  x
) ( .r `  s ) ( f `
 y ) ) )
4241, 19, 40wral 2556 . . . . . . 7  wff  A. x  e.  v  A. y  e.  v  ( (
f `  ( x
( +g  `  r ) y ) )  =  ( ( f `  x ) ( +g  `  s ) ( f `
 y ) )  /\  ( f `  ( x ( .r
`  r ) y ) )  =  ( ( f `  x
) ( .r `  s ) ( f `
 y ) ) )
4318, 42wa 358 . . . . . 6  wff  ( ( f `  ( 1r
`  r ) )  =  ( 1r `  s )  /\  A. x  e.  v  A. y  e.  v  (
( f `  (
x ( +g  `  r
) y ) )  =  ( ( f `
 x ) ( +g  `  s ) ( f `  y
) )  /\  (
f `  ( x
( .r `  r
) y ) )  =  ( ( f `
 x ) ( .r `  s ) ( f `  y
) ) ) )
449cv 1631 . . . . . . 7  class  w
45 cmap 6788 . . . . . . 7  class  ^m
4644, 40, 45co 5874 . . . . . 6  class  ( w  ^m  v )
4743, 14, 46crab 2560 . . . . 5  class  { f  e.  ( w  ^m  v )  |  ( ( f `  ( 1r `  r ) )  =  ( 1r `  s )  /\  A. x  e.  v  A. y  e.  v  (
( f `  (
x ( +g  `  r
) y ) )  =  ( ( f `
 x ) ( +g  `  s ) ( f `  y
) )  /\  (
f `  ( x
( .r `  r
) y ) )  =  ( ( f `
 x ) ( .r `  s ) ( f `  y
) ) ) ) }
489, 11, 47csb 3094 . . . 4  class  [_ ( Base `  s )  /  w ]_ { f  e.  ( w  ^m  v
)  |  ( ( f `  ( 1r
`  r ) )  =  ( 1r `  s )  /\  A. x  e.  v  A. y  e.  v  (
( f `  (
x ( +g  `  r
) y ) )  =  ( ( f `
 x ) ( +g  `  s ) ( f `  y
) )  /\  (
f `  ( x
( .r `  r
) y ) )  =  ( ( f `
 x ) ( .r `  s ) ( f `  y
) ) ) ) }
495, 8, 48csb 3094 . . 3  class  [_ ( Base `  r )  / 
v ]_ [_ ( Base `  s )  /  w ]_ { f  e.  ( w  ^m  v )  |  ( ( f `
 ( 1r `  r ) )  =  ( 1r `  s
)  /\  A. x  e.  v  A. y  e.  v  ( (
f `  ( x
( +g  `  r ) y ) )  =  ( ( f `  x ) ( +g  `  s ) ( f `
 y ) )  /\  ( f `  ( x ( .r
`  r ) y ) )  =  ( ( f `  x
) ( .r `  s ) ( f `
 y ) ) ) ) }
502, 3, 4, 4, 49cmpt2 5876 . 2  class  ( r  e.  Ring ,  s  e. 
Ring  |->  [_ ( Base `  r
)  /  v ]_ [_ ( Base `  s
)  /  w ]_ { f  e.  ( w  ^m  v )  |  ( ( f `
 ( 1r `  r ) )  =  ( 1r `  s
)  /\  A. x  e.  v  A. y  e.  v  ( (
f `  ( x
( +g  `  r ) y ) )  =  ( ( f `  x ) ( +g  `  s ) ( f `
 y ) )  /\  ( f `  ( x ( .r
`  r ) y ) )  =  ( ( f `  x
) ( .r `  s ) ( f `
 y ) ) ) ) } )
511, 50wceq 1632 1  wff RingHom  =  ( r  e.  Ring ,  s  e.  Ring  |->  [_ ( Base `  r )  / 
v ]_ [_ ( Base `  s )  /  w ]_ { f  e.  ( w  ^m  v )  |  ( ( f `
 ( 1r `  r ) )  =  ( 1r `  s
)  /\  A. x  e.  v  A. y  e.  v  ( (
f `  ( x
( +g  `  r ) y ) )  =  ( ( f `  x ) ( +g  `  s ) ( f `
 y ) )  /\  ( f `  ( x ( .r
`  r ) y ) )  =  ( ( f `  x
) ( .r `  s ) ( f `
 y ) ) ) ) } )
Colors of variables: wff set class
This definition is referenced by:  dfrhm2  15514
  Copyright terms: Public domain W3C validator